Step | Hyp | Ref
| Expression |
1 | | eluzel2 9532 |
. . . . . . 7
โข (๐พ โ
(โคโฅโ๐) โ ๐ โ โค) |
2 | 1 | adantl 277 |
. . . . . 6
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ๐ โ โค) |
3 | 2 | zred 9374 |
. . . . 5
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ๐ โ โ) |
4 | 3 | ltp1d 8886 |
. . . 4
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ๐ < (๐ + 1)) |
5 | | fzdisj 10051 |
. . . 4
โข (๐ < (๐ + 1) โ ((๐...๐) โฉ ((๐ + 1)...๐พ)) = โ
) |
6 | 4, 5 | syl 14 |
. . 3
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ((๐...๐) โฉ ((๐ + 1)...๐พ)) = โ
) |
7 | | fprodeq0.2 |
. . . . . . . 8
โข (๐ โ ๐ โ ๐) |
8 | | eluzel2 9532 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
9 | | fprodeq0.1 |
. . . . . . . . 9
โข ๐ =
(โคโฅโ๐) |
10 | 8, 9 | eleq2s 2272 |
. . . . . . . 8
โข (๐ โ ๐ โ ๐ โ โค) |
11 | 7, 10 | syl 14 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
12 | 11 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ๐ โ โค) |
13 | | eluzelz 9536 |
. . . . . . 7
โข (๐พ โ
(โคโฅโ๐) โ ๐พ โ โค) |
14 | 13 | adantl 277 |
. . . . . 6
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ๐พ โ โค) |
15 | 12, 14, 2 | 3jca 1177 |
. . . . 5
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (๐ โ โค โง ๐พ โ โค โง ๐ โ โค)) |
16 | | eluzle 9539 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐) โ ๐ โค ๐) |
17 | 16, 9 | eleq2s 2272 |
. . . . . . 7
โข (๐ โ ๐ โ ๐ โค ๐) |
18 | 7, 17 | syl 14 |
. . . . . 6
โข (๐ โ ๐ โค ๐) |
19 | | eluzle 9539 |
. . . . . 6
โข (๐พ โ
(โคโฅโ๐) โ ๐ โค ๐พ) |
20 | 18, 19 | anim12i 338 |
. . . . 5
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (๐ โค ๐ โง ๐ โค ๐พ)) |
21 | | elfz2 10014 |
. . . . 5
โข (๐ โ (๐...๐พ) โ ((๐ โ โค โง ๐พ โ โค โง ๐ โ โค) โง (๐ โค ๐ โง ๐ โค ๐พ))) |
22 | 15, 20, 21 | sylanbrc 417 |
. . . 4
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ๐ โ (๐...๐พ)) |
23 | | fzsplit 10050 |
. . . 4
โข (๐ โ (๐...๐พ) โ (๐...๐พ) = ((๐...๐) โช ((๐ + 1)...๐พ))) |
24 | 22, 23 | syl 14 |
. . 3
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (๐...๐พ) = ((๐...๐) โช ((๐ + 1)...๐พ))) |
25 | 12, 14 | fzfigd 10430 |
. . 3
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (๐...๐พ) โ Fin) |
26 | | elfzelz 10024 |
. . . . . 6
โข (๐ โ (๐...๐พ) โ ๐ โ โค) |
27 | 26 | adantl 277 |
. . . . 5
โข (((๐ โง ๐พ โ (โคโฅโ๐)) โง ๐ โ (๐...๐พ)) โ ๐ โ โค) |
28 | 12 | adantr 276 |
. . . . 5
โข (((๐ โง ๐พ โ (โคโฅโ๐)) โง ๐ โ (๐...๐พ)) โ ๐ โ โค) |
29 | 2 | adantr 276 |
. . . . 5
โข (((๐ โง ๐พ โ (โคโฅโ๐)) โง ๐ โ (๐...๐พ)) โ ๐ โ โค) |
30 | | fzdcel 10039 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ โค) โ
DECID ๐
โ (๐...๐)) |
31 | 27, 28, 29, 30 | syl3anc 1238 |
. . . 4
โข (((๐ โง ๐พ โ (โคโฅโ๐)) โง ๐ โ (๐...๐พ)) โ DECID ๐ โ (๐...๐)) |
32 | 31 | ralrimiva 2550 |
. . 3
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐พ)DECID ๐ โ (๐...๐)) |
33 | | elfzuz 10020 |
. . . . . 6
โข (๐ โ (๐...๐พ) โ ๐ โ (โคโฅโ๐)) |
34 | 33, 9 | eleqtrrdi 2271 |
. . . . 5
โข (๐ โ (๐...๐พ) โ ๐ โ ๐) |
35 | | fprodeq0.3 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) |
36 | 34, 35 | sylan2 286 |
. . . 4
โข ((๐ โง ๐ โ (๐...๐พ)) โ ๐ด โ โ) |
37 | 36 | adantlr 477 |
. . 3
โข (((๐ โง ๐พ โ (โคโฅโ๐)) โง ๐ โ (๐...๐พ)) โ ๐ด โ โ) |
38 | 6, 24, 25, 32, 37 | fprodsplitdc 11603 |
. 2
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐พ)๐ด = (โ๐ โ (๐...๐)๐ด ยท โ๐ โ ((๐ + 1)...๐พ)๐ด)) |
39 | 7, 9 | eleqtrdi 2270 |
. . . . . 6
โข (๐ โ ๐ โ (โคโฅโ๐)) |
40 | | elfzuz 10020 |
. . . . . . . 8
โข (๐ โ (๐...๐) โ ๐ โ (โคโฅโ๐)) |
41 | 40, 9 | eleqtrrdi 2271 |
. . . . . . 7
โข (๐ โ (๐...๐) โ ๐ โ ๐) |
42 | 41, 35 | sylan2 286 |
. . . . . 6
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
43 | 39, 42 | fprodm1s 11608 |
. . . . 5
โข (๐ โ โ๐ โ (๐...๐)๐ด = (โ๐ โ (๐...(๐ โ 1))๐ด ยท โฆ๐ / ๐โฆ๐ด)) |
44 | | fprodeq0.4 |
. . . . . . 7
โข ((๐ โง ๐ = ๐) โ ๐ด = 0) |
45 | 7, 44 | csbied 3103 |
. . . . . 6
โข (๐ โ โฆ๐ / ๐โฆ๐ด = 0) |
46 | 45 | oveq2d 5890 |
. . . . 5
โข (๐ โ (โ๐ โ (๐...(๐ โ 1))๐ด ยท โฆ๐ / ๐โฆ๐ด) = (โ๐ โ (๐...(๐ โ 1))๐ด ยท 0)) |
47 | | eluzelz 9536 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
48 | 39, 47 | syl 14 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
49 | | peano2zm 9290 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
50 | 48, 49 | syl 14 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) โ โค) |
51 | 11, 50 | fzfigd 10430 |
. . . . . . 7
โข (๐ โ (๐...(๐ โ 1)) โ Fin) |
52 | | elfzuz 10020 |
. . . . . . . . 9
โข (๐ โ (๐...(๐ โ 1)) โ ๐ โ (โคโฅโ๐)) |
53 | 52, 9 | eleqtrrdi 2271 |
. . . . . . . 8
โข (๐ โ (๐...(๐ โ 1)) โ ๐ โ ๐) |
54 | 53, 35 | sylan2 286 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐...(๐ โ 1))) โ ๐ด โ โ) |
55 | 51, 54 | fprodcl 11614 |
. . . . . 6
โข (๐ โ โ๐ โ (๐...(๐ โ 1))๐ด โ โ) |
56 | 55 | mul01d 8349 |
. . . . 5
โข (๐ โ (โ๐ โ (๐...(๐ โ 1))๐ด ยท 0) = 0) |
57 | 43, 46, 56 | 3eqtrd 2214 |
. . . 4
โข (๐ โ โ๐ โ (๐...๐)๐ด = 0) |
58 | 57 | adantr 276 |
. . 3
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐)๐ด = 0) |
59 | 58 | oveq1d 5889 |
. 2
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (โ๐ โ (๐...๐)๐ด ยท โ๐ โ ((๐ + 1)...๐พ)๐ด) = (0 ยท โ๐ โ ((๐ + 1)...๐พ)๐ด)) |
60 | 2 | peano2zd 9377 |
. . . . 5
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (๐ + 1) โ โค) |
61 | 60, 14 | fzfigd 10430 |
. . . 4
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ ((๐ + 1)...๐พ) โ Fin) |
62 | 9 | peano2uzs 9583 |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐ + 1) โ ๐) |
63 | 7, 62 | syl 14 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ ๐) |
64 | | elfzuz 10020 |
. . . . . . . 8
โข (๐ โ ((๐ + 1)...๐พ) โ ๐ โ (โคโฅโ(๐ + 1))) |
65 | 9 | uztrn2 9544 |
. . . . . . . 8
โข (((๐ + 1) โ ๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ๐ โ ๐) |
66 | 63, 64, 65 | syl2an 289 |
. . . . . . 7
โข ((๐ โง ๐ โ ((๐ + 1)...๐พ)) โ ๐ โ ๐) |
67 | 66 | adantrl 478 |
. . . . . 6
โข ((๐ โง (๐พ โ (โคโฅโ๐) โง ๐ โ ((๐ + 1)...๐พ))) โ ๐ โ ๐) |
68 | 67, 35 | syldan 282 |
. . . . 5
โข ((๐ โง (๐พ โ (โคโฅโ๐) โง ๐ โ ((๐ + 1)...๐พ))) โ ๐ด โ โ) |
69 | 68 | anassrs 400 |
. . . 4
โข (((๐ โง ๐พ โ (โคโฅโ๐)) โง ๐ โ ((๐ + 1)...๐พ)) โ ๐ด โ โ) |
70 | 61, 69 | fprodcl 11614 |
. . 3
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ ((๐ + 1)...๐พ)๐ด โ โ) |
71 | 70 | mul02d 8348 |
. 2
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ (0 ยท
โ๐ โ ((๐ + 1)...๐พ)๐ด) = 0) |
72 | 38, 59, 71 | 3eqtrd 2214 |
1
โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐พ)๐ด = 0) |