Theorem ltexp2

Description: Ordering law for exponentiation. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 5-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑦 ) )
2		oveq2	⊢ ( 𝑥 = 𝑀 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑀 ) )
3		oveq2	⊢ ( 𝑥 = 𝑁 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑁 ) )
4		zssre	⊢ ℤ ⊆ ℝ
5		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
6		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
7		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
8		0lt1	⊢ 0 < 1
9	8	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 1 )
10		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 < 𝐴 )
11	6 7 5 9 10	lttrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
12	5 11	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
13		rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℤ ) → ( 𝐴 ↑ 𝑥 ) ∈ ℝ+ )
14	12 13	sylan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐴 ↑ 𝑥 ) ∈ ℝ+ )
15	14	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐴 ↑ 𝑥 ) ∈ ℝ )
16		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∈ ℝ )
17		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
18		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
19		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 1 < 𝐴 )
20		ltexp2a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 1 < 𝐴 ∧ 𝑥 < 𝑦 ) ) → ( 𝐴 ↑ 𝑥 ) < ( 𝐴 ↑ 𝑦 ) )
21	20	expr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑥 < 𝑦 → ( 𝐴 ↑ 𝑥 ) < ( 𝐴 ↑ 𝑦 ) ) )
22	16 17 18 19 21	syl31anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 < 𝑦 → ( 𝐴 ↑ 𝑥 ) < ( 𝐴 ↑ 𝑦 ) ) )
23	1 2 3 4 15 22	ltord1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) ) )
24	23	ancom2s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) ) )
25	24	exp43	⊢ ( 𝐴 ∈ ℝ → ( 1 < 𝐴 → ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℤ → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) ) ) ) ) )
26	25	com24	⊢ ( 𝐴 ∈ ℝ → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 1 < 𝐴 → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) ) ) ) ) )
27	26	3imp1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) ) )