Metamath Proof Explorer

Theorem expmordi

Description: Base ordering relationship for exponentiation of nonnegative reals to a fixed positive integer power. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion expmordi ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑎 = 1 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 1 ) )
2 oveq2 ⊢ ( 𝑎 = 1 → ( 𝐵 ↑ 𝑎 ) = ( 𝐵 ↑ 1 ) )
3 1 2 breq12d ⊢ ( 𝑎 = 1 → ( ( 𝐴 ↑ 𝑎 ) < ( 𝐵 ↑ 𝑎 ) ↔ ( 𝐴 ↑ 1 ) < ( 𝐵 ↑ 1 ) ) )
4 3 imbi2d ⊢ ( 𝑎 = 1 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 ↑ 𝑎 ) < ( 𝐵 ↑ 𝑎 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 ↑ 1 ) < ( 𝐵 ↑ 1 ) ) ) )
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 exp1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
20 exp1 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 1 ) = 𝐵 )
21 19 20 breqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 1 ) < ( 𝐵 ↑ 1 ) ↔ 𝐴 < 𝐵 ) )
22 17 18 21 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ↑ 1 ) < ( 𝐵 ↑ 1 ) ↔ 𝐴 < 𝐵 ) )
23 22 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 ↑ 1 ) < ( 𝐵 ↑ 1 ) )
24 23 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 ↑ 1 ) < ( 𝐵 ↑ 1 ) )
25 simp2ll ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 𝐴 ∈ ℝ )
26 nnnn0 ⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℕ0 )
27 26 3ad2ant1 ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 𝑏 ∈ ℕ0 )
28 25 27 reexpcld ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐴 ↑ 𝑏 ) ∈ ℝ )
29 simp2lr ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 𝐵 ∈ ℝ )
30 29 27 reexpcld ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐵 ↑ 𝑏 ) ∈ ℝ )
31 28 30 jca ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( ( 𝐴 ↑ 𝑏 ) ∈ ℝ ∧ ( 𝐵 ↑ 𝑏 ) ∈ ℝ ) )
32 simp2rl ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 0 ≤ 𝐴 )
33 25 27 32 expge0d ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 0 ≤ ( 𝐴 ↑ 𝑏 ) )
34 simp3 ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) )
35 33 34 jca ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 0 ≤ ( 𝐴 ↑ 𝑏 ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) )
36 simp2l ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
37 simp2r ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) )
38 ltmul12a ⊢ ( ( ( ( ( 𝐴 ↑ 𝑏 ) ∈ ℝ ∧ ( 𝐵 ↑ 𝑏 ) ∈ ℝ ) ∧ ( 0 ≤ ( 𝐴 ↑ 𝑏 ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ) → ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) < ( ( 𝐵 ↑ 𝑏 ) · 𝐵 ) )
39 31 35 36 37 38 syl22anc ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) < ( ( 𝐵 ↑ 𝑏 ) · 𝐵 ) )
40 25 recnd ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 𝐴 ∈ ℂ )
41 40 27 expp1d ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) = ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) )
42 29 recnd ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → 𝐵 ∈ ℂ )
43 42 27 expp1d ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐵 ↑ ( 𝑏 + 1 ) ) = ( ( 𝐵 ↑ 𝑏 ) · 𝐵 ) )
44 39 41 43 3brtr4d ⊢ ( ( 𝑏 ∈ ℕ ∧ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) < ( 𝐵 ↑ ( 𝑏 + 1 ) ) )
45 44 3exp ⊢ ( 𝑏 ∈ ℕ → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) < ( 𝐵 ↑ ( 𝑏 + 1 ) ) ) ) )
46 45 a2d ⊢ ( 𝑏 ∈ ℕ → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 ↑ 𝑏 ) < ( 𝐵 ↑ 𝑏 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) < ( 𝐵 ↑ ( 𝑏 + 1 ) ) ) ) )
47 4 8 12 16 24 46 nnind ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) ) )
48 47 impcom ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) )
49 48 3impa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) < ( 𝐵 ↑ 𝑁 ) )