| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. 2
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 2 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
| 3 | 2 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 0 → (𝑀↑(𝑗 + 1)) = (𝑀↑(0 + 1))) |
| 4 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = 0 → (!‘𝑗) =
(!‘0)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 0 → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘0))) |
| 6 | 3, 5 | breq12d 5156 |
. . . . . 6
⊢ (𝑗 = 0 → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑(0 + 1)) ≤ ((𝑀↑𝑀) · (!‘0)))) |
| 7 | 6 | imbi2d 340 |
. . . . 5
⊢ (𝑗 = 0 → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑(0 + 1)) ≤ ((𝑀↑𝑀) · (!‘0))))) |
| 8 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
| 9 | 8 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑀↑(𝑗 + 1)) = (𝑀↑(𝑘 + 1))) |
| 10 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) |
| 11 | 10 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘𝑘))) |
| 12 | 9, 11 | breq12d 5156 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)))) |
| 13 | 12 | imbi2d 340 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))))) |
| 14 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) |
| 15 | 14 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑀↑(𝑗 + 1)) = (𝑀↑((𝑘 + 1) + 1))) |
| 16 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) |
| 17 | 16 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
| 18 | 15, 17 | breq12d 5156 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
| 19 | 18 | imbi2d 340 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
| 20 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
| 21 | 20 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑀↑(𝑗 + 1)) = (𝑀↑(𝑁 + 1))) |
| 22 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (!‘𝑗) = (!‘𝑁)) |
| 23 | 22 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘𝑁))) |
| 24 | 21, 23 | breq12d 5156 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
| 25 | 24 | imbi2d 340 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))))) |
| 26 | | nnre 12273 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 27 | | nnge1 12294 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 1 ≤
𝑀) |
| 28 | | elnnuz 12922 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈
(ℤ≥‘1)) |
| 29 | 28 | biimpi 216 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘1)) |
| 30 | 26, 27, 29 | leexp2ad 14293 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑1) ≤ (𝑀↑𝑀)) |
| 31 | | 0p1e1 12388 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 32 | 31 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑀↑(0 + 1)) = (𝑀↑1) |
| 33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑(0 + 1)) = (𝑀↑1)) |
| 34 | | fac0 14315 |
. . . . . . . 8
⊢
(!‘0) = 1 |
| 35 | 34 | oveq2i 7442 |
. . . . . . 7
⊢ ((𝑀↑𝑀) · (!‘0)) = ((𝑀↑𝑀) · 1) |
| 36 | | nnnn0 12533 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 37 | 26, 36 | reexpcld 14203 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑀↑𝑀) ∈ ℝ) |
| 38 | 37 | recnd 11289 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀↑𝑀) ∈ ℂ) |
| 39 | 38 | mulridd 11278 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑀↑𝑀) · 1) = (𝑀↑𝑀)) |
| 40 | 35, 39 | eqtrid 2789 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑀↑𝑀) · (!‘0)) = (𝑀↑𝑀)) |
| 41 | 30, 33, 40 | 3brtr4d 5175 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀↑(0 + 1)) ≤ ((𝑀↑𝑀) · (!‘0))) |
| 42 | 26 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑀 ∈ ℝ) |
| 43 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑘 ∈ ℕ0) |
| 44 | | peano2nn0 12566 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑘 + 1) ∈
ℕ0) |
| 46 | 42, 45 | reexpcld 14203 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑(𝑘 + 1)) ∈ ℝ) |
| 47 | 36 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑀 ∈
ℕ0) |
| 48 | 42, 47 | reexpcld 14203 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑𝑀) ∈ ℝ) |
| 49 | 43 | faccld 14323 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (!‘𝑘) ∈ ℕ) |
| 50 | 49 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (!‘𝑘) ∈ ℝ) |
| 51 | 48, 50 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑𝑀) · (!‘𝑘)) ∈ ℝ) |
| 52 | | nn0re 12535 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
| 53 | | peano2re 11434 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
| 54 | 43, 52, 53 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ) |
| 55 | | nngt0 12297 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
| 56 | 55 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 0 < 𝑀) |
| 57 | | 0re 11263 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
| 58 | | ltle 11349 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ) → (0 < 𝑀 → 0 ≤ 𝑀)) |
| 59 | 57, 58 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℝ → (0 <
𝑀 → 0 ≤ 𝑀)) |
| 60 | 42, 56, 59 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 0 ≤ 𝑀) |
| 61 | 42, 45, 60 | expge0d 14204 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 0 ≤ (𝑀↑(𝑘 + 1))) |
| 62 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) |
| 63 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑀 ≤ (𝑘 + 1)) |
| 64 | 46, 51, 42, 54, 61, 60, 62, 63 | lemul12ad 12210 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑(𝑘 + 1)) · 𝑀) ≤ (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
| 65 | 64 | anandis 678 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑(𝑘 + 1)) · 𝑀) ≤ (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
| 66 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
| 67 | | expp1 14109 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝑀↑((𝑘 + 1) + 1)) = ((𝑀↑(𝑘 + 1)) · 𝑀)) |
| 68 | 66, 44, 67 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑((𝑘 + 1) + 1)) = ((𝑀↑(𝑘 + 1)) · 𝑀)) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑((𝑘 + 1) + 1)) = ((𝑀↑(𝑘 + 1)) · 𝑀)) |
| 70 | | facp1 14317 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
| 71 | 70 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
| 72 | 71 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) · (!‘(𝑘 + 1))) = ((𝑀↑𝑀) · ((!‘𝑘) · (𝑘 + 1)))) |
| 73 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑𝑀) ∈
ℂ) |
| 74 | | faccl 14322 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
| 75 | 74 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℂ) |
| 76 | 75 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (!‘𝑘) ∈
ℂ) |
| 77 | | nn0cn 12536 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
| 78 | | peano2cn 11433 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℂ → (𝑘 + 1) ∈
ℂ) |
| 79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℂ) |
| 81 | 73, 76, 80 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1)) = ((𝑀↑𝑀) · ((!‘𝑘) · (𝑘 + 1)))) |
| 82 | 72, 81 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) · (!‘(𝑘 + 1))) = (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑𝑀) · (!‘(𝑘 + 1))) = (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
| 84 | 65, 69, 83 | 3brtr4d 5175 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
| 85 | 84 | exp32 420 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀 ≤ (𝑘 + 1) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
| 86 | 85 | com23 86 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀 ≤ (𝑘 + 1) → ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
| 87 | | nn0ltp1le 12676 |
. . . . . . . . . . 11
⊢ (((𝑘 + 1) ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝑘 + 1) < 𝑀 ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
| 88 | 44, 36, 87 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 + 1) < 𝑀 ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
| 89 | | peano2nn0 12566 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 1) ∈ ℕ0
→ ((𝑘 + 1) + 1) ∈
ℕ0) |
| 90 | 44, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((𝑘 + 1) + 1) ∈
ℕ0) |
| 91 | | reexpcl 14119 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ ((𝑘 + 1) + 1) ∈
ℕ0) → (𝑀↑((𝑘 + 1) + 1)) ∈ ℝ) |
| 92 | 26, 90, 91 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑((𝑘 + 1) + 1)) ∈
ℝ) |
| 93 | 92 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑((𝑘 + 1) + 1)) ∈ ℝ) |
| 94 | 37 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑𝑀) ∈ ℝ) |
| 95 | 44 | faccld 14323 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1))
∈ ℕ) |
| 96 | 95 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1))
∈ ℝ) |
| 97 | | remulcl 11240 |
. . . . . . . . . . . . . 14
⊢ (((𝑀↑𝑀) ∈ ℝ ∧ (!‘(𝑘 + 1)) ∈ ℝ) →
((𝑀↑𝑀) · (!‘(𝑘 + 1))) ∈ ℝ) |
| 98 | 37, 96, 97 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) · (!‘(𝑘 + 1))) ∈
ℝ) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑀↑𝑀) · (!‘(𝑘 + 1))) ∈ ℝ) |
| 100 | 26 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 𝑀 ∈ ℝ) |
| 101 | 27 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 1 ≤ 𝑀) |
| 102 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑘 + 1) + 1) ≤ 𝑀) |
| 103 | 90 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑘 + 1) + 1) ∈
ℕ0) |
| 104 | 103 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑘 + 1) + 1) ∈
ℤ) |
| 105 | | nnz 12634 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 106 | 105 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 𝑀 ∈ ℤ) |
| 107 | | eluz 12892 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑘 + 1) + 1) ∈ ℤ ∧
𝑀 ∈ ℤ) →
(𝑀 ∈
(ℤ≥‘((𝑘 + 1) + 1)) ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
| 108 | 104, 106,
107 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀 ∈
(ℤ≥‘((𝑘 + 1) + 1)) ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
| 109 | 102, 108 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 𝑀 ∈
(ℤ≥‘((𝑘 + 1) + 1))) |
| 110 | 100, 101,
109 | leexp2ad 14293 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑((𝑘 + 1) + 1)) ≤ (𝑀↑𝑀)) |
| 111 | 37, 96 | anim12i 613 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) ∈ ℝ ∧
(!‘(𝑘 + 1)) ∈
ℝ)) |
| 112 | | nn0re 12535 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
| 113 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℕ0) |
| 114 | | nn0ge0 12551 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ 𝑀) |
| 115 | 112, 113,
114 | expge0d 14204 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ (𝑀↑𝑀)) |
| 116 | 36, 115 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 ≤
(𝑀↑𝑀)) |
| 117 | 95 | nnge1d 12314 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ 1 ≤ (!‘(𝑘 +
1))) |
| 118 | 116, 117 | anim12i 613 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (0 ≤ (𝑀↑𝑀) ∧ 1 ≤ (!‘(𝑘 + 1)))) |
| 119 | | lemulge11 12130 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀↑𝑀) ∈ ℝ ∧ (!‘(𝑘 + 1)) ∈ ℝ) ∧ (0
≤ (𝑀↑𝑀) ∧ 1 ≤ (!‘(𝑘 + 1)))) → (𝑀↑𝑀) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
| 120 | 111, 118,
119 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑𝑀) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
| 121 | 120 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑𝑀) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
| 122 | 93, 94, 99, 110, 121 | letrd 11418 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
| 123 | 122 | ex 412 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((𝑘 + 1) + 1) ≤
𝑀 → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
| 124 | 88, 123 | sylbid 240 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 + 1) < 𝑀 → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
| 125 | 124 | a1dd 50 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 + 1) < 𝑀 → ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
| 126 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
| 127 | | lelttric 11368 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑀 ≤ (𝑘 + 1) ∨ (𝑘 + 1) < 𝑀)) |
| 128 | 26, 126, 127 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀 ≤ (𝑘 + 1) ∨ (𝑘 + 1) < 𝑀)) |
| 129 | 86, 125, 128 | mpjaod 861 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
| 130 | 129 | expcom 413 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑀 ∈ ℕ
→ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
| 131 | 130 | a2d 29 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝑀 ∈ ℕ
→ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) → (𝑀 ∈ ℕ → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
| 132 | 7, 13, 19, 25, 41, 131 | nn0ind 12713 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑀 ∈ ℕ
→ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
| 133 | 132 | impcom 407 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 134 | | faccl 14322 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
| 135 | 134 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ0) |
| 136 | 135 | nn0ge0d 12590 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (!‘𝑁)) |
| 137 | | nn0p1nn 12565 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
| 138 | 137 | 0expd 14179 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (0↑(𝑁 + 1)) =
0) |
| 139 | | 0exp0e1 14107 |
. . . . . . . 8
⊢
(0↑0) = 1 |
| 140 | 139 | oveq1i 7441 |
. . . . . . 7
⊢
((0↑0) · (!‘𝑁)) = (1 · (!‘𝑁)) |
| 141 | 134 | nncnd 12282 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
| 142 | 141 | mullidd 11279 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1 · (!‘𝑁)) = (!‘𝑁)) |
| 143 | 140, 142 | eqtrid 2789 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((0↑0) · (!‘𝑁)) = (!‘𝑁)) |
| 144 | 136, 138,
143 | 3brtr4d 5175 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0↑(𝑁 + 1))
≤ ((0↑0) · (!‘𝑁))) |
| 145 | | oveq1 7438 |
. . . . . 6
⊢ (𝑀 = 0 → (𝑀↑(𝑁 + 1)) = (0↑(𝑁 + 1))) |
| 146 | | oveq12 7440 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝑀 = 0) → (𝑀↑𝑀) = (0↑0)) |
| 147 | 146 | anidms 566 |
. . . . . . 7
⊢ (𝑀 = 0 → (𝑀↑𝑀) = (0↑0)) |
| 148 | 147 | oveq1d 7446 |
. . . . . 6
⊢ (𝑀 = 0 → ((𝑀↑𝑀) · (!‘𝑁)) = ((0↑0) · (!‘𝑁))) |
| 149 | 145, 148 | breq12d 5156 |
. . . . 5
⊢ (𝑀 = 0 → ((𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)) ↔ (0↑(𝑁 + 1)) ≤ ((0↑0) ·
(!‘𝑁)))) |
| 150 | 144, 149 | imbitrrid 246 |
. . . 4
⊢ (𝑀 = 0 → (𝑁 ∈ ℕ0 → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
| 151 | 150 | imp 406 |
. . 3
⊢ ((𝑀 = 0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 152 | 133, 151 | jaoian 959 |
. 2
⊢ (((𝑀 ∈ ℕ ∨ 𝑀 = 0) ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 153 | 1, 152 | sylanb 581 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |