Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β {(π β 1)}) β π β {(π β 1)}) |
2 | | wilthlem2.s |
. . . . . . . . . . . . . 14
β’ (π β π β π΄) |
3 | | eleq2 2823 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((π β 1) β π₯ β (π β 1) β π)) |
4 | | eleq2 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (((π¦β(π β 2)) mod π) β π₯ β ((π¦β(π β 2)) mod π) β π)) |
5 | 4 | raleqbi1dv 3306 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯ β βπ¦ β π ((π¦β(π β 2)) mod π) β π)) |
6 | 3, 5 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (((π β 1) β π₯ β§ βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯) β ((π β 1) β π β§ βπ¦ β π ((π¦β(π β 2)) mod π) β π))) |
7 | | wilthlem.a |
. . . . . . . . . . . . . . 15
β’ π΄ = {π₯ β π« (1...(π β 1)) β£ ((π β 1) β π₯ β§ βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯)} |
8 | 6, 7 | elrab2 3649 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (π β π« (1...(π β 1)) β§ ((π β 1) β π β§ βπ¦ β π ((π¦β(π β 2)) mod π) β π))) |
9 | 2, 8 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β (π β π« (1...(π β 1)) β§ ((π β 1) β π β§ βπ¦ β π ((π¦β(π β 2)) mod π) β π))) |
10 | 9 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β ((π β 1) β π β§ βπ¦ β π ((π¦β(π β 2)) mod π) β π)) |
11 | 10 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (π β 1) β π) |
12 | 11 | snssd 4770 |
. . . . . . . . . 10
β’ (π β {(π β 1)} β π) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β {(π β 1)}) β {(π β 1)} β π) |
14 | 1, 13 | eqssd 3962 |
. . . . . . . 8
β’ ((π β§ π β {(π β 1)}) β π = {(π β 1)}) |
15 | 14 | reseq2d 5938 |
. . . . . . 7
β’ ((π β§ π β {(π β 1)}) β ( I βΎ π) = ( I βΎ {(π β 1)})) |
16 | | mptresid 6005 |
. . . . . . 7
β’ ( I
βΎ {(π β 1)}) =
(π§ β {(π β 1)} β¦ π§) |
17 | 15, 16 | eqtrdi 2789 |
. . . . . 6
β’ ((π β§ π β {(π β 1)}) β ( I βΎ π) = (π§ β {(π β 1)} β¦ π§)) |
18 | 17 | oveq2d 7374 |
. . . . 5
β’ ((π β§ π β {(π β 1)}) β (π Ξ£g ( I βΎ
π)) = (π Ξ£g (π§ β {(π β 1)} β¦ π§))) |
19 | 18 | oveq1d 7373 |
. . . 4
β’ ((π β§ π β {(π β 1)}) β ((π Ξ£g ( I βΎ
π)) mod π) = ((π Ξ£g (π§ β {(π β 1)} β¦ π§)) mod π)) |
20 | | wilthlem2.p |
. . . . . . . . . . . 12
β’ (π β π β β) |
21 | | prmnn 16555 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β β) |
23 | 22 | nncnd 12174 |
. . . . . . . . . 10
β’ (π β π β β) |
24 | | ax-1cn 11114 |
. . . . . . . . . 10
β’ 1 β
β |
25 | | negsub 11454 |
. . . . . . . . . 10
β’ ((π β β β§ 1 β
β) β (π + -1) =
(π β
1)) |
26 | 23, 24, 25 | sylancl 587 |
. . . . . . . . 9
β’ (π β (π + -1) = (π β 1)) |
27 | | neg1cn 12272 |
. . . . . . . . . 10
β’ -1 β
β |
28 | | addcom 11346 |
. . . . . . . . . 10
β’ ((π β β β§ -1 β
β) β (π + -1) =
(-1 + π)) |
29 | 23, 27, 28 | sylancl 587 |
. . . . . . . . 9
β’ (π β (π + -1) = (-1 + π)) |
30 | 26, 29 | eqtr3d 2775 |
. . . . . . . 8
β’ (π β (π β 1) = (-1 + π)) |
31 | | cnring 20835 |
. . . . . . . . . 10
β’
βfld β Ring |
32 | | wilthlem.t |
. . . . . . . . . . 11
β’ π =
(mulGrpββfld) |
33 | 32 | ringmgp 19975 |
. . . . . . . . . 10
β’
(βfld β Ring β π β Mnd) |
34 | 31, 33 | mp1i 13 |
. . . . . . . . 9
β’ (π β π β Mnd) |
35 | | nnm1nn0 12459 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β0) |
36 | 22, 35 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β 1) β
β0) |
37 | 36 | nn0cnd 12480 |
. . . . . . . . 9
β’ (π β (π β 1) β β) |
38 | | cnfldbas 20816 |
. . . . . . . . . . 11
β’ β =
(Baseββfld) |
39 | 32, 38 | mgpbas 19907 |
. . . . . . . . . 10
β’ β =
(Baseβπ) |
40 | | id 22 |
. . . . . . . . . 10
β’ (π§ = (π β 1) β π§ = (π β 1)) |
41 | 39, 40 | gsumsn 19736 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π β 1) β β β§
(π β 1) β
β) β (π
Ξ£g (π§ β {(π β 1)} β¦ π§)) = (π β 1)) |
42 | 34, 37, 37, 41 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π Ξ£g (π§ β {(π β 1)} β¦ π§)) = (π β 1)) |
43 | 23 | mulid2d 11178 |
. . . . . . . . 9
β’ (π β (1 Β· π) = π) |
44 | 43 | oveq2d 7374 |
. . . . . . . 8
β’ (π β (-1 + (1 Β· π)) = (-1 + π)) |
45 | 30, 42, 44 | 3eqtr4d 2783 |
. . . . . . 7
β’ (π β (π Ξ£g (π§ β {(π β 1)} β¦ π§)) = (-1 + (1 Β· π))) |
46 | 45 | oveq1d 7373 |
. . . . . 6
β’ (π β ((π Ξ£g (π§ β {(π β 1)} β¦ π§)) mod π) = ((-1 + (1 Β· π)) mod π)) |
47 | | neg1rr 12273 |
. . . . . . . 8
β’ -1 β
β |
48 | 47 | a1i 11 |
. . . . . . 7
β’ (π β -1 β
β) |
49 | 22 | nnrpd 12960 |
. . . . . . 7
β’ (π β π β
β+) |
50 | | 1zzd 12539 |
. . . . . . 7
β’ (π β 1 β
β€) |
51 | | modcyc 13817 |
. . . . . . 7
β’ ((-1
β β β§ π
β β+ β§ 1 β β€) β ((-1 + (1 Β·
π)) mod π) = (-1 mod π)) |
52 | 48, 49, 50, 51 | syl3anc 1372 |
. . . . . 6
β’ (π β ((-1 + (1 Β· π)) mod π) = (-1 mod π)) |
53 | 46, 52 | eqtrd 2773 |
. . . . 5
β’ (π β ((π Ξ£g (π§ β {(π β 1)} β¦ π§)) mod π) = (-1 mod π)) |
54 | 53 | adantr 482 |
. . . 4
β’ ((π β§ π β {(π β 1)}) β ((π Ξ£g (π§ β {(π β 1)} β¦ π§)) mod π) = (-1 mod π)) |
55 | 19, 54 | eqtrd 2773 |
. . 3
β’ ((π β§ π β {(π β 1)}) β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π)) |
56 | 55 | ex 414 |
. 2
β’ (π β (π β {(π β 1)} β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π))) |
57 | | nss 4007 |
. . 3
β’ (Β¬
π β {(π β 1)} β βπ§(π§ β π β§ Β¬ π§ β {(π β 1)})) |
58 | | cnfld1 20838 |
. . . . . . . . . 10
β’ 1 =
(1rββfld) |
59 | 32, 58 | ringidval 19920 |
. . . . . . . . 9
β’ 1 =
(0gβπ) |
60 | | cnfldmul 20818 |
. . . . . . . . . 10
β’ Β·
= (.rββfld) |
61 | 32, 60 | mgpplusg 19905 |
. . . . . . . . 9
β’ Β·
= (+gβπ) |
62 | | cncrng 20834 |
. . . . . . . . . . 11
β’
βfld β CRing |
63 | 32 | crngmgp 19977 |
. . . . . . . . . . 11
β’
(βfld β CRing β π β CMnd) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
β’ π β CMnd |
65 | 64 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β CMnd) |
66 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β π΄) |
67 | | f1oi 6823 |
. . . . . . . . . . . 12
β’ ( I
βΎ π):πβ1-1-ontoβπ |
68 | | f1of 6785 |
. . . . . . . . . . . 12
β’ (( I
βΎ π):πβ1-1-ontoβπ β ( I βΎ π):πβΆπ) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . 11
β’ ( I
βΎ π):πβΆπ |
70 | 9 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β π β π« (1...(π β 1))) |
71 | 70 | elpwid 4570 |
. . . . . . . . . . . . 13
β’ (π β π β (1...(π β 1))) |
72 | | fzssz 13449 |
. . . . . . . . . . . . 13
β’
(1...(π β 1))
β β€ |
73 | 71, 72 | sstrdi 3957 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
74 | | zsscn 12512 |
. . . . . . . . . . . 12
β’ β€
β β |
75 | 73, 74 | sstrdi 3957 |
. . . . . . . . . . 11
β’ (π β π β β) |
76 | | fss 6686 |
. . . . . . . . . . 11
β’ ((( I
βΎ π):πβΆπ β§ π β β) β ( I βΎ π):πβΆβ) |
77 | 69, 75, 76 | sylancr 588 |
. . . . . . . . . 10
β’ (π β ( I βΎ π):πβΆβ) |
78 | 77 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ( I βΎ π):πβΆβ) |
79 | | fzfi 13883 |
. . . . . . . . . . . 12
β’
(1...(π β 1))
β Fin |
80 | | ssfi 9120 |
. . . . . . . . . . . 12
β’
(((1...(π β
1)) β Fin β§ π
β (1...(π β
1))) β π β
Fin) |
81 | 79, 71, 80 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β π β Fin) |
82 | | 1ex 11156 |
. . . . . . . . . . . 12
β’ 1 β
V |
83 | 82 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 1 β
V) |
84 | 77, 81, 83 | fdmfifsupp 9320 |
. . . . . . . . . 10
β’ (π β ( I βΎ π) finSupp 1) |
85 | 84 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ( I βΎ π) finSupp 1) |
86 | | disjdif 4432 |
. . . . . . . . . 10
β’ ({π§, ((π§β(π β 2)) mod π)} β© (π β {π§, ((π§β(π β 2)) mod π)})) = β
|
87 | 86 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ({π§, ((π§β(π β 2)) mod π)} β© (π β {π§, ((π§β(π β 2)) mod π)})) = β
) |
88 | | undif2 4437 |
. . . . . . . . . 10
β’ ({π§, ((π§β(π β 2)) mod π)} βͺ (π β {π§, ((π§β(π β 2)) mod π)})) = ({π§, ((π§β(π β 2)) mod π)} βͺ π) |
89 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π§ β π) |
90 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π§ β (π¦β(π β 2)) = (π§β(π β 2))) |
91 | 90 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π¦ = π§ β ((π¦β(π β 2)) mod π) = ((π§β(π β 2)) mod π)) |
92 | 91 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (((π¦β(π β 2)) mod π) β π β ((π§β(π β 2)) mod π) β π)) |
93 | 10 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β βπ¦ β π ((π¦β(π β 2)) mod π) β π) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β βπ¦ β π ((π¦β(π β 2)) mod π) β π) |
95 | 92, 94, 89 | rspcdva 3581 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π§β(π β 2)) mod π) β π) |
96 | 89, 95 | prssd 4783 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β {π§, ((π§β(π β 2)) mod π)} β π) |
97 | | ssequn1 4141 |
. . . . . . . . . . 11
β’ ({π§, ((π§β(π β 2)) mod π)} β π β ({π§, ((π§β(π β 2)) mod π)} βͺ π) = π) |
98 | 96, 97 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ({π§, ((π§β(π β 2)) mod π)} βͺ π) = π) |
99 | 88, 98 | eqtr2id 2786 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π = ({π§, ((π§β(π β 2)) mod π)} βͺ (π β {π§, ((π§β(π β 2)) mod π)}))) |
100 | 39, 59, 61, 65, 66, 78, 85, 87, 99 | gsumsplit 19710 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g ( I βΎ
π)) = ((π Ξ£g (( I βΎ
π) βΎ {π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g (( I βΎ
π) βΎ (π β {π§, ((π§β(π β 2)) mod π)}))))) |
101 | 96 | resabs1d 5969 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (( I βΎ π) βΎ {π§, ((π§β(π β 2)) mod π)}) = ( I βΎ {π§, ((π§β(π β 2)) mod π)})) |
102 | 101 | oveq2d 7374 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g (( I βΎ
π) βΎ {π§, ((π§β(π β 2)) mod π)})) = (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)}))) |
103 | | difss 4092 |
. . . . . . . . . . . 12
β’ (π β {π§, ((π§β(π β 2)) mod π)}) β π |
104 | | resabs1 5968 |
. . . . . . . . . . . 12
β’ ((π β {π§, ((π§β(π β 2)) mod π)}) β π β (( I βΎ π) βΎ (π β {π§, ((π§β(π β 2)) mod π)})) = ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)}))) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . . . 11
β’ (( I
βΎ π) βΎ (π β {π§, ((π§β(π β 2)) mod π)})) = ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)})) |
106 | 105 | oveq2i 7369 |
. . . . . . . . . 10
β’ (π Ξ£g (( I
βΎ π) βΎ (π β {π§, ((π§β(π β 2)) mod π)}))) = (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) |
107 | 106 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g (( I βΎ
π) βΎ (π β {π§, ((π§β(π β 2)) mod π)}))) = (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) |
108 | 102, 107 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Ξ£g (( I βΎ
π) βΎ {π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g (( I βΎ
π) βΎ (π β {π§, ((π§β(π β 2)) mod π)})))) = ((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))))) |
109 | 100, 108 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g ( I βΎ
π)) = ((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))))) |
110 | 109 | oveq1d 7373 |
. . . . . 6
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Ξ£g ( I βΎ
π)) mod π) = (((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) mod π)) |
111 | | prfi 9269 |
. . . . . . . . . 10
β’ {π§, ((π§β(π β 2)) mod π)} β Fin |
112 | 111 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β {π§, ((π§β(π β 2)) mod π)} β Fin) |
113 | | zsubrg 20866 |
. . . . . . . . . 10
β’ β€
β (SubRingββfld) |
114 | 32 | subrgsubm 20249 |
. . . . . . . . . 10
β’ (β€
β (SubRingββfld) β β€ β
(SubMndβπ)) |
115 | 113, 114 | mp1i 13 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β β€ β
(SubMndβπ)) |
116 | | f1oi 6823 |
. . . . . . . . . . 11
β’ ( I
βΎ {π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}β1-1-ontoβ{π§, ((π§β(π β 2)) mod π)} |
117 | | f1of 6785 |
. . . . . . . . . . 11
β’ (( I
βΎ {π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}β1-1-ontoβ{π§, ((π§β(π β 2)) mod π)} β ( I βΎ {π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}βΆ{π§, ((π§β(π β 2)) mod π)}) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . 10
β’ ( I
βΎ {π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}βΆ{π§, ((π§β(π β 2)) mod π)} |
119 | 73 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β β€) |
120 | 96, 119 | sstrd 3955 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β {π§, ((π§β(π β 2)) mod π)} β β€) |
121 | | fss 6686 |
. . . . . . . . . 10
β’ ((( I
βΎ {π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}βΆ{π§, ((π§β(π β 2)) mod π)} β§ {π§, ((π§β(π β 2)) mod π)} β β€) β ( I βΎ
{π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}βΆβ€) |
122 | 118, 120,
121 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ( I βΎ {π§, ((π§β(π β 2)) mod π)}):{π§, ((π§β(π β 2)) mod π)}βΆβ€) |
123 | 82 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β 1 β
V) |
124 | 122, 112,
123 | fdmfifsupp 9320 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ( I βΎ {π§, ((π§β(π β 2)) mod π)}) finSupp 1) |
125 | 59, 65, 112, 115, 122, 124 | gsumsubmcl 19701 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) β β€) |
126 | 125 | zred 12612 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) β β) |
127 | | 1red 11161 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β 1 β
β) |
128 | 71 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β (1...(π β 1))) |
129 | 128 | ssdifssd 4103 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β {π§, ((π§β(π β 2)) mod π)}) β (1...(π β 1))) |
130 | | ssfi 9120 |
. . . . . . . . 9
β’
(((1...(π β
1)) β Fin β§ (π
β {π§, ((π§β(π β 2)) mod π)}) β (1...(π β 1))) β (π β {π§, ((π§β(π β 2)) mod π)}) β Fin) |
131 | 79, 129, 130 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β {π§, ((π§β(π β 2)) mod π)}) β Fin) |
132 | | f1oi 6823 |
. . . . . . . . . 10
β’ ( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})β1-1-ontoβ(π β {π§, ((π§β(π β 2)) mod π)}) |
133 | | f1of 6785 |
. . . . . . . . . 10
β’ (( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})β1-1-ontoβ(π β {π§, ((π§β(π β 2)) mod π)}) β ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})βΆ(π β {π§, ((π§β(π β 2)) mod π)})) |
134 | 132, 133 | ax-mp 5 |
. . . . . . . . 9
β’ ( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})βΆ(π β {π§, ((π§β(π β 2)) mod π)}) |
135 | 119 | ssdifssd 4103 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β {π§, ((π§β(π β 2)) mod π)}) β β€) |
136 | | fss 6686 |
. . . . . . . . 9
β’ ((( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})βΆ(π β {π§, ((π§β(π β 2)) mod π)}) β§ (π β {π§, ((π§β(π β 2)) mod π)}) β β€) β ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})βΆβ€) |
137 | 134, 135,
136 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)})):(π β {π§, ((π§β(π β 2)) mod π)})βΆβ€) |
138 | 137, 131,
123 | fdmfifsupp 9320 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)})) finSupp 1) |
139 | 59, 65, 131, 115, 137, 138 | gsumsubmcl 19701 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) β β€) |
140 | 49 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β
β+) |
141 | 34 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β Mnd) |
142 | 75 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β β) |
143 | 142, 89 | sseldd 3946 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π§ β β) |
144 | | id 22 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β π€ = π§) |
145 | 39, 144 | gsumsn 19736 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ π§ β β β§ π§ β β) β (π Ξ£g
(π€ β {π§} β¦ π€)) = π§) |
146 | 141, 143,
143, 145 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g (π€ β {π§} β¦ π€)) = π§) |
147 | 146 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β (π Ξ£g (π€ β {π§} β¦ π€)) = π§) |
148 | | mptresid 6005 |
. . . . . . . . . . . 12
β’ ( I
βΎ {π§}) = (π€ β {π§} β¦ π€) |
149 | | dfsn2 4600 |
. . . . . . . . . . . . . 14
β’ {π§} = {π§, π§} |
150 | | animorrl 980 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β (π§ = 1 β¨ π§ = (π β 1))) |
151 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β β) |
152 | 128, 89 | sseldd 3946 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π§ β (1...(π β 1))) |
153 | | wilthlem1 26433 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π§ β (1...(π β 1))) β (π§ = ((π§β(π β 2)) mod π) β (π§ = 1 β¨ π§ = (π β 1)))) |
154 | 151, 152,
153 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π§ = ((π§β(π β 2)) mod π) β (π§ = 1 β¨ π§ = (π β 1)))) |
155 | 154 | biimpar 479 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ (π§ = 1 β¨ π§ = (π β 1))) β π§ = ((π§β(π β 2)) mod π)) |
156 | 150, 155 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β π§ = ((π§β(π β 2)) mod π)) |
157 | 156 | preq2d 4702 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β {π§, π§} = {π§, ((π§β(π β 2)) mod π)}) |
158 | 149, 157 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β {π§} = {π§, ((π§β(π β 2)) mod π)}) |
159 | 158 | reseq2d 5938 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β ( I βΎ {π§}) = ( I βΎ {π§, ((π§β(π β 2)) mod π)})) |
160 | 148, 159 | eqtr3id 2787 |
. . . . . . . . . . 11
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β (π€ β {π§} β¦ π€) = ( I βΎ {π§, ((π§β(π β 2)) mod π)})) |
161 | 160 | oveq2d 7374 |
. . . . . . . . . 10
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β (π Ξ£g (π€ β {π§} β¦ π€)) = (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)}))) |
162 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β π§ = 1) |
163 | 147, 161,
162 | 3eqtr3d 2781 |
. . . . . . . . 9
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) = 1) |
164 | 163 | oveq1d 7373 |
. . . . . . . 8
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ = 1) β ((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) mod π) = (1 mod π)) |
165 | | df-pr 4590 |
. . . . . . . . . . . . . . 15
β’ {π§, ((π§β(π β 2)) mod π)} = ({π§} βͺ {((π§β(π β 2)) mod π)}) |
166 | 165 | reseq2i 5935 |
. . . . . . . . . . . . . 14
β’ ( I
βΎ {π§, ((π§β(π β 2)) mod π)}) = ( I βΎ ({π§} βͺ {((π§β(π β 2)) mod π)})) |
167 | | mptresid 6005 |
. . . . . . . . . . . . . 14
β’ ( I
βΎ ({π§} βͺ {((π§β(π β 2)) mod π)})) = (π€ β ({π§} βͺ {((π§β(π β 2)) mod π)}) β¦ π€) |
168 | 166, 167 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ ( I
βΎ {π§, ((π§β(π β 2)) mod π)}) = (π€ β ({π§} βͺ {((π§β(π β 2)) mod π)}) β¦ π€) |
169 | 168 | oveq2i 7369 |
. . . . . . . . . . . 12
β’ (π Ξ£g ( I
βΎ {π§, ((π§β(π β 2)) mod π)})) = (π Ξ£g (π€ β ({π§} βͺ {((π§β(π β 2)) mod π)}) β¦ π€)) |
170 | 64 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β π β CMnd) |
171 | | snfi 8991 |
. . . . . . . . . . . . . 14
β’ {π§} β Fin |
172 | 171 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β {π§} β Fin) |
173 | | elsni 4604 |
. . . . . . . . . . . . . . . 16
β’ (π€ β {π§} β π€ = π§) |
174 | 173 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π€ β {π§}) β π€ = π§) |
175 | 143 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π€ β {π§}) β π§ β β) |
176 | 174, 175 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π€ β {π§}) β π€ β β) |
177 | 176 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β§ π€ β {π§}) β π€ β β) |
178 | 142, 95 | sseldd 3946 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π§β(π β 2)) mod π) β β) |
179 | 178 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β ((π§β(π β 2)) mod π) β β) |
180 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ π§ β {(π β 1)}) |
181 | | velsn 4603 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {(π β 1)} β π§ = (π β 1)) |
182 | 180, 181 | sylnib 328 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ π§ = (π β 1)) |
183 | | biorf 936 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π§ = (π β 1) β (π§ = 1 β (π§ = (π β 1) β¨ π§ = 1))) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π§ = 1 β (π§ = (π β 1) β¨ π§ = 1))) |
185 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§β(π β 2)) mod π) β V |
186 | 185 | elsn 4602 |
. . . . . . . . . . . . . . . . . 18
β’ (((π§β(π β 2)) mod π) β {π§} β ((π§β(π β 2)) mod π) = π§) |
187 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . 18
β’ (((π§β(π β 2)) mod π) = π§ β π§ = ((π§β(π β 2)) mod π)) |
188 | 186, 187 | bitri 275 |
. . . . . . . . . . . . . . . . 17
β’ (((π§β(π β 2)) mod π) β {π§} β π§ = ((π§β(π β 2)) mod π)) |
189 | | orcom 869 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ = (π β 1) β¨ π§ = 1) β (π§ = 1 β¨ π§ = (π β 1))) |
190 | 154, 188,
189 | 3bitr4g 314 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (((π§β(π β 2)) mod π) β {π§} β (π§ = (π β 1) β¨ π§ = 1))) |
191 | 184, 190 | bitr4d 282 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π§ = 1 β ((π§β(π β 2)) mod π) β {π§})) |
192 | 191 | necon3abid 2977 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π§ β 1 β Β¬ ((π§β(π β 2)) mod π) β {π§})) |
193 | 192 | biimpa 478 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β Β¬ ((π§β(π β 2)) mod π) β {π§}) |
194 | | id 22 |
. . . . . . . . . . . . 13
β’ (π€ = ((π§β(π β 2)) mod π) β π€ = ((π§β(π β 2)) mod π)) |
195 | 39, 61, 170, 172, 177, 179, 193, 179, 194 | gsumunsn 19742 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β (π Ξ£g (π€ β ({π§} βͺ {((π§β(π β 2)) mod π)}) β¦ π€)) = ((π Ξ£g (π€ β {π§} β¦ π€)) Β· ((π§β(π β 2)) mod π))) |
196 | 169, 195 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) = ((π Ξ£g (π€ β {π§} β¦ π€)) Β· ((π§β(π β 2)) mod π))) |
197 | 146 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β (π Ξ£g (π€ β {π§} β¦ π€)) = π§) |
198 | 197 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β ((π Ξ£g (π€ β {π§} β¦ π€)) Β· ((π§β(π β 2)) mod π)) = (π§ Β· ((π§β(π β 2)) mod π))) |
199 | 196, 198 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β (π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) = (π§ Β· ((π§β(π β 2)) mod π))) |
200 | 199 | oveq1d 7373 |
. . . . . . . . 9
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β ((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) mod π) = ((π§ Β· ((π§β(π β 2)) mod π)) mod π)) |
201 | 152 | elfzelzd 13448 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π§ β β€) |
202 | 22 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β β) |
203 | | fzm1ndvds 16209 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π§ β (1...(π β 1))) β Β¬ π β₯ π§) |
204 | 202, 152,
203 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ π β₯ π§) |
205 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ ((π§β(π β 2)) mod π) = ((π§β(π β 2)) mod π) |
206 | 205 | prmdiv 16662 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π§ β β€ β§ Β¬
π β₯ π§) β (((π§β(π β 2)) mod π) β (1...(π β 1)) β§ π β₯ ((π§ Β· ((π§β(π β 2)) mod π)) β 1))) |
207 | 151, 201,
204, 206 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (((π§β(π β 2)) mod π) β (1...(π β 1)) β§ π β₯ ((π§ Β· ((π§β(π β 2)) mod π)) β 1))) |
208 | 207 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β₯ ((π§ Β· ((π§β(π β 2)) mod π)) β 1)) |
209 | | elfznn 13476 |
. . . . . . . . . . . . . . 15
β’ (π§ β (1...(π β 1)) β π§ β β) |
210 | 152, 209 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π§ β β) |
211 | 128, 95 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π§β(π β 2)) mod π) β (1...(π β 1))) |
212 | | elfznn 13476 |
. . . . . . . . . . . . . . 15
β’ (((π§β(π β 2)) mod π) β (1...(π β 1)) β ((π§β(π β 2)) mod π) β β) |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π§β(π β 2)) mod π) β β) |
214 | 210, 213 | nnmulcld 12211 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π§ Β· ((π§β(π β 2)) mod π)) β β) |
215 | 214 | nnzd 12531 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π§ Β· ((π§β(π β 2)) mod π)) β β€) |
216 | | 1zzd 12539 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β 1 β
β€) |
217 | | moddvds 16152 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π§ Β· ((π§β(π β 2)) mod π)) β β€ β§ 1 β β€)
β (((π§ Β·
((π§β(π β 2)) mod π)) mod π) = (1 mod π) β π β₯ ((π§ Β· ((π§β(π β 2)) mod π)) β 1))) |
218 | 202, 215,
216, 217 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (((π§ Β· ((π§β(π β 2)) mod π)) mod π) = (1 mod π) β π β₯ ((π§ Β· ((π§β(π β 2)) mod π)) β 1))) |
219 | 208, 218 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π§ Β· ((π§β(π β 2)) mod π)) mod π) = (1 mod π)) |
220 | 219 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β ((π§ Β· ((π§β(π β 2)) mod π)) mod π) = (1 mod π)) |
221 | 200, 220 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π§ β 1) β ((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) mod π) = (1 mod π)) |
222 | 164, 221 | pm2.61dane 3029 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) mod π) = (1 mod π)) |
223 | | modmul1 13835 |
. . . . . . 7
β’ ((((π Ξ£g ( I
βΎ {π§, ((π§β(π β 2)) mod π)})) β β β§ 1 β β)
β§ ((π
Ξ£g ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)}))) β β€ β§ π β β+) β§ ((π Ξ£g ( I
βΎ {π§, ((π§β(π β 2)) mod π)})) mod π) = (1 mod π)) β (((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) mod π) = ((1 Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) mod π)) |
224 | 126, 127,
139, 140, 222, 223 | syl221anc 1382 |
. . . . . 6
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (((π Ξ£g ( I βΎ
{π§, ((π§β(π β 2)) mod π)})) Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) mod π) = ((1 Β· (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) mod π)) |
225 | 139 | zcnd 12613 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) β β) |
226 | 225 | mulid2d 11178 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (1 Β· (π Ξ£g ( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})))) = (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) |
227 | 226 | oveq1d 7373 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((1 Β· (π Ξ£g ( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})))) mod π) = ((π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) mod π)) |
228 | | sseqin2 4176 |
. . . . . . . . . . 11
β’ ({π§, ((π§β(π β 2)) mod π)} β π β (π β© {π§, ((π§β(π β 2)) mod π)}) = {π§, ((π§β(π β 2)) mod π)}) |
229 | 96, 228 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β© {π§, ((π§β(π β 2)) mod π)}) = {π§, ((π§β(π β 2)) mod π)}) |
230 | | vex 3448 |
. . . . . . . . . . . 12
β’ π§ β V |
231 | 230 | prnz 4739 |
. . . . . . . . . . 11
β’ {π§, ((π§β(π β 2)) mod π)} β β
|
232 | 231 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β {π§, ((π§β(π β 2)) mod π)} β β
) |
233 | 229, 232 | eqnetrd 3008 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β© {π§, ((π§β(π β 2)) mod π)}) β β
) |
234 | | disj4 4419 |
. . . . . . . . . 10
β’ ((π β© {π§, ((π§β(π β 2)) mod π)}) = β
β Β¬ (π β {π§, ((π§β(π β 2)) mod π)}) β π) |
235 | 234 | necon2abii 2991 |
. . . . . . . . 9
β’ ((π β {π§, ((π§β(π β 2)) mod π)}) β π β (π β© {π§, ((π§β(π β 2)) mod π)}) β β
) |
236 | 233, 235 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β {π§, ((π§β(π β 2)) mod π)}) β π) |
237 | | psseq1 4048 |
. . . . . . . . . 10
β’ (π = (π β {π§, ((π§β(π β 2)) mod π)}) β (π β π β (π β {π§, ((π§β(π β 2)) mod π)}) β π)) |
238 | | reseq2 5933 |
. . . . . . . . . . . . 13
β’ (π = (π β {π§, ((π§β(π β 2)) mod π)}) β ( I βΎ π ) = ( I βΎ (π β {π§, ((π§β(π β 2)) mod π)}))) |
239 | 238 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = (π β {π§, ((π§β(π β 2)) mod π)}) β (π Ξ£g ( I βΎ
π )) = (π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)})))) |
240 | 239 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π = (π β {π§, ((π§β(π β 2)) mod π)}) β ((π Ξ£g ( I βΎ
π )) mod π) = ((π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) mod π)) |
241 | 240 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (π = (π β {π§, ((π§β(π β 2)) mod π)}) β (((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π) β ((π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) mod π) = (-1 mod π))) |
242 | 237, 241 | imbi12d 345 |
. . . . . . . . 9
β’ (π = (π β {π§, ((π§β(π β 2)) mod π)}) β ((π β π β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π)) β ((π β {π§, ((π§β(π β 2)) mod π)}) β π β ((π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) mod π) = (-1 mod π)))) |
243 | | wilthlem2.r |
. . . . . . . . . 10
β’ (π β βπ β π΄ (π β π β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) |
244 | 243 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β βπ β π΄ (π β π β ((π Ξ£g ( I βΎ
π )) mod π) = (-1 mod π))) |
245 | | ovex 7391 |
. . . . . . . . . . . 12
β’
(1...(π β 1))
β V |
246 | 245 | elpw2 5303 |
. . . . . . . . . . 11
β’ ((π β {π§, ((π§β(π β 2)) mod π)}) β π« (1...(π β 1)) β (π β {π§, ((π§β(π β 2)) mod π)}) β (1...(π β 1))) |
247 | 129, 246 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β {π§, ((π§β(π β 2)) mod π)}) β π« (1...(π β 1))) |
248 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β π) |
249 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π β 1) β (π β 1) = π§) |
250 | 181, 249 | bitri 275 |
. . . . . . . . . . . . . . 15
β’ (π§ β {(π β 1)} β (π β 1) = π§) |
251 | 180, 250 | sylnib 328 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ (π β 1) = π§) |
252 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ ((π β 1) = ((π§β(π β 2)) mod π) β ((π β 1)β(π β 2)) = (((π§β(π β 2)) mod π)β(π β 2))) |
253 | 252 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) = ((π§β(π β 2)) mod π) β (((π β 1)β(π β 2)) mod π) = ((((π§β(π β 2)) mod π)β(π β 2)) mod π)) |
254 | 202, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β
β0) |
255 | | nn0uz 12810 |
. . . . . . . . . . . . . . . . . . . 20
β’
β0 = (β€β₯β0) |
256 | 254, 255 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β
(β€β₯β0)) |
257 | | eluzfz2 13455 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β 1) β
(β€β₯β0) β (π β 1) β (0...(π β 1))) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β (0...(π β 1))) |
259 | | prmz 16556 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β€) |
260 | 151, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β β€) |
261 | 119, 248 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β β€) |
262 | | 1z 12538 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
β€ |
263 | | zsubcl 12550 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β 1) β β€ β§
1 β β€) β ((π β 1) β 1) β
β€) |
264 | 261, 262,
263 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) β 1) β
β€) |
265 | | dvdsmul1 16165 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ ((π β 1) β 1) β
β€) β π β₯
(π Β· ((π β 1) β
1))) |
266 | 260, 264,
265 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β₯ (π Β· ((π β 1) β 1))) |
267 | 202 | nncnd 12174 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β β) |
268 | 264 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) β 1) β
β) |
269 | 267, 268 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Β· ((π β 1) β 1)) β
β) |
270 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β 1 β
β) |
271 | 254 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β β) |
272 | 267, 270,
271 | subdird 11617 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) Β· (π β 1)) = ((π Β· (π β 1)) β (1 Β· (π β 1)))) |
273 | 267, 271 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Β· (π β 1)) β
β) |
274 | 273, 267,
270 | subsubd 11545 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Β· (π β 1)) β (π β 1)) = (((π Β· (π β 1)) β π) + 1)) |
275 | 271 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (1 Β· (π β 1)) = (π β 1)) |
276 | 275 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Β· (π β 1)) β (1 Β· (π β 1))) = ((π Β· (π β 1)) β (π β 1))) |
277 | 267, 271 | muls1d 11620 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π Β· ((π β 1) β 1)) = ((π Β· (π β 1)) β π)) |
278 | 277 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Β· ((π β 1) β 1)) + 1) = (((π Β· (π β 1)) β π) + 1)) |
279 | 274, 276,
278 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Β· (π β 1)) β (1 Β· (π β 1))) = ((π Β· ((π β 1) β 1)) +
1)) |
280 | 272, 279 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) Β· (π β 1)) = ((π Β· ((π β 1) β 1)) +
1)) |
281 | 269, 270,
280 | mvrraddd 11572 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (((π β 1) Β· (π β 1)) β 1) = (π Β· ((π β 1) β 1))) |
282 | 266, 281 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π β₯ (((π β 1) Β· (π β 1)) β 1)) |
283 | 128, 248 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β (1...(π β 1))) |
284 | | fzm1ndvds 16209 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (π β 1) β (1...(π β 1))) β Β¬ π β₯ (π β 1)) |
285 | 202, 283,
284 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ π β₯ (π β 1)) |
286 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β 1)β(π β 2)) mod π) = (((π β 1)β(π β 2)) mod π) |
287 | 286 | prmdiveq 16663 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π β 1) β β€ β§
Β¬ π β₯ (π β 1)) β (((π β 1) β (0...(π β 1)) β§ π β₯ (((π β 1) Β· (π β 1)) β 1)) β (π β 1) = (((π β 1)β(π β 2)) mod π))) |
288 | 151, 261,
285, 287 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (((π β 1) β (0...(π β 1)) β§ π β₯ (((π β 1) Β· (π β 1)) β 1)) β (π β 1) = (((π β 1)β(π β 2)) mod π))) |
289 | 258, 282,
288 | mpbi2and 711 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) = (((π β 1)β(π β 2)) mod π)) |
290 | 205 | prmdivdiv 16664 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π§ β (1...(π β 1))) β π§ = ((((π§β(π β 2)) mod π)β(π β 2)) mod π)) |
291 | 151, 152,
290 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β π§ = ((((π§β(π β 2)) mod π)β(π β 2)) mod π)) |
292 | 289, 291 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) = π§ β (((π β 1)β(π β 2)) mod π) = ((((π§β(π β 2)) mod π)β(π β 2)) mod π))) |
293 | 253, 292 | syl5ibr 246 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) = ((π§β(π β 2)) mod π) β (π β 1) = π§)) |
294 | 251, 293 | mtod 197 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ (π β 1) = ((π§β(π β 2)) mod π)) |
295 | | ioran 983 |
. . . . . . . . . . . . . 14
β’ (Β¬
((π β 1) = π§ β¨ (π β 1) = ((π§β(π β 2)) mod π)) β (Β¬ (π β 1) = π§ β§ Β¬ (π β 1) = ((π§β(π β 2)) mod π))) |
296 | 251, 294,
295 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ ((π β 1) = π§ β¨ (π β 1) = ((π§β(π β 2)) mod π))) |
297 | | ovex 7391 |
. . . . . . . . . . . . . 14
β’ (π β 1) β
V |
298 | 297 | elpr 4610 |
. . . . . . . . . . . . 13
β’ ((π β 1) β {π§, ((π§β(π β 2)) mod π)} β ((π β 1) = π§ β¨ (π β 1) = ((π§β(π β 2)) mod π))) |
299 | 296, 298 | sylnibr 329 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β Β¬ (π β 1) β {π§, ((π§β(π β 2)) mod π)}) |
300 | 248, 299 | eldifd 3922 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β 1) β (π β {π§, ((π§β(π β 2)) mod π)})) |
301 | | eldifi 4087 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π β {π§, ((π§β(π β 2)) mod π)}) β π¦ β π) |
302 | 94 | r19.21bi 3233 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β ((π¦β(π β 2)) mod π) β π) |
303 | 301, 302 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β (π β {π§, ((π§β(π β 2)) mod π)})) β ((π¦β(π β 2)) mod π) β π) |
304 | | eldif 3921 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π β {π§, ((π§β(π β 2)) mod π)}) β (π¦ β π β§ Β¬ π¦ β {π§, ((π§β(π β 2)) mod π)})) |
305 | 151 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β π β β) |
306 | 128 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β π¦ β (1...(π β 1))) |
307 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦β(π β 2)) mod π) = ((π¦β(π β 2)) mod π) |
308 | 307 | prmdivdiv 16664 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π¦ β (1...(π β 1))) β π¦ = ((((π¦β(π β 2)) mod π)β(π β 2)) mod π)) |
309 | 305, 306,
308 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β π¦ = ((((π¦β(π β 2)) mod π)β(π β 2)) mod π)) |
310 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π¦β(π β 2)) mod π) = π§ β (((π¦β(π β 2)) mod π)β(π β 2)) = (π§β(π β 2))) |
311 | 310 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦β(π β 2)) mod π) = π§ β ((((π¦β(π β 2)) mod π)β(π β 2)) mod π) = ((π§β(π β 2)) mod π)) |
312 | 311 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦β(π β 2)) mod π) = π§ β (π¦ = ((((π¦β(π β 2)) mod π)β(π β 2)) mod π) β π¦ = ((π§β(π β 2)) mod π))) |
313 | 309, 312 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β (((π¦β(π β 2)) mod π) = π§ β π¦ = ((π§β(π β 2)) mod π))) |
314 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦β(π β 2)) mod π) = ((π§β(π β 2)) mod π) β (((π¦β(π β 2)) mod π)β(π β 2)) = (((π§β(π β 2)) mod π)β(π β 2))) |
315 | 314 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦β(π β 2)) mod π) = ((π§β(π β 2)) mod π) β ((((π¦β(π β 2)) mod π)β(π β 2)) mod π) = ((((π§β(π β 2)) mod π)β(π β 2)) mod π)) |
316 | 291 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β π§ = ((((π§β(π β 2)) mod π)β(π β 2)) mod π)) |
317 | 309, 316 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β (π¦ = π§ β ((((π¦β(π β 2)) mod π)β(π β 2)) mod π) = ((((π§β(π β 2)) mod π)β(π β 2)) mod π))) |
318 | 315, 317 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β (((π¦β(π β 2)) mod π) = ((π§β(π β 2)) mod π) β π¦ = π§)) |
319 | 313, 318 | orim12d 964 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β ((((π¦β(π β 2)) mod π) = π§ β¨ ((π¦β(π β 2)) mod π) = ((π§β(π β 2)) mod π)) β (π¦ = ((π§β(π β 2)) mod π) β¨ π¦ = π§))) |
320 | | ovex 7391 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦β(π β 2)) mod π) β V |
321 | 320 | elpr 4610 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦β(π β 2)) mod π) β {π§, ((π§β(π β 2)) mod π)} β (((π¦β(π β 2)) mod π) = π§ β¨ ((π¦β(π β 2)) mod π) = ((π§β(π β 2)) mod π))) |
322 | | vex 3448 |
. . . . . . . . . . . . . . . . . . 19
β’ π¦ β V |
323 | 322 | elpr 4610 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β {π§, ((π§β(π β 2)) mod π)} β (π¦ = π§ β¨ π¦ = ((π§β(π β 2)) mod π))) |
324 | | orcom 869 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ = π§ β¨ π¦ = ((π§β(π β 2)) mod π)) β (π¦ = ((π§β(π β 2)) mod π) β¨ π¦ = π§)) |
325 | 323, 324 | bitri 275 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β {π§, ((π§β(π β 2)) mod π)} β (π¦ = ((π§β(π β 2)) mod π) β¨ π¦ = π§)) |
326 | 319, 321,
325 | 3imtr4g 296 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β (((π¦β(π β 2)) mod π) β {π§, ((π§β(π β 2)) mod π)} β π¦ β {π§, ((π§β(π β 2)) mod π)})) |
327 | 326 | con3d 152 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β π) β (Β¬ π¦ β {π§, ((π§β(π β 2)) mod π)} β Β¬ ((π¦β(π β 2)) mod π) β {π§, ((π§β(π β 2)) mod π)})) |
328 | 327 | impr 456 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ (π¦ β π β§ Β¬ π¦ β {π§, ((π§β(π β 2)) mod π)})) β Β¬ ((π¦β(π β 2)) mod π) β {π§, ((π§β(π β 2)) mod π)}) |
329 | 304, 328 | sylan2b 595 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β (π β {π§, ((π§β(π β 2)) mod π)})) β Β¬ ((π¦β(π β 2)) mod π) β {π§, ((π§β(π β 2)) mod π)}) |
330 | 303, 329 | eldifd 3922 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β§ π¦ β (π β {π§, ((π§β(π β 2)) mod π)})) β ((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)})) |
331 | 330 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β βπ¦ β (π β {π§, ((π§β(π β 2)) mod π)})((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)})) |
332 | 300, 331 | jca 513 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β 1) β (π β {π§, ((π§β(π β 2)) mod π)}) β§ βπ¦ β (π β {π§, ((π§β(π β 2)) mod π)})((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)}))) |
333 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π₯ = (π β {π§, ((π§β(π β 2)) mod π)}) β ((π β 1) β π₯ β (π β 1) β (π β {π§, ((π§β(π β 2)) mod π)}))) |
334 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (π₯ = (π β {π§, ((π§β(π β 2)) mod π)}) β (((π¦β(π β 2)) mod π) β π₯ β ((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)}))) |
335 | 334 | raleqbi1dv 3306 |
. . . . . . . . . . . 12
β’ (π₯ = (π β {π§, ((π§β(π β 2)) mod π)}) β (βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯ β βπ¦ β (π β {π§, ((π§β(π β 2)) mod π)})((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)}))) |
336 | 333, 335 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π₯ = (π β {π§, ((π§β(π β 2)) mod π)}) β (((π β 1) β π₯ β§ βπ¦ β π₯ ((π¦β(π β 2)) mod π) β π₯) β ((π β 1) β (π β {π§, ((π§β(π β 2)) mod π)}) β§ βπ¦ β (π β {π§, ((π§β(π β 2)) mod π)})((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)})))) |
337 | 336, 7 | elrab2 3649 |
. . . . . . . . . 10
β’ ((π β {π§, ((π§β(π β 2)) mod π)}) β π΄ β ((π β {π§, ((π§β(π β 2)) mod π)}) β π« (1...(π β 1)) β§ ((π β 1) β (π β {π§, ((π§β(π β 2)) mod π)}) β§ βπ¦ β (π β {π§, ((π§β(π β 2)) mod π)})((π¦β(π β 2)) mod π) β (π β {π§, ((π§β(π β 2)) mod π)})))) |
338 | 247, 332,
337 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β (π β {π§, ((π§β(π β 2)) mod π)}) β π΄) |
339 | 242, 244,
338 | rspcdva 3581 |
. . . . . . . 8
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π β {π§, ((π§β(π β 2)) mod π)}) β π β ((π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) mod π) = (-1 mod π))) |
340 | 236, 339 | mpd 15 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Ξ£g ( I βΎ
(π β {π§, ((π§β(π β 2)) mod π)}))) mod π) = (-1 mod π)) |
341 | 227, 340 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((1 Β· (π Ξ£g ( I
βΎ (π β {π§, ((π§β(π β 2)) mod π)})))) mod π) = (-1 mod π)) |
342 | 110, 224,
341 | 3eqtrd 2777 |
. . . . 5
β’ ((π β§ (π§ β π β§ Β¬ π§ β {(π β 1)})) β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π)) |
343 | 342 | ex 414 |
. . . 4
β’ (π β ((π§ β π β§ Β¬ π§ β {(π β 1)}) β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π))) |
344 | 343 | exlimdv 1937 |
. . 3
β’ (π β (βπ§(π§ β π β§ Β¬ π§ β {(π β 1)}) β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π))) |
345 | 57, 344 | biimtrid 241 |
. 2
β’ (π β (Β¬ π β {(π β 1)} β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π))) |
346 | 56, 345 | pm2.61d 179 |
1
β’ (π β ((π Ξ£g ( I βΎ
π)) mod π) = (-1 mod π)) |