Proof of Theorem faclbnd4lem3
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℕ
∨ 𝐾 =
0)) |
| 2 | | 0exp 14138 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ →
(0↑𝐾) =
0) |
| 3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (0↑𝐾) =
0) |
| 4 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
| 5 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 6 | | nn0sqcl 14130 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (𝐾↑2) ∈
ℕ0) |
| 7 | | nn0expcl 14116 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ (𝐾↑2) ∈ ℕ0) →
(2↑(𝐾↑2)) ∈
ℕ0) |
| 8 | 5, 6, 7 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ (2↑(𝐾↑2))
∈ ℕ0) |
| 9 | 8 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (2↑(𝐾↑2)) ∈
ℕ0) |
| 10 | | nn0addcl 12561 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 + 𝐾) ∈
ℕ0) |
| 11 | | nn0expcl 14116 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ (𝑀 + 𝐾) ∈ ℕ0)
→ (𝑀↑(𝑀 + 𝐾)) ∈
ℕ0) |
| 12 | 10, 11 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀↑(𝑀 + 𝐾)) ∈
ℕ0) |
| 13 | 9, 12 | nn0mulcld 12592 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈
ℕ0) |
| 14 | 4, 13 | sylan2 593 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ ((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) ∈
ℕ0) |
| 15 | 14 | nn0ge0d 12590 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 0 ≤ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) |
| 16 | 3, 15 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (0↑𝐾) ≤
((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾)))) |
| 17 | | 1nn 12277 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
| 18 | | elnn0 12528 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 19 | | nnnn0 12533 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 20 | | 0nn0 12541 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
| 21 | | nn0addcl 12561 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 0 ∈ ℕ0) → (𝑀 + 0) ∈
ℕ0) |
| 22 | 19, 20, 21 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑀 + 0) ∈
ℕ0) |
| 23 | | nnexpcl 14115 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ (𝑀 + 0) ∈
ℕ0) → (𝑀↑(𝑀 + 0)) ∈ ℕ) |
| 24 | 22, 23 | mpdan 687 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑀↑(𝑀 + 0)) ∈ ℕ) |
| 25 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 = 0 → 𝑀 = 0) |
| 26 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = 0 → (𝑀 + 0) = (0 + 0)) |
| 27 | | 00id 11436 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 0) =
0 |
| 28 | 26, 27 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 = 0 → (𝑀 + 0) = 0) |
| 29 | 25, 28 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑀 = 0 → (𝑀↑(𝑀 + 0)) = (0↑0)) |
| 30 | | 0exp0e1 14107 |
. . . . . . . . . . . . . 14
⊢
(0↑0) = 1 |
| 31 | 29, 30 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑀 = 0 → (𝑀↑(𝑀 + 0)) = 1) |
| 32 | 31, 17 | eqeltrdi 2849 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝑀↑(𝑀 + 0)) ∈ ℕ) |
| 33 | 24, 32 | jaoi 858 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → (𝑀↑(𝑀 + 0)) ∈ ℕ) |
| 34 | 18, 33 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (𝑀↑(𝑀 + 0)) ∈
ℕ) |
| 35 | | nnmulcl 12290 |
. . . . . . . . . 10
⊢ ((1
∈ ℕ ∧ (𝑀↑(𝑀 + 0)) ∈ ℕ) → (1 ·
(𝑀↑(𝑀 + 0))) ∈ ℕ) |
| 36 | 17, 34, 35 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (1 · (𝑀↑(𝑀 + 0))) ∈ ℕ) |
| 37 | 36 | nnge1d 12314 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ 1 ≤ (1 · (𝑀↑(𝑀 + 0)))) |
| 38 | 37 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 = 0) → 1 ≤
(1 · (𝑀↑(𝑀 + 0)))) |
| 39 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝐾 = 0 → (0↑𝐾) = (0↑0)) |
| 40 | 39, 30 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝐾 = 0 → (0↑𝐾) = 1) |
| 41 | | sq0i 14232 |
. . . . . . . . . . . 12
⊢ (𝐾 = 0 → (𝐾↑2) = 0) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝐾 = 0 → (2↑(𝐾↑2)) =
(2↑0)) |
| 43 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 44 | | exp0 14106 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ → (2↑0) = 1) |
| 45 | 43, 44 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(2↑0) = 1 |
| 46 | 42, 45 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝐾 = 0 → (2↑(𝐾↑2)) = 1) |
| 47 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝐾 = 0 → (𝑀 + 𝐾) = (𝑀 + 0)) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝐾 = 0 → (𝑀↑(𝑀 + 𝐾)) = (𝑀↑(𝑀 + 0))) |
| 49 | 46, 48 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝐾 = 0 → ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) = (1 · (𝑀↑(𝑀 + 0)))) |
| 50 | 40, 49 | breq12d 5156 |
. . . . . . . 8
⊢ (𝐾 = 0 → ((0↑𝐾) ≤ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ↔ 1 ≤ (1 · (𝑀↑(𝑀 + 0))))) |
| 51 | 50 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 = 0) →
((0↑𝐾) ≤
((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) ↔ 1 ≤ (1 · (𝑀↑(𝑀 + 0))))) |
| 52 | 38, 51 | mpbird 257 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 = 0) →
(0↑𝐾) ≤
((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾)))) |
| 53 | 16, 52 | jaodan 960 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈ ℕ
∨ 𝐾 = 0)) →
(0↑𝐾) ≤
((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾)))) |
| 54 | 1, 53 | sylan2b 594 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (0↑𝐾) ≤ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) |
| 55 | | nn0cn 12536 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
| 56 | 55 | exp0d 14180 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀↑0) =
1) |
| 57 | 56 | oveq2d 7447 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ ((0↑𝐾) ·
(𝑀↑0)) =
((0↑𝐾) ·
1)) |
| 58 | | nn0expcl 14116 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 𝐾 ∈ ℕ0) →
(0↑𝐾) ∈
ℕ0) |
| 59 | 20, 58 | mpan 690 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (0↑𝐾) ∈
ℕ0) |
| 60 | 59 | nn0cnd 12589 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (0↑𝐾) ∈
ℂ) |
| 61 | 60 | mulridd 11278 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ ((0↑𝐾) ·
1) = (0↑𝐾)) |
| 62 | 57, 61 | sylan9eq 2797 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((0↑𝐾) · (𝑀↑0)) = (0↑𝐾)) |
| 63 | 13 | nn0cnd 12589 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ) |
| 64 | 63 | mulridd 11278 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · 1) = ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) |
| 65 | 54, 62, 64 | 3brtr4d 5175 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((0↑𝐾) · (𝑀↑0)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · 1)) |
| 66 | 65 | adantr 480 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ 𝑁 = 0) → ((0↑𝐾) · (𝑀↑0)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · 1)) |
| 67 | | oveq1 7438 |
. . . . 5
⊢ (𝑁 = 0 → (𝑁↑𝐾) = (0↑𝐾)) |
| 68 | | oveq2 7439 |
. . . . 5
⊢ (𝑁 = 0 → (𝑀↑𝑁) = (𝑀↑0)) |
| 69 | 67, 68 | oveq12d 7449 |
. . . 4
⊢ (𝑁 = 0 → ((𝑁↑𝐾) · (𝑀↑𝑁)) = ((0↑𝐾) · (𝑀↑0))) |
| 70 | | fveq2 6906 |
. . . . . 6
⊢ (𝑁 = 0 → (!‘𝑁) =
(!‘0)) |
| 71 | | fac0 14315 |
. . . . . 6
⊢
(!‘0) = 1 |
| 72 | 70, 71 | eqtrdi 2793 |
. . . . 5
⊢ (𝑁 = 0 → (!‘𝑁) = 1) |
| 73 | 72 | oveq2d 7447 |
. . . 4
⊢ (𝑁 = 0 → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · 1)) |
| 74 | 69, 73 | breq12d 5156 |
. . 3
⊢ (𝑁 = 0 → (((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ↔ ((0↑𝐾) · (𝑀↑0)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · 1))) |
| 75 | 74 | adantl 481 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ 𝑁 = 0) → (((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ↔ ((0↑𝐾) · (𝑀↑0)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · 1))) |
| 76 | 66, 75 | mpbird 257 |
1
⊢ (((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) ∧ 𝑁 = 0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |