Step | Hyp | Ref
| Expression |
1 | | mullid 7954 |
. . 3
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
2 | 1 | adantl 277 |
. 2
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ โ) โ (1 ยท ๐) = ๐) |
3 | | 1cnd 7972 |
. 2
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ 1 โ
โ) |
4 | | prodrb.3 |
. . 3
โข (๐ โ ๐ โ (โคโฅโ๐)) |
5 | 4 | adantr 276 |
. 2
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ ๐ โ (โคโฅโ๐)) |
6 | | eluzelz 9536 |
. . . . 5
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
7 | 5, 6 | syl 14 |
. . . 4
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ ๐ โ โค) |
8 | | prodrbdc.dc |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ DECID
๐ โ ๐ด) |
9 | | exmiddc 836 |
. . . . . . . . 9
โข
(DECID ๐ โ ๐ด โ (๐ โ ๐ด โจ ยฌ ๐ โ ๐ด)) |
10 | 8, 9 | syl 14 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ โ ๐ด โจ ยฌ ๐ โ ๐ด)) |
11 | | iftrue 3539 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ if(๐ โ ๐ด, ๐ต, 1) = ๐ต) |
12 | 11 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ต, 1) = ๐ต) |
13 | | prodmo.2 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
14 | 12, 13 | eqeltrd 2254 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ต, 1) โ โ) |
15 | 14 | ex 115 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐ด โ if(๐ โ ๐ด, ๐ต, 1) โ โ)) |
16 | | iffalse 3542 |
. . . . . . . . . . . 12
โข (ยฌ
๐ โ ๐ด โ if(๐ โ ๐ด, ๐ต, 1) = 1) |
17 | | ax-1cn 7903 |
. . . . . . . . . . . 12
โข 1 โ
โ |
18 | 16, 17 | eqeltrdi 2268 |
. . . . . . . . . . 11
โข (ยฌ
๐ โ ๐ด โ if(๐ โ ๐ด, ๐ต, 1) โ โ) |
19 | 18 | a1i 9 |
. . . . . . . . . 10
โข (๐ โ (ยฌ ๐ โ ๐ด โ if(๐ โ ๐ด, ๐ต, 1) โ โ)) |
20 | 15, 19 | jaod 717 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ๐ด โจ ยฌ ๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ต, 1) โ โ)) |
21 | 20 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((๐ โ ๐ด โจ ยฌ ๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ต, 1) โ โ)) |
22 | 10, 21 | mpd 13 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ if(๐ โ ๐ด, ๐ต, 1) โ โ) |
23 | 22 | ralrimiva 2550 |
. . . . . 6
โข (๐ โ โ๐ โ (โคโฅโ๐)if(๐ โ ๐ด, ๐ต, 1) โ โ) |
24 | | nfcv 2319 |
. . . . . . . . . 10
โข
โฒ๐๐ |
25 | 24 | nfel1 2330 |
. . . . . . . . 9
โข
โฒ๐ ๐ โ ๐ด |
26 | | nfcsb1v 3090 |
. . . . . . . . 9
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
27 | | nfcv 2319 |
. . . . . . . . 9
โข
โฒ๐1 |
28 | 25, 26, 27 | nfif 3562 |
. . . . . . . 8
โข
โฒ๐if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) |
29 | 28 | nfel1 2330 |
. . . . . . 7
โข
โฒ๐if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ |
30 | | eleq1 2240 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐ด โ ๐ โ ๐ด)) |
31 | | csbeq1a 3066 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
32 | 30, 31 | ifbieq1d 3556 |
. . . . . . . 8
โข (๐ = ๐ โ if(๐ โ ๐ด, ๐ต, 1) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
33 | 32 | eleq1d 2246 |
. . . . . . 7
โข (๐ = ๐ โ (if(๐ โ ๐ด, ๐ต, 1) โ โ โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ)) |
34 | 29, 33 | rspc 2835 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ (โ๐ โ (โคโฅโ๐)if(๐ โ ๐ด, ๐ต, 1) โ โ โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ)) |
35 | 4, 23, 34 | sylc 62 |
. . . . 5
โข (๐ โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) |
36 | 35 | adantr 276 |
. . . 4
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) |
37 | | prodmo.1 |
. . . . 5
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) |
38 | 24, 28, 32, 37 | fvmptf 5608 |
. . . 4
โข ((๐ โ โค โง if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) โ (๐นโ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
39 | 7, 36, 38 | syl2anc 411 |
. . 3
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ (๐นโ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
40 | 39, 36 | eqeltrd 2254 |
. 2
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ (๐นโ๐) โ โ) |
41 | | elfzelz 10024 |
. . . 4
โข (๐ โ (๐...(๐ โ 1)) โ ๐ โ โค) |
42 | | elfzuz 10020 |
. . . . . 6
โข (๐ โ (๐...(๐ โ 1)) โ ๐ โ (โคโฅโ๐)) |
43 | 42 | adantl 277 |
. . . . 5
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ ๐ โ (โคโฅโ๐)) |
44 | 23 | ad2antrr 488 |
. . . . 5
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ โ๐ โ
(โคโฅโ๐)if(๐ โ ๐ด, ๐ต, 1) โ โ) |
45 | | nfv 1528 |
. . . . . . . 8
โข
โฒ๐ ๐ โ ๐ด |
46 | | nfcsb1v 3090 |
. . . . . . . 8
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
47 | 45, 46, 27 | nfif 3562 |
. . . . . . 7
โข
โฒ๐if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) |
48 | 47 | nfel1 2330 |
. . . . . 6
โข
โฒ๐if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ |
49 | | eleq1w 2238 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ โ ๐ด โ ๐ โ ๐ด)) |
50 | | csbeq1a 3066 |
. . . . . . . 8
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
51 | 49, 50 | ifbieq1d 3556 |
. . . . . . 7
โข (๐ = ๐ โ if(๐ โ ๐ด, ๐ต, 1) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
52 | 51 | eleq1d 2246 |
. . . . . 6
โข (๐ = ๐ โ (if(๐ โ ๐ด, ๐ต, 1) โ โ โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ)) |
53 | 48, 52 | rspc 2835 |
. . . . 5
โข (๐ โ
(โคโฅโ๐) โ (โ๐ โ (โคโฅโ๐)if(๐ โ ๐ด, ๐ต, 1) โ โ โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ)) |
54 | 43, 44, 53 | sylc 62 |
. . . 4
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) |
55 | | nfcv 2319 |
. . . . 5
โข
โฒ๐๐ |
56 | 55, 47, 51, 37 | fvmptf 5608 |
. . . 4
โข ((๐ โ โค โง if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) โ (๐นโ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
57 | 41, 54, 56 | syl2an2 594 |
. . 3
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
58 | | uznfz 10102 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐) โ ยฌ ๐ โ (๐...(๐ โ 1))) |
59 | 58 | con2i 627 |
. . . . . 6
โข (๐ โ (๐...(๐ โ 1)) โ ยฌ ๐ โ (โคโฅโ๐)) |
60 | 59 | adantl 277 |
. . . . 5
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ ยฌ ๐ โ
(โคโฅโ๐)) |
61 | | ssel 3149 |
. . . . . 6
โข (๐ด โ
(โคโฅโ๐) โ (๐ โ ๐ด โ ๐ โ (โคโฅโ๐))) |
62 | 61 | ad2antlr 489 |
. . . . 5
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ (๐ โ ๐ด โ ๐ โ (โคโฅโ๐))) |
63 | 60, 62 | mtod 663 |
. . . 4
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ ยฌ ๐ โ ๐ด) |
64 | 63 | iffalsed 3544 |
. . 3
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) = 1) |
65 | 57, 64 | eqtrd 2210 |
. 2
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ๐) = 1) |
66 | | eluzelz 9536 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
67 | | simpr 110 |
. . . . 5
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ (โคโฅโ๐)) |
68 | 23 | ad2antrr 488 |
. . . . 5
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (โคโฅโ๐)) โ โ๐ โ
(โคโฅโ๐)if(๐ โ ๐ด, ๐ต, 1) โ โ) |
69 | 67, 68, 53 | sylc 62 |
. . . 4
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (โคโฅโ๐)) โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) |
70 | 66, 69, 56 | syl2an2 594 |
. . 3
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
71 | 70, 69 | eqeltrd 2254 |
. 2
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) โ โ) |
72 | | mulcl 7937 |
. . 3
โข ((๐ โ โ โง ๐ง โ โ) โ (๐ ยท ๐ง) โ โ) |
73 | 72 | adantl 277 |
. 2
โข (((๐ โง ๐ด โ (โคโฅโ๐)) โง (๐ โ โ โง ๐ง โ โ)) โ (๐ ยท ๐ง) โ โ) |
74 | 2, 3, 5, 40, 65, 71, 73 | seq3id 10507 |
1
โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ (seq๐( ยท , ๐น) โพ
(โคโฅโ๐)) = seq๐( ยท , ๐น)) |