Metamath Proof Explorer

Theorem leexp1a

Description: Weak base ordering relationship for exponentiation of real bases to a fixed nonnegative integer exponent. (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 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )