Step | Hyp | Ref
| Expression |
1 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = 0 → (𝐴↑𝑗) = (𝐴↑0)) |
2 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = 0 → (𝐵↑𝑗) = (𝐵↑0)) |
3 | 1, 2 | breq12d 3978 |
. . . . . 6
⊢ (𝑗 = 0 → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑0) ≤ (𝐵↑0))) |
4 | 3 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = 0 → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑0) ≤ (𝐵↑0)))) |
5 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
6 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐵↑𝑗) = (𝐵↑𝑘)) |
7 | 5, 6 | breq12d 3978 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑𝑘) ≤ (𝐵↑𝑘))) |
8 | 7 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑘) ≤ (𝐵↑𝑘)))) |
9 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
10 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝐵↑𝑗) = (𝐵↑(𝑘 + 1))) |
11 | 9, 10 | breq12d 3978 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1)))) |
12 | 11 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))))) |
13 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
14 | | oveq2 5829 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝐵↑𝑗) = (𝐵↑𝑁)) |
15 | 13, 14 | breq12d 3978 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑𝑁) ≤ (𝐵↑𝑁))) |
16 | 15 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)))) |
17 | | recn 7860 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
18 | | recn 7860 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
19 | | exp0 10418 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
20 | 19 | adantr 274 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1) |
21 | | 1le1 8442 |
. . . . . . . . 9
⊢ 1 ≤
1 |
22 | 20, 21 | eqbrtrdi 4003 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) ≤
1) |
23 | | exp0 10418 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1) |
24 | 23 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1) |
25 | 22, 24 | breqtrrd 3992 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) ≤ (𝐵↑0)) |
26 | 17, 18, 25 | syl2an 287 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴↑0) ≤ (𝐵↑0)) |
27 | 26 | adantr 274 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑0) ≤ (𝐵↑0)) |
28 | | simpll 519 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
29 | | reexpcl 10431 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℝ) |
30 | 28, 29 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴↑𝑘) ∈ ℝ) |
31 | | simplll 523 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℝ) |
32 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
33 | | simplrl 525 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 0 ≤
𝐴) |
34 | | expge0 10450 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0
∧ 0 ≤ 𝐴) → 0
≤ (𝐴↑𝑘)) |
35 | 31, 32, 33, 34 | syl3anc 1220 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 0 ≤
(𝐴↑𝑘)) |
36 | | simplr 520 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
37 | | reexpcl 10431 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑𝑘) ∈
ℝ) |
38 | 36, 37 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐵↑𝑘) ∈ ℝ) |
39 | 30, 35, 38 | jca31 307 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤ (𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ)) |
40 | | simpl 108 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) |
41 | | simpl 108 |
. . . . . . . . . . . . . 14
⊢ ((0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵) → 0 ≤ 𝐴) |
42 | 40, 41 | anim12i 336 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
43 | 42 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
44 | | simpllr 524 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℝ) |
45 | 39, 43, 44 | jca32 308 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤ (𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ) ∧ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ))) |
46 | 45 | adantr 274 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → ((((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤ (𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ) ∧ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ))) |
47 | | simpr 109 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐴↑𝑘) ≤ (𝐵↑𝑘)) |
48 | | simplrr 526 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ≤ 𝐵) |
49 | 48 | adantr 274 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → 𝐴 ≤ 𝐵) |
50 | 47, 49 | jca 304 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → ((𝐴↑𝑘) ≤ (𝐵↑𝑘) ∧ 𝐴 ≤ 𝐵)) |
51 | | lemul12a 8728 |
. . . . . . . . . 10
⊢
(((((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤
(𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ) ∧ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ)) → (((𝐴↑𝑘) ≤ (𝐵↑𝑘) ∧ 𝐴 ≤ 𝐵) → ((𝐴↑𝑘) · 𝐴) ≤ ((𝐵↑𝑘) · 𝐵))) |
52 | 46, 50, 51 | sylc 62 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → ((𝐴↑𝑘) · 𝐴) ≤ ((𝐵↑𝑘) · 𝐵)) |
53 | | expp1 10421 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
54 | 17, 53 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
55 | 54 | adantlr 469 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
56 | 55 | adantlr 469 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
57 | 56 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
58 | | expp1 10421 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) |
59 | 18, 58 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) |
60 | 59 | adantll 468 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) |
61 | 60 | adantlr 469 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) |
62 | 61 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) |
63 | 52, 57, 62 | 3brtr4d 3996 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))) |
64 | 63 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝐴↑𝑘) ≤ (𝐵↑𝑘) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1)))) |
65 | 64 | expcom 115 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (((𝐴 ∈ ℝ
∧ 𝐵 ∈ ℝ)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → ((𝐴↑𝑘) ≤ (𝐵↑𝑘) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))))) |
66 | 65 | a2d 26 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((((𝐴 ∈ ℝ
∧ 𝐵 ∈ ℝ)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))))) |
67 | 4, 8, 12, 16, 27, 66 | nn0ind 9273 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ ℝ
∧ 𝐵 ∈ ℝ)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))) |
68 | 67 | exp4c 366 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ ℝ
→ (𝐵 ∈ ℝ
→ ((0 ≤ 𝐴 ∧
𝐴 ≤ 𝐵) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))))) |
69 | 68 | com3l 81 |
. 2
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝑁 ∈ ℕ0
→ ((0 ≤ 𝐴 ∧
𝐴 ≤ 𝐵) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))))) |
70 | 69 | 3imp1 1202 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) |