Step | Hyp | Ref
| Expression |
1 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = 0 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑0)) |
2 | 1 | oveq2d 5866 |
. . . . 5
⊢ (𝑚 = 0 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑0))) |
3 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = 0 → (𝑁 + 𝑚) = (𝑁 + 0)) |
4 | 3 | fveq2d 5498 |
. . . . 5
⊢ (𝑚 = 0 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 0))) |
5 | 2, 4 | breq12d 4000 |
. . . 4
⊢ (𝑚 = 0 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑0)) ≤ (!‘(𝑁 + 0)))) |
6 | 5 | imbi2d 229 |
. . 3
⊢ (𝑚 = 0 → ((𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚))) ↔ (𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑0)) ≤
(!‘(𝑁 +
0))))) |
7 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = 𝑘 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑘)) |
8 | 7 | oveq2d 5866 |
. . . . 5
⊢ (𝑚 = 𝑘 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) |
9 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝑁 + 𝑚) = (𝑁 + 𝑘)) |
10 | 9 | fveq2d 5498 |
. . . . 5
⊢ (𝑚 = 𝑘 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑘))) |
11 | 8, 10 | breq12d 4000 |
. . . 4
⊢ (𝑚 = 𝑘 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)))) |
12 | 11 | imbi2d 229 |
. . 3
⊢ (𝑚 = 𝑘 → ((𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚))) ↔ (𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))))) |
13 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = (𝑘 + 1) → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑(𝑘 + 1))) |
14 | 13 | oveq2d 5866 |
. . . . 5
⊢ (𝑚 = (𝑘 + 1) → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1)))) |
15 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = (𝑘 + 1) → (𝑁 + 𝑚) = (𝑁 + (𝑘 + 1))) |
16 | 15 | fveq2d 5498 |
. . . . 5
⊢ (𝑚 = (𝑘 + 1) → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + (𝑘 + 1)))) |
17 | 14, 16 | breq12d 4000 |
. . . 4
⊢ (𝑚 = (𝑘 + 1) → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1))))) |
18 | 17 | imbi2d 229 |
. . 3
⊢ (𝑚 = (𝑘 + 1) → ((𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚))) ↔ (𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))))) |
19 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑀)) |
20 | 19 | oveq2d 5866 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑀))) |
21 | | oveq2 5858 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (𝑁 + 𝑚) = (𝑁 + 𝑀)) |
22 | 21 | fveq2d 5498 |
. . . . 5
⊢ (𝑚 = 𝑀 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑀))) |
23 | 20, 22 | breq12d 4000 |
. . . 4
⊢ (𝑚 = 𝑀 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀)))) |
24 | 23 | imbi2d 229 |
. . 3
⊢ (𝑚 = 𝑀 → ((𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚))) ↔ (𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))))) |
25 | | faccl 10656 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
26 | 25 | nnred 8878 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℝ) |
27 | 26 | leidd 8420 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ≤
(!‘𝑁)) |
28 | | nn0cn 9132 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
29 | | peano2cn 8041 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
30 | 28, 29 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
31 | 30 | exp0d 10590 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1)↑0) =
1) |
32 | 31 | oveq2d 5866 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
= ((!‘𝑁) ·
1)) |
33 | 25 | nncnd 8879 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
34 | 33 | mulid1d 7924 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· 1) = (!‘𝑁)) |
35 | 32, 34 | eqtrd 2203 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
= (!‘𝑁)) |
36 | 28 | addid1d 8055 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 0) = 𝑁) |
37 | 36 | fveq2d 5498 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 0)) =
(!‘𝑁)) |
38 | 27, 35, 37 | 3brtr4d 4019 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
≤ (!‘(𝑁 +
0))) |
39 | 26 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑁) ∈ ℝ) |
40 | | peano2nn0 9162 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
41 | 40 | nn0red 9176 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
42 | | reexpcl 10480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 + 1) ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑𝑘) ∈
ℝ) |
43 | 41, 42 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℝ) |
44 | 39, 43 | remulcld 7937 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ) |
45 | | nnnn0 9129 |
. . . . . . . . . . . . . . 15
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℕ0) |
46 | 45 | nn0ge0d 9178 |
. . . . . . . . . . . . . 14
⊢
((!‘𝑁) ∈
ℕ → 0 ≤ (!‘𝑁)) |
47 | 25, 46 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (!‘𝑁)) |
48 | 47 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ (!‘𝑁)) |
49 | 41 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ∈ ℝ) |
50 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℕ0) |
51 | 40 | nn0ge0d 9178 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (𝑁 +
1)) |
52 | 51 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ (𝑁 + 1)) |
53 | 49, 50, 52 | expge0d 10614 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ ((𝑁 + 1)↑𝑘)) |
54 | 39, 43, 48, 53 | mulge0d 8527 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) |
55 | 44, 54 | jca 304 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘)))) |
56 | | nn0addcl 9157 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 𝑘) ∈
ℕ0) |
57 | | faccl 10656 |
. . . . . . . . . . . 12
⊢ ((𝑁 + 𝑘) ∈ ℕ0 →
(!‘(𝑁 + 𝑘)) ∈
ℕ) |
58 | 56, 57 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℕ) |
59 | 58 | nnred 8878 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℝ) |
60 | | nn0re 9131 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
61 | | peano2nn0 9162 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
62 | 61 | nn0red 9176 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
63 | | readdcl 7887 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑁 + (𝑘 + 1)) ∈ ℝ) |
64 | 60, 62, 63 | syl2an 287 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + (𝑘 + 1)) ∈ ℝ) |
65 | 49, 52, 64 | jca31 307 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ)) |
66 | 55, 59, 65 | jca31 307 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))) |
67 | 66 | adantr 274 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))) |
68 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) |
69 | 36 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 0) = 𝑁) |
70 | | nn0ge0 9147 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) |
71 | 70 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ 𝑘) |
72 | | nn0re 9131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
73 | 72 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℝ) |
74 | 60 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑁 ∈ ℝ) |
75 | | 0re 7907 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
76 | | leadd2 8337 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝑘
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) |
77 | 75, 76 | mp3an1 1319 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤
𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) |
78 | 73, 74, 77 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) |
79 | 71, 78 | mpbid 146 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 0) ≤ (𝑁 + 𝑘)) |
80 | 69, 79 | eqbrtrrd 4011 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑁 ≤ (𝑁 + 𝑘)) |
81 | 56 | nn0red 9176 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 𝑘) ∈ ℝ) |
82 | | 1re 7906 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
83 | | leadd1 8336 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ ∧ 1 ∈ ℝ)
→ (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) |
84 | 82, 83 | mp3an3 1321 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) |
85 | 74, 81, 84 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) |
86 | 80, 85 | mpbid 146 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1)) |
87 | | nn0cn 9132 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
88 | | ax-1cn 7854 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
89 | | addass 7891 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) |
90 | 88, 89 | mp3an3 1321 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) |
91 | 28, 87, 90 | syl2an 287 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) |
92 | 86, 91 | breqtrd 4013 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) |
93 | 92 | adantr 274 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) |
94 | 68, 93 | jca 304 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1)))) |
95 | | lemul12a 8765 |
. . . . . . . 8
⊢
((((((!‘𝑁)
· ((𝑁 +
1)↑𝑘)) ∈ ℝ
∧ 0 ≤ ((!‘𝑁)
· ((𝑁 +
1)↑𝑘))) ∧
(!‘(𝑁 + 𝑘)) ∈ ℝ) ∧
(((𝑁 + 1) ∈ ℝ
∧ 0 ≤ (𝑁 + 1)) ∧
(𝑁 + (𝑘 + 1)) ∈ ℝ)) →
((((!‘𝑁) ·
((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) ≤ ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1))))) |
96 | 67, 94, 95 | sylc 62 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) ≤ ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
97 | | expp1 10470 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1))) |
98 | 30, 97 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1))) |
99 | 98 | oveq2d 5866 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))) |
100 | 33 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑁) ∈ ℂ) |
101 | | expcl 10481 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑𝑘) ∈
ℂ) |
102 | 30, 101 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℂ) |
103 | 30 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ∈ ℂ) |
104 | 100, 102,
103 | mulassd 7930 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))) |
105 | 99, 104 | eqtr4d 2206 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1))) |
106 | 105 | adantr 274 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1))) |
107 | | facp1 10651 |
. . . . . . . . . 10
⊢ ((𝑁 + 𝑘) ∈ ℕ0 →
(!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1))) |
108 | 56, 107 | syl 14 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1))) |
109 | 91 | fveq2d 5498 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = (!‘(𝑁 + (𝑘 + 1)))) |
110 | 91 | oveq2d 5866 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
111 | 108, 109,
110 | 3eqtr3d 2211 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
112 | 111 | adantr 274 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
113 | 96, 106, 112 | 3brtr4d 4019 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))) |
114 | 113 | ex 114 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1))))) |
115 | 114 | expcom 115 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝑁 ∈
ℕ0 → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))))) |
116 | 115 | a2d 26 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝑁 ∈
ℕ0 → ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (𝑁 ∈ ℕ0 →
((!‘𝑁) ·
((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))))) |
117 | 6, 12, 18, 24, 38, 116 | nn0ind 9313 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈
ℕ0 → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀)))) |
118 | 117 | impcom 124 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))) |