Theorem expordit 6539

Description: Ordering relationship for exponentiation.

Assertion

Ref	Expression
expordit	|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^M) < (A^N))

Proof of Theorem expordit

Step	Hyp	Ref	Expression
1		expgt1t 6531	. . . 4 |- ((A e. RR /\ (N - M) e. NN /\ 1 < A) -> 1 < (A^(N - M)))
2		3simp1 787	. . . . 5 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> A e. RR)
3	2	adantr 389	. . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> A e. RR)
4		znnsubt 6132	. . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> (N - M) e. NN))
5		nn0zt 6109	. . . . . . . 8 |- (M e. NN0 -> M e. ZZ)
6		nn0zt 6109	. . . . . . . 8 |- (N e. NN0 -> N e. ZZ)
7	4, 5, 6	syl2an 454	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> (M < N <-> (N - M) e. NN))
8	7	3adant1 796	. . . . . 6 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (M < N <-> (N - M) e. NN))
9	8	biimpa 416	. . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (N - M) e. NN)
10	9	adantrl 394	. . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (N - M) e. NN)
11		simprl 414	. . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 1 < A)
12	1, 3, 10, 11	syl3anc 857	. . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 1 < (A^(N - M)))
13		ltmul1t 5794	. . . 4 |- (((1 e. RR /\ (A^(N - M)) e. RR /\ (A^M) e. RR) /\ 0 < (A^M)) -> (1 < (A^(N - M)) <-> (1 x. (A^M)) < ((A^(N - M)) x. (A^M))))
14		1re 5415	. . . . . 6 |- 1 e. RR
15	14	a1i 8	. . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 1 e. RR)
16		reexpclt 6520	. . . . . . 7 |- ((A e. RR /\ (N - M) e. NN0) -> (A^(N - M)) e. RR)
17	2	adantr 389	. . . . . . 7 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> A e. RR)
18		nnnn0t 6061	. . . . . . . 8 |- ((N - M) e. NN -> (N - M) e. NN0)
19	9, 18	syl 10	. . . . . . 7 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (N - M) e. NN0)
20	16, 17, 19	sylanc 471	. . . . . 6 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (A^(N - M)) e. RR)
21	20	adantrl 394	. . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^(N - M)) e. RR)
22		reexpclt 6520	. . . . . . 7 |- ((A e. RR /\ M e. NN0) -> (A^M) e. RR)
23	22	3adant3 798	. . . . . 6 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (A^M) e. RR)
24	23	adantr 389	. . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^M) e. RR)
25	15, 21, 24	3jca 818	. . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 e. RR /\ (A^(N - M)) e. RR /\ (A^M) e. RR))
26		lt01 5661	. . . . . . . . . 10 |- 0 < 1
27		0re 5420	. . . . . . . . . . 11 |- 0 e. RR
28		axlttrn 5484	. . . . . . . . . . 11 |- ((0 e. RR /\ 1 e. RR /\ A e. RR) -> ((0 < 1 /\ 1 < A) -> 0 < A))
29	27, 14, 28	mp3an12 904	. . . . . . . . . 10 |- (A e. RR -> ((0 < 1 /\ 1 < A) -> 0 < A))
30	26, 29	mpani 697	. . . . . . . . 9 |- (A e. RR -> (1 < A -> 0 < A))
31	30	adantr 389	. . . . . . . 8 |- ((A e. RR /\ M e. NN0) -> (1 < A -> 0 < A))
32		expgt0t 6528	. . . . . . . . 9 |- ((A e. RR /\ M e. NN0 /\ 0 < A) -> 0 < (A^M))
33	32	3expia 834	. . . . . . . 8 |- ((A e. RR /\ M e. NN0) -> (0 < A -> 0 < (A^M)))
34	31, 33	syld 27	. . . . . . 7 |- ((A e. RR /\ M e. NN0) -> (1 < A -> 0 < (A^M)))
35	34	3adant3 798	. . . . . 6 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (1 < A -> 0 < (A^M)))
36	35	imp 350	. . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ 1 < A) -> 0 < (A^M))
37	36	adantrr 395	. . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> 0 < (A^M))
38	13, 25, 37	sylanc 471	. . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 < (A^(N - M)) <-> (1 x. (A^M)) < ((A^(N - M)) x. (A^M))))
39	12, 38	mpbid 195	. 2 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 x. (A^M)) < ((A^(N - M)) x. (A^M)))
40		expclt 6521	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> (A^M) e. CC)
41		recnt 5293	. . . . . 6 |- (A e. RR -> A e. CC)
42	40, 41	sylan 448	. . . . 5 |- ((A e. RR /\ M e. NN0) -> (A^M) e. CC)
43		mulid2t 5397	. . . . 5 |- ((A^M) e. CC -> (1 x. (A^M)) = (A^M))
44	42, 43	syl 10	. . . 4 |- ((A e. RR /\ M e. NN0) -> (1 x. (A^M)) = (A^M))
45	44	3adant3 798	. . 3 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (1 x. (A^M)) = (A^M))
46	45	adantr 389	. 2 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (1 x. (A^M)) = (A^M))
47	2	recnd 5295	. . . . . . 7 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> A e. CC)
48	47	adantr 389	. . . . . 6 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> A e. CC)
49		3simp2 788	. . . . . . 7 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> M e. NN0)
50	49	adantr 389	. . . . . 6 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> M e. NN0)
51	48, 9, 50	3jca 818	. . . . 5 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ M < N) -> (A e. CC /\ (N - M) e. NN /\ M e. NN0))
52	51	adantrl 394	. . . 4 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A e. CC /\ (N - M) e. NN /\ M e. NN0))
53		expaddt 6535	. . . . 5 |- ((A e. CC /\ (N - M) e. NN0 /\ M e. NN0) -> (A^((N - M) + M)) = ((A^(N - M)) x. (A^M)))
54	53, 18	syl3an2 859	. . . 4 |- ((A e. CC /\ (N - M) e. NN /\ M e. NN0) -> (A^((N - M) + M)) = ((A^(N - M)) x. (A^M)))
55	52, 54	syl 10	. . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^((N - M) + M)) = ((A^(N - M)) x. (A^M)))
56		npcant 5379	. . . . . . . 8 |- ((N e. CC /\ M e. CC) -> ((N - M) + M) = N)
57		nn0cnt 6064	. . . . . . . 8 |- (N e. NN0 -> N e. CC)
58		nn0cnt 6064	. . . . . . . 8 |- (M e. NN0 -> M e. CC)
59	56, 57, 58	syl2an 454	. . . . . . 7 |- ((N e. NN0 /\ M e. NN0) -> ((N - M) + M) = N)
60	59	ancoms 436	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((N - M) + M) = N)
61	60	3adant1 796	. . . . 5 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> ((N - M) + M) = N)
62	61	opreq2d 3967	. . . 4 |- ((A e. RR /\ M e. NN0 /\ N e. NN0) -> (A^((N - M) + M)) = (A^N))
63	62	adantr 389	. . 3 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^((N - M) + M)) = (A^N))
64	55, 63	eqtr3d 1506	. 2 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> ((A^(N - M)) x. (A^M)) = (A^N))
65	39, 46, 64	3brtr3d 2639	1 |- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 <