Metamath Proof Explorer

Theorem leexp2a

Description: Weak ordering relationship for exponentiation of a fixed real base greater than or equal to 1 to integer exponents. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Assertion leexp2a ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℝ )
2 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 ∈ ℝ )
3 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ∈ ℝ )
4 0lt1 ⊢ 0 < 1
5 4 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < 1 )
6 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ≤ 𝐴 )
7 2 3 1 5 6 ltletrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < 𝐴 )
8 1 7 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℝ+ )
9 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
10 9 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℤ )
11 rpexpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ+ )
12 8 10 11 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ+ )
13 12 rpred ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
15 14 mullidd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 · ( 𝐴 ↑ 𝑀 ) ) = ( 𝐴 ↑ 𝑀 ) )
16 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
17 16 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
18 expge1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 1 ≤ 𝐴 ) → 1 ≤ ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) )
19 1 17 6 18 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ≤ ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) )
20 1 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℂ )
21 7 gt0ne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ≠ 0 )
22 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
23 22 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℤ )
24 expsub ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) )
25 20 21 23 10 24 syl22anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) )
26 19 25 breqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ≤ ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) )
27 rpexpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
28 8 23 27 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
29 28 rpred ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
30 3 29 12 lemuldivd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 1 · ( 𝐴 ↑ 𝑀 ) ) ≤ ( 𝐴 ↑ 𝑁 ) ↔ 1 ≤ ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ 𝑀 ) ) ) )
31 26 30 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 · ( 𝐴 ↑ 𝑀 ) ) ≤ ( 𝐴 ↑ 𝑁 ) )
32 15 31 eqbrtrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) )