Step | Hyp | Ref
| Expression |
1 | | fveq2 5468 |
. . 3
⊢ (𝑤 = 0 → (!‘𝑤) =
(!‘0)) |
2 | | oveq2 5832 |
. . . 4
⊢ (𝑤 = 0 → (1...𝑤) = (1...0)) |
3 | 2 | prodeq1d 11461 |
. . 3
⊢ (𝑤 = 0 → ∏𝑘 ∈ (1...𝑤)𝑘 = ∏𝑘 ∈ (1...0)𝑘) |
4 | 1, 3 | eqeq12d 2172 |
. 2
⊢ (𝑤 = 0 → ((!‘𝑤) = ∏𝑘 ∈ (1...𝑤)𝑘 ↔ (!‘0) = ∏𝑘 ∈ (1...0)𝑘)) |
5 | | fveq2 5468 |
. . 3
⊢ (𝑤 = 𝑥 → (!‘𝑤) = (!‘𝑥)) |
6 | | oveq2 5832 |
. . . 4
⊢ (𝑤 = 𝑥 → (1...𝑤) = (1...𝑥)) |
7 | 6 | prodeq1d 11461 |
. . 3
⊢ (𝑤 = 𝑥 → ∏𝑘 ∈ (1...𝑤)𝑘 = ∏𝑘 ∈ (1...𝑥)𝑘) |
8 | 5, 7 | eqeq12d 2172 |
. 2
⊢ (𝑤 = 𝑥 → ((!‘𝑤) = ∏𝑘 ∈ (1...𝑤)𝑘 ↔ (!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘)) |
9 | | fveq2 5468 |
. . 3
⊢ (𝑤 = (𝑥 + 1) → (!‘𝑤) = (!‘(𝑥 + 1))) |
10 | | oveq2 5832 |
. . . 4
⊢ (𝑤 = (𝑥 + 1) → (1...𝑤) = (1...(𝑥 + 1))) |
11 | 10 | prodeq1d 11461 |
. . 3
⊢ (𝑤 = (𝑥 + 1) → ∏𝑘 ∈ (1...𝑤)𝑘 = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘) |
12 | 9, 11 | eqeq12d 2172 |
. 2
⊢ (𝑤 = (𝑥 + 1) → ((!‘𝑤) = ∏𝑘 ∈ (1...𝑤)𝑘 ↔ (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘)) |
13 | | fveq2 5468 |
. . 3
⊢ (𝑤 = 𝐴 → (!‘𝑤) = (!‘𝐴)) |
14 | | oveq2 5832 |
. . . 4
⊢ (𝑤 = 𝐴 → (1...𝑤) = (1...𝐴)) |
15 | 14 | prodeq1d 11461 |
. . 3
⊢ (𝑤 = 𝐴 → ∏𝑘 ∈ (1...𝑤)𝑘 = ∏𝑘 ∈ (1...𝐴)𝑘) |
16 | 13, 15 | eqeq12d 2172 |
. 2
⊢ (𝑤 = 𝐴 → ((!‘𝑤) = ∏𝑘 ∈ (1...𝑤)𝑘 ↔ (!‘𝐴) = ∏𝑘 ∈ (1...𝐴)𝑘)) |
17 | | prod0 11482 |
. . 3
⊢
∏𝑘 ∈
∅ 𝑘 =
1 |
18 | | fz10 9948 |
. . . 4
⊢ (1...0) =
∅ |
19 | 18 | prodeq1i 11458 |
. . 3
⊢
∏𝑘 ∈
(1...0)𝑘 = ∏𝑘 ∈ ∅ 𝑘 |
20 | | fac0 10602 |
. . 3
⊢
(!‘0) = 1 |
21 | 17, 19, 20 | 3eqtr4ri 2189 |
. 2
⊢
(!‘0) = ∏𝑘 ∈ (1...0)𝑘 |
22 | | elnn0 9092 |
. . 3
⊢ (𝑥 ∈ ℕ0
↔ (𝑥 ∈ ℕ
∨ 𝑥 =
0)) |
23 | | simpr 109 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ ∧
(!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘) → (!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘) |
24 | 23 | oveq1d 5839 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧
(!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘) → ((!‘𝑥) · (𝑥 + 1)) = (∏𝑘 ∈ (1...𝑥)𝑘 · (𝑥 + 1))) |
25 | | nnnn0 9097 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
26 | | facp1 10604 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ (!‘(𝑥 + 1)) =
((!‘𝑥) ·
(𝑥 + 1))) |
27 | 25, 26 | syl 14 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ →
(!‘(𝑥 + 1)) =
((!‘𝑥) ·
(𝑥 + 1))) |
28 | | elnnuz 9475 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈
(ℤ≥‘1)) |
29 | 28 | biimpi 119 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
(ℤ≥‘1)) |
30 | | elfzelz 9928 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑥 + 1)) → 𝑘 ∈ ℤ) |
31 | 30 | zcnd 9287 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝑥 + 1)) → 𝑘 ∈ ℂ) |
32 | 31 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑥 + 1))) → 𝑘 ∈ ℂ) |
33 | | id 19 |
. . . . . . . . 9
⊢ (𝑘 = (𝑥 + 1) → 𝑘 = (𝑥 + 1)) |
34 | 29, 32, 33 | fprodp1 11497 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ →
∏𝑘 ∈ (1...(𝑥 + 1))𝑘 = (∏𝑘 ∈ (1...𝑥)𝑘 · (𝑥 + 1))) |
35 | 27, 34 | eqeq12d 2172 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ →
((!‘(𝑥 + 1)) =
∏𝑘 ∈ (1...(𝑥 + 1))𝑘 ↔ ((!‘𝑥) · (𝑥 + 1)) = (∏𝑘 ∈ (1...𝑥)𝑘 · (𝑥 + 1)))) |
36 | 35 | adantr 274 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧
(!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘) → ((!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘 ↔ ((!‘𝑥) · (𝑥 + 1)) = (∏𝑘 ∈ (1...𝑥)𝑘 · (𝑥 + 1)))) |
37 | 24, 36 | mpbird 166 |
. . . . 5
⊢ ((𝑥 ∈ ℕ ∧
(!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘) → (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘) |
38 | 37 | ex 114 |
. . . 4
⊢ (𝑥 ∈ ℕ →
((!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘 → (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘)) |
39 | | 1zzd 9194 |
. . . . . . 7
⊢ (𝑥 = 0 → 1 ∈
ℤ) |
40 | | 1cnd 7894 |
. . . . . . 7
⊢ (𝑥 = 0 → 1 ∈
ℂ) |
41 | | id 19 |
. . . . . . . 8
⊢ (𝑘 = 1 → 𝑘 = 1) |
42 | 41 | fprod1 11491 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 1 ∈ ℂ) → ∏𝑘 ∈ (1...1)𝑘 = 1) |
43 | 39, 40, 42 | syl2anc 409 |
. . . . . 6
⊢ (𝑥 = 0 → ∏𝑘 ∈ (1...1)𝑘 = 1) |
44 | | oveq1 5831 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1)) |
45 | | 0p1e1 8947 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
46 | 44, 45 | eqtrdi 2206 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑥 + 1) = 1) |
47 | 46 | oveq2d 5840 |
. . . . . . 7
⊢ (𝑥 = 0 → (1...(𝑥 + 1)) =
(1...1)) |
48 | 47 | prodeq1d 11461 |
. . . . . 6
⊢ (𝑥 = 0 → ∏𝑘 ∈ (1...(𝑥 + 1))𝑘 = ∏𝑘 ∈ (1...1)𝑘) |
49 | | fv0p1e1 8948 |
. . . . . . 7
⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) =
(!‘1)) |
50 | | fac1 10603 |
. . . . . . 7
⊢
(!‘1) = 1 |
51 | 49, 50 | eqtrdi 2206 |
. . . . . 6
⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = 1) |
52 | 43, 48, 51 | 3eqtr4rd 2201 |
. . . . 5
⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘) |
53 | 52 | a1d 22 |
. . . 4
⊢ (𝑥 = 0 → ((!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘 → (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘)) |
54 | 38, 53 | jaoi 706 |
. . 3
⊢ ((𝑥 ∈ ℕ ∨ 𝑥 = 0) → ((!‘𝑥) = ∏𝑘 ∈ (1...𝑥)𝑘 → (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘)) |
55 | 22, 54 | sylbi 120 |
. 2
⊢ (𝑥 ∈ ℕ0
→ ((!‘𝑥) =
∏𝑘 ∈ (1...𝑥)𝑘 → (!‘(𝑥 + 1)) = ∏𝑘 ∈ (1...(𝑥 + 1))𝑘)) |
56 | 4, 8, 12, 16, 21, 55 | nn0ind 9278 |
1
⊢ (𝐴 ∈ ℕ0
→ (!‘𝐴) =
∏𝑘 ∈ (1...𝐴)𝑘) |