Step | Hyp | Ref
| Expression |
1 | | iffalse 4537 |
. . . . . 6
β’ (Β¬
(π΄β2) = 1 β
if((π΄β2) = 1, 1, 0) =
0) |
2 | 1 | necon1ai 2969 |
. . . . 5
β’
(if((π΄β2) = 1,
1, 0) β 0 β (π΄β2) = 1) |
3 | | iftrue 4534 |
. . . . . 6
β’ ((π΄β2) = 1 β if((π΄β2) = 1, 1, 0) =
1) |
4 | | ax-1ne0 11176 |
. . . . . . 7
β’ 1 β
0 |
5 | 4 | a1i 11 |
. . . . . 6
β’ ((π΄β2) = 1 β 1 β
0) |
6 | 3, 5 | eqnetrd 3009 |
. . . . 5
β’ ((π΄β2) = 1 β if((π΄β2) = 1, 1, 0) β
0) |
7 | 2, 6 | impbii 208 |
. . . 4
β’
(if((π΄β2) = 1,
1, 0) β 0 β (π΄β2) = 1) |
8 | | zre 12559 |
. . . . . . . 8
β’ (π΄ β β€ β π΄ β
β) |
9 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β π΄ β β) |
10 | | absresq 15246 |
. . . . . . 7
β’ (π΄ β β β
((absβπ΄)β2) =
(π΄β2)) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β ((absβπ΄)β2) = (π΄β2)) |
12 | | sq1 14156 |
. . . . . . 7
β’
(1β2) = 1 |
13 | 12 | a1i 11 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (1β2) =
1) |
14 | 11, 13 | eqeq12d 2749 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (((absβπ΄)β2) = (1β2) β
(π΄β2) =
1)) |
15 | 9 | recnd 11239 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β π΄ β β) |
16 | 15 | abscld 15380 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (absβπ΄) β
β) |
17 | 15 | absge0d 15388 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β 0 β€
(absβπ΄)) |
18 | | 1re 11211 |
. . . . . . 7
β’ 1 β
β |
19 | | 0le1 11734 |
. . . . . . 7
β’ 0 β€
1 |
20 | | sq11 14093 |
. . . . . . 7
β’
((((absβπ΄)
β β β§ 0 β€ (absβπ΄)) β§ (1 β β β§ 0 β€ 1))
β (((absβπ΄)β2) = (1β2) β
(absβπ΄) =
1)) |
21 | 18, 19, 20 | mpanr12 704 |
. . . . . 6
β’
(((absβπ΄)
β β β§ 0 β€ (absβπ΄)) β (((absβπ΄)β2) = (1β2) β
(absβπ΄) =
1)) |
22 | 16, 17, 21 | syl2anc 585 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (((absβπ΄)β2) = (1β2) β
(absβπ΄) =
1)) |
23 | 14, 22 | bitr3d 281 |
. . . 4
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β ((π΄β2) = 1 β (absβπ΄) = 1)) |
24 | 7, 23 | bitrid 283 |
. . 3
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (if((π΄β2) = 1, 1, 0) β 0
β (absβπ΄) =
1)) |
25 | | oveq2 7414 |
. . . . 5
β’ (π = 0 β (π΄ /L π) = (π΄ /L 0)) |
26 | | lgs0 26803 |
. . . . . 6
β’ (π΄ β β€ β (π΄ /L 0) =
if((π΄β2) = 1, 1,
0)) |
27 | 26 | adantr 482 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L 0) =
if((π΄β2) = 1, 1,
0)) |
28 | 25, 27 | sylan9eqr 2795 |
. . . 4
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (π΄ /L π) = if((π΄β2) = 1, 1, 0)) |
29 | 28 | neeq1d 3001 |
. . 3
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β ((π΄ /L π) β 0 β if((π΄β2) = 1, 1, 0) β
0)) |
30 | | oveq2 7414 |
. . . . 5
β’ (π = 0 β (π΄ gcd π) = (π΄ gcd 0)) |
31 | | gcdid0 16458 |
. . . . . 6
β’ (π΄ β β€ β (π΄ gcd 0) = (absβπ΄)) |
32 | 31 | adantr 482 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€) β (π΄ gcd 0) = (absβπ΄)) |
33 | 30, 32 | sylan9eqr 2795 |
. . . 4
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β (π΄ gcd π) = (absβπ΄)) |
34 | 33 | eqeq1d 2735 |
. . 3
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β ((π΄ gcd π) = 1 β (absβπ΄) = 1)) |
35 | 24, 29, 34 | 3bitr4d 311 |
. 2
β’ (((π΄ β β€ β§ π β β€) β§ π = 0) β ((π΄ /L π) β 0 β (π΄ gcd π) = 1)) |
36 | | eqid 2733 |
. . . . . 6
β’ (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
37 | 36 | lgsval4 26810 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
38 | 37 | neeq1d 3001 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((π΄ /L π) β 0 β (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))) β 0)) |
39 | | neeq1 3004 |
. . . . . . 7
β’ (-1 =
if((π < 0 β§ π΄ < 0), -1, 1) β (-1 β
0 β if((π < 0 β§
π΄ < 0), -1, 1) β
0)) |
40 | | neeq1 3004 |
. . . . . . 7
β’ (1 =
if((π < 0 β§ π΄ < 0), -1, 1) β (1 β
0 β if((π < 0 β§
π΄ < 0), -1, 1) β
0)) |
41 | | neg1ne0 12325 |
. . . . . . 7
β’ -1 β
0 |
42 | 39, 40, 41, 4 | keephyp 4599 |
. . . . . 6
β’ if((π < 0 β§ π΄ < 0), -1, 1) β 0 |
43 | 42 | biantrur 532 |
. . . . 5
β’ ((seq1(
Β· , (π β
β β¦ if(π β
β, ((π΄
/L π)β(π pCnt π)), 1)))β(absβπ)) β 0 β (if((π < 0 β§ π΄ < 0), -1, 1) β 0 β§ (seq1(
Β· , (π β
β β¦ if(π β
β, ((π΄
/L π)β(π pCnt π)), 1)))β(absβπ)) β 0)) |
44 | | neg1cn 12323 |
. . . . . . . 8
β’ -1 β
β |
45 | | ax-1cn 11165 |
. . . . . . . 8
β’ 1 β
β |
46 | 44, 45 | ifcli 4575 |
. . . . . . 7
β’ if((π < 0 β§ π΄ < 0), -1, 1) β
β |
47 | 46 | a1i 11 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β if((π < 0 β§ π΄ < 0), -1, 1) β
β) |
48 | | nnabscl 15269 |
. . . . . . . . 9
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
49 | 48 | 3adant1 1131 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (absβπ) β
β) |
50 | | nnuz 12862 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
51 | 49, 50 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (absβπ) β
(β€β₯β1)) |
52 | 36 | lgsfcl3 26811 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)),
1)):ββΆβ€) |
53 | | elfznn 13527 |
. . . . . . . . 9
β’ (π β (1...(absβπ)) β π β β) |
54 | | ffvelcdm 7081 |
. . . . . . . . 9
β’ (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)):ββΆβ€ β§ π β β) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
55 | 52, 53, 54 | syl2an 597 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
56 | 55 | zcnd 12664 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β) |
57 | | mulcl 11191 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
58 | 57 | adantl 483 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
59 | 51, 56, 58 | seqcl 13985 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) β β) |
60 | 47, 59 | mulne0bd 11862 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((if((π < 0 β§ π΄ < 0), -1, 1) β 0 β§ (seq1(
Β· , (π β
β β¦ if(π β
β, ((π΄
/L π)β(π pCnt π)), 1)))β(absβπ)) β 0) β (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))) β 0)) |
61 | 43, 60 | bitr2id 284 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))) β 0 β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β 0)) |
62 | | gcd2n0cl 16447 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ gcd π) β β) |
63 | | eluz2b3 12903 |
. . . . . . . . 9
β’ ((π΄ gcd π) β (β€β₯β2)
β ((π΄ gcd π) β β β§ (π΄ gcd π) β 1)) |
64 | | exprmfct 16638 |
. . . . . . . . 9
β’ ((π΄ gcd π) β (β€β₯β2)
β βπ β
β π β₯ (π΄ gcd π)) |
65 | 63, 64 | sylbir 234 |
. . . . . . . 8
β’ (((π΄ gcd π) β β β§ (π΄ gcd π) β 1) β βπ β β π β₯ (π΄ gcd π)) |
66 | 57 | adantl 483 |
. . . . . . . . . 10
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
67 | 56 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β) |
68 | | mul02 11389 |
. . . . . . . . . . 11
β’ (π β β β (0
Β· π) =
0) |
69 | 68 | adantl 483 |
. . . . . . . . . 10
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β β) β (0 Β· π) = 0) |
70 | | mul01 11390 |
. . . . . . . . . . 11
β’ (π β β β (π Β· 0) =
0) |
71 | 70 | adantl 483 |
. . . . . . . . . 10
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β β) β (π Β· 0) = 0) |
72 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β₯ (π΄ gcd π)) |
73 | | prmz 16609 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β€) |
74 | 73 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β β€) |
75 | | simpl1 1192 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π΄ β β€) |
76 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β β€) |
77 | | dvdsgcdb 16484 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π΄ β β€ β§ π β β€) β ((π β₯ π΄ β§ π β₯ π) β π β₯ (π΄ gcd π))) |
78 | 74, 75, 76, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β ((π β₯ π΄ β§ π β₯ π) β π β₯ (π΄ gcd π))) |
79 | 72, 78 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π β₯ π΄ β§ π β₯ π)) |
80 | 79 | simprd 497 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β₯ π) |
81 | | dvdsabsb 16216 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (absβπ))) |
82 | 74, 76, 81 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π β₯ π β π β₯ (absβπ))) |
83 | 80, 82 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β₯ (absβπ)) |
84 | 49 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (absβπ) β β) |
85 | | dvdsle 16250 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§
(absβπ) β
β) β (π β₯
(absβπ) β π β€ (absβπ))) |
86 | 74, 84, 85 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π β₯ (absβπ) β π β€ (absβπ))) |
87 | 83, 86 | mpd 15 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β€ (absβπ)) |
88 | | prmnn 16608 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
89 | 88 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β β) |
90 | 89, 50 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β
(β€β₯β1)) |
91 | 84 | nnzd 12582 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (absβπ) β β€) |
92 | | elfz5 13490 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β1) β§ (absβπ) β β€) β (π β (1...(absβπ)) β π β€ (absβπ))) |
93 | 90, 91, 92 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π β (1...(absβπ)) β π β€ (absβπ))) |
94 | 87, 93 | mpbird 257 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β (1...(absβπ))) |
95 | | eleq1w 2817 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β β β π β β)) |
96 | | oveq2 7414 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π΄ /L π) = (π΄ /L π)) |
97 | | oveq1 7413 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π pCnt π) = (π pCnt π)) |
98 | 96, 97 | oveq12d 7424 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β(π pCnt π))) |
99 | 95, 98 | ifbieq1d 4552 |
. . . . . . . . . . . . 13
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
100 | | ovex 7439 |
. . . . . . . . . . . . . 14
β’ ((π΄ /L π)β(π pCnt π)) β V |
101 | | 1ex 11207 |
. . . . . . . . . . . . . 14
β’ 1 β
V |
102 | 100, 101 | ifex 4578 |
. . . . . . . . . . . . 13
β’ if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β V |
103 | 99, 36, 102 | fvmpt 6996 |
. . . . . . . . . . . 12
β’ (π β β β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
104 | 89, 103 | syl 17 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
105 | | iftrue 4534 |
. . . . . . . . . . . 12
β’ (π β β β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = ((π΄ /L π)β(π pCnt π))) |
106 | 105 | ad2antrl 727 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = ((π΄ /L π)β(π pCnt π))) |
107 | | oveq2 7414 |
. . . . . . . . . . . . . . . 16
β’ (π = 2 β (π΄ /L π) = (π΄ /L 2)) |
108 | | lgs2 26807 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β€ β (π΄ /L 2) = if(2
β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1,
-1))) |
109 | 75, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π΄ /L 2) = if(2 β₯
π΄, 0, if((π΄ mod 8) β {1, 7}, 1,
-1))) |
110 | 107, 109 | sylan9eqr 2795 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π = 2) β (π΄ /L π) = if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1,
-1))) |
111 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π = 2) β π = 2) |
112 | 79 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β₯ π΄) |
113 | 112 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π = 2) β π β₯ π΄) |
114 | 111, 113 | eqbrtrrd 5172 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π = 2) β 2 β₯ π΄) |
115 | 114 | iftrued 4536 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π = 2) β if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)) =
0) |
116 | 110, 115 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π = 2) β (π΄ /L π) = 0) |
117 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π΄ β β€) |
118 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β β) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β β) |
120 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β 2) |
121 | | eldifsn 4790 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β β {2})
β (π β β
β§ π β
2)) |
122 | 119, 120,
121 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β (β β
{2})) |
123 | | lgsval3 26808 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β€ β§ π β (β β {2}))
β (π΄
/L π) =
((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) |
124 | 117, 122,
123 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π΄ /L π) = ((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) |
125 | | oddprm 16740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (β β {2})
β ((π β 1) / 2)
β β) |
126 | 122, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((π β 1) / 2) β
β) |
127 | 126 | nnnn0d 12529 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((π β 1) / 2) β
β0) |
128 | | zexpcl 14039 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β€ β§ ((π β 1) / 2) β
β0) β (π΄β((π β 1) / 2)) β
β€) |
129 | 117, 127,
128 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π΄β((π β 1) / 2)) β
β€) |
130 | 129 | zred 12663 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π΄β((π β 1) / 2)) β
β) |
131 | | 0red 11214 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β 0 β
β) |
132 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β 1 β
β) |
133 | 119, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β β) |
134 | 133 | nnrpd 13011 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β β+) |
135 | | 0zd 12567 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β 0 β
β€) |
136 | 112 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β₯ π΄) |
137 | | dvdsval3 16198 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β β§ π΄ β β€) β (π β₯ π΄ β (π΄ mod π) = 0)) |
138 | 133, 117,
137 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π β₯ π΄ β (π΄ mod π) = 0)) |
139 | 136, 138 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π΄ mod π) = 0) |
140 | | 0mod 13864 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β+
β (0 mod π) =
0) |
141 | 134, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (0 mod π) = 0) |
142 | 139, 141 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π΄ mod π) = (0 mod π)) |
143 | | modexp 14198 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄ β β€ β§ 0 β
β€) β§ (((π β
1) / 2) β β0 β§ π β β+) β§ (π΄ mod π) = (0 mod π)) β ((π΄β((π β 1) / 2)) mod π) = ((0β((π β 1) / 2)) mod π)) |
144 | 117, 135,
127, 134, 142, 143 | syl221anc 1382 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((π΄β((π β 1) / 2)) mod π) = ((0β((π β 1) / 2)) mod π)) |
145 | 126 | 0expd 14101 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (0β((π β 1) / 2)) = 0) |
146 | 145 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((0β((π β 1) / 2)) mod π) = (0 mod π)) |
147 | 144, 146 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((π΄β((π β 1) / 2)) mod π) = (0 mod π)) |
148 | | modadd1 13870 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄β((π β 1) / 2)) β β β§ 0
β β) β§ (1 β β β§ π β β+) β§ ((π΄β((π β 1) / 2)) mod π) = (0 mod π)) β (((π΄β((π β 1) / 2)) + 1) mod π) = ((0 + 1) mod π)) |
149 | 130, 131,
132, 134, 147, 148 | syl221anc 1382 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (((π΄β((π β 1) / 2)) + 1) mod π) = ((0 + 1) mod π)) |
150 | | 0p1e1 12331 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 + 1) =
1 |
151 | 150 | oveq1i 7416 |
. . . . . . . . . . . . . . . . . . 19
β’ ((0 + 1)
mod π) = (1 mod π) |
152 | 149, 151 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (((π΄β((π β 1) / 2)) + 1) mod π) = (1 mod π)) |
153 | 133 | nnred 12224 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β β) |
154 | | prmuz2 16630 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β π β
(β€β₯β2)) |
155 | 119, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β π β
(β€β₯β2)) |
156 | | eluz2b2 12902 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
157 | 155, 156 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π β β β§ 1 < π)) |
158 | 157 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β 1 < π) |
159 | | 1mod 13865 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ 1 <
π) β (1 mod π) = 1) |
160 | 153, 158,
159 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (1 mod π) = 1) |
161 | 152, 160 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (((π΄β((π β 1) / 2)) + 1) mod π) = 1) |
162 | 161 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((((π΄β((π β 1) / 2)) + 1) mod π) β 1) = (1 β
1)) |
163 | | 1m1e0 12281 |
. . . . . . . . . . . . . . . 16
β’ (1
β 1) = 0 |
164 | 162, 163 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β ((((π΄β((π β 1) / 2)) + 1) mod π) β 1) = 0) |
165 | 124, 164 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β§ π β 2) β (π΄ /L π) = 0) |
166 | 116, 165 | pm2.61dane 3030 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π΄ /L π) = 0) |
167 | 166 | oveq1d 7421 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β ((π΄ /L π)β(π pCnt π)) = (0β(π pCnt π))) |
168 | | zq 12935 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β π β
β) |
169 | 76, 168 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β π β β) |
170 | | pcabs 16805 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
171 | 118, 169,
170 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π pCnt (absβπ)) = (π pCnt π)) |
172 | | pcelnn 16800 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§
(absβπ) β
β) β ((π pCnt
(absβπ)) β
β β π β₯
(absβπ))) |
173 | 118, 84, 172 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β ((π pCnt (absβπ)) β β β π β₯ (absβπ))) |
174 | 83, 173 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π pCnt (absβπ)) β β) |
175 | 171, 174 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (π pCnt π) β β) |
176 | 175 | 0expd 14101 |
. . . . . . . . . . . 12
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (0β(π pCnt π)) = 0) |
177 | 167, 176 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β ((π΄ /L π)β(π pCnt π)) = 0) |
178 | 104, 106,
177 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = 0) |
179 | 66, 67, 69, 71, 94, 84, 178 | seqz 14013 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π β β β§ π β₯ (π΄ gcd π))) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = 0) |
180 | 179 | rexlimdvaa 3157 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (βπ β β π β₯ (π΄ gcd π) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = 0)) |
181 | 65, 180 | syl5 34 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (((π΄ gcd π) β β β§ (π΄ gcd π) β 1) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = 0)) |
182 | 62, 181 | mpand 694 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((π΄ gcd π) β 1 β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = 0)) |
183 | 182 | necon1d 2963 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) β 0 β (π΄ gcd π) = 1)) |
184 | 51 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β (absβπ) β
(β€β₯β1)) |
185 | 53 | adantl 483 |
. . . . . . . . . 10
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β (1...(absβπ))) β π β β) |
186 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π = π β (π β β β π β β)) |
187 | | oveq2 7414 |
. . . . . . . . . . . . 13
β’ (π = π β (π΄ /L π) = (π΄ /L π)) |
188 | | oveq1 7413 |
. . . . . . . . . . . . 13
β’ (π = π β (π pCnt π) = (π pCnt π)) |
189 | 187, 188 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ (π = π β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β(π pCnt π))) |
190 | 186, 189 | ifbieq1d 4552 |
. . . . . . . . . . 11
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
191 | | ovex 7439 |
. . . . . . . . . . . 12
β’ ((π΄ /L π)β(π pCnt π)) β V |
192 | 191, 101 | ifex 4578 |
. . . . . . . . . . 11
β’ if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β V |
193 | 190, 36, 192 | fvmpt 6996 |
. . . . . . . . . 10
β’ (π β β β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
194 | 185, 193 | syl 17 |
. . . . . . . . 9
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
195 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π΄ β β€) |
196 | | prmz 16609 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β€) |
197 | 196 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π β β€) |
198 | | lgscl 26804 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β
β€) |
199 | 195, 197,
198 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π΄ /L π) β β€) |
200 | 199 | zcnd 12664 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π΄ /L π) β β) |
201 | 200 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β (π΄ /L π) β β) |
202 | | oveq2 7414 |
. . . . . . . . . . . . . . . . 17
β’ (π = 2 β (π΄ /L π) = (π΄ /L 2)) |
203 | 195 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β π΄ β β€) |
204 | 203, 108 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β (π΄ /L 2) = if(2 β₯
π΄, 0, if((π΄ mod 8) β {1, 7}, 1,
-1))) |
205 | 202, 204 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π = 2) β (π΄ /L π) = if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1,
-1))) |
206 | | nprmdvds1 16640 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β Β¬
π β₯
1) |
207 | 206 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β Β¬ π β₯ 1) |
208 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π β β€) |
209 | | dvdsgcdb 16484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β€ β§ π΄ β β€ β§ π β β€) β ((π β₯ π΄ β§ π β₯ π) β π β₯ (π΄ gcd π))) |
210 | 197, 195,
208, 209 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β ((π β₯ π΄ β§ π β₯ π) β π β₯ (π΄ gcd π))) |
211 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π΄ gcd π) = 1) |
212 | 211 | breq2d 5160 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π β₯ (π΄ gcd π) β π β₯ 1)) |
213 | 210, 212 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β ((π β₯ π΄ β§ π β₯ π) β π β₯ 1)) |
214 | 207, 213 | mtbird 325 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β Β¬ (π β₯ π΄ β§ π β₯ π)) |
215 | | imnan 401 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β₯ π΄ β Β¬ π β₯ π) β Β¬ (π β₯ π΄ β§ π β₯ π)) |
216 | 214, 215 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π β₯ π΄ β Β¬ π β₯ π)) |
217 | 216 | con2d 134 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π β₯ π β Β¬ π β₯ π΄)) |
218 | 217 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β Β¬ π β₯ π΄) |
219 | | breq1 5151 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 2 β (π β₯ π΄ β 2 β₯ π΄)) |
220 | 219 | notbid 318 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 2 β (Β¬ π β₯ π΄ β Β¬ 2 β₯ π΄)) |
221 | 218, 220 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β (π = 2 β Β¬ 2 β₯ π΄)) |
222 | 221 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π = 2) β Β¬ 2 β₯ π΄) |
223 | 222 | iffalsed 4539 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π = 2) β if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)) = if((π΄ mod 8) β {1, 7}, 1,
-1)) |
224 | 205, 223 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π = 2) β (π΄ /L π) = if((π΄ mod 8) β {1, 7}, 1,
-1)) |
225 | | neeq1 3004 |
. . . . . . . . . . . . . . . . 17
β’ (1 =
if((π΄ mod 8) β {1, 7},
1, -1) β (1 β 0 β if((π΄ mod 8) β {1, 7}, 1, -1) β
0)) |
226 | | neeq1 3004 |
. . . . . . . . . . . . . . . . 17
β’ (-1 =
if((π΄ mod 8) β {1, 7},
1, -1) β (-1 β 0 β if((π΄ mod 8) β {1, 7}, 1, -1) β
0)) |
227 | 225, 226,
4, 41 | keephyp 4599 |
. . . . . . . . . . . . . . . 16
β’ if((π΄ mod 8) β {1, 7}, 1, -1)
β 0 |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π = 2) β if((π΄ mod 8) β {1, 7}, 1, -1) β
0) |
229 | 224, 228 | eqnetrd 3009 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π = 2) β (π΄ /L π) β 0) |
230 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π β β) |
231 | 230 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β β) |
232 | 231, 206 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β Β¬ π β₯ 1) |
233 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β₯ π) |
234 | 231, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β β€) |
235 | 203 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π΄ β β€) |
236 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β 2) |
237 | | eldifsn 4790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (β β {2})
β (π β β
β§ π β
2)) |
238 | 231, 236,
237 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β (β β
{2})) |
239 | | oddprm 16740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (β β {2})
β ((π β 1) / 2)
β β) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π β 1) / 2) β
β) |
241 | 240 | nnnn0d 12529 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π β 1) / 2) β
β0) |
242 | | zexpcl 14039 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β€ β§ ((π β 1) / 2) β
β0) β (π΄β((π β 1) / 2)) β
β€) |
243 | 235, 241,
242 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π΄β((π β 1) / 2)) β
β€) |
244 | 208 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β β€) |
245 | | dvdsgcd 16483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β€ β§ (π΄β((π β 1) / 2)) β β€ β§ π β β€) β ((π β₯ (π΄β((π β 1) / 2)) β§ π β₯ π) β π β₯ ((π΄β((π β 1) / 2)) gcd π))) |
246 | 234, 243,
244, 245 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π β₯ (π΄β((π β 1) / 2)) β§ π β₯ π) β π β₯ ((π΄β((π β 1) / 2)) gcd π))) |
247 | 233, 246 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π β₯ (π΄β((π β 1) / 2)) β π β₯ ((π΄β((π β 1) / 2)) gcd π))) |
248 | 235 | zcnd 12664 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π΄ β β) |
249 | 248, 241 | absexpd 15396 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (absβ(π΄β((π β 1) / 2))) = ((absβπ΄)β((π β 1) / 2))) |
250 | 249 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((absβ(π΄β((π β 1) / 2))) gcd (absβπ)) = (((absβπ΄)β((π β 1) / 2)) gcd (absβπ))) |
251 | | gcdabs 16469 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄β((π β 1) / 2)) β β€ β§ π β β€) β
((absβ(π΄β((π β 1) / 2))) gcd
(absβπ)) = ((π΄β((π β 1) / 2)) gcd π)) |
252 | 243, 244,
251 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((absβ(π΄β((π β 1) / 2))) gcd (absβπ)) = ((π΄β((π β 1) / 2)) gcd π)) |
253 | | gcdabs 16469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄ β β€ β§ π β β€) β
((absβπ΄) gcd
(absβπ)) = (π΄ gcd π)) |
254 | 235, 244,
253 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((absβπ΄) gcd (absβπ)) = (π΄ gcd π)) |
255 | 211 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π΄ gcd π) = 1) |
256 | 254, 255 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((absβπ΄) gcd (absβπ)) = 1) |
257 | 218 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β Β¬ π β₯ π΄) |
258 | | dvds0 16212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β€ β π β₯ 0) |
259 | 234, 258 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β₯ 0) |
260 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π΄ = 0 β (π β₯ π΄ β π β₯ 0)) |
261 | 259, 260 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π΄ = 0 β π β₯ π΄)) |
262 | 261 | necon3bd 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (Β¬ π β₯ π΄ β π΄ β 0)) |
263 | 257, 262 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π΄ β 0) |
264 | | nnabscl 15269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄ β β€ β§ π΄ β 0) β (absβπ΄) β
β) |
265 | 235, 263,
264 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (absβπ΄) β β) |
266 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π β 0) |
267 | 208, 266,
48 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (absβπ) β
β) |
268 | 267 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (absβπ) β β) |
269 | | rplpwr 16496 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((absβπ΄)
β β β§ (absβπ) β β β§ ((π β 1) / 2) β β) β
(((absβπ΄) gcd
(absβπ)) = 1 β
(((absβπ΄)β((π β 1) / 2)) gcd (absβπ)) = 1)) |
270 | 265, 268,
240, 269 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (((absβπ΄) gcd (absβπ)) = 1 β (((absβπ΄)β((π β 1) / 2)) gcd (absβπ)) = 1)) |
271 | 256, 270 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (((absβπ΄)β((π β 1) / 2)) gcd (absβπ)) = 1) |
272 | 250, 252,
271 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π΄β((π β 1) / 2)) gcd π) = 1) |
273 | 272 | breq2d 5160 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π β₯ ((π΄β((π β 1) / 2)) gcd π) β π β₯ 1)) |
274 | 247, 273 | sylibd 238 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π β₯ (π΄β((π β 1) / 2)) β π β₯ 1)) |
275 | 232, 274 | mtod 197 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β Β¬ π β₯ (π΄β((π β 1) / 2))) |
276 | | prmnn 16608 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β) |
277 | 276 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π β β) |
278 | 277 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β β) |
279 | | dvdsval3 16198 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π΄β((π β 1) / 2)) β β€) β
(π β₯ (π΄β((π β 1) / 2)) β ((π΄β((π β 1) / 2)) mod π) = 0)) |
280 | 278, 243,
279 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π β₯ (π΄β((π β 1) / 2)) β ((π΄β((π β 1) / 2)) mod π) = 0)) |
281 | 280 | necon3bbid 2979 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (Β¬ π β₯ (π΄β((π β 1) / 2)) β ((π΄β((π β 1) / 2)) mod π) β 0)) |
282 | 275, 281 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π΄β((π β 1) / 2)) mod π) β 0) |
283 | | lgsvalmod 26809 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β€ β§ π β (β β {2}))
β ((π΄
/L π) mod
π) = ((π΄β((π β 1) / 2)) mod π)) |
284 | 235, 238,
283 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π΄ /L π) mod π) = ((π΄β((π β 1) / 2)) mod π)) |
285 | 278 | nnrpd 13011 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β π β β+) |
286 | | 0mod 13864 |
. . . . . . . . . . . . . . . . 17
β’ (π β β+
β (0 mod π) =
0) |
287 | 285, 286 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (0 mod π) = 0) |
288 | 282, 284,
287 | 3netr4d 3019 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β ((π΄ /L π) mod π) β (0 mod π)) |
289 | | oveq1 7413 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ /L π) = 0 β ((π΄ /L π) mod π) = (0 mod π)) |
290 | 289 | necon3i 2974 |
. . . . . . . . . . . . . . 15
β’ (((π΄ /L π) mod π) β (0 mod π) β (π΄ /L π) β 0) |
291 | 288, 290 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β§ π β 2) β (π΄ /L π) β 0) |
292 | 229, 291 | pm2.61dane 3030 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β (π΄ /L π) β 0) |
293 | | pczcl 16778 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π β β€ β§ π β 0)) β (π pCnt π) β
β0) |
294 | 230, 208,
266, 293 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π pCnt π) β
β0) |
295 | 294 | nn0zd 12581 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π pCnt π) β β€) |
296 | 295 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β (π pCnt π) β β€) |
297 | | neeq1 3004 |
. . . . . . . . . . . . . 14
β’ (π₯ = ((π΄ /L π)β(π pCnt π)) β (π₯ β 0 β ((π΄ /L π)β(π pCnt π)) β 0)) |
298 | | expclz 14047 |
. . . . . . . . . . . . . 14
β’ (((π΄ /L π) β β β§ (π΄ /L π) β 0 β§ (π pCnt π) β β€) β ((π΄ /L π)β(π pCnt π)) β β) |
299 | | expne0i 14057 |
. . . . . . . . . . . . . 14
β’ (((π΄ /L π) β β β§ (π΄ /L π) β 0 β§ (π pCnt π) β β€) β ((π΄ /L π)β(π pCnt π)) β 0) |
300 | 297, 298,
299 | elrabd 3685 |
. . . . . . . . . . . . 13
β’ (((π΄ /L π) β β β§ (π΄ /L π) β 0 β§ (π pCnt π) β β€) β ((π΄ /L π)β(π pCnt π)) β {π₯ β β β£ π₯ β 0}) |
301 | 201, 292,
296, 300 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ π β₯ π) β ((π΄ /L π)β(π pCnt π)) β {π₯ β β β£ π₯ β 0}) |
302 | | dvdsabsb 16216 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (absβπ))) |
303 | 197, 208,
302 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π β₯ π β π β₯ (absβπ))) |
304 | 303 | notbid 318 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (Β¬ π β₯ π β Β¬ π β₯ (absβπ))) |
305 | | pceq0 16801 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§
(absβπ) β
β) β ((π pCnt
(absβπ)) = 0 β
Β¬ π β₯
(absβπ))) |
306 | 230, 267,
305 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β ((π pCnt (absβπ)) = 0 β Β¬ π β₯ (absβπ))) |
307 | 208, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β π β β) |
308 | | pcabs 16805 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
309 | 230, 307,
308 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
310 | 309 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β ((π pCnt (absβπ)) = 0 β (π pCnt π) = 0)) |
311 | 304, 306,
310 | 3bitr2rd 308 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β ((π pCnt π) = 0 β Β¬ π β₯ π)) |
312 | 311 | biimpar 479 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ Β¬ π β₯ π) β (π pCnt π) = 0) |
313 | 312 | oveq2d 7422 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ Β¬ π β₯ π) β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β0)) |
314 | 200 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ Β¬ π β₯ π) β (π΄ /L π) β β) |
315 | 314 | exp0d 14102 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ Β¬ π β₯ π) β ((π΄ /L π)β0) = 1) |
316 | 313, 315 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ Β¬ π β₯ π) β ((π΄ /L π)β(π pCnt π)) = 1) |
317 | | neeq1 3004 |
. . . . . . . . . . . . . . 15
β’ (π₯ = 1 β (π₯ β 0 β 1 β 0)) |
318 | 317 | elrab 3683 |
. . . . . . . . . . . . . 14
β’ (1 β
{π₯ β β β£
π₯ β 0} β (1 β
β β§ 1 β 0)) |
319 | 45, 4, 318 | mpbir2an 710 |
. . . . . . . . . . . . 13
β’ 1 β
{π₯ β β β£
π₯ β 0} |
320 | 316, 319 | eqeltrdi 2842 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β 0)
β§ (π΄ gcd π) = 1) β§ π β β) β§ Β¬ π β₯ π) β ((π΄ /L π)β(π pCnt π)) β {π₯ β β β£ π₯ β 0}) |
321 | 301, 320 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β β) β ((π΄ /L π)β(π pCnt π)) β {π₯ β β β£ π₯ β 0}) |
322 | 319 | a1i 11 |
. . . . . . . . . . 11
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ Β¬ π β β) β 1 β {π₯ β β β£ π₯ β 0}) |
323 | 321, 322 | ifclda 4563 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β {π₯ β β β£ π₯ β 0}) |
324 | 323 | adantr 482 |
. . . . . . . . 9
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β (1...(absβπ))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β {π₯ β β β£ π₯ β 0}) |
325 | 194, 324 | eqeltrd 2834 |
. . . . . . . 8
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β {π₯ β β β£ π₯ β 0}) |
326 | | neeq1 3004 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ β 0 β π β 0)) |
327 | 326 | elrab 3683 |
. . . . . . . . . . 11
β’ (π β {π₯ β β β£ π₯ β 0} β (π β β β§ π β 0)) |
328 | | neeq1 3004 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (π₯ β 0 β π¦ β 0)) |
329 | 328 | elrab 3683 |
. . . . . . . . . . 11
β’ (π¦ β {π₯ β β β£ π₯ β 0} β (π¦ β β β§ π¦ β 0)) |
330 | | mulcl 11191 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π¦ β β) β (π Β· π¦) β β) |
331 | 330 | ad2ant2r 746 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β 0) β§ (π¦ β β β§ π¦ β 0)) β (π Β· π¦) β β) |
332 | | mulne0 11853 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β 0) β§ (π¦ β β β§ π¦ β 0)) β (π Β· π¦) β 0) |
333 | 331, 332 | jca 513 |
. . . . . . . . . . 11
β’ (((π β β β§ π β 0) β§ (π¦ β β β§ π¦ β 0)) β ((π Β· π¦) β β β§ (π Β· π¦) β 0)) |
334 | 327, 329,
333 | syl2anb 599 |
. . . . . . . . . 10
β’ ((π β {π₯ β β β£ π₯ β 0} β§ π¦ β {π₯ β β β£ π₯ β 0}) β ((π Β· π¦) β β β§ (π Β· π¦) β 0)) |
335 | | neeq1 3004 |
. . . . . . . . . . 11
β’ (π₯ = (π Β· π¦) β (π₯ β 0 β (π Β· π¦) β 0)) |
336 | 335 | elrab 3683 |
. . . . . . . . . 10
β’ ((π Β· π¦) β {π₯ β β β£ π₯ β 0} β ((π Β· π¦) β β β§ (π Β· π¦) β 0)) |
337 | 334, 336 | sylibr 233 |
. . . . . . . . 9
β’ ((π β {π₯ β β β£ π₯ β 0} β§ π¦ β {π₯ β β β£ π₯ β 0}) β (π Β· π¦) β {π₯ β β β£ π₯ β 0}) |
338 | 337 | adantl 483 |
. . . . . . . 8
β’ ((((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β§ (π β {π₯ β β β£ π₯ β 0} β§ π¦ β {π₯ β β β£ π₯ β 0})) β (π Β· π¦) β {π₯ β β β£ π₯ β 0}) |
339 | 184, 325,
338 | seqcl 13985 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β {π₯ β β β£ π₯ β 0}) |
340 | | neeq1 3004 |
. . . . . . . . 9
β’ (π₯ = (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β (π₯ β 0 β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β 0)) |
341 | 340 | elrab 3683 |
. . . . . . . 8
β’ ((seq1(
Β· , (π β
β β¦ if(π β
β, ((π΄
/L π)β(π pCnt π)), 1)))β(absβπ)) β {π₯ β β β£ π₯ β 0} β ((seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β β β§ (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) β 0)) |
342 | 341 | simprbi 498 |
. . . . . . 7
β’ ((seq1(
Β· , (π β
β β¦ if(π β
β, ((π΄
/L π)β(π pCnt π)), 1)))β(absβπ)) β {π₯ β β β£ π₯ β 0} β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β 0) |
343 | 339, 342 | syl 17 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β 0) β§ (π΄ gcd π) = 1) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β 0) |
344 | 343 | ex 414 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((π΄ gcd π) = 1 β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β 0)) |
345 | 183, 344 | impbid 211 |
. . . 4
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) β 0 β (π΄ gcd π) = 1)) |
346 | 38, 61, 345 | 3bitrd 305 |
. . 3
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β ((π΄ /L π) β 0 β (π΄ gcd π) = 1)) |
347 | 346 | 3expa 1119 |
. 2
β’ (((π΄ β β€ β§ π β β€) β§ π β 0) β ((π΄ /L π) β 0 β (π΄ gcd π) = 1)) |
348 | 35, 347 | pm2.61dane 3030 |
1
β’ ((π΄ β β€ β§ π β β€) β ((π΄ /L π) β 0 β (π΄ gcd π) = 1)) |