| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 0 → (𝐴↑𝑗) = (𝐴↑0)) | 
| 2 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 0 → (𝐵↑𝑗) = (𝐵↑0)) | 
| 3 | 1, 2 | breq12d 5156 | . . . . . 6
⊢ (𝑗 = 0 → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑0) ≤ (𝐵↑0))) | 
| 4 | 3 | imbi2d 340 | . . . . 5
⊢ (𝑗 = 0 → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑0) ≤ (𝐵↑0)))) | 
| 5 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) | 
| 6 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝐵↑𝑗) = (𝐵↑𝑘)) | 
| 7 | 5, 6 | breq12d 5156 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑𝑘) ≤ (𝐵↑𝑘))) | 
| 8 | 7 | imbi2d 340 | . . . . 5
⊢ (𝑗 = 𝑘 → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑘) ≤ (𝐵↑𝑘)))) | 
| 9 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) | 
| 10 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝐵↑𝑗) = (𝐵↑(𝑘 + 1))) | 
| 11 | 9, 10 | breq12d 5156 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1)))) | 
| 12 | 11 | imbi2d 340 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))))) | 
| 13 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) | 
| 14 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝐵↑𝑗) = (𝐵↑𝑁)) | 
| 15 | 13, 14 | breq12d 5156 | . . . . . 6
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) ≤ (𝐵↑𝑗) ↔ (𝐴↑𝑁) ≤ (𝐵↑𝑁))) | 
| 16 | 15 | imbi2d 340 | . . . . 5
⊢ (𝑗 = 𝑁 → ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑗) ≤ (𝐵↑𝑗)) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)))) | 
| 17 |  | recn 11245 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 18 |  | recn 11245 | . . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 19 |  | exp0 14106 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) | 
| 20 | 19 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) = 1) | 
| 21 |  | 1le1 11891 | . . . . . . . . 9
⊢ 1 ≤
1 | 
| 22 | 20, 21 | eqbrtrdi 5182 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) ≤
1) | 
| 23 |  | exp0 14106 | . . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (𝐵↑0) = 1) | 
| 24 | 23 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑0) = 1) | 
| 25 | 22, 24 | breqtrrd 5171 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑0) ≤ (𝐵↑0)) | 
| 26 | 17, 18, 25 | syl2an 596 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴↑0) ≤ (𝐵↑0)) | 
| 27 | 26 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑0) ≤ (𝐵↑0)) | 
| 28 |  | reexpcl 14119 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℝ) | 
| 29 | 28 | ad4ant14 752 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴↑𝑘) ∈ ℝ) | 
| 30 |  | simplll 775 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℝ) | 
| 31 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 32 |  | simplrl 777 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 0 ≤
𝐴) | 
| 33 |  | expge0 14139 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0
∧ 0 ≤ 𝐴) → 0
≤ (𝐴↑𝑘)) | 
| 34 | 30, 31, 32, 33 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 0 ≤
(𝐴↑𝑘)) | 
| 35 |  | reexpcl 14119 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑𝑘) ∈
ℝ) | 
| 36 | 35 | ad4ant24 754 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐵↑𝑘) ∈ ℝ) | 
| 37 | 29, 34, 36 | jca31 514 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤ (𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ)) | 
| 38 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) | 
| 39 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵) → 0 ≤ 𝐴) | 
| 40 | 38, 39 | anim12i 613 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) | 
| 42 |  | simpllr 776 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℝ) | 
| 43 | 37, 41, 42 | jca32 515 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤ (𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ) ∧ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ))) | 
| 44 | 43 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → ((((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤ (𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ) ∧ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ))) | 
| 45 |  | simplrr 778 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ≤ 𝐵) | 
| 46 | 45 | anim1ci 616 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → ((𝐴↑𝑘) ≤ (𝐵↑𝑘) ∧ 𝐴 ≤ 𝐵)) | 
| 47 |  | lemul12a 12125 | . . . . . . . . . 10
⊢
(((((𝐴↑𝑘) ∈ ℝ ∧ 0 ≤
(𝐴↑𝑘)) ∧ (𝐵↑𝑘) ∈ ℝ) ∧ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ)) → (((𝐴↑𝑘) ≤ (𝐵↑𝑘) ∧ 𝐴 ≤ 𝐵) → ((𝐴↑𝑘) · 𝐴) ≤ ((𝐵↑𝑘) · 𝐵))) | 
| 48 | 44, 46, 47 | sylc 65 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → ((𝐴↑𝑘) · 𝐴) ≤ ((𝐵↑𝑘) · 𝐵)) | 
| 49 |  | expp1 14109 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) | 
| 50 | 17, 49 | sylan 580 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) | 
| 51 | 50 | ad5ant14 758 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) | 
| 52 |  | expp1 14109 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) | 
| 53 | 18, 52 | sylan 580 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) | 
| 54 | 53 | ad5ant24 761 | . . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) | 
| 55 | 48, 51, 54 | 3brtr4d 5175 | . . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ (0 ≤ 𝐴
∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))) | 
| 56 | 55 | ex 412 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝐴↑𝑘) ≤ (𝐵↑𝑘) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1)))) | 
| 57 | 56 | expcom 413 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (((𝐴 ∈ ℝ
∧ 𝐵 ∈ ℝ)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → ((𝐴↑𝑘) ≤ (𝐵↑𝑘) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))))) | 
| 58 | 57 | a2d 29 | . . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((((𝐴 ∈ ℝ
∧ 𝐵 ∈ ℝ)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑘) ≤ (𝐵↑𝑘)) → (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑(𝑘 + 1)) ≤ (𝐵↑(𝑘 + 1))))) | 
| 59 | 4, 8, 12, 16, 27, 58 | nn0ind 12713 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ ℝ
∧ 𝐵 ∈ ℝ)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))) | 
| 60 | 59 | exp4c 432 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ ℝ
→ (𝐵 ∈ ℝ
→ ((0 ≤ 𝐴 ∧
𝐴 ≤ 𝐵) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))))) | 
| 61 | 60 | com3l 89 | . 2
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝑁 ∈ ℕ0
→ ((0 ≤ 𝐴 ∧
𝐴 ≤ 𝐵) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))))) | 
| 62 | 61 | 3imp1 1348 | 1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) |