Metamath Proof Explorer


Theorem leexp2r

Description: Weak ordering relationship for exponentiation. (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 mulid1d ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ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 ) ) → ( 𝐴𝑁 ) ≤ ( 𝐴𝑀 ) )