Step | Hyp | Ref
| Expression |
1 | | sqff1o.2 |
. 2
β’ πΉ = (π β π β¦ {π β β β£ π β₯ π}) |
2 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π₯ = π β (ΞΌβπ₯) = (ΞΌβπ)) |
3 | 2 | neeq1d 3000 |
. . . . . . . . . 10
β’ (π₯ = π β ((ΞΌβπ₯) β 0 β (ΞΌβπ) β 0)) |
4 | | breq1 5109 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
5 | 3, 4 | anbi12d 632 |
. . . . . . . . 9
β’ (π₯ = π β (((ΞΌβπ₯) β 0 β§ π₯ β₯ π) β ((ΞΌβπ) β 0 β§ π β₯ π))) |
6 | | sqff1o.1 |
. . . . . . . . 9
β’ π = {π₯ β β β£ ((ΞΌβπ₯) β 0 β§ π₯ β₯ π)} |
7 | 5, 6 | elrab2 3649 |
. . . . . . . 8
β’ (π β π β (π β β β§ ((ΞΌβπ) β 0 β§ π β₯ π))) |
8 | 7 | simprbi 498 |
. . . . . . 7
β’ (π β π β ((ΞΌβπ) β 0 β§ π β₯ π)) |
9 | 8 | simprd 497 |
. . . . . 6
β’ (π β π β π β₯ π) |
10 | 9 | ad2antlr 726 |
. . . . 5
β’ (((π β β β§ π β π) β§ π β β) β π β₯ π) |
11 | | prmz 16556 |
. . . . . . 7
β’ (π β β β π β
β€) |
12 | 11 | adantl 483 |
. . . . . 6
β’ (((π β β β§ π β π) β§ π β β) β π β β€) |
13 | | simplr 768 |
. . . . . . . . 9
β’ (((π β β β§ π β π) β§ π β β) β π β π) |
14 | 13, 7 | sylib 217 |
. . . . . . . 8
β’ (((π β β β§ π β π) β§ π β β) β (π β β β§ ((ΞΌβπ) β 0 β§ π β₯ π))) |
15 | 14 | simpld 496 |
. . . . . . 7
β’ (((π β β β§ π β π) β§ π β β) β π β β) |
16 | 15 | nnzd 12531 |
. . . . . 6
β’ (((π β β β§ π β π) β§ π β β) β π β β€) |
17 | | nnz 12525 |
. . . . . . 7
β’ (π β β β π β
β€) |
18 | 17 | ad2antrr 725 |
. . . . . 6
β’ (((π β β β§ π β π) β§ π β β) β π β β€) |
19 | | dvdstr 16181 |
. . . . . 6
β’ ((π β β€ β§ π β β€ β§ π β β€) β ((π β₯ π β§ π β₯ π) β π β₯ π)) |
20 | 12, 16, 18, 19 | syl3anc 1372 |
. . . . 5
β’ (((π β β β§ π β π) β§ π β β) β ((π β₯ π β§ π β₯ π) β π β₯ π)) |
21 | 10, 20 | mpan2d 693 |
. . . 4
β’ (((π β β β§ π β π) β§ π β β) β (π β₯ π β π β₯ π)) |
22 | 21 | ss2rabdv 4034 |
. . 3
β’ ((π β β β§ π β π) β {π β β β£ π β₯ π} β {π β β β£ π β₯ π}) |
23 | | prmex 16558 |
. . . . 5
β’ β
β V |
24 | 23 | rabex 5290 |
. . . 4
β’ {π β β β£ π β₯ π} β V |
25 | 24 | elpw 4565 |
. . 3
β’ ({π β β β£ π β₯ π} β π« {π β β β£ π β₯ π} β {π β β β£ π β₯ π} β {π β β β£ π β₯ π}) |
26 | 22, 25 | sylibr 233 |
. 2
β’ ((π β β β§ π β π) β {π β β β£ π β₯ π} β π« {π β β β£ π β₯ π}) |
27 | | cnveq 5830 |
. . . . . . 7
β’ (π¦ = (π β β β¦ if(π β π§, 1, 0)) β β‘π¦ = β‘(π β β β¦ if(π β π§, 1, 0))) |
28 | 27 | imaeq1d 6013 |
. . . . . 6
β’ (π¦ = (π β β β¦ if(π β π§, 1, 0)) β (β‘π¦ β β) = (β‘(π β β β¦ if(π β π§, 1, 0)) β β)) |
29 | 28 | eleq1d 2819 |
. . . . 5
β’ (π¦ = (π β β β¦ if(π β π§, 1, 0)) β ((β‘π¦ β β) β Fin β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β
Fin)) |
30 | | 1nn0 12434 |
. . . . . . . . . 10
β’ 1 β
β0 |
31 | | 0nn0 12433 |
. . . . . . . . . 10
β’ 0 β
β0 |
32 | 30, 31 | ifcli 4534 |
. . . . . . . . 9
β’ if(π β π§, 1, 0) β
β0 |
33 | 32 | rgenw 3065 |
. . . . . . . 8
β’
βπ β
β if(π β π§, 1, 0) β
β0 |
34 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β β¦ if(π β π§, 1, 0)) = (π β β β¦ if(π β π§, 1, 0)) |
35 | 34 | fmpt 7059 |
. . . . . . . 8
β’
(βπ β
β if(π β π§, 1, 0) β
β0 β (π β β β¦ if(π β π§, 1,
0)):ββΆβ0) |
36 | 33, 35 | mpbi 229 |
. . . . . . 7
β’ (π β β β¦ if(π β π§, 1,
0)):ββΆβ0 |
37 | 36 | a1i 11 |
. . . . . 6
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (π β β β¦ if(π β π§, 1,
0)):ββΆβ0) |
38 | | nn0ex 12424 |
. . . . . . 7
β’
β0 β V |
39 | 38, 23 | elmap 8812 |
. . . . . 6
β’ ((π β β β¦ if(π β π§, 1, 0)) β (β0
βm β) β (π β β β¦ if(π β π§, 1,
0)):ββΆβ0) |
40 | 37, 39 | sylibr 233 |
. . . . 5
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (π β β β¦ if(π β π§, 1, 0)) β (β0
βm β)) |
41 | | fzfi 13883 |
. . . . . 6
β’
(1...π) β
Fin |
42 | | ffn 6669 |
. . . . . . . . . . 11
β’ ((π β β β¦ if(π β π§, 1, 0)):ββΆβ0
β (π β β
β¦ if(π β π§, 1, 0)) Fn
β) |
43 | | elpreima 7009 |
. . . . . . . . . . 11
β’ ((π β β β¦ if(π β π§, 1, 0)) Fn β β (π₯ β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β (π₯ β β β§ ((π β β β¦ if(π β π§, 1, 0))βπ₯) β β))) |
44 | 36, 42, 43 | mp2b 10 |
. . . . . . . . . 10
β’ (π₯ β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β (π₯ β β β§ ((π β β β¦ if(π β π§, 1, 0))βπ₯) β β)) |
45 | | elequ1 2114 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (π β π§ β π₯ β π§)) |
46 | 45 | ifbid 4510 |
. . . . . . . . . . . . 13
β’ (π = π₯ β if(π β π§, 1, 0) = if(π₯ β π§, 1, 0)) |
47 | 30, 31 | ifcli 4534 |
. . . . . . . . . . . . . 14
β’ if(π₯ β π§, 1, 0) β
β0 |
48 | 47 | elexi 3463 |
. . . . . . . . . . . . 13
β’ if(π₯ β π§, 1, 0) β V |
49 | 46, 34, 48 | fvmpt 6949 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((π β β β¦ if(π β π§, 1, 0))βπ₯) = if(π₯ β π§, 1, 0)) |
50 | 49 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π₯ β β β (((π β β β¦ if(π β π§, 1, 0))βπ₯) β β β if(π₯ β π§, 1, 0) β β)) |
51 | 50 | biimpa 478 |
. . . . . . . . . 10
β’ ((π₯ β β β§ ((π β β β¦ if(π β π§, 1, 0))βπ₯) β β) β if(π₯ β π§, 1, 0) β β) |
52 | 44, 51 | sylbi 216 |
. . . . . . . . 9
β’ (π₯ β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β if(π₯ β π§, 1, 0) β β) |
53 | | 0nnn 12194 |
. . . . . . . . . . 11
β’ Β¬ 0
β β |
54 | | iffalse 4496 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π§ β if(π₯ β π§, 1, 0) = 0) |
55 | 54 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π§ β (if(π₯ β π§, 1, 0) β β β 0 β
β)) |
56 | 53, 55 | mtbiri 327 |
. . . . . . . . . 10
β’ (Β¬
π₯ β π§ β Β¬ if(π₯ β π§, 1, 0) β β) |
57 | 56 | con4i 114 |
. . . . . . . . 9
β’ (if(π₯ β π§, 1, 0) β β β π₯ β π§) |
58 | 52, 57 | syl 17 |
. . . . . . . 8
β’ (π₯ β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β π₯ β π§) |
59 | 58 | ssriv 3949 |
. . . . . . 7
β’ (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β π§ |
60 | | elpwi 4568 |
. . . . . . . . 9
β’ (π§ β π« {π β β β£ π β₯ π} β π§ β {π β β β£ π β₯ π}) |
61 | 60 | adantl 483 |
. . . . . . . 8
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β π§ β {π β β β£ π β₯ π}) |
62 | | prmssnn 16557 |
. . . . . . . . . 10
β’ β
β β |
63 | | rabss2 4036 |
. . . . . . . . . 10
β’ (β
β β β {π
β β β£ π
β₯ π} β {π β β β£ π β₯ π}) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . 9
β’ {π β β β£ π β₯ π} β {π β β β£ π β₯ π} |
65 | | dvdsssfz1 16205 |
. . . . . . . . . 10
β’ (π β β β {π β β β£ π β₯ π} β (1...π)) |
66 | 65 | adantr 482 |
. . . . . . . . 9
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β {π β β β£ π β₯ π} β (1...π)) |
67 | 64, 66 | sstrid 3956 |
. . . . . . . 8
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β {π β β β£ π β₯ π} β (1...π)) |
68 | 61, 67 | sstrd 3955 |
. . . . . . 7
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β π§ β (1...π)) |
69 | 59, 68 | sstrid 3956 |
. . . . . 6
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β (1...π)) |
70 | | ssfi 9120 |
. . . . . 6
β’
(((1...π) β Fin
β§ (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β (1...π)) β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β
Fin) |
71 | 41, 69, 70 | sylancr 588 |
. . . . 5
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (β‘(π β β β¦ if(π β π§, 1, 0)) β β) β
Fin) |
72 | 29, 40, 71 | elrabd 3648 |
. . . 4
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (π β β β¦ if(π β π§, 1, 0)) β {π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin}) |
73 | | sqff1o.3 |
. . . . . . 7
β’ πΊ = (π β β β¦ (π β β β¦ (π pCnt π))) |
74 | | eqid 2733 |
. . . . . . 7
β’ {π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin} = {π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin} |
75 | 73, 74 | 1arith 16804 |
. . . . . 6
β’ πΊ:ββ1-1-ontoβ{π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin} |
76 | | f1ocnv 6797 |
. . . . . 6
β’ (πΊ:ββ1-1-ontoβ{π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin} β β‘πΊ:{π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin}β1-1-ontoββ) |
77 | | f1of 6785 |
. . . . . 6
β’ (β‘πΊ:{π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin}β1-1-ontoββ β β‘πΊ:{π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin}βΆβ) |
78 | 75, 76, 77 | mp2b 10 |
. . . . 5
β’ β‘πΊ:{π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin}βΆβ |
79 | 78 | ffvelcdmi 7035 |
. . . 4
β’ ((π β β β¦ if(π β π§, 1, 0)) β {π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin} β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β) |
80 | 72, 79 | syl 17 |
. . 3
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β) |
81 | | f1ocnvfv2 7224 |
. . . . . . . . . . . 12
β’ ((πΊ:ββ1-1-ontoβ{π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin} β§ (π β β β¦ if(π β π§, 1, 0)) β {π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin}) β (πΊβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) = (π β β β¦ if(π β π§, 1, 0))) |
82 | 75, 72, 81 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (πΊβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) = (π β β β¦ if(π β π§, 1, 0))) |
83 | 73 | 1arithlem1 16800 |
. . . . . . . . . . . 12
β’ ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β β (πΊβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) = (π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))) |
84 | 80, 83 | syl 17 |
. . . . . . . . . . 11
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (πΊβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) = (π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))) |
85 | 82, 84 | eqtr3d 2775 |
. . . . . . . . . 10
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (π β β β¦ if(π β π§, 1, 0)) = (π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))) |
86 | 85 | fveq1d 6845 |
. . . . . . . . 9
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β ((π β β β¦ if(π β π§, 1, 0))βπ) = ((π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))βπ)) |
87 | | elequ1 2114 |
. . . . . . . . . . 11
β’ (π = π β (π β π§ β π β π§)) |
88 | 87 | ifbid 4510 |
. . . . . . . . . 10
β’ (π = π β if(π β π§, 1, 0) = if(π β π§, 1, 0)) |
89 | 30, 31 | ifcli 4534 |
. . . . . . . . . . 11
β’ if(π β π§, 1, 0) β
β0 |
90 | 89 | elexi 3463 |
. . . . . . . . . 10
β’ if(π β π§, 1, 0) β V |
91 | 88, 34, 90 | fvmpt 6949 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ if(π β π§, 1, 0))βπ) = if(π β π§, 1, 0)) |
92 | 86, 91 | sylan9req 2794 |
. . . . . . . 8
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β ((π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))βπ) = if(π β π§, 1, 0)) |
93 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) = (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) |
94 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) = (π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) |
95 | | ovex 7391 |
. . . . . . . . . 10
β’ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β V |
96 | 93, 94, 95 | fvmpt 6949 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))βπ) = (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) |
97 | 96 | adantl 483 |
. . . . . . . 8
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β ((π β β β¦ (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))))βπ) = (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) |
98 | 92, 97 | eqtr3d 2775 |
. . . . . . 7
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β if(π β π§, 1, 0) = (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) |
99 | | breq1 5109 |
. . . . . . . 8
β’ (1 =
if(π β π§, 1, 0) β (1 β€ 1 β
if(π β π§, 1, 0) β€
1)) |
100 | | breq1 5109 |
. . . . . . . 8
β’ (0 =
if(π β π§, 1, 0) β (0 β€ 1 β
if(π β π§, 1, 0) β€
1)) |
101 | | 1le1 11788 |
. . . . . . . 8
β’ 1 β€
1 |
102 | | 0le1 11683 |
. . . . . . . 8
β’ 0 β€
1 |
103 | 99, 100, 101, 102 | keephyp 4558 |
. . . . . . 7
β’ if(π β π§, 1, 0) β€ 1 |
104 | 98, 103 | eqbrtrrdi 5146 |
. . . . . 6
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ 1) |
105 | 104 | ralrimiva 3140 |
. . . . 5
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β βπ β β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ 1) |
106 | | issqf 26501 |
. . . . . 6
β’ ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β β
((ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0 β βπ β β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ 1)) |
107 | 80, 106 | syl 17 |
. . . . 5
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β ((ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0 β βπ β β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ 1)) |
108 | 105, 107 | mpbird 257 |
. . . 4
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0) |
109 | | iftrue 4493 |
. . . . . . . . . . . 12
β’ (π β π§ β if(π β π§, 1, 0) = 1) |
110 | 109 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β if(π β π§, 1, 0) = 1) |
111 | 61 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β π β {π β β β£ π β₯ π}) |
112 | | breq1 5109 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β₯ π β π β₯ π)) |
113 | 112 | elrab 3646 |
. . . . . . . . . . . . . . 15
β’ (π β {π β β β£ π β₯ π} β (π β β β§ π β₯ π)) |
114 | 111, 113 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β (π β β β§ π β₯ π)) |
115 | 114 | simprd 497 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β π β₯ π) |
116 | 114 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β π β β) |
117 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β π β β) |
118 | | pcelnn 16747 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β ((π pCnt π) β β β π β₯ π)) |
119 | 116, 117,
118 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β ((π pCnt π) β β β π β₯ π)) |
120 | 115, 119 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β (π pCnt π) β β) |
121 | 120 | nnge1d 12206 |
. . . . . . . . . . 11
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β 1 β€ (π pCnt π)) |
122 | 110, 121 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β π§) β if(π β π§, 1, 0) β€ (π pCnt π)) |
123 | 122 | ex 414 |
. . . . . . . . 9
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (π β π§ β if(π β π§, 1, 0) β€ (π pCnt π))) |
124 | 123 | adantr 482 |
. . . . . . . 8
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β (π β π§ β if(π β π§, 1, 0) β€ (π pCnt π))) |
125 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β π β β) |
126 | 17 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β π β β€) |
127 | | pcge0 16739 |
. . . . . . . . . 10
β’ ((π β β β§ π β β€) β 0 β€
(π pCnt π)) |
128 | 125, 126,
127 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β 0 β€ (π pCnt π)) |
129 | | iffalse 4496 |
. . . . . . . . . 10
β’ (Β¬
π β π§ β if(π β π§, 1, 0) = 0) |
130 | 129 | breq1d 5116 |
. . . . . . . . 9
β’ (Β¬
π β π§ β (if(π β π§, 1, 0) β€ (π pCnt π) β 0 β€ (π pCnt π))) |
131 | 128, 130 | syl5ibrcom 247 |
. . . . . . . 8
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β (Β¬ π β π§ β if(π β π§, 1, 0) β€ (π pCnt π))) |
132 | 124, 131 | pm2.61d 179 |
. . . . . . 7
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β if(π β π§, 1, 0) β€ (π pCnt π)) |
133 | 98, 132 | eqbrtrrd 5130 |
. . . . . 6
β’ (((π β β β§ π§ β π« {π β β β£ π β₯ π}) β§ π β β) β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ (π pCnt π)) |
134 | 133 | ralrimiva 3140 |
. . . . 5
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β βπ β β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ (π pCnt π)) |
135 | 80 | nnzd 12531 |
. . . . . 6
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β€) |
136 | 17 | adantr 482 |
. . . . . 6
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β π β β€) |
137 | | pc2dvds 16756 |
. . . . . 6
β’ (((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β€ β§ π β β€) β ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π β βπ β β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ (π pCnt π))) |
138 | 135, 136,
137 | syl2anc 585 |
. . . . 5
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π β βπ β β (π pCnt (β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β€ (π pCnt π))) |
139 | 134, 138 | mpbird 257 |
. . . 4
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π) |
140 | 108, 139 | jca 513 |
. . 3
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β ((ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0 β§ (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π)) |
141 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β (ΞΌβπ₯) = (ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0))))) |
142 | 141 | neeq1d 3000 |
. . . . 5
β’ (π₯ = (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β ((ΞΌβπ₯) β 0 β
(ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0)) |
143 | | breq1 5109 |
. . . . 5
β’ (π₯ = (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β (π₯ β₯ π β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π)) |
144 | 142, 143 | anbi12d 632 |
. . . 4
β’ (π₯ = (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β (((ΞΌβπ₯) β 0 β§ π₯ β₯ π) β ((ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0 β§ (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π))) |
145 | 144, 6 | elrab2 3649 |
. . 3
β’ ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β π β ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β β β§
((ΞΌβ(β‘πΊβ(π β β β¦ if(π β π§, 1, 0)))) β 0 β§ (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β₯ π))) |
146 | 80, 140, 145 | sylanbrc 584 |
. 2
β’ ((π β β β§ π§ β π« {π β β β£ π β₯ π}) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β π) |
147 | | eqcom 2740 |
. . 3
β’ (π = (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) = π) |
148 | 7 | simplbi 499 |
. . . . . . 7
β’ (π β π β π β β) |
149 | 148 | ad2antrl 727 |
. . . . . 6
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β π β β) |
150 | 23 | mptex 7174 |
. . . . . 6
β’ (π β β β¦ (π pCnt π)) β V |
151 | 73 | fvmpt2 6960 |
. . . . . 6
β’ ((π β β β§ (π β β β¦ (π pCnt π)) β V) β (πΊβπ) = (π β β β¦ (π pCnt π))) |
152 | 149, 150,
151 | sylancl 587 |
. . . . 5
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (πΊβπ) = (π β β β¦ (π pCnt π))) |
153 | 152 | eqeq1d 2735 |
. . . 4
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((πΊβπ) = (π β β β¦ if(π β π§, 1, 0)) β (π β β β¦ (π pCnt π)) = (π β β β¦ if(π β π§, 1, 0)))) |
154 | 75 | a1i 11 |
. . . . 5
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β πΊ:ββ1-1-ontoβ{π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin}) |
155 | 72 | adantrl 715 |
. . . . 5
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (π β β β¦ if(π β π§, 1, 0)) β {π¦ β (β0
βm β) β£ (β‘π¦ β β) β
Fin}) |
156 | | f1ocnvfvb 7226 |
. . . . 5
β’ ((πΊ:ββ1-1-ontoβ{π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin} β§ π β β β§ (π β β β¦ if(π β π§, 1, 0)) β {π¦ β (β0
βm β) β£ (β‘π¦ β β) β Fin}) β ((πΊβπ) = (π β β β¦ if(π β π§, 1, 0)) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) = π)) |
157 | 154, 149,
155, 156 | syl3anc 1372 |
. . . 4
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((πΊβπ) = (π β β β¦ if(π β π§, 1, 0)) β (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) = π)) |
158 | 23 | a1i 11 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β β β
V) |
159 | | 0cnd 11153 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β 0 β
β) |
160 | | 1cnd 11155 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β 1 β
β) |
161 | | 0ne1 12229 |
. . . . . . . 8
β’ 0 β
1 |
162 | 161 | a1i 11 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β 0 β 1) |
163 | 158, 159,
160, 162 | pw2f1olem 9023 |
. . . . . 6
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((π§ β π« β β§ (π β β β¦ (π pCnt π)) = (π β β β¦ if(π β π§, 1, 0))) β ((π β β β¦ (π pCnt π)) β ({0, 1} βm β)
β§ π§ = (β‘(π β β β¦ (π pCnt π)) β {1})))) |
164 | | ssrab2 4038 |
. . . . . . . . 9
β’ {π β β β£ π β₯ π} β β |
165 | 164 | sspwi 4573 |
. . . . . . . 8
β’ π«
{π β β β£
π β₯ π} β π« β |
166 | | simprr 772 |
. . . . . . . 8
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β π§ β π« {π β β β£ π β₯ π}) |
167 | 165, 166 | sselid 3943 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β π§ β π« β) |
168 | 167 | biantrurd 534 |
. . . . . 6
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((π β β β¦ (π pCnt π)) = (π β β β¦ if(π β π§, 1, 0)) β (π§ β π« β β§ (π β β β¦ (π pCnt π)) = (π β β β¦ if(π β π§, 1, 0))))) |
169 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
170 | 148 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β π) β π β β) |
171 | | pccl 16726 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (π pCnt π) β
β0) |
172 | 169, 170,
171 | syl2anr 598 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β π) β§ π β β) β (π pCnt π) β
β0) |
173 | | elnn0 12420 |
. . . . . . . . . . . . . 14
β’ ((π pCnt π) β β0 β ((π pCnt π) β β β¨ (π pCnt π) = 0)) |
174 | 172, 173 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) β β β¨ (π pCnt π) = 0)) |
175 | 174 | orcomd 870 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) = 0 β¨ (π pCnt π) β β)) |
176 | 8 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (ΞΌβπ) β 0) |
177 | 176 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β π) β (ΞΌβπ) β 0) |
178 | | issqf 26501 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
((ΞΌβπ) β 0
β βπ β
β (π pCnt π) β€ 1)) |
179 | 170, 178 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β π) β ((ΞΌβπ) β 0 β βπ β β (π pCnt π) β€ 1)) |
180 | 177, 179 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β π) β βπ β β (π pCnt π) β€ 1) |
181 | 180 | r19.21bi 3233 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β π) β§ π β β) β (π pCnt π) β€ 1) |
182 | | nnle1eq1 12188 |
. . . . . . . . . . . . . 14
β’ ((π pCnt π) β β β ((π pCnt π) β€ 1 β (π pCnt π) = 1)) |
183 | 181, 182 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) β β β (π pCnt π) = 1)) |
184 | 183 | orim2d 966 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β π) β§ π β β) β (((π pCnt π) = 0 β¨ (π pCnt π) β β) β ((π pCnt π) = 0 β¨ (π pCnt π) = 1))) |
185 | 175, 184 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) = 0 β¨ (π pCnt π) = 1)) |
186 | | ovex 7391 |
. . . . . . . . . . . 12
β’ (π pCnt π) β V |
187 | 186 | elpr 4610 |
. . . . . . . . . . 11
β’ ((π pCnt π) β {0, 1} β ((π pCnt π) = 0 β¨ (π pCnt π) = 1)) |
188 | 185, 187 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β β β§ π β π) β§ π β β) β (π pCnt π) β {0, 1}) |
189 | 188 | fmpttd 7064 |
. . . . . . . . 9
β’ ((π β β β§ π β π) β (π β β β¦ (π pCnt π)):ββΆ{0, 1}) |
190 | 189 | adantrr 716 |
. . . . . . . 8
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (π β β β¦ (π pCnt π)):ββΆ{0, 1}) |
191 | | prex 5390 |
. . . . . . . . 9
β’ {0, 1}
β V |
192 | 191, 23 | elmap 8812 |
. . . . . . . 8
β’ ((π β β β¦ (π pCnt π)) β ({0, 1} βm β)
β (π β β
β¦ (π pCnt π)):ββΆ{0,
1}) |
193 | 190, 192 | sylibr 233 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (π β β β¦ (π pCnt π)) β ({0, 1} βm
β)) |
194 | 193 | biantrurd 534 |
. . . . . 6
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (π§ = (β‘(π β β β¦ (π pCnt π)) β {1}) β ((π β β β¦ (π pCnt π)) β ({0, 1} βm β)
β§ π§ = (β‘(π β β β¦ (π pCnt π)) β {1})))) |
195 | 163, 168,
194 | 3bitr4d 311 |
. . . . 5
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((π β β β¦ (π pCnt π)) = (π β β β¦ if(π β π§, 1, 0)) β π§ = (β‘(π β β β¦ (π pCnt π)) β {1}))) |
196 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β β¦ (π pCnt π)) = (π β β β¦ (π pCnt π)) |
197 | 196 | mptiniseg 6192 |
. . . . . . . 8
β’ (1 β
β0 β (β‘(π β β β¦ (π pCnt π)) β {1}) = {π β β β£ (π pCnt π) = 1}) |
198 | 30, 197 | ax-mp 5 |
. . . . . . 7
β’ (β‘(π β β β¦ (π pCnt π)) β {1}) = {π β β β£ (π pCnt π) = 1} |
199 | | id 22 |
. . . . . . . . . . . 12
β’ ((π pCnt π) = 1 β (π pCnt π) = 1) |
200 | | 1nn 12169 |
. . . . . . . . . . . 12
β’ 1 β
β |
201 | 199, 200 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ ((π pCnt π) = 1 β (π pCnt π) β β) |
202 | 201, 183 | impbid2 225 |
. . . . . . . . . 10
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) = 1 β (π pCnt π) β β)) |
203 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β β β§ π β π) β§ π β β) β π β β) |
204 | | pcelnn 16747 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β ((π pCnt π) β β β π β₯ π)) |
205 | 203, 15, 204 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) β β β π β₯ π)) |
206 | 202, 205 | bitrd 279 |
. . . . . . . . 9
β’ (((π β β β§ π β π) β§ π β β) β ((π pCnt π) = 1 β π β₯ π)) |
207 | 206 | rabbidva 3413 |
. . . . . . . 8
β’ ((π β β β§ π β π) β {π β β β£ (π pCnt π) = 1} = {π β β β£ π β₯ π}) |
208 | 207 | adantrr 716 |
. . . . . . 7
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β {π β β β£ (π pCnt π) = 1} = {π β β β£ π β₯ π}) |
209 | 198, 208 | eqtrid 2785 |
. . . . . 6
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (β‘(π β β β¦ (π pCnt π)) β {1}) = {π β β β£ π β₯ π}) |
210 | 209 | eqeq2d 2744 |
. . . . 5
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (π§ = (β‘(π β β β¦ (π pCnt π)) β {1}) β π§ = {π β β β£ π β₯ π})) |
211 | 195, 210 | bitrd 279 |
. . . 4
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((π β β β¦ (π pCnt π)) = (π β β β¦ if(π β π§, 1, 0)) β π§ = {π β β β£ π β₯ π})) |
212 | 153, 157,
211 | 3bitr3d 309 |
. . 3
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β ((β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) = π β π§ = {π β β β£ π β₯ π})) |
213 | 147, 212 | bitrid 283 |
. 2
β’ ((π β β β§ (π β π β§ π§ β π« {π β β β£ π β₯ π})) β (π = (β‘πΊβ(π β β β¦ if(π β π§, 1, 0))) β π§ = {π β β β£ π β₯ π})) |
214 | 1, 26, 146, 213 | f1o2d 7608 |
1
β’ (π β β β πΉ:πβ1-1-ontoβπ« {π β β β£ π β₯ π}) |