Step | Hyp | Ref
| Expression |
1 | | nfcv 2319 |
. . . 4
โข
โฒ๐๐ด |
2 | | nfcsb1v 3091 |
. . . 4
โข
โฒ๐โฆ๐ / ๐โฆ๐ด |
3 | | csbeq1a 3067 |
. . . 4
โข (๐ = ๐ โ ๐ด = โฆ๐ / ๐โฆ๐ด) |
4 | 1, 2, 3 | cbvprodi 11568 |
. . 3
โข
โ๐ โ
{๐}๐ด = โ๐ โ {๐}โฆ๐ / ๐โฆ๐ด |
5 | | csbeq1 3061 |
. . . 4
โข (๐ = ({โจ1, ๐โฉ}โ๐) โ โฆ๐ / ๐โฆ๐ด = โฆ({โจ1, ๐โฉ}โ๐) / ๐โฆ๐ด) |
6 | | 1nn 8930 |
. . . . 5
โข 1 โ
โ |
7 | 6 | a1i 9 |
. . . 4
โข ((๐ โ ๐ โง ๐ต โ โ) โ 1 โ
โ) |
8 | | 1z 9279 |
. . . . . 6
โข 1 โ
โค |
9 | | f1osng 5503 |
. . . . . . 7
โข ((1
โ โค โง ๐
โ ๐) โ {โจ1,
๐โฉ}:{1}โ1-1-ontoโ{๐}) |
10 | | fzsn 10066 |
. . . . . . . . 9
โข (1 โ
โค โ (1...1) = {1}) |
11 | 8, 10 | ax-mp 5 |
. . . . . . . 8
โข (1...1) =
{1} |
12 | | f1oeq2 5451 |
. . . . . . . 8
โข ((1...1)
= {1} โ ({โจ1, ๐โฉ}:(1...1)โ1-1-ontoโ{๐} โ {โจ1, ๐โฉ}:{1}โ1-1-ontoโ{๐})) |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
โข
({โจ1, ๐โฉ}:(1...1)โ1-1-ontoโ{๐} โ {โจ1, ๐โฉ}:{1}โ1-1-ontoโ{๐}) |
14 | 9, 13 | sylibr 134 |
. . . . . 6
โข ((1
โ โค โง ๐
โ ๐) โ {โจ1,
๐โฉ}:(1...1)โ1-1-ontoโ{๐}) |
15 | 8, 14 | mpan 424 |
. . . . 5
โข (๐ โ ๐ โ {โจ1, ๐โฉ}:(1...1)โ1-1-ontoโ{๐}) |
16 | 15 | adantr 276 |
. . . 4
โข ((๐ โ ๐ โง ๐ต โ โ) โ {โจ1, ๐โฉ}:(1...1)โ1-1-ontoโ{๐}) |
17 | | velsn 3610 |
. . . . . 6
โข (๐ โ {๐} โ ๐ = ๐) |
18 | | csbeq1 3061 |
. . . . . . 7
โข (๐ = ๐ โ โฆ๐ / ๐โฆ๐ด = โฆ๐ / ๐โฆ๐ด) |
19 | | prodsnf.1 |
. . . . . . . . . 10
โข
โฒ๐๐ต |
20 | 19 | a1i 9 |
. . . . . . . . 9
โข (๐ โ ๐ โ โฒ๐๐ต) |
21 | | prodsnf.2 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ด = ๐ต) |
22 | 20, 21 | csbiegf 3101 |
. . . . . . . 8
โข (๐ โ ๐ โ โฆ๐ / ๐โฆ๐ด = ๐ต) |
23 | 22 | adantr 276 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ต โ โ) โ โฆ๐ / ๐โฆ๐ด = ๐ต) |
24 | 18, 23 | sylan9eqr 2232 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ = ๐) โ โฆ๐ / ๐โฆ๐ด = ๐ต) |
25 | 17, 24 | sylan2b 287 |
. . . . 5
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ {๐}) โ โฆ๐ / ๐โฆ๐ด = ๐ต) |
26 | | simplr 528 |
. . . . 5
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ {๐}) โ ๐ต โ โ) |
27 | 25, 26 | eqeltrd 2254 |
. . . 4
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ {๐}) โ โฆ๐ / ๐โฆ๐ด โ โ) |
28 | 11 | eleq2i 2244 |
. . . . . 6
โข (๐ โ (1...1) โ ๐ โ {1}) |
29 | | velsn 3610 |
. . . . . 6
โข (๐ โ {1} โ ๐ = 1) |
30 | 28, 29 | bitri 184 |
. . . . 5
โข (๐ โ (1...1) โ ๐ = 1) |
31 | | fvsng 5713 |
. . . . . . . . . . 11
โข ((1
โ โค โง ๐
โ ๐) โ ({โจ1,
๐โฉ}โ1) = ๐) |
32 | 8, 31 | mpan 424 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ({โจ1, ๐โฉ}โ1) = ๐) |
33 | 32 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ต โ โ) โ ({โจ1, ๐โฉ}โ1) = ๐) |
34 | 33 | csbeq1d 3065 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ต โ โ) โ
โฆ({โจ1, ๐โฉ}โ1) / ๐โฆ๐ด = โฆ๐ / ๐โฆ๐ด) |
35 | | simpr 110 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ต โ โ) โ ๐ต โ โ) |
36 | | fvsng 5713 |
. . . . . . . . 9
โข ((1
โ โค โง ๐ต
โ โ) โ ({โจ1, ๐ตโฉ}โ1) = ๐ต) |
37 | 8, 35, 36 | sylancr 414 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ต โ โ) โ ({โจ1, ๐ตโฉ}โ1) = ๐ต) |
38 | 23, 34, 37 | 3eqtr4rd 2221 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ต โ โ) โ ({โจ1, ๐ตโฉ}โ1) =
โฆ({โจ1, ๐โฉ}โ1) / ๐โฆ๐ด) |
39 | | fveq2 5516 |
. . . . . . . 8
โข (๐ = 1 โ ({โจ1, ๐ตโฉ}โ๐) = ({โจ1, ๐ตโฉ}โ1)) |
40 | | fveq2 5516 |
. . . . . . . . 9
โข (๐ = 1 โ ({โจ1, ๐โฉ}โ๐) = ({โจ1, ๐โฉ}โ1)) |
41 | 40 | csbeq1d 3065 |
. . . . . . . 8
โข (๐ = 1 โ
โฆ({โจ1, ๐โฉ}โ๐) / ๐โฆ๐ด = โฆ({โจ1, ๐โฉ}โ1) / ๐โฆ๐ด) |
42 | 39, 41 | eqeq12d 2192 |
. . . . . . 7
โข (๐ = 1 โ (({โจ1, ๐ตโฉ}โ๐) = โฆ({โจ1, ๐โฉ}โ๐) / ๐โฆ๐ด โ ({โจ1, ๐ตโฉ}โ1) = โฆ({โจ1,
๐โฉ}โ1) / ๐โฆ๐ด)) |
43 | 38, 42 | syl5ibrcom 157 |
. . . . . 6
โข ((๐ โ ๐ โง ๐ต โ โ) โ (๐ = 1 โ ({โจ1, ๐ตโฉ}โ๐) = โฆ({โจ1, ๐โฉ}โ๐) / ๐โฆ๐ด)) |
44 | 43 | imp 124 |
. . . . 5
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ = 1) โ ({โจ1, ๐ตโฉ}โ๐) = โฆ({โจ1, ๐โฉ}โ๐) / ๐โฆ๐ด) |
45 | 30, 44 | sylan2b 287 |
. . . 4
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (1...1)) โ ({โจ1, ๐ตโฉ}โ๐) = โฆ({โจ1, ๐โฉ}โ๐) / ๐โฆ๐ด) |
46 | 5, 7, 16, 27, 45 | fprodseq 11591 |
. . 3
โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}โฆ๐ / ๐โฆ๐ด = (seq1( ยท , (๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1)))โ1)) |
47 | 4, 46 | eqtrid 2222 |
. 2
โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}๐ด = (seq1( ยท , (๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1)))โ1)) |
48 | | 1zzd 9280 |
. . . 4
โข ((๐ โ ๐ โง ๐ต โ โ) โ 1 โ
โค) |
49 | | eqid 2177 |
. . . . . 6
โข (๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1)) = (๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1)) |
50 | | breq1 4007 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โค 1 โ ๐ โค 1)) |
51 | | fveq2 5516 |
. . . . . . 7
โข (๐ = ๐ โ ({โจ1, ๐ตโฉ}โ๐) = ({โจ1, ๐ตโฉ}โ๐)) |
52 | 50, 51 | ifbieq1d 3557 |
. . . . . 6
โข (๐ = ๐ โ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1) = if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1)) |
53 | | elnnuz 9564 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
54 | 53 | biimpri 133 |
. . . . . . 7
โข (๐ โ
(โคโฅโ1) โ ๐ โ โ) |
55 | 54 | adantl 277 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ ๐ โ
โ) |
56 | | simpr 110 |
. . . . . . . . . . 11
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
๐ โค 1) |
57 | | eluzle 9540 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ1) โ 1 โค ๐) |
58 | 57 | ad2antlr 489 |
. . . . . . . . . . 11
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ 1
โค ๐) |
59 | 54 | nnzd 9374 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ1) โ ๐ โ โค) |
60 | 59 | ad2antlr 489 |
. . . . . . . . . . . . 13
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
๐ โ
โค) |
61 | 60 | zred 9375 |
. . . . . . . . . . . 12
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
๐ โ
โ) |
62 | | 1red 7972 |
. . . . . . . . . . . 12
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ 1
โ โ) |
63 | 61, 62 | letri3d 8073 |
. . . . . . . . . . 11
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
(๐ = 1 โ (๐ โค 1 โง 1 โค ๐))) |
64 | 56, 58, 63 | mpbir2and 944 |
. . . . . . . . . 10
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
๐ = 1) |
65 | 64 | fveq2d 5520 |
. . . . . . . . 9
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
({โจ1, ๐ตโฉ}โ๐) = ({โจ1, ๐ตโฉ}โ1)) |
66 | 37 | ad2antrr 488 |
. . . . . . . . 9
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
({โจ1, ๐ตโฉ}โ1) = ๐ต) |
67 | 65, 66 | eqtrd 2210 |
. . . . . . . 8
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
({โจ1, ๐ตโฉ}โ๐) = ๐ต) |
68 | 35 | ad2antrr 488 |
. . . . . . . 8
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
๐ต โ
โ) |
69 | 67, 68 | eqeltrd 2254 |
. . . . . . 7
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ๐ โค 1) โ
({โจ1, ๐ตโฉ}โ๐) โ โ) |
70 | | 1cnd 7973 |
. . . . . . 7
โข ((((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ โค 1)
โ 1 โ โ) |
71 | 55 | nnzd 9374 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ ๐ โ
โค) |
72 | | 1zzd 9280 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ 1 โ โค) |
73 | | zdcle 9329 |
. . . . . . . 8
โข ((๐ โ โค โง 1 โ
โค) โ DECID ๐ โค 1) |
74 | 71, 72, 73 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ DECID ๐ โค 1) |
75 | 69, 70, 74 | ifcldadc 3564 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ if(๐ โค 1,
({โจ1, ๐ตโฉ}โ๐), 1) โ โ) |
76 | 49, 52, 55, 75 | fvmptd3 5610 |
. . . . 5
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ ((๐ โ โ
โฆ if(๐ โค 1,
({โจ1, ๐ตโฉ}โ๐), 1))โ๐) = if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1)) |
77 | 76, 75 | eqeltrd 2254 |
. . . 4
โข (((๐ โ ๐ โง ๐ต โ โ) โง ๐ โ (โคโฅโ1))
โ ((๐ โ โ
โฆ if(๐ โค 1,
({โจ1, ๐ตโฉ}โ๐), 1))โ๐) โ โ) |
78 | | mulcl 7938 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
79 | 78 | adantl 277 |
. . . 4
โข (((๐ โ ๐ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ ยท ๐) โ โ) |
80 | 48, 77, 79 | seq3-1 10460 |
. . 3
โข ((๐ โ ๐ โง ๐ต โ โ) โ (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โค 1, ({โจ1,
๐ตโฉ}โ๐), 1)))โ1) = ((๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1))โ1)) |
81 | | breq1 4007 |
. . . . . 6
โข (๐ = 1 โ (๐ โค 1 โ 1 โค 1)) |
82 | 81, 39 | ifbieq1d 3557 |
. . . . 5
โข (๐ = 1 โ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1) = if(1 โค 1, ({โจ1, ๐ตโฉ}โ1),
1)) |
83 | | 1le1 8529 |
. . . . . . . 8
โข 1 โค
1 |
84 | 83 | iftruei 3541 |
. . . . . . 7
โข if(1 โค
1, ({โจ1, ๐ตโฉ}โ1), 1) = ({โจ1, ๐ตโฉ}โ1) |
85 | 84, 37 | eqtrid 2222 |
. . . . . 6
โข ((๐ โ ๐ โง ๐ต โ โ) โ if(1 โค 1,
({โจ1, ๐ตโฉ}โ1), 1) = ๐ต) |
86 | 85, 35 | eqeltrd 2254 |
. . . . 5
โข ((๐ โ ๐ โง ๐ต โ โ) โ if(1 โค 1,
({โจ1, ๐ตโฉ}โ1), 1) โ
โ) |
87 | 49, 82, 7, 86 | fvmptd3 5610 |
. . . 4
โข ((๐ โ ๐ โง ๐ต โ โ) โ ((๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1))โ1) = if(1 โค 1, ({โจ1,
๐ตโฉ}โ1),
1)) |
88 | 87, 85 | eqtrd 2210 |
. . 3
โข ((๐ โ ๐ โง ๐ต โ โ) โ ((๐ โ โ โฆ if(๐ โค 1, ({โจ1, ๐ตโฉ}โ๐), 1))โ1) = ๐ต) |
89 | 80, 88 | eqtrd 2210 |
. 2
โข ((๐ โ ๐ โง ๐ต โ โ) โ (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โค 1, ({โจ1,
๐ตโฉ}โ๐), 1)))โ1) = ๐ต) |
90 | 47, 89 | eqtrd 2210 |
1
โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}๐ด = ๐ต) |