Step | Hyp | Ref
| Expression |
1 | | pcmpt.2 |
. . . . . . . . 9
β’ (π β βπ β β π΄ β
β0) |
2 | | nfv 1528 |
. . . . . . . . . 10
β’
β²π π΄ β
β0 |
3 | | nfcsb1v 3091 |
. . . . . . . . . . 11
β’
β²πβ¦π / πβ¦π΄ |
4 | 3 | nfel1 2330 |
. . . . . . . . . 10
β’
β²πβ¦π / πβ¦π΄ β β0 |
5 | | csbeq1a 3067 |
. . . . . . . . . . 11
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
6 | 5 | eleq1d 2246 |
. . . . . . . . . 10
β’ (π = π β (π΄ β β0 β
β¦π / πβ¦π΄ β
β0)) |
7 | 2, 4, 6 | cbvralw 2699 |
. . . . . . . . 9
β’
(βπ β
β π΄ β
β0 β βπ β β β¦π / πβ¦π΄ β
β0) |
8 | 1, 7 | sylib 122 |
. . . . . . . 8
β’ (π β βπ β β β¦π / πβ¦π΄ β
β0) |
9 | | csbeq1 3061 |
. . . . . . . . . 10
β’ (π = π β β¦π / πβ¦π΄ = β¦π / πβ¦π΄) |
10 | 9 | eleq1d 2246 |
. . . . . . . . 9
β’ (π = π β (β¦π / πβ¦π΄ β β0 β
β¦π / πβ¦π΄ β
β0)) |
11 | 10 | rspcv 2838 |
. . . . . . . 8
β’ (π β β β
(βπ β β
β¦π / πβ¦π΄ β β0 β
β¦π / πβ¦π΄ β
β0)) |
12 | 8, 11 | mpan9 281 |
. . . . . . 7
β’ ((π β§ π β β) β β¦π / πβ¦π΄ β
β0) |
13 | 12 | nn0ge0d 9232 |
. . . . . 6
β’ ((π β§ π β β) β 0 β€
β¦π / πβ¦π΄) |
14 | | 0le0 9008 |
. . . . . . 7
β’ 0 β€
0 |
15 | 14 | a1i 9 |
. . . . . 6
β’ ((π β§ π β β) β 0 β€
0) |
16 | | prmz 12111 |
. . . . . . . 8
β’ (π β β β π β
β€) |
17 | | pcmptdvds.3 |
. . . . . . . . . 10
β’ (π β π β (β€β₯βπ)) |
18 | | eluzelz 9537 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β€) |
19 | 17, 18 | syl 14 |
. . . . . . . . 9
β’ (π β π β β€) |
20 | 19 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β€) |
21 | | zdcle 9329 |
. . . . . . . 8
β’ ((π β β€ β§ π β β€) β
DECID π β€
π) |
22 | 16, 20, 21 | syl2an2 594 |
. . . . . . 7
β’ ((π β§ π β β) β DECID
π β€ π) |
23 | | pcmpt.3 |
. . . . . . . . . . 11
β’ (π β π β β) |
24 | 23 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
25 | 24 | nnzd 9374 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β€) |
26 | | zdcle 9329 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β€) β
DECID π β€
π) |
27 | 16, 25, 26 | syl2an2 594 |
. . . . . . . 8
β’ ((π β§ π β β) β DECID
π β€ π) |
28 | | dcn 842 |
. . . . . . . 8
β’
(DECID π β€ π β DECID Β¬ π β€ π) |
29 | 27, 28 | syl 14 |
. . . . . . 7
β’ ((π β§ π β β) β DECID
Β¬ π β€ π) |
30 | | dcan2 934 |
. . . . . . 7
β’
(DECID π β€ π β (DECID Β¬ π β€ π β DECID (π β€ π β§ Β¬ π β€ π))) |
31 | 22, 29, 30 | sylc 62 |
. . . . . 6
β’ ((π β§ π β β) β DECID
(π β€ π β§ Β¬ π β€ π)) |
32 | | breq2 4008 |
. . . . . . 7
β’
(β¦π /
πβ¦π΄ = if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0) β (0 β€ β¦π / πβ¦π΄ β 0 β€ if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0))) |
33 | | breq2 4008 |
. . . . . . 7
β’ (0 =
if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0) β (0 β€ 0 β 0 β€
if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0))) |
34 | 32, 33 | ifbothdc 3568 |
. . . . . 6
β’ ((0 β€
β¦π / πβ¦π΄ β§ 0 β€ 0 β§ DECID
(π β€ π β§ Β¬ π β€ π)) β 0 β€ if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0)) |
35 | 13, 15, 31, 34 | syl3anc 1238 |
. . . . 5
β’ ((π β§ π β β) β 0 β€ if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0)) |
36 | | pcmpt.1 |
. . . . . . 7
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) |
37 | | nfcv 2319 |
. . . . . . . 8
β’
β²πif(π β β, (πβπ΄), 1) |
38 | | nfv 1528 |
. . . . . . . . 9
β’
β²π π β β |
39 | | nfcv 2319 |
. . . . . . . . . 10
β’
β²ππ |
40 | | nfcv 2319 |
. . . . . . . . . 10
β’
β²πβ |
41 | 39, 40, 3 | nfov 5905 |
. . . . . . . . 9
β’
β²π(πββ¦π / πβ¦π΄) |
42 | | nfcv 2319 |
. . . . . . . . 9
β’
β²π1 |
43 | 38, 41, 42 | nfif 3563 |
. . . . . . . 8
β’
β²πif(π β β, (πββ¦π / πβ¦π΄), 1) |
44 | | eleq1w 2238 |
. . . . . . . . 9
β’ (π = π β (π β β β π β β)) |
45 | | id 19 |
. . . . . . . . . 10
β’ (π = π β π = π) |
46 | 45, 5 | oveq12d 5893 |
. . . . . . . . 9
β’ (π = π β (πβπ΄) = (πββ¦π / πβ¦π΄)) |
47 | 44, 46 | ifbieq1d 3557 |
. . . . . . . 8
β’ (π = π β if(π β β, (πβπ΄), 1) = if(π β β, (πββ¦π / πβ¦π΄), 1)) |
48 | 37, 43, 47 | cbvmpt 4099 |
. . . . . . 7
β’ (π β β β¦ if(π β β, (πβπ΄), 1)) = (π β β β¦ if(π β β, (πββ¦π / πβ¦π΄), 1)) |
49 | 36, 48 | eqtri 2198 |
. . . . . 6
β’ πΉ = (π β β β¦ if(π β β, (πββ¦π / πβ¦π΄), 1)) |
50 | 8 | adantr 276 |
. . . . . 6
β’ ((π β§ π β β) β βπ β β
β¦π / πβ¦π΄ β
β0) |
51 | | simpr 110 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
52 | 17 | adantr 276 |
. . . . . 6
β’ ((π β§ π β β) β π β (β€β₯βπ)) |
53 | 49, 50, 24, 51, 9, 52 | pcmpt2 12342 |
. . . . 5
β’ ((π β§ π β β) β (π pCnt ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ))) = if((π β€ π β§ Β¬ π β€ π), β¦π / πβ¦π΄, 0)) |
54 | 35, 53 | breqtrrd 4032 |
. . . 4
β’ ((π β§ π β β) β 0 β€ (π pCnt ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)))) |
55 | 54 | ralrimiva 2550 |
. . 3
β’ (π β βπ β β 0 β€ (π pCnt ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)))) |
56 | 36, 1 | pcmptcl 12340 |
. . . . . . . 8
β’ (π β (πΉ:ββΆβ β§ seq1( Β·
, πΉ):ββΆβ)) |
57 | 56 | simprd 114 |
. . . . . . 7
β’ (π β seq1( Β· , πΉ):ββΆβ) |
58 | | eluznn 9600 |
. . . . . . . 8
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
59 | 23, 17, 58 | syl2anc 411 |
. . . . . . 7
β’ (π β π β β) |
60 | 57, 59 | ffvelcdmd 5653 |
. . . . . 6
β’ (π β (seq1( Β· , πΉ)βπ) β β) |
61 | 60 | nnzd 9374 |
. . . . 5
β’ (π β (seq1( Β· , πΉ)βπ) β β€) |
62 | 57, 23 | ffvelcdmd 5653 |
. . . . 5
β’ (π β (seq1( Β· , πΉ)βπ) β β) |
63 | | znq 9624 |
. . . . 5
β’ (((seq1(
Β· , πΉ)βπ) β β€ β§ (seq1(
Β· , πΉ)βπ) β β) β ((seq1(
Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β) |
64 | 61, 62, 63 | syl2anc 411 |
. . . 4
β’ (π β ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β) |
65 | | pcz 12331 |
. . . 4
β’ (((seq1(
Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β β (((seq1( Β· ,
πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β€ β βπ β β 0 β€ (π pCnt ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ))))) |
66 | 64, 65 | syl 14 |
. . 3
β’ (π β (((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β€ β βπ β β 0 β€ (π pCnt ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ))))) |
67 | 55, 66 | mpbird 167 |
. 2
β’ (π β ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β€) |
68 | 62 | nnzd 9374 |
. . 3
β’ (π β (seq1( Β· , πΉ)βπ) β β€) |
69 | 62 | nnne0d 8964 |
. . 3
β’ (π β (seq1( Β· , πΉ)βπ) β 0) |
70 | | dvdsval2 11797 |
. . 3
β’ (((seq1(
Β· , πΉ)βπ) β β€ β§ (seq1(
Β· , πΉ)βπ) β 0 β§ (seq1( Β· ,
πΉ)βπ) β β€) β ((seq1( Β· ,
πΉ)βπ) β₯ (seq1( Β· , πΉ)βπ) β ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β€)) |
71 | 68, 69, 61, 70 | syl3anc 1238 |
. 2
β’ (π β ((seq1( Β· , πΉ)βπ) β₯ (seq1( Β· , πΉ)βπ) β ((seq1( Β· , πΉ)βπ) / (seq1( Β· , πΉ)βπ)) β β€)) |
72 | 67, 71 | mpbird 167 |
1
β’ (π β (seq1( Β· , πΉ)βπ) β₯ (seq1( Β· , πΉ)βπ)) |