Proof of Theorem fac2xp3
| Step | Hyp | Ref
| Expression |
| 1 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 2 | | nn0cn 12536 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℂ) |
| 3 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ (2 · 𝑥)
∈ ℂ) |
| 5 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 6 | | addass 11242 |
. . . . . . . . 9
⊢ (((2
· 𝑥) ∈ ℂ
∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + 2) + 1) = ((2 · 𝑥) + (2 + 1))) |
| 7 | 1, 5, 6 | mp3an23 1455 |
. . . . . . . 8
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
2) + 1) = ((2 · 𝑥) +
(2 + 1))) |
| 8 | 4, 7 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0
→ (((2 · 𝑥) +
2) + 1) = ((2 · 𝑥) +
(2 + 1))) |
| 9 | | df-3 12330 |
. . . . . . . . 9
⊢ 3 = (2 +
1) |
| 10 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ 3 = (2 + 1)) |
| 11 | 10 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0
→ ((2 · 𝑥) + 3)
= ((2 · 𝑥) + (2 +
1))) |
| 12 | 8, 11 | eqtr4d 2780 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
→ (((2 · 𝑥) +
2) + 1) = ((2 · 𝑥) +
3)) |
| 13 | 12 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
→ (!‘(((2 · 𝑥) + 2) + 1)) = (!‘((2 · 𝑥) + 3))) |
| 14 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 15 | | nn0mulcl 12562 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ 𝑥 ∈ ℕ0) → (2
· 𝑥) ∈
ℕ0) |
| 16 | 14, 15 | mpan 690 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0
→ (2 · 𝑥)
∈ ℕ0) |
| 17 | | nn0addcl 12561 |
. . . . . . . 8
⊢ (((2
· 𝑥) ∈
ℕ0 ∧ 2 ∈ ℕ0) → ((2 ·
𝑥) + 2) ∈
ℕ0) |
| 18 | 14, 17 | mpan2 691 |
. . . . . . 7
⊢ ((2
· 𝑥) ∈
ℕ0 → ((2 · 𝑥) + 2) ∈
ℕ0) |
| 19 | 16, 18 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
→ ((2 · 𝑥) + 2)
∈ ℕ0) |
| 20 | | facp1 14317 |
. . . . . 6
⊢ (((2
· 𝑥) + 2) ∈
ℕ0 → (!‘(((2 · 𝑥) + 2) + 1)) = ((!‘((2 · 𝑥) + 2)) · (((2 ·
𝑥) + 2) +
1))) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
→ (!‘(((2 · 𝑥) + 2) + 1)) = ((!‘((2 · 𝑥) + 2)) · (((2 ·
𝑥) + 2) +
1))) |
| 22 | 13, 21 | eqtr3d 2779 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 3)) = ((!‘((2 · 𝑥) + 2)) · (((2 ·
𝑥) + 2) +
1))) |
| 23 | 12 | oveq2d 7447 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ ((!‘((2 · 𝑥) + 2)) · (((2 · 𝑥) + 2) + 1)) = ((!‘((2
· 𝑥) + 2)) ·
((2 · 𝑥) +
3))) |
| 24 | 22, 23 | eqtrd 2777 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 3)) = ((!‘((2 · 𝑥) + 2)) · ((2 ·
𝑥) + 3))) |
| 25 | | addass 11242 |
. . . . . . . . . . 11
⊢ (((2
· 𝑥) ∈ ℂ
∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + 1) + 1) = ((2 · 𝑥) + (1 + 1))) |
| 26 | 5, 5, 25 | mp3an23 1455 |
. . . . . . . . . 10
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
1) + 1) = ((2 · 𝑥) +
(1 + 1))) |
| 27 | 4, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ (((2 · 𝑥) +
1) + 1) = ((2 · 𝑥) +
(1 + 1))) |
| 28 | | df-2 12329 |
. . . . . . . . . . 11
⊢ 2 = (1 +
1) |
| 29 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0
→ 2 = (1 + 1)) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ ((2 · 𝑥) + 2)
= ((2 · 𝑥) + (1 +
1))) |
| 31 | 27, 30 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ (((2 · 𝑥) +
1) + 1) = ((2 · 𝑥) +
2)) |
| 32 | 31 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0
→ (!‘(((2 · 𝑥) + 1) + 1)) = (!‘((2 · 𝑥) + 2))) |
| 33 | | peano2nn0 12566 |
. . . . . . . . 9
⊢ ((2
· 𝑥) ∈
ℕ0 → ((2 · 𝑥) + 1) ∈
ℕ0) |
| 34 | 16, 33 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ ((2 · 𝑥) + 1)
∈ ℕ0) |
| 35 | | facp1 14317 |
. . . . . . . 8
⊢ (((2
· 𝑥) + 1) ∈
ℕ0 → (!‘(((2 · 𝑥) + 1) + 1)) = ((!‘((2 · 𝑥) + 1)) · (((2 ·
𝑥) + 1) +
1))) |
| 36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0
→ (!‘(((2 · 𝑥) + 1) + 1)) = ((!‘((2 · 𝑥) + 1)) · (((2 ·
𝑥) + 1) +
1))) |
| 37 | 32, 36 | eqtr3d 2779 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 2)) = ((!‘((2 · 𝑥) + 1)) · (((2 ·
𝑥) + 1) +
1))) |
| 38 | 31 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
→ ((!‘((2 · 𝑥) + 1)) · (((2 · 𝑥) + 1) + 1)) = ((!‘((2
· 𝑥) + 1)) ·
((2 · 𝑥) +
2))) |
| 39 | 37, 38 | eqtrd 2777 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 2)) = ((!‘((2 · 𝑥) + 1)) · ((2 ·
𝑥) + 2))) |
| 40 | 39 | oveq1d 7446 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ ((!‘((2 · 𝑥) + 2)) · ((2 · 𝑥) + 3)) = (((!‘((2
· 𝑥) + 1)) ·
((2 · 𝑥) + 2))
· ((2 · 𝑥) +
3))) |
| 41 | 40 | eqeq2d 2748 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ ((!‘((2 · 𝑥) + 3)) = ((!‘((2 · 𝑥) + 2)) · ((2 ·
𝑥) + 3)) ↔
(!‘((2 · 𝑥) +
3)) = (((!‘((2 · 𝑥) + 1)) · ((2 · 𝑥) + 2)) · ((2 ·
𝑥) + 3)))) |
| 42 | 24, 41 | mpbid 232 |
. 2
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 3)) = (((!‘((2 · 𝑥) + 1)) · ((2 ·
𝑥) + 2)) · ((2
· 𝑥) +
3))) |
| 43 | | faccl 14322 |
. . . . 5
⊢ (((2
· 𝑥) + 1) ∈
ℕ0 → (!‘((2 · 𝑥) + 1)) ∈ ℕ) |
| 44 | 34, 43 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 1)) ∈ ℕ) |
| 45 | | nncn 12274 |
. . . 4
⊢
((!‘((2 · 𝑥) + 1)) ∈ ℕ → (!‘((2
· 𝑥) + 1)) ∈
ℂ) |
| 46 | 44, 45 | syl 17 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 1)) ∈ ℂ) |
| 47 | | addcl 11237 |
. . . 4
⊢ (((2
· 𝑥) ∈ ℂ
∧ 2 ∈ ℂ) → ((2 · 𝑥) + 2) ∈ ℂ) |
| 48 | 4, 1, 47 | sylancl 586 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ ((2 · 𝑥) + 2)
∈ ℂ) |
| 49 | | 3cn 12347 |
. . . 4
⊢ 3 ∈
ℂ |
| 50 | | addcl 11237 |
. . . 4
⊢ (((2
· 𝑥) ∈ ℂ
∧ 3 ∈ ℂ) → ((2 · 𝑥) + 3) ∈ ℂ) |
| 51 | 4, 49, 50 | sylancl 586 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ ((2 · 𝑥) + 3)
∈ ℂ) |
| 52 | | mulass 11243 |
. . 3
⊢
(((!‘((2 · 𝑥) + 1)) ∈ ℂ ∧ ((2 ·
𝑥) + 2) ∈ ℂ
∧ ((2 · 𝑥) + 3)
∈ ℂ) → (((!‘((2 · 𝑥) + 1)) · ((2 · 𝑥) + 2)) · ((2 ·
𝑥) + 3)) = ((!‘((2
· 𝑥) + 1)) ·
(((2 · 𝑥) + 2)
· ((2 · 𝑥) +
3)))) |
| 53 | 46, 48, 51, 52 | syl3anc 1373 |
. 2
⊢ (𝑥 ∈ ℕ0
→ (((!‘((2 · 𝑥) + 1)) · ((2 · 𝑥) + 2)) · ((2 ·
𝑥) + 3)) = ((!‘((2
· 𝑥) + 1)) ·
(((2 · 𝑥) + 2)
· ((2 · 𝑥) +
3)))) |
| 54 | 42, 53 | eqtrd 2777 |
1
⊢ (𝑥 ∈ ℕ0
→ (!‘((2 · 𝑥) + 3)) = ((!‘((2 · 𝑥) + 1)) · (((2 ·
𝑥) + 2) · ((2
· 𝑥) +
3)))) |