Metamath Proof Explorer


Theorem leexp1a

Description: Weak base ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005)

Ref Expression
Assertion leexp1a ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑗 = 0 → ( 𝐴𝑗 ) = ( 𝐴 ↑ 0 ) )
2 oveq2 ( 𝑗 = 0 → ( 𝐵𝑗 ) = ( 𝐵 ↑ 0 ) )
3 1 2 breq12d ( 𝑗 = 0 → ( ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ↔ ( 𝐴 ↑ 0 ) ≤ ( 𝐵 ↑ 0 ) ) )
4 3 imbi2d ( 𝑗 = 0 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴 ↑ 0 ) ≤ ( 𝐵 ↑ 0 ) ) ) )
5 oveq2 ( 𝑗 = 𝑘 → ( 𝐴𝑗 ) = ( 𝐴𝑘 ) )
6 oveq2 ( 𝑗 = 𝑘 → ( 𝐵𝑗 ) = ( 𝐵𝑘 ) )
7 5 6 breq12d ( 𝑗 = 𝑘 → ( ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ↔ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) )
8 7 imbi2d ( 𝑗 = 𝑘 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) ) )
9 oveq2 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
10 oveq2 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐵𝑗 ) = ( 𝐵 ↑ ( 𝑘 + 1 ) ) )
11 9 10 breq12d ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ↔ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐵 ↑ ( 𝑘 + 1 ) ) ) )
12 11 imbi2d ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐵 ↑ ( 𝑘 + 1 ) ) ) ) )
13 oveq2 ( 𝑗 = 𝑁 → ( 𝐴𝑗 ) = ( 𝐴𝑁 ) )
14 oveq2 ( 𝑗 = 𝑁 → ( 𝐵𝑗 ) = ( 𝐵𝑁 ) )
15 13 14 breq12d ( 𝑗 = 𝑁 → ( ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ↔ ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) ) )
16 15 imbi2d ( 𝑗 = 𝑁 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑗 ) ≤ ( 𝐵𝑗 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) ) ) )
17 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
18 recn ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
19 exp0 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
20 19 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 0 ) = 1 )
21 1le1 1 ≤ 1
22 20 21 eqbrtrdi ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 0 ) ≤ 1 )
23 exp0 ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 0 ) = 1 )
24 23 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 0 ) = 1 )
25 22 24 breqtrrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 0 ) ≤ ( 𝐵 ↑ 0 ) )
26 17 18 25 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑ 0 ) ≤ ( 𝐵 ↑ 0 ) )
27 26 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴 ↑ 0 ) ≤ ( 𝐵 ↑ 0 ) )
28 reexpcl ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℝ )
29 28 ad4ant14 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℝ )
30 simplll ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
31 simpr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
32 simplrl ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 𝐴 )
33 expge0 ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → 0 ≤ ( 𝐴𝑘 ) )
34 30 31 32 33 syl3anc ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( 𝐴𝑘 ) )
35 reexpcl ( ( 𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) ∈ ℝ )
36 35 ad4ant24 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) ∈ ℝ )
37 29 34 36 jca31 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝐴𝑘 ) ) ∧ ( 𝐵𝑘 ) ∈ ℝ ) )
38 simpl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
39 simpl ( ( 0 ≤ 𝐴𝐴𝐵 ) → 0 ≤ 𝐴 )
40 38 39 anim12i ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
41 40 adantr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
42 simpllr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℝ )
43 37 41 42 jca32 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝐴𝑘 ) ) ∧ ( 𝐵𝑘 ) ∈ ℝ ) ∧ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ) )
44 43 adantr ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝐴𝑘 ) ) ∧ ( 𝐵𝑘 ) ∈ ℝ ) ∧ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ) )
45 simplrr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴𝐵 )
46 45 anim1ci ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ∧ 𝐴𝐵 ) )
47 lemul12a ( ( ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝐴𝑘 ) ) ∧ ( 𝐵𝑘 ) ∈ ℝ ) ∧ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ) → ( ( ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ∧ 𝐴𝐵 ) → ( ( 𝐴𝑘 ) · 𝐴 ) ≤ ( ( 𝐵𝑘 ) · 𝐵 ) ) )
48 44 46 47 sylc ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( ( 𝐴𝑘 ) · 𝐴 ) ≤ ( ( 𝐵𝑘 ) · 𝐵 ) )
49 expp1 ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴𝑘 ) · 𝐴 ) )
50 17 49 sylan ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴𝑘 ) · 𝐴 ) )
51 50 ad5ant14 ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴𝑘 ) · 𝐴 ) )
52 expp1 ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐵𝑘 ) · 𝐵 ) )
53 18 52 sylan ( ( 𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐵𝑘 ) · 𝐵 ) )
54 53 ad5ant24 ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( 𝐵 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐵𝑘 ) · 𝐵 ) )
55 48 51 54 3brtr4d ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐵 ↑ ( 𝑘 + 1 ) ) )
56 55 ex ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐵 ↑ ( 𝑘 + 1 ) ) ) )
57 56 expcom ( 𝑘 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐵 ↑ ( 𝑘 + 1 ) ) ) ) )
58 57 a2d ( 𝑘 ∈ ℕ0 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑘 ) ≤ ( 𝐵𝑘 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐵 ↑ ( 𝑘 + 1 ) ) ) ) )
59 4 8 12 16 27 58 nn0ind ( 𝑁 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) ) )
60 59 exp4c ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( ( 0 ≤ 𝐴𝐴𝐵 ) → ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) ) ) ) )
61 60 com3l ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 𝑁 ∈ ℕ0 → ( ( 0 ≤ 𝐴𝐴𝐵 ) → ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) ) ) ) )
62 61 3imp1 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( 𝐴𝑁 ) ≤ ( 𝐵𝑁 ) )