Metamath Proof Explorer

Theorem leexp2r

Description: Weak ordering relationship for exponentiation of a fixed real base in [ 0 , 1 ] to integer exponents. (Contributed by Paul Chapman, 14-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑗 = 𝑀 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑀 ) )
2 1 breq1d ⊢ ( 𝑗 = 𝑀 → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
3 2 imbi2d ⊢ ( 𝑗 = 𝑀 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
4 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
5 4 breq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
6 5 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
7 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
8 7 breq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
9 8 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
10 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
11 10 breq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
12 11 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
13 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
15 14 leidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑀 ) )
16 simprll ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝐴 ∈ ℝ )
17 1red ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 1 ∈ ℝ )
18 simprlr ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝑀 ∈ ℕ0 )
19 simpl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
20 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
21 18 19 20 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝑘 ∈ ℕ0 )
22 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
23 16 21 22 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
24 simprrl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 0 ≤ 𝐴 )
25 expge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → 0 ≤ ( 𝐴 ↑ 𝑘 ) )
26 16 21 24 25 syl3anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 0 ≤ ( 𝐴 ↑ 𝑘 ) )
27 simprrr ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝐴 ≤ 1 )
28 16 17 23 26 27 lemul2ad ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ≤ ( ( 𝐴 ↑ 𝑘 ) · 1 ) )
29 16 recnd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝐴 ∈ ℂ )
30 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
31 29 21 30 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
32 23 recnd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
33 32 mulridd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · 1 ) = ( 𝐴 ↑ 𝑘 ) )
34 33 eqcomd ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) · 1 ) )
35 28 31 34 3brtr4d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑘 ) )
36 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
37 21 36 syl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
38 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
39 16 37 38 syl2anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
40 13 ad2antrl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
41 letr ⊢ ( ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 𝐴 ↑ 𝑘 ) ∈ ℝ ∧ ( 𝐴 ↑ 𝑀 ) ∈ ℝ ) → ( ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑘 ) ∧ ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
42 39 23 40 41 syl3anc ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑘 ) ∧ ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
43 35 42 mpand ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
44 43 ex ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
45 44 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
46 3 6 9 12 15 45 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
47 46 expd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
48 47 com12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
49 48 3impia ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
50 49 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) )