Step | Hyp | Ref
| Expression |
1 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = 0 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑0)) |
2 | 1 | oveq2d 7248 |
. . 3
⊢ (𝑚 = 0 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑0))) |
3 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = 0 → (𝑁 + 𝑚) = (𝑁 + 0)) |
4 | 3 | fveq2d 6740 |
. . 3
⊢ (𝑚 = 0 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 0))) |
5 | 2, 4 | breq12d 5081 |
. 2
⊢ (𝑚 = 0 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑0)) ≤ (!‘(𝑁 + 0)))) |
6 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = 𝑘 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑘)) |
7 | 6 | oveq2d 7248 |
. . 3
⊢ (𝑚 = 𝑘 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) |
8 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = 𝑘 → (𝑁 + 𝑚) = (𝑁 + 𝑘)) |
9 | 8 | fveq2d 6740 |
. . 3
⊢ (𝑚 = 𝑘 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑘))) |
10 | 7, 9 | breq12d 5081 |
. 2
⊢ (𝑚 = 𝑘 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)))) |
11 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = (𝑘 + 1) → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑(𝑘 + 1))) |
12 | 11 | oveq2d 7248 |
. . 3
⊢ (𝑚 = (𝑘 + 1) → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1)))) |
13 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = (𝑘 + 1) → (𝑁 + 𝑚) = (𝑁 + (𝑘 + 1))) |
14 | 13 | fveq2d 6740 |
. . 3
⊢ (𝑚 = (𝑘 + 1) → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + (𝑘 + 1)))) |
15 | 12, 14 | breq12d 5081 |
. 2
⊢ (𝑚 = (𝑘 + 1) → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1))))) |
16 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = 𝑀 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑀)) |
17 | 16 | oveq2d 7248 |
. . 3
⊢ (𝑚 = 𝑀 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑀))) |
18 | | oveq2 7240 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑁 + 𝑚) = (𝑁 + 𝑀)) |
19 | 18 | fveq2d 6740 |
. . 3
⊢ (𝑚 = 𝑀 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑀))) |
20 | 17, 19 | breq12d 5081 |
. 2
⊢ (𝑚 = 𝑀 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀)))) |
21 | | faccl 13877 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
22 | 21 | nnred 11870 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℝ) |
23 | 22 | leidd 11423 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ≤
(!‘𝑁)) |
24 | | nn0cn 12125 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
25 | | peano2cn 11029 |
. . . . . . 7
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
27 | 26 | exp0d 13738 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1)↑0) =
1) |
28 | 27 | oveq2d 7248 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
= ((!‘𝑁) ·
1)) |
29 | 21 | nncnd 11871 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
30 | 29 | mulid1d 10875 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· 1) = (!‘𝑁)) |
31 | 28, 30 | eqtrd 2778 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
= (!‘𝑁)) |
32 | 24 | addid1d 11057 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 0) = 𝑁) |
33 | 32 | fveq2d 6740 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 0)) =
(!‘𝑁)) |
34 | 23, 31, 33 | 3brtr4d 5100 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
≤ (!‘(𝑁 +
0))) |
35 | 22 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑁) ∈ ℝ) |
36 | | peano2nn0 12155 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
37 | 36 | nn0red 12176 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
38 | | reexpcl 13679 |
. . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑𝑘) ∈
ℝ) |
39 | 37, 38 | sylan 583 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℝ) |
40 | 35, 39 | remulcld 10888 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ) |
41 | | nnnn0 12122 |
. . . . . . . . . . 11
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℕ0) |
42 | 41 | nn0ge0d 12178 |
. . . . . . . . . 10
⊢
((!‘𝑁) ∈
ℕ → 0 ≤ (!‘𝑁)) |
43 | 21, 42 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (!‘𝑁)) |
44 | 43 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ (!‘𝑁)) |
45 | 37 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ∈ ℝ) |
46 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℕ0) |
47 | 36 | nn0ge0d 12178 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (𝑁 +
1)) |
48 | 47 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ (𝑁 + 1)) |
49 | 45, 46, 48 | expge0d 13762 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ ((𝑁 + 1)↑𝑘)) |
50 | 35, 39, 44, 49 | mulge0d 11434 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) |
51 | 40, 50 | jca 515 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘)))) |
52 | | nn0addcl 12150 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 𝑘) ∈
ℕ0) |
53 | 52 | faccld 13878 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℕ) |
54 | 53 | nnred 11870 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℝ) |
55 | | nn0re 12124 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
56 | | peano2nn0 12155 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
57 | 56 | nn0red 12176 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
58 | | readdcl 10837 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑁 + (𝑘 + 1)) ∈ ℝ) |
59 | 55, 57, 58 | syl2an 599 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + (𝑘 + 1)) ∈ ℝ) |
60 | 45, 48, 59 | jca31 518 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ)) |
61 | 51, 54, 60 | jca31 518 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))) |
62 | 61 | adantr 484 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))) |
63 | 32 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 0) = 𝑁) |
64 | | nn0ge0 12140 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) |
65 | 64 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ 𝑘) |
66 | | 0re 10860 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
67 | | nn0re 12124 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
68 | 67 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℝ) |
69 | 55 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑁 ∈ ℝ) |
70 | | leadd2 11326 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝑘
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) |
71 | 66, 68, 69, 70 | mp3an2i 1468 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) |
72 | 65, 71 | mpbid 235 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 0) ≤ (𝑁 + 𝑘)) |
73 | 63, 72 | eqbrtrrd 5092 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑁 ≤ (𝑁 + 𝑘)) |
74 | 52 | nn0red 12176 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 𝑘) ∈ ℝ) |
75 | | 1re 10858 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
76 | | leadd1 11325 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ ∧ 1 ∈ ℝ)
→ (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) |
77 | 75, 76 | mp3an3 1452 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) |
78 | 69, 74, 77 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) |
79 | 73, 78 | mpbid 235 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1)) |
80 | | nn0cn 12125 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
81 | | ax-1cn 10812 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
82 | | addass 10841 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) |
83 | 81, 82 | mp3an3 1452 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) |
84 | 24, 80, 83 | syl2an 599 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) |
85 | 79, 84 | breqtrd 5094 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) |
86 | 85 | anim1ci 619 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1)))) |
87 | | lemul12a 11715 |
. . . 4
⊢
((((((!‘𝑁)
· ((𝑁 +
1)↑𝑘)) ∈ ℝ
∧ 0 ≤ ((!‘𝑁)
· ((𝑁 +
1)↑𝑘))) ∧
(!‘(𝑁 + 𝑘)) ∈ ℝ) ∧
(((𝑁 + 1) ∈ ℝ
∧ 0 ≤ (𝑁 + 1)) ∧
(𝑁 + (𝑘 + 1)) ∈ ℝ)) →
((((!‘𝑁) ·
((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) ≤ ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1))))) |
88 | 62, 86, 87 | sylc 65 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) ≤ ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
89 | | expp1 13669 |
. . . . . . 7
⊢ (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1))) |
90 | 26, 89 | sylan 583 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1))) |
91 | 90 | oveq2d 7248 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))) |
92 | 29 | adantr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑁) ∈ ℂ) |
93 | | expcl 13680 |
. . . . . . 7
⊢ (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑𝑘) ∈
ℂ) |
94 | 26, 93 | sylan 583 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℂ) |
95 | 26 | adantr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ∈ ℂ) |
96 | 92, 94, 95 | mulassd 10881 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))) |
97 | 91, 96 | eqtr4d 2781 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1))) |
98 | 97 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1))) |
99 | | facp1 13872 |
. . . . . 6
⊢ ((𝑁 + 𝑘) ∈ ℕ0 →
(!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1))) |
100 | 52, 99 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1))) |
101 | 84 | fveq2d 6740 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = (!‘(𝑁 + (𝑘 + 1)))) |
102 | 84 | oveq2d 7248 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
103 | 100, 101,
102 | 3eqtr3d 2786 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
104 | 103 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) |
105 | 88, 98, 104 | 3brtr4d 5100 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))) |
106 | 5, 10, 15, 20, 34, 105 | nn0indd 12299 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))) |