Step | Hyp | Ref
| Expression |
1 | | bpos.3 |
. . . . 5
β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1)) |
2 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
3 | | 5nn 12246 |
. . . . . . . . . . . 12
β’ 5 β
β |
4 | | bpos.1 |
. . . . . . . . . . . 12
β’ (π β π β
(β€β₯β5)) |
5 | | eluznn 12850 |
. . . . . . . . . . . 12
β’ ((5
β β β§ π
β (β€β₯β5)) β π β β) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β π β β) |
7 | 6 | nnnn0d 12480 |
. . . . . . . . . 10
β’ (π β π β
β0) |
8 | | fzctr 13560 |
. . . . . . . . . 10
β’ (π β β0
β π β (0...(2
Β· π))) |
9 | | bccl2 14230 |
. . . . . . . . . 10
β’ (π β (0...(2 Β· π)) β ((2 Β· π)Cπ) β β) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . 9
β’ (π β ((2 Β· π)Cπ) β β) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β ((2 Β· π)Cπ) β β) |
12 | 2, 11 | pccld 16729 |
. . . . . . 7
β’ ((π β§ π β β) β (π pCnt ((2 Β· π)Cπ)) β
β0) |
13 | 12 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ β β (π pCnt ((2 Β· π)Cπ)) β
β0) |
14 | 13 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β βπ β β (π pCnt ((2 Β· π)Cπ)) β
β0) |
15 | | bpos.4 |
. . . . . . . . 9
β’ πΎ = (ββ((2 Β·
π) / 3)) |
16 | | 2nn 12233 |
. . . . . . . . . . . . 13
β’ 2 β
β |
17 | | nnmulcl 12184 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
18 | 16, 6, 17 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (2 Β· π) β
β) |
19 | 18 | nnred 12175 |
. . . . . . . . . . 11
β’ (π β (2 Β· π) β
β) |
20 | | 3nn 12239 |
. . . . . . . . . . 11
β’ 3 β
β |
21 | | nndivre 12201 |
. . . . . . . . . . 11
β’ (((2
Β· π) β β
β§ 3 β β) β ((2 Β· π) / 3) β β) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . . . . . 10
β’ (π β ((2 Β· π) / 3) β
β) |
23 | 22 | flcld 13710 |
. . . . . . . . 9
β’ (π β (ββ((2
Β· π) / 3)) β
β€) |
24 | 15, 23 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β πΎ β β€) |
25 | | 3re 12240 |
. . . . . . . . . . . . . 14
β’ 3 β
β |
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 3 β
β) |
27 | | 5re 12247 |
. . . . . . . . . . . . . 14
β’ 5 β
β |
28 | 27 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 5 β
β) |
29 | 6 | nnred 12175 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
30 | | 3lt5 12338 |
. . . . . . . . . . . . . . 15
β’ 3 <
5 |
31 | 25, 27, 30 | ltleii 11285 |
. . . . . . . . . . . . . 14
β’ 3 β€
5 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 3 β€ 5) |
33 | | eluzle 12783 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β5) β 5 β€ π) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 5 β€ π) |
35 | 26, 28, 29, 32, 34 | letrd 11319 |
. . . . . . . . . . . 12
β’ (π β 3 β€ π) |
36 | | 2re 12234 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
37 | | 2pos 12263 |
. . . . . . . . . . . . . . 15
β’ 0 <
2 |
38 | 36, 37 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (2 β
β β§ 0 < 2) |
39 | | lemul2 12015 |
. . . . . . . . . . . . . 14
β’ ((3
β β β§ π
β β β§ (2 β β β§ 0 < 2)) β (3 β€ π β (2 Β· 3) β€ (2
Β· π))) |
40 | 25, 38, 39 | mp3an13 1453 |
. . . . . . . . . . . . 13
β’ (π β β β (3 β€
π β (2 Β· 3)
β€ (2 Β· π))) |
41 | 29, 40 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (3 β€ π β (2 Β· 3) β€ (2 Β·
π))) |
42 | 35, 41 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (2 Β· 3) β€ (2
Β· π)) |
43 | | 3pos 12265 |
. . . . . . . . . . . . . 14
β’ 0 <
3 |
44 | 25, 43 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (3 β
β β§ 0 < 3) |
45 | | lemuldiv 12042 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ (2 Β· π) β β β§ (3 β β
β§ 0 < 3)) β ((2 Β· 3) β€ (2 Β· π) β 2 β€ ((2 Β· π) / 3))) |
46 | 36, 44, 45 | mp3an13 1453 |
. . . . . . . . . . . 12
β’ ((2
Β· π) β β
β ((2 Β· 3) β€ (2 Β· π) β 2 β€ ((2 Β· π) / 3))) |
47 | 19, 46 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((2 Β· 3) β€ (2
Β· π) β 2 β€
((2 Β· π) /
3))) |
48 | 42, 47 | mpbid 231 |
. . . . . . . . . 10
β’ (π β 2 β€ ((2 Β· π) / 3)) |
49 | | 2z 12542 |
. . . . . . . . . . 11
β’ 2 β
β€ |
50 | | flge 13717 |
. . . . . . . . . . 11
β’ ((((2
Β· π) / 3) β
β β§ 2 β β€) β (2 β€ ((2 Β· π) / 3) β 2 β€ (ββ((2
Β· π) /
3)))) |
51 | 22, 49, 50 | sylancl 587 |
. . . . . . . . . 10
β’ (π β (2 β€ ((2 Β· π) / 3) β 2 β€
(ββ((2 Β· π) / 3)))) |
52 | 48, 51 | mpbid 231 |
. . . . . . . . 9
β’ (π β 2 β€ (ββ((2
Β· π) /
3))) |
53 | 52, 15 | breqtrrdi 5152 |
. . . . . . . 8
β’ (π β 2 β€ πΎ) |
54 | 49 | eluz1i 12778 |
. . . . . . . 8
β’ (πΎ β
(β€β₯β2) β (πΎ β β€ β§ 2 β€ πΎ)) |
55 | 24, 53, 54 | sylanbrc 584 |
. . . . . . 7
β’ (π β πΎ β
(β€β₯β2)) |
56 | | eluz2nn 12816 |
. . . . . . 7
β’ (πΎ β
(β€β₯β2) β πΎ β β) |
57 | 55, 56 | syl 17 |
. . . . . 6
β’ (π β πΎ β β) |
58 | 57 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β πΎ β β) |
59 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
60 | | oveq1 7369 |
. . . . 5
β’ (π = π β (π pCnt ((2 Β· π)Cπ)) = (π pCnt ((2 Β· π)Cπ))) |
61 | 1, 14, 58, 59, 60 | pcmpt 16771 |
. . . 4
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΉ)βπΎ)) = if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0)) |
62 | | iftrue 4497 |
. . . . . 6
β’ (π β€ πΎ β if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0) = (π pCnt ((2 Β· π)Cπ))) |
63 | 62 | adantl 483 |
. . . . 5
β’ (((π β§ π β β) β§ π β€ πΎ) β if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0) = (π pCnt ((2 Β· π)Cπ))) |
64 | | iffalse 4500 |
. . . . . . 7
β’ (Β¬
π β€ πΎ β if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0) = 0) |
65 | 64 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ Β¬ π β€ πΎ) β if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0) = 0) |
66 | 24 | zred 12614 |
. . . . . . . . 9
β’ (π β πΎ β β) |
67 | | prmz 16558 |
. . . . . . . . . 10
β’ (π β β β π β
β€) |
68 | 67 | zred 12614 |
. . . . . . . . 9
β’ (π β β β π β
β) |
69 | | ltnle 11241 |
. . . . . . . . 9
β’ ((πΎ β β β§ π β β) β (πΎ < π β Β¬ π β€ πΎ)) |
70 | 66, 68, 69 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΎ < π β Β¬ π β€ πΎ)) |
71 | 70 | biimpar 479 |
. . . . . . 7
β’ (((π β§ π β β) β§ Β¬ π β€ πΎ) β πΎ < π) |
72 | 6 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β π β β) |
73 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β π β β) |
74 | 36 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β 2 β β) |
75 | 66 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β πΎ β β) |
76 | 67 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β π β β€) |
77 | 76 | zred 12614 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β π β β) |
78 | 53 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β 2 β€ πΎ) |
79 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β πΎ < π) |
80 | 74, 75, 77, 78, 79 | lelttrd 11320 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β 2 < π) |
81 | 15, 79 | eqbrtrrid 5146 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β (ββ((2 Β· π) / 3)) < π) |
82 | 22 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β ((2 Β· π) / 3) β β) |
83 | | fllt 13718 |
. . . . . . . . . . . 12
β’ ((((2
Β· π) / 3) β
β β§ π β
β€) β (((2 Β· π) / 3) < π β (ββ((2 Β· π) / 3)) < π)) |
84 | 82, 76, 83 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β (((2 Β· π) / 3) < π β (ββ((2 Β· π) / 3)) < π)) |
85 | 81, 84 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β ((2 Β· π) / 3) < π) |
86 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β π β€ π) |
87 | 72, 73, 80, 85, 86 | bposlem2 26649 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (πΎ < π β§ π β€ π)) β (π pCnt ((2 Β· π)Cπ)) = 0) |
88 | 87 | expr 458 |
. . . . . . . 8
β’ (((π β§ π β β) β§ πΎ < π) β (π β€ π β (π pCnt ((2 Β· π)Cπ)) = 0)) |
89 | | rspe 3235 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π < π β§ π β€ (2 Β· π))) β βπ β β (π < π β§ π β€ (2 Β· π))) |
90 | 89 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π < π β§ π β€ (2 Β· π))) β βπ β β (π < π β§ π β€ (2 Β· π))) |
91 | | bpos.2 |
. . . . . . . . . . . . . 14
β’ (π β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) |
92 | 91 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π < π β§ π β€ (2 Β· π))) β Β¬ βπ β β (π < π β§ π β€ (2 Β· π))) |
93 | 90, 92 | pm2.21dd 194 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π < π β§ π β€ (2 Β· π))) β (π pCnt ((2 Β· π)Cπ)) = 0) |
94 | 93 | expr 458 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π < π) β (π β€ (2 Β· π) β (π pCnt ((2 Β· π)Cπ)) = 0)) |
95 | 10 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((2 Β· π)Cπ) β β€) |
96 | 7 | faccld 14191 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (!βπ) β β) |
97 | 96, 96 | nnmulcld 12213 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((!βπ) Β· (!βπ)) β
β) |
98 | 97 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((!βπ) Β· (!βπ)) β
β€) |
99 | | dvdsmul1 16167 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((2
Β· π)Cπ) β β€ β§
((!βπ) Β·
(!βπ)) β
β€) β ((2 Β· π)Cπ) β₯ (((2 Β· π)Cπ) Β· ((!βπ) Β· (!βπ)))) |
100 | 95, 98, 99 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((2 Β· π)Cπ) β₯ (((2 Β· π)Cπ) Β· ((!βπ) Β· (!βπ)))) |
101 | | bcctr 26639 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β ((2 Β· π)Cπ) = ((!β(2 Β· π)) / ((!βπ) Β· (!βπ)))) |
102 | 7, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((2 Β· π)Cπ) = ((!β(2 Β· π)) / ((!βπ) Β· (!βπ)))) |
103 | 102 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((2 Β· π)Cπ) Β· ((!βπ) Β· (!βπ))) = (((!β(2 Β· π)) / ((!βπ) Β· (!βπ))) Β· ((!βπ) Β· (!βπ)))) |
104 | 18 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (2 Β· π) β
β0) |
105 | 104 | faccld 14191 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (!β(2 Β· π)) β
β) |
106 | 105 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (!β(2 Β· π)) β
β) |
107 | 97 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((!βπ) Β· (!βπ)) β
β) |
108 | 97 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((!βπ) Β· (!βπ)) β 0) |
109 | 106, 107,
108 | divcan1d 11939 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((!β(2 Β·
π)) / ((!βπ) Β· (!βπ))) Β· ((!βπ) Β· (!βπ))) = (!β(2 Β· π))) |
110 | 103, 109 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((2 Β· π)Cπ) Β· ((!βπ) Β· (!βπ))) = (!β(2 Β· π))) |
111 | 100, 110 | breqtrd 5136 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((2 Β· π)Cπ) β₯ (!β(2 Β· π))) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((2 Β· π)Cπ) β₯ (!β(2 Β· π))) |
113 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β β€) |
114 | 95 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((2 Β· π)Cπ) β β€) |
115 | 105 | nnzd 12533 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (!β(2 Β· π)) β
β€) |
116 | 115 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (!β(2 Β·
π)) β
β€) |
117 | | dvdstr 16183 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ ((2
Β· π)Cπ) β β€ β§
(!β(2 Β· π))
β β€) β ((π
β₯ ((2 Β· π)Cπ) β§ ((2 Β· π)Cπ) β₯ (!β(2 Β· π))) β π β₯ (!β(2 Β· π)))) |
118 | 113, 114,
116, 117 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((π β₯ ((2 Β· π)Cπ) β§ ((2 Β· π)Cπ) β₯ (!β(2 Β· π))) β π β₯ (!β(2 Β· π)))) |
119 | 112, 118 | mpan2d 693 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π β₯ ((2 Β· π)Cπ) β π β₯ (!β(2 Β· π)))) |
120 | | prmfac1 16604 |
. . . . . . . . . . . . . . . . 17
β’ (((2
Β· π) β
β0 β§ π
β β β§ π
β₯ (!β(2 Β· π))) β π β€ (2 Β· π)) |
121 | 120 | 3expia 1122 |
. . . . . . . . . . . . . . . 16
β’ (((2
Β· π) β
β0 β§ π
β β) β (π
β₯ (!β(2 Β· π)) β π β€ (2 Β· π))) |
122 | 104, 121 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π β₯ (!β(2 Β· π)) β π β€ (2 Β· π))) |
123 | 119, 122 | syld 47 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π β₯ ((2 Β· π)Cπ) β π β€ (2 Β· π))) |
124 | 123 | con3d 152 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (Β¬ π β€ (2 Β· π) β Β¬ π β₯ ((2 Β· π)Cπ))) |
125 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
126 | | pceq0 16750 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ ((2
Β· π)Cπ) β β) β ((π pCnt ((2 Β· π)Cπ)) = 0 β Β¬ π β₯ ((2 Β· π)Cπ))) |
127 | 125, 10, 126 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π pCnt ((2 Β· π)Cπ)) = 0 β Β¬ π β₯ ((2 Β· π)Cπ))) |
128 | 124, 127 | sylibrd 259 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (Β¬ π β€ (2 Β· π) β (π pCnt ((2 Β· π)Cπ)) = 0)) |
129 | 128 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π < π) β (Β¬ π β€ (2 Β· π) β (π pCnt ((2 Β· π)Cπ)) = 0)) |
130 | 94, 129 | pm2.61d 179 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π < π) β (π pCnt ((2 Β· π)Cπ)) = 0) |
131 | 130 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π < π β (π pCnt ((2 Β· π)Cπ)) = 0)) |
132 | 131 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β β) β§ πΎ < π) β (π < π β (π pCnt ((2 Β· π)Cπ)) = 0)) |
133 | | lelttric 11269 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π β€ π β¨ π < π)) |
134 | 68, 29, 133 | syl2anr 598 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π β€ π β¨ π < π)) |
135 | 134 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β β) β§ πΎ < π) β (π β€ π β¨ π < π)) |
136 | 88, 132, 135 | mpjaod 859 |
. . . . . . 7
β’ (((π β§ π β β) β§ πΎ < π) β (π pCnt ((2 Β· π)Cπ)) = 0) |
137 | 71, 136 | syldan 592 |
. . . . . 6
β’ (((π β§ π β β) β§ Β¬ π β€ πΎ) β (π pCnt ((2 Β· π)Cπ)) = 0) |
138 | 65, 137 | eqtr4d 2780 |
. . . . 5
β’ (((π β§ π β β) β§ Β¬ π β€ πΎ) β if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0) = (π pCnt ((2 Β· π)Cπ))) |
139 | 63, 138 | pm2.61dan 812 |
. . . 4
β’ ((π β§ π β β) β if(π β€ πΎ, (π pCnt ((2 Β· π)Cπ)), 0) = (π pCnt ((2 Β· π)Cπ))) |
140 | 61, 139 | eqtrd 2777 |
. . 3
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΉ)βπΎ)) = (π pCnt ((2 Β· π)Cπ))) |
141 | 140 | ralrimiva 3144 |
. 2
β’ (π β βπ β β (π pCnt (seq1( Β· , πΉ)βπΎ)) = (π pCnt ((2 Β· π)Cπ))) |
142 | 1, 13 | pcmptcl 16770 |
. . . . . 6
β’ (π β (πΉ:ββΆβ β§ seq1( Β·
, πΉ):ββΆβ)) |
143 | 142 | simprd 497 |
. . . . 5
β’ (π β seq1( Β· , πΉ):ββΆβ) |
144 | 143, 57 | ffvelcdmd 7041 |
. . . 4
β’ (π β (seq1( Β· , πΉ)βπΎ) β β) |
145 | 144 | nnnn0d 12480 |
. . 3
β’ (π β (seq1( Β· , πΉ)βπΎ) β
β0) |
146 | 10 | nnnn0d 12480 |
. . 3
β’ (π β ((2 Β· π)Cπ) β
β0) |
147 | | pc11 16759 |
. . 3
β’ (((seq1(
Β· , πΉ)βπΎ) β β0
β§ ((2 Β· π)Cπ) β β0)
β ((seq1( Β· , πΉ)βπΎ) = ((2 Β· π)Cπ) β βπ β β (π pCnt (seq1( Β· , πΉ)βπΎ)) = (π pCnt ((2 Β· π)Cπ)))) |
148 | 145, 146,
147 | syl2anc 585 |
. 2
β’ (π β ((seq1( Β· , πΉ)βπΎ) = ((2 Β· π)Cπ) β βπ β β (π pCnt (seq1( Β· , πΉ)βπΎ)) = (π pCnt ((2 Β· π)Cπ)))) |
149 | 141, 148 | mpbird 257 |
1
β’ (π β (seq1( Β· , πΉ)βπΎ) = ((2 Β· π)Cπ)) |