Step | Hyp | Ref
| Expression |
1 | | fprodntriv.2 |
. . . . 5
โข (๐ โ ๐ โ ๐) |
2 | | fprodntriv.1 |
. . . . 5
โข ๐ =
(โคโฅโ๐) |
3 | 1, 2 | eleqtrdi 2835 |
. . . 4
โข (๐ โ ๐ โ (โคโฅโ๐)) |
4 | | peano2uz 12913 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
5 | 3, 4 | syl 17 |
. . 3
โข (๐ โ (๐ + 1) โ
(โคโฅโ๐)) |
6 | 5, 2 | eleqtrrdi 2836 |
. 2
โข (๐ โ (๐ + 1) โ ๐) |
7 | | ax-1ne0 11205 |
. . 3
โข 1 โ
0 |
8 | | eqid 2725 |
. . . 4
โข
(โคโฅโ(๐ + 1)) =
(โคโฅโ(๐ + 1)) |
9 | | eluzelz 12860 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
10 | 9, 2 | eleq2s 2843 |
. . . . . 6
โข (๐ โ ๐ โ ๐ โ โค) |
11 | 1, 10 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โค) |
12 | 11 | peano2zd 12697 |
. . . 4
โข (๐ โ (๐ + 1) โ โค) |
13 | | seqex 13998 |
. . . . 5
โข seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ V |
14 | 13 | a1i 11 |
. . . 4
โข (๐ โ seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ V) |
15 | | 1cnd 11237 |
. . . 4
โข (๐ โ 1 โ
โ) |
16 | | simpr 483 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ๐ โ
(โคโฅโ(๐ + 1))) |
17 | | fprodntriv.3 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ (๐...๐)) |
18 | 17 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ด โ (๐...๐)) |
19 | 11 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ โค) |
20 | 19 | zred 12694 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ โ) |
21 | 19 | peano2zd 12697 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ (๐ + 1) โ โค) |
22 | 21 | zred 12694 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ (๐ + 1) โ โ) |
23 | | elfzelz 13531 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ + 1)...๐) โ ๐ โ โค) |
24 | 23 | adantl 480 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ โค) |
25 | 24 | zred 12694 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ โ) |
26 | 20 | ltp1d 12172 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ < (๐ + 1)) |
27 | | elfzle1 13534 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ + 1)...๐) โ (๐ + 1) โค ๐) |
28 | 27 | adantl 480 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ (๐ + 1) โค ๐) |
29 | 20, 22, 25, 26, 28 | ltletrd 11402 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ < ๐) |
30 | 20, 25 | ltnled 11389 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ (๐ < ๐ โ ยฌ ๐ โค ๐)) |
31 | 29, 30 | mpbid 231 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ยฌ ๐ โค ๐) |
32 | 31 | intnand 487 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ยฌ (๐ โค ๐ โง ๐ โค ๐)) |
33 | 32 | intnand 487 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ยฌ ((๐ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ โค ๐ โง ๐ โค ๐))) |
34 | | elfz2 13521 |
. . . . . . . . . 10
โข (๐ โ (๐...๐) โ ((๐ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ โค ๐ โง ๐ โค ๐))) |
35 | 33, 34 | sylnibr 328 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ยฌ ๐ โ (๐...๐)) |
36 | 18, 35 | ssneldd 3975 |
. . . . . . . 8
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ยฌ ๐ โ ๐ด) |
37 | 36 | iffalsed 4535 |
. . . . . . 7
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) = 1) |
38 | | fzssuz 13572 |
. . . . . . . . . 10
โข ((๐ + 1)...๐) โ
(โคโฅโ(๐ + 1)) |
39 | 5 | adantr 479 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (๐ + 1) โ
(โคโฅโ๐)) |
40 | | uzss 12873 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ
(โคโฅโ๐) โ
(โคโฅโ(๐ + 1)) โ
(โคโฅโ๐)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ
(โคโฅโ(๐ + 1)) โ
(โคโฅโ๐)) |
42 | 41, 2 | sseqtrrdi 4024 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ
(โคโฅโ(๐ + 1)) โ ๐) |
43 | 38, 42 | sstrid 3984 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ ((๐ + 1)...๐) โ ๐) |
44 | 43 | sselda 3972 |
. . . . . . . 8
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ ๐) |
45 | | ax-1cn 11194 |
. . . . . . . . 9
โข 1 โ
โ |
46 | 37, 45 | eqeltrdi 2833 |
. . . . . . . 8
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) |
47 | | nfcv 2892 |
. . . . . . . . 9
โข
โฒ๐๐ |
48 | | nfv 1909 |
. . . . . . . . . 10
โข
โฒ๐ ๐ โ ๐ด |
49 | | nfcsb1v 3910 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
50 | | nfcv 2892 |
. . . . . . . . . 10
โข
โฒ๐1 |
51 | 48, 49, 50 | nfif 4554 |
. . . . . . . . 9
โข
โฒ๐if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) |
52 | | eleq1w 2808 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ ๐ด โ ๐ โ ๐ด)) |
53 | | csbeq1a 3899 |
. . . . . . . . . 10
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
54 | 52, 53 | ifbieq1d 4548 |
. . . . . . . . 9
โข (๐ = ๐ โ if(๐ โ ๐ด, ๐ต, 1) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
55 | | eqid 2725 |
. . . . . . . . 9
โข (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1)) = (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1)) |
56 | 47, 51, 54, 55 | fvmptf 7020 |
. . . . . . . 8
โข ((๐ โ ๐ โง if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) โ โ) โ ((๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
57 | 44, 46, 56 | syl2anc 582 |
. . . . . . 7
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ((๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
58 | | elfzuz 13527 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1)...๐) โ ๐ โ (โคโฅโ(๐ + 1))) |
59 | 58 | adantl 480 |
. . . . . . . 8
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ (โคโฅโ(๐ + 1))) |
60 | | 1ex 11238 |
. . . . . . . . 9
โข 1 โ
V |
61 | 60 | fvconst2 7211 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ(๐ + 1)) โ
(((โคโฅโ(๐ + 1)) ร {1})โ๐) = 1) |
62 | 59, 61 | syl 17 |
. . . . . . 7
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ
(((โคโฅโ(๐ + 1)) ร {1})โ๐) = 1) |
63 | 37, 57, 62 | 3eqtr4d 2775 |
. . . . . 6
โข (((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โง ๐ โ ((๐ + 1)...๐)) โ ((๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐) = (((โคโฅโ(๐ + 1)) ร {1})โ๐)) |
64 | 16, 63 | seqfveq 14021 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1)))โ๐) = (seq(๐ + 1)( ยท ,
((โคโฅโ(๐ + 1)) ร {1}))โ๐)) |
65 | 8 | prodf1 15867 |
. . . . . 6
โข (๐ โ
(โคโฅโ(๐ + 1)) โ (seq(๐ + 1)( ยท ,
((โคโฅโ(๐ + 1)) ร {1}))โ๐) = 1) |
66 | 65 | adantl 480 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (seq(๐ + 1)( ยท ,
((โคโฅโ(๐ + 1)) ร {1}))โ๐) = 1) |
67 | 64, 66 | eqtrd 2765 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ(๐ + 1))) โ (seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1)))โ๐) = 1) |
68 | 8, 12, 14, 15, 67 | climconst 15517 |
. . 3
โข (๐ โ seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ 1) |
69 | | neeq1 2993 |
. . . . 5
โข (๐ฆ = 1 โ (๐ฆ โ 0 โ 1 โ 0)) |
70 | | breq2 5147 |
. . . . 5
โข (๐ฆ = 1 โ (seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ โ seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ 1)) |
71 | 69, 70 | anbi12d 630 |
. . . 4
โข (๐ฆ = 1 โ ((๐ฆ โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ (1 โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ 1))) |
72 | 60, 71 | spcev 3586 |
. . 3
โข ((1 โ
0 โง seq(๐ + 1)(
ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ 1) โ โ๐ฆ(๐ฆ โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |
73 | 7, 68, 72 | sylancr 585 |
. 2
โข (๐ โ โ๐ฆ(๐ฆ โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |
74 | | seqeq1 13999 |
. . . . . 6
โข (๐ = (๐ + 1) โ seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) = seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1)))) |
75 | 74 | breq1d 5153 |
. . . . 5
โข (๐ = (๐ + 1) โ (seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ โ seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |
76 | 75 | anbi2d 628 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ฆ โ 0 โง seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ (๐ฆ โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ))) |
77 | 76 | exbidv 1916 |
. . 3
โข (๐ = (๐ + 1) โ (โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ โ๐ฆ(๐ฆ โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ))) |
78 | 77 | rspcev 3602 |
. 2
โข (((๐ + 1) โ ๐ โง โ๐ฆ(๐ฆ โ 0 โง seq(๐ + 1)( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |
79 | 6, 73, 78 | syl2anc 582 |
1
โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |