Theorem ltexp2a

Description: Exponent ordering relationship for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	ltexp2a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝐴 ∈ ℝ )
2		0red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 0 ∈ ℝ )
3		1red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 1 ∈ ℝ )
4		0lt1	⊢ 0 < 1
5	4	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 0 < 1 )
6		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 1 < 𝐴 )
7	2 3 1 5 6	lttrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 0 < 𝐴 )
8	1 7	elrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝐴 ∈ ℝ+ )
9		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝑀 ∈ ℤ )
10		rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ+ )
11	8 9 10	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ+ )
12	11	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
13	12	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
14	13	mullidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 1 · ( 𝐴 ↑ 𝑀 ) ) = ( 𝐴 ↑ 𝑀 ) )
15		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝑀 < 𝑁 )
16		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝑁 ∈ ℤ )
17		znnsub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
18	9 16 17	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
19	15 18	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝑁 − 𝑀 ) ∈ ℕ )
20		expgt1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 1 < 𝐴 ) → 1 < ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) )
21	1 19 6 20	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 1 < ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) )
22	1	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝐴 ∈ ℂ )
23	7	gt0ne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 𝐴 ≠ 0 )
24		expsub	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) )
25	22 23 16 9 24	syl22anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) )
26	21 25	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → 1 < ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) )
27		rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
28	8 16 27	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
29	28	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
30	3 29 11	ltmuldivd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( ( 1 · ( 𝐴 ↑ 𝑀 ) ) < ( 𝐴 ↑ 𝑁 ) ↔ 1 < ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) ) )
31	26 30	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 1 · ( 𝐴 ↑ 𝑀 ) ) < ( 𝐴 ↑ 𝑁 ) )
32	14 31	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) )