Step | Hyp | Ref
| Expression |
1 | | fveq2 5515 |
. . 3
โข (๐ค = 0 โ (!โ๐ค) =
(!โ0)) |
2 | | oveq2 5882 |
. . . 4
โข (๐ค = 0 โ (1...๐ค) = (1...0)) |
3 | 2 | prodeq1d 11571 |
. . 3
โข (๐ค = 0 โ โ๐ โ (1...๐ค)๐ = โ๐ โ (1...0)๐) |
4 | 1, 3 | eqeq12d 2192 |
. 2
โข (๐ค = 0 โ ((!โ๐ค) = โ๐ โ (1...๐ค)๐ โ (!โ0) = โ๐ โ (1...0)๐)) |
5 | | fveq2 5515 |
. . 3
โข (๐ค = ๐ฅ โ (!โ๐ค) = (!โ๐ฅ)) |
6 | | oveq2 5882 |
. . . 4
โข (๐ค = ๐ฅ โ (1...๐ค) = (1...๐ฅ)) |
7 | 6 | prodeq1d 11571 |
. . 3
โข (๐ค = ๐ฅ โ โ๐ โ (1...๐ค)๐ = โ๐ โ (1...๐ฅ)๐) |
8 | 5, 7 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ฅ โ ((!โ๐ค) = โ๐ โ (1...๐ค)๐ โ (!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐)) |
9 | | fveq2 5515 |
. . 3
โข (๐ค = (๐ฅ + 1) โ (!โ๐ค) = (!โ(๐ฅ + 1))) |
10 | | oveq2 5882 |
. . . 4
โข (๐ค = (๐ฅ + 1) โ (1...๐ค) = (1...(๐ฅ + 1))) |
11 | 10 | prodeq1d 11571 |
. . 3
โข (๐ค = (๐ฅ + 1) โ โ๐ โ (1...๐ค)๐ = โ๐ โ (1...(๐ฅ + 1))๐) |
12 | 9, 11 | eqeq12d 2192 |
. 2
โข (๐ค = (๐ฅ + 1) โ ((!โ๐ค) = โ๐ โ (1...๐ค)๐ โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐)) |
13 | | fveq2 5515 |
. . 3
โข (๐ค = ๐ด โ (!โ๐ค) = (!โ๐ด)) |
14 | | oveq2 5882 |
. . . 4
โข (๐ค = ๐ด โ (1...๐ค) = (1...๐ด)) |
15 | 14 | prodeq1d 11571 |
. . 3
โข (๐ค = ๐ด โ โ๐ โ (1...๐ค)๐ = โ๐ โ (1...๐ด)๐) |
16 | 13, 15 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ด โ ((!โ๐ค) = โ๐ โ (1...๐ค)๐ โ (!โ๐ด) = โ๐ โ (1...๐ด)๐)) |
17 | | prod0 11592 |
. . 3
โข
โ๐ โ
โ
๐ =
1 |
18 | | fz10 10045 |
. . . 4
โข (1...0) =
โ
|
19 | 18 | prodeq1i 11568 |
. . 3
โข
โ๐ โ
(1...0)๐ = โ๐ โ โ
๐ |
20 | | fac0 10707 |
. . 3
โข
(!โ0) = 1 |
21 | 17, 19, 20 | 3eqtr4ri 2209 |
. 2
โข
(!โ0) = โ๐ โ (1...0)๐ |
22 | | elnn0 9177 |
. . 3
โข (๐ฅ โ โ0
โ (๐ฅ โ โ
โจ ๐ฅ =
0)) |
23 | | simpr 110 |
. . . . . . 7
โข ((๐ฅ โ โ โง
(!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐) โ (!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐) |
24 | 23 | oveq1d 5889 |
. . . . . 6
โข ((๐ฅ โ โ โง
(!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐) โ ((!โ๐ฅ) ยท (๐ฅ + 1)) = (โ๐ โ (1...๐ฅ)๐ ยท (๐ฅ + 1))) |
25 | | nnnn0 9182 |
. . . . . . . . 9
โข (๐ฅ โ โ โ ๐ฅ โ
โ0) |
26 | | facp1 10709 |
. . . . . . . . 9
โข (๐ฅ โ โ0
โ (!โ(๐ฅ + 1)) =
((!โ๐ฅ) ยท
(๐ฅ + 1))) |
27 | 25, 26 | syl 14 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(!โ(๐ฅ + 1)) =
((!โ๐ฅ) ยท
(๐ฅ + 1))) |
28 | | elnnuz 9563 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ ๐ฅ โ
(โคโฅโ1)) |
29 | 28 | biimpi 120 |
. . . . . . . . 9
โข (๐ฅ โ โ โ ๐ฅ โ
(โคโฅโ1)) |
30 | | elfzelz 10024 |
. . . . . . . . . . 11
โข (๐ โ (1...(๐ฅ + 1)) โ ๐ โ โค) |
31 | 30 | zcnd 9375 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ฅ + 1)) โ ๐ โ โ) |
32 | 31 | adantl 277 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ โ (1...(๐ฅ + 1))) โ ๐ โ โ) |
33 | | id 19 |
. . . . . . . . 9
โข (๐ = (๐ฅ + 1) โ ๐ = (๐ฅ + 1)) |
34 | 29, 32, 33 | fprodp1 11607 |
. . . . . . . 8
โข (๐ฅ โ โ โ
โ๐ โ (1...(๐ฅ + 1))๐ = (โ๐ โ (1...๐ฅ)๐ ยท (๐ฅ + 1))) |
35 | 27, 34 | eqeq12d 2192 |
. . . . . . 7
โข (๐ฅ โ โ โ
((!โ(๐ฅ + 1)) =
โ๐ โ (1...(๐ฅ + 1))๐ โ ((!โ๐ฅ) ยท (๐ฅ + 1)) = (โ๐ โ (1...๐ฅ)๐ ยท (๐ฅ + 1)))) |
36 | 35 | adantr 276 |
. . . . . 6
โข ((๐ฅ โ โ โง
(!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐) โ ((!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐ โ ((!โ๐ฅ) ยท (๐ฅ + 1)) = (โ๐ โ (1...๐ฅ)๐ ยท (๐ฅ + 1)))) |
37 | 24, 36 | mpbird 167 |
. . . . 5
โข ((๐ฅ โ โ โง
(!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐) โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐) |
38 | 37 | ex 115 |
. . . 4
โข (๐ฅ โ โ โ
((!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐ โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐)) |
39 | | 1zzd 9279 |
. . . . . . 7
โข (๐ฅ = 0 โ 1 โ
โค) |
40 | | 1cnd 7972 |
. . . . . . 7
โข (๐ฅ = 0 โ 1 โ
โ) |
41 | | id 19 |
. . . . . . . 8
โข (๐ = 1 โ ๐ = 1) |
42 | 41 | fprod1 11601 |
. . . . . . 7
โข ((1
โ โค โง 1 โ โ) โ โ๐ โ (1...1)๐ = 1) |
43 | 39, 40, 42 | syl2anc 411 |
. . . . . 6
โข (๐ฅ = 0 โ โ๐ โ (1...1)๐ = 1) |
44 | | oveq1 5881 |
. . . . . . . . 9
โข (๐ฅ = 0 โ (๐ฅ + 1) = (0 + 1)) |
45 | | 0p1e1 9032 |
. . . . . . . . 9
โข (0 + 1) =
1 |
46 | 44, 45 | eqtrdi 2226 |
. . . . . . . 8
โข (๐ฅ = 0 โ (๐ฅ + 1) = 1) |
47 | 46 | oveq2d 5890 |
. . . . . . 7
โข (๐ฅ = 0 โ (1...(๐ฅ + 1)) =
(1...1)) |
48 | 47 | prodeq1d 11571 |
. . . . . 6
โข (๐ฅ = 0 โ โ๐ โ (1...(๐ฅ + 1))๐ = โ๐ โ (1...1)๐) |
49 | | fv0p1e1 9033 |
. . . . . . 7
โข (๐ฅ = 0 โ (!โ(๐ฅ + 1)) =
(!โ1)) |
50 | | fac1 10708 |
. . . . . . 7
โข
(!โ1) = 1 |
51 | 49, 50 | eqtrdi 2226 |
. . . . . 6
โข (๐ฅ = 0 โ (!โ(๐ฅ + 1)) = 1) |
52 | 43, 48, 51 | 3eqtr4rd 2221 |
. . . . 5
โข (๐ฅ = 0 โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐) |
53 | 52 | a1d 22 |
. . . 4
โข (๐ฅ = 0 โ ((!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐ โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐)) |
54 | 38, 53 | jaoi 716 |
. . 3
โข ((๐ฅ โ โ โจ ๐ฅ = 0) โ ((!โ๐ฅ) = โ๐ โ (1...๐ฅ)๐ โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐)) |
55 | 22, 54 | sylbi 121 |
. 2
โข (๐ฅ โ โ0
โ ((!โ๐ฅ) =
โ๐ โ (1...๐ฅ)๐ โ (!โ(๐ฅ + 1)) = โ๐ โ (1...(๐ฅ + 1))๐)) |
56 | 4, 8, 12, 16, 21, 55 | nn0ind 9366 |
1
โข (๐ด โ โ0
โ (!โ๐ด) =
โ๐ โ (1...๐ด)๐) |