Metamath Proof Explorer

Theorem leexp1a

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

Ref Expression
Assertion leexp1a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ N ∈ ℕ 0 ∧ 0 ≤ A ∧ A ≤ B → A N ≤ B N

Proof

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