This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 < 𝐴 ∧ 𝑀 < 𝑁 ) ) → ( 𝐴 ↑ 𝑀 ) < ( 𝐴 ↑ 𝑁 ) )