| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = 0 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑0)) | 
| 2 | 1 | oveq2d 7447 | . . 3
⊢ (𝑚 = 0 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑0))) | 
| 3 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = 0 → (𝑁 + 𝑚) = (𝑁 + 0)) | 
| 4 | 3 | fveq2d 6910 | . . 3
⊢ (𝑚 = 0 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 0))) | 
| 5 | 2, 4 | breq12d 5156 | . 2
⊢ (𝑚 = 0 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑0)) ≤ (!‘(𝑁 + 0)))) | 
| 6 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = 𝑘 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑘)) | 
| 7 | 6 | oveq2d 7447 | . . 3
⊢ (𝑚 = 𝑘 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) | 
| 8 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = 𝑘 → (𝑁 + 𝑚) = (𝑁 + 𝑘)) | 
| 9 | 8 | fveq2d 6910 | . . 3
⊢ (𝑚 = 𝑘 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑘))) | 
| 10 | 7, 9 | breq12d 5156 | . 2
⊢ (𝑚 = 𝑘 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)))) | 
| 11 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = (𝑘 + 1) → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑(𝑘 + 1))) | 
| 12 | 11 | oveq2d 7447 | . . 3
⊢ (𝑚 = (𝑘 + 1) → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1)))) | 
| 13 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = (𝑘 + 1) → (𝑁 + 𝑚) = (𝑁 + (𝑘 + 1))) | 
| 14 | 13 | fveq2d 6910 | . . 3
⊢ (𝑚 = (𝑘 + 1) → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + (𝑘 + 1)))) | 
| 15 | 12, 14 | breq12d 5156 | . 2
⊢ (𝑚 = (𝑘 + 1) → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1))))) | 
| 16 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = 𝑀 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑀)) | 
| 17 | 16 | oveq2d 7447 | . . 3
⊢ (𝑚 = 𝑀 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑀))) | 
| 18 |  | oveq2 7439 | . . . 4
⊢ (𝑚 = 𝑀 → (𝑁 + 𝑚) = (𝑁 + 𝑀)) | 
| 19 | 18 | fveq2d 6910 | . . 3
⊢ (𝑚 = 𝑀 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑀))) | 
| 20 | 17, 19 | breq12d 5156 | . 2
⊢ (𝑚 = 𝑀 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀)))) | 
| 21 |  | faccl 14322 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) | 
| 22 | 21 | nnred 12281 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℝ) | 
| 23 | 22 | leidd 11829 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ≤
(!‘𝑁)) | 
| 24 |  | nn0cn 12536 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) | 
| 25 |  | peano2cn 11433 | . . . . . . 7
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) | 
| 26 | 24, 25 | syl 17 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) | 
| 27 | 26 | exp0d 14180 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1)↑0) =
1) | 
| 28 | 27 | oveq2d 7447 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
= ((!‘𝑁) ·
1)) | 
| 29 | 21 | nncnd 12282 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) | 
| 30 | 29 | mulridd 11278 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· 1) = (!‘𝑁)) | 
| 31 | 28, 30 | eqtrd 2777 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
= (!‘𝑁)) | 
| 32 | 24 | addridd 11461 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 0) = 𝑁) | 
| 33 | 32 | fveq2d 6910 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 0)) =
(!‘𝑁)) | 
| 34 | 23, 31, 33 | 3brtr4d 5175 | . 2
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· ((𝑁 + 1)↑0))
≤ (!‘(𝑁 +
0))) | 
| 35 | 22 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑁) ∈ ℝ) | 
| 36 |  | peano2nn0 12566 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 37 | 36 | nn0red 12588 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) | 
| 38 |  | reexpcl 14119 | . . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑𝑘) ∈
ℝ) | 
| 39 | 37, 38 | sylan 580 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℝ) | 
| 40 | 35, 39 | remulcld 11291 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ) | 
| 41 |  | nnnn0 12533 | . . . . . . . . . . 11
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℕ0) | 
| 42 | 41 | nn0ge0d 12590 | . . . . . . . . . 10
⊢
((!‘𝑁) ∈
ℕ → 0 ≤ (!‘𝑁)) | 
| 43 | 21, 42 | syl 17 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (!‘𝑁)) | 
| 44 | 43 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ (!‘𝑁)) | 
| 45 | 37 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ∈ ℝ) | 
| 46 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℕ0) | 
| 47 | 36 | nn0ge0d 12590 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ (𝑁 +
1)) | 
| 48 | 47 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ (𝑁 + 1)) | 
| 49 | 45, 46, 48 | expge0d 14204 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ ((𝑁 + 1)↑𝑘)) | 
| 50 | 35, 39, 44, 49 | mulge0d 11840 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) | 
| 51 | 40, 50 | jca 511 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘)))) | 
| 52 |  | nn0addcl 12561 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 𝑘) ∈
ℕ0) | 
| 53 | 52 | faccld 14323 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℕ) | 
| 54 | 53 | nnred 12281 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℝ) | 
| 55 |  | nn0re 12535 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) | 
| 56 |  | peano2nn0 12566 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) | 
| 57 | 56 | nn0red 12588 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) | 
| 58 |  | readdcl 11238 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑁 + (𝑘 + 1)) ∈ ℝ) | 
| 59 | 55, 57, 58 | syl2an 596 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + (𝑘 + 1)) ∈ ℝ) | 
| 60 | 45, 48, 59 | jca31 514 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ)) | 
| 61 | 51, 54, 60 | jca31 514 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))) | 
| 62 | 61 | adantr 480 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤
((!‘𝑁) ·
((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))) | 
| 63 | 32 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 0) = 𝑁) | 
| 64 |  | nn0ge0 12551 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) | 
| 65 | 64 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 0 ≤ 𝑘) | 
| 66 |  | 0re 11263 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 67 |  | nn0re 12535 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) | 
| 68 | 67 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℝ) | 
| 69 | 55 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑁 ∈ ℝ) | 
| 70 |  | leadd2 11732 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝑘
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) | 
| 71 | 66, 68, 69, 70 | mp3an2i 1468 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘))) | 
| 72 | 65, 71 | mpbid 232 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 0) ≤ (𝑁 + 𝑘)) | 
| 73 | 63, 72 | eqbrtrrd 5167 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → 𝑁 ≤ (𝑁 + 𝑘)) | 
| 74 | 52 | nn0red 12588 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 𝑘) ∈ ℝ) | 
| 75 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 76 |  | leadd1 11731 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ ∧ 1 ∈ ℝ)
→ (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) | 
| 77 | 75, 76 | mp3an3 1452 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) | 
| 78 | 69, 74, 77 | syl2anc 584 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))) | 
| 79 | 73, 78 | mpbid 232 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1)) | 
| 80 |  | nn0cn 12536 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 81 |  | ax-1cn 11213 | . . . . . . . 8
⊢ 1 ∈
ℂ | 
| 82 |  | addass 11242 | . . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) | 
| 83 | 81, 82 | mp3an3 1452 | . . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) | 
| 84 | 24, 80, 83 | syl2an 596 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1))) | 
| 85 | 79, 84 | breqtrd 5169 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) | 
| 86 | 85 | anim1ci 616 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1)))) | 
| 87 |  | lemul12a 12125 | . . . 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 14109 | . . . . . . 7
⊢ (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1))) | 
| 90 | 26, 89 | sylan 580 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1))) | 
| 91 | 90 | oveq2d 7447 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))) | 
| 92 | 29 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑁) ∈ ℂ) | 
| 93 |  | expcl 14120 | . . . . . . 7
⊢ (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 + 1)↑𝑘) ∈
ℂ) | 
| 94 | 26, 93 | sylan 580 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℂ) | 
| 95 | 26 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑁 + 1) ∈ ℂ) | 
| 96 | 92, 94, 95 | mulassd 11284 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))) | 
| 97 | 91, 96 | eqtr4d 2780 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1))) | 
| 98 | 97 | adantr 480 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1))) | 
| 99 |  | facp1 14317 | . . . . . 6
⊢ ((𝑁 + 𝑘) ∈ ℕ0 →
(!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1))) | 
| 100 | 52, 99 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1))) | 
| 101 | 84 | fveq2d 6910 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = (!‘(𝑁 + (𝑘 + 1)))) | 
| 102 | 84 | oveq2d 7447 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) | 
| 103 | 100, 101,
102 | 3eqtr3d 2785 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) | 
| 104 | 103 | adantr 480 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))) | 
| 105 | 88, 98, 104 | 3brtr4d 5175 | . 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))) | 
| 106 | 5, 10, 15, 20, 34, 105 | nn0indd 12715 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))) |