Step | Hyp | Ref
| Expression |
1 | | elnn0 9137 |
. 2
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
2 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
3 | 2 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = 0 → (𝑀↑(𝑗 + 1)) = (𝑀↑(0 + 1))) |
4 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑗 = 0 → (!‘𝑗) =
(!‘0)) |
5 | 4 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = 0 → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘0))) |
6 | 3, 5 | breq12d 4002 |
. . . . . 6
⊢ (𝑗 = 0 → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑(0 + 1)) ≤ ((𝑀↑𝑀) · (!‘0)))) |
7 | 6 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = 0 → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑(0 + 1)) ≤ ((𝑀↑𝑀) · (!‘0))))) |
8 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
9 | 8 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑀↑(𝑗 + 1)) = (𝑀↑(𝑘 + 1))) |
10 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) |
11 | 10 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘𝑘))) |
12 | 9, 11 | breq12d 4002 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)))) |
13 | 12 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))))) |
14 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) |
15 | 14 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑀↑(𝑗 + 1)) = (𝑀↑((𝑘 + 1) + 1))) |
16 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) |
17 | 16 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
18 | 15, 17 | breq12d 4002 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
19 | 18 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
20 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
21 | 20 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑀↑(𝑗 + 1)) = (𝑀↑(𝑁 + 1))) |
22 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (!‘𝑗) = (!‘𝑁)) |
23 | 22 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → ((𝑀↑𝑀) · (!‘𝑗)) = ((𝑀↑𝑀) · (!‘𝑁))) |
24 | 21, 23 | breq12d 4002 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗)) ↔ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
25 | 24 | imbi2d 229 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑀 ∈ ℕ → (𝑀↑(𝑗 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑗))) ↔ (𝑀 ∈ ℕ → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))))) |
26 | | nnre 8885 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
27 | | nnge1 8901 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 1 ≤
𝑀) |
28 | | elnnuz 9523 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈
(ℤ≥‘1)) |
29 | 28 | biimpi 119 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘1)) |
30 | 26, 27, 29 | leexp2ad 10638 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑1) ≤ (𝑀↑𝑀)) |
31 | | 0p1e1 8992 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
32 | 31 | oveq2i 5864 |
. . . . . . 7
⊢ (𝑀↑(0 + 1)) = (𝑀↑1) |
33 | 32 | a1i 9 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑀↑(0 + 1)) = (𝑀↑1)) |
34 | | fac0 10662 |
. . . . . . . 8
⊢
(!‘0) = 1 |
35 | 34 | oveq2i 5864 |
. . . . . . 7
⊢ ((𝑀↑𝑀) · (!‘0)) = ((𝑀↑𝑀) · 1) |
36 | | nnnn0 9142 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
37 | 26, 36 | reexpcld 10626 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑀↑𝑀) ∈ ℝ) |
38 | 37 | recnd 7948 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀↑𝑀) ∈ ℂ) |
39 | 38 | mulid1d 7937 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑀↑𝑀) · 1) = (𝑀↑𝑀)) |
40 | 35, 39 | eqtrid 2215 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑀↑𝑀) · (!‘0)) = (𝑀↑𝑀)) |
41 | 30, 33, 40 | 3brtr4d 4021 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀↑(0 + 1)) ≤ ((𝑀↑𝑀) · (!‘0))) |
42 | 26 | ad3antrrr 489 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑀 ∈ ℝ) |
43 | | simpllr 529 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑘 ∈ ℕ0) |
44 | | peano2nn0 9175 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
45 | 43, 44 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑘 + 1) ∈
ℕ0) |
46 | 42, 45 | reexpcld 10626 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑(𝑘 + 1)) ∈ ℝ) |
47 | 36 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑀 ∈
ℕ0) |
48 | 42, 47 | reexpcld 10626 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑𝑀) ∈ ℝ) |
49 | 43 | faccld 10670 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (!‘𝑘) ∈ ℕ) |
50 | 49 | nnred 8891 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (!‘𝑘) ∈ ℝ) |
51 | 48, 50 | remulcld 7950 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑𝑀) · (!‘𝑘)) ∈ ℝ) |
52 | | nn0re 9144 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
53 | | peano2re 8055 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
54 | 43, 52, 53 | 3syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ) |
55 | | nngt0 8903 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
56 | 55 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 0 < 𝑀) |
57 | | 0re 7920 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
58 | | ltle 8007 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ) → (0 < 𝑀 → 0 ≤ 𝑀)) |
59 | 57, 58 | mpan 422 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℝ → (0 <
𝑀 → 0 ≤ 𝑀)) |
60 | 42, 56, 59 | sylc 62 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 0 ≤ 𝑀) |
61 | 42, 45, 60 | expge0d 10627 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 0 ≤ (𝑀↑(𝑘 + 1))) |
62 | | simplr 525 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) |
63 | | simprr 527 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → 𝑀 ≤ (𝑘 + 1)) |
64 | 46, 51, 42, 54, 61, 60, 62, 63 | lemul12ad 8858 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) ∧ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑(𝑘 + 1)) · 𝑀) ≤ (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
65 | 64 | anandis 587 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑(𝑘 + 1)) · 𝑀) ≤ (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
66 | | nncn 8886 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
67 | | expp1 10483 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝑀↑((𝑘 + 1) + 1)) = ((𝑀↑(𝑘 + 1)) · 𝑀)) |
68 | 66, 44, 67 | syl2an 287 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑((𝑘 + 1) + 1)) = ((𝑀↑(𝑘 + 1)) · 𝑀)) |
69 | 68 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑((𝑘 + 1) + 1)) = ((𝑀↑(𝑘 + 1)) · 𝑀)) |
70 | | facp1 10664 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
71 | 70 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
72 | 71 | oveq2d 5869 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) · (!‘(𝑘 + 1))) = ((𝑀↑𝑀) · ((!‘𝑘) · (𝑘 + 1)))) |
73 | 38 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑𝑀) ∈
ℂ) |
74 | | faccl 10669 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
75 | 74 | nncnd 8892 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℂ) |
76 | 75 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (!‘𝑘) ∈
ℂ) |
77 | | nn0cn 9145 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
78 | | peano2cn 8054 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℂ → (𝑘 + 1) ∈
ℂ) |
79 | 77, 78 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) |
80 | 79 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℂ) |
81 | 73, 76, 80 | mulassd 7943 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1)) = ((𝑀↑𝑀) · ((!‘𝑘) · (𝑘 + 1)))) |
82 | 72, 81 | eqtr4d 2206 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) · (!‘(𝑘 + 1))) = (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
83 | 82 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → ((𝑀↑𝑀) · (!‘(𝑘 + 1))) = (((𝑀↑𝑀) · (!‘𝑘)) · (𝑘 + 1))) |
84 | 65, 69, 83 | 3brtr4d 4021 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) ∧ 𝑀 ≤ (𝑘 + 1))) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
85 | 84 | exp32 363 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀 ≤ (𝑘 + 1) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
86 | 85 | com23 78 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀 ≤ (𝑘 + 1) → ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
87 | | nn0ltp1le 9274 |
. . . . . . . . . . 11
⊢ (((𝑘 + 1) ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝑘 + 1) < 𝑀 ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
88 | 44, 36, 87 | syl2anr 288 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 + 1) < 𝑀 ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
89 | | peano2nn0 9175 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 1) ∈ ℕ0
→ ((𝑘 + 1) + 1) ∈
ℕ0) |
90 | 44, 89 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((𝑘 + 1) + 1) ∈
ℕ0) |
91 | | reexpcl 10493 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ ((𝑘 + 1) + 1) ∈
ℕ0) → (𝑀↑((𝑘 + 1) + 1)) ∈ ℝ) |
92 | 26, 90, 91 | syl2an 287 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑((𝑘 + 1) + 1)) ∈
ℝ) |
93 | 92 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑((𝑘 + 1) + 1)) ∈ ℝ) |
94 | 37 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑𝑀) ∈ ℝ) |
95 | 44 | faccld 10670 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1))
∈ ℕ) |
96 | 95 | nnred 8891 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1))
∈ ℝ) |
97 | | remulcl 7902 |
. . . . . . . . . . . . . 14
⊢ (((𝑀↑𝑀) ∈ ℝ ∧ (!‘(𝑘 + 1)) ∈ ℝ) →
((𝑀↑𝑀) · (!‘(𝑘 + 1))) ∈ ℝ) |
98 | 37, 96, 97 | syl2an 287 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) · (!‘(𝑘 + 1))) ∈
ℝ) |
99 | 98 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑀↑𝑀) · (!‘(𝑘 + 1))) ∈ ℝ) |
100 | 26 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 𝑀 ∈ ℝ) |
101 | 27 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 1 ≤ 𝑀) |
102 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑘 + 1) + 1) ≤ 𝑀) |
103 | 90 | ad2antlr 486 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑘 + 1) + 1) ∈
ℕ0) |
104 | 103 | nn0zd 9332 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → ((𝑘 + 1) + 1) ∈
ℤ) |
105 | | nnz 9231 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
106 | 105 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 𝑀 ∈ ℤ) |
107 | | eluz 9500 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑘 + 1) + 1) ∈ ℤ ∧
𝑀 ∈ ℤ) →
(𝑀 ∈
(ℤ≥‘((𝑘 + 1) + 1)) ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
108 | 104, 106,
107 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀 ∈
(ℤ≥‘((𝑘 + 1) + 1)) ↔ ((𝑘 + 1) + 1) ≤ 𝑀)) |
109 | 102, 108 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → 𝑀 ∈
(ℤ≥‘((𝑘 + 1) + 1))) |
110 | 100, 101,
109 | leexp2ad 10638 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑((𝑘 + 1) + 1)) ≤ (𝑀↑𝑀)) |
111 | 37, 96 | anim12i 336 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑𝑀) ∈ ℝ ∧
(!‘(𝑘 + 1)) ∈
ℝ)) |
112 | | nn0re 9144 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
113 | | id 19 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℕ0) |
114 | | nn0ge0 9160 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ 𝑀) |
115 | 112, 113,
114 | expge0d 10627 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ (𝑀↑𝑀)) |
116 | 36, 115 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 ≤
(𝑀↑𝑀)) |
117 | 95 | nnge1d 8921 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ 1 ≤ (!‘(𝑘 +
1))) |
118 | 116, 117 | anim12i 336 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (0 ≤ (𝑀↑𝑀) ∧ 1 ≤ (!‘(𝑘 + 1)))) |
119 | | lemulge11 8782 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀↑𝑀) ∈ ℝ ∧ (!‘(𝑘 + 1)) ∈ ℝ) ∧ (0
≤ (𝑀↑𝑀) ∧ 1 ≤ (!‘(𝑘 + 1)))) → (𝑀↑𝑀) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
120 | 111, 118,
119 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀↑𝑀) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
121 | 120 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑𝑀) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
122 | 93, 94, 99, 110, 121 | letrd 8043 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
∧ ((𝑘 + 1) + 1) ≤
𝑀) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))) |
123 | 122 | ex 114 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (((𝑘 + 1) + 1) ≤
𝑀 → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
124 | 88, 123 | sylbid 149 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 + 1) < 𝑀 → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
125 | 124 | a1dd 48 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 + 1) < 𝑀 → ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
126 | 105 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ 𝑀 ∈
ℤ) |
127 | 44 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℕ0) |
128 | 127 | nn0zd 9332 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℤ) |
129 | | zlelttric 9257 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑘 + 1) ∈ ℤ) →
(𝑀 ≤ (𝑘 + 1) ∨ (𝑘 + 1) < 𝑀)) |
130 | 126, 128,
129 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑀 ≤ (𝑘 + 1) ∨ (𝑘 + 1) < 𝑀)) |
131 | 86, 125, 130 | mpjaod 713 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1))))) |
132 | 131 | expcom 115 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑀 ∈ ℕ
→ ((𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘)) → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
133 | 132 | a2d 26 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝑀 ∈ ℕ
→ (𝑀↑(𝑘 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑘))) → (𝑀 ∈ ℕ → (𝑀↑((𝑘 + 1) + 1)) ≤ ((𝑀↑𝑀) · (!‘(𝑘 + 1)))))) |
134 | 7, 13, 19, 25, 41, 133 | nn0ind 9326 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑀 ∈ ℕ
→ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
135 | 134 | impcom 124 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
136 | | faccl 10669 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
137 | 136 | nnnn0d 9188 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ0) |
138 | 137 | nn0ge0d 9191 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (!‘𝑁)) |
139 | | nn0p1nn 9174 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
140 | 139 | 0expd 10625 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (0↑(𝑁 + 1)) =
0) |
141 | | 0exp0e1 10481 |
. . . . . . . 8
⊢
(0↑0) = 1 |
142 | 141 | oveq1i 5863 |
. . . . . . 7
⊢
((0↑0) · (!‘𝑁)) = (1 · (!‘𝑁)) |
143 | 136 | nncnd 8892 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
144 | 143 | mulid2d 7938 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1 · (!‘𝑁)) = (!‘𝑁)) |
145 | 142, 144 | eqtrid 2215 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((0↑0) · (!‘𝑁)) = (!‘𝑁)) |
146 | 138, 140,
145 | 3brtr4d 4021 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0↑(𝑁 + 1))
≤ ((0↑0) · (!‘𝑁))) |
147 | | oveq1 5860 |
. . . . . 6
⊢ (𝑀 = 0 → (𝑀↑(𝑁 + 1)) = (0↑(𝑁 + 1))) |
148 | | oveq12 5862 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝑀 = 0) → (𝑀↑𝑀) = (0↑0)) |
149 | 148 | anidms 395 |
. . . . . . 7
⊢ (𝑀 = 0 → (𝑀↑𝑀) = (0↑0)) |
150 | 149 | oveq1d 5868 |
. . . . . 6
⊢ (𝑀 = 0 → ((𝑀↑𝑀) · (!‘𝑁)) = ((0↑0) · (!‘𝑁))) |
151 | 147, 150 | breq12d 4002 |
. . . . 5
⊢ (𝑀 = 0 → ((𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)) ↔ (0↑(𝑁 + 1)) ≤ ((0↑0) ·
(!‘𝑁)))) |
152 | 146, 151 | syl5ibr 155 |
. . . 4
⊢ (𝑀 = 0 → (𝑁 ∈ ℕ0 → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
153 | 152 | imp 123 |
. . 3
⊢ ((𝑀 = 0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
154 | 135, 153 | jaoian 790 |
. 2
⊢ (((𝑀 ∈ ℕ ∨ 𝑀 = 0) ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
155 | 1, 154 | sylanb 282 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |