Step | Hyp | Ref
| Expression |
1 | | znchr.y |
. . . . 5
β’ π =
(β€/nβ€βπ) |
2 | 1 | zncrng 21100 |
. . . 4
β’ (π β β0
β π β
CRing) |
3 | 2 | adantr 482 |
. . 3
β’ ((π β β0
β§ π΄ β β€)
β π β
CRing) |
4 | | znunit.u |
. . . 4
β’ π = (Unitβπ) |
5 | | eqid 2733 |
. . . 4
β’
(1rβπ) = (1rβπ) |
6 | | eqid 2733 |
. . . 4
β’
(β₯rβπ) = (β₯rβπ) |
7 | 4, 5, 6 | crngunit 20192 |
. . 3
β’ (π β CRing β ((πΏβπ΄) β π β (πΏβπ΄)(β₯rβπ)(1rβπ))) |
8 | 3, 7 | syl 17 |
. 2
β’ ((π β β0
β§ π΄ β β€)
β ((πΏβπ΄) β π β (πΏβπ΄)(β₯rβπ)(1rβπ))) |
9 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
10 | | znunit.l |
. . . . . . 7
β’ πΏ = (β€RHomβπ) |
11 | 1, 9, 10 | znzrhfo 21103 |
. . . . . 6
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
12 | 11 | adantr 482 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€)
β πΏ:β€βontoβ(Baseβπ)) |
13 | | fof 6806 |
. . . . 5
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
14 | 12, 13 | syl 17 |
. . . 4
β’ ((π β β0
β§ π΄ β β€)
β πΏ:β€βΆ(Baseβπ)) |
15 | | ffvelcdm 7084 |
. . . 4
β’ ((πΏ:β€βΆ(Baseβπ) β§ π΄ β β€) β (πΏβπ΄) β (Baseβπ)) |
16 | 14, 15 | sylancom 589 |
. . 3
β’ ((π β β0
β§ π΄ β β€)
β (πΏβπ΄) β (Baseβπ)) |
17 | | eqid 2733 |
. . . 4
β’
(.rβπ) = (.rβπ) |
18 | 9, 6, 17 | dvdsr2 20177 |
. . 3
β’ ((πΏβπ΄) β (Baseβπ) β ((πΏβπ΄)(β₯rβπ)(1rβπ) β βπ₯ β (Baseβπ)(π₯(.rβπ)(πΏβπ΄)) = (1rβπ))) |
19 | 16, 18 | syl 17 |
. 2
β’ ((π β β0
β§ π΄ β β€)
β ((πΏβπ΄)(β₯rβπ)(1rβπ) β βπ₯ β (Baseβπ)(π₯(.rβπ)(πΏβπ΄)) = (1rβπ))) |
20 | | forn 6809 |
. . . . . 6
β’ (πΏ:β€βontoβ(Baseβπ) β ran πΏ = (Baseβπ)) |
21 | 12, 20 | syl 17 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€)
β ran πΏ =
(Baseβπ)) |
22 | 21 | rexeqdv 3327 |
. . . 4
β’ ((π β β0
β§ π΄ β β€)
β (βπ₯ β ran
πΏ(π₯(.rβπ)(πΏβπ΄)) = (1rβπ) β βπ₯ β (Baseβπ)(π₯(.rβπ)(πΏβπ΄)) = (1rβπ))) |
23 | | ffn 6718 |
. . . . 5
β’ (πΏ:β€βΆ(Baseβπ) β πΏ Fn β€) |
24 | | oveq1 7416 |
. . . . . . 7
β’ (π₯ = (πΏβπ) β (π₯(.rβπ)(πΏβπ΄)) = ((πΏβπ)(.rβπ)(πΏβπ΄))) |
25 | 24 | eqeq1d 2735 |
. . . . . 6
β’ (π₯ = (πΏβπ) β ((π₯(.rβπ)(πΏβπ΄)) = (1rβπ) β ((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ))) |
26 | 25 | rexrn 7089 |
. . . . 5
β’ (πΏ Fn β€ β (βπ₯ β ran πΏ(π₯(.rβπ)(πΏβπ΄)) = (1rβπ) β βπ β β€ ((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ))) |
27 | 14, 23, 26 | 3syl 18 |
. . . 4
β’ ((π β β0
β§ π΄ β β€)
β (βπ₯ β ran
πΏ(π₯(.rβπ)(πΏβπ΄)) = (1rβπ) β βπ β β€ ((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ))) |
28 | 22, 27 | bitr3d 281 |
. . 3
β’ ((π β β0
β§ π΄ β β€)
β (βπ₯ β
(Baseβπ)(π₯(.rβπ)(πΏβπ΄)) = (1rβπ) β βπ β β€ ((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ))) |
29 | | crngring 20068 |
. . . . . . . . . 10
β’ (π β CRing β π β Ring) |
30 | 3, 29 | syl 17 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β β€)
β π β
Ring) |
31 | 10 | zrhrhm 21061 |
. . . . . . . . 9
β’ (π β Ring β πΏ β (β€ring
RingHom π)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β β€)
β πΏ β
(β€ring RingHom π)) |
33 | 32 | adantr 482 |
. . . . . . 7
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β πΏ β
(β€ring RingHom π)) |
34 | | simpr 486 |
. . . . . . 7
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β π β
β€) |
35 | | simplr 768 |
. . . . . . 7
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β π΄ β
β€) |
36 | | zringbas 21023 |
. . . . . . . 8
β’ β€ =
(Baseββ€ring) |
37 | | zringmulr 21027 |
. . . . . . . 8
β’ Β·
= (.rββ€ring) |
38 | 36, 37, 17 | rhmmul 20264 |
. . . . . . 7
β’ ((πΏ β (β€ring
RingHom π) β§ π β β€ β§ π΄ β β€) β (πΏβ(π Β· π΄)) = ((πΏβπ)(.rβπ)(πΏβπ΄))) |
39 | 33, 34, 35, 38 | syl3anc 1372 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β (πΏβ(π Β· π΄)) = ((πΏβπ)(.rβπ)(πΏβπ΄))) |
40 | 30 | adantr 482 |
. . . . . . 7
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β π β
Ring) |
41 | 10, 5 | zrh1 21062 |
. . . . . . 7
β’ (π β Ring β (πΏβ1) =
(1rβπ)) |
42 | 40, 41 | syl 17 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β (πΏβ1) =
(1rβπ)) |
43 | 39, 42 | eqeq12d 2749 |
. . . . 5
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β ((πΏβ(π Β· π΄)) = (πΏβ1) β ((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ))) |
44 | | simpll 766 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β π β
β0) |
45 | 34, 35 | zmulcld 12672 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β (π Β· π΄) β
β€) |
46 | | 1zzd 12593 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β 1 β β€) |
47 | 1, 10 | zndvds 21105 |
. . . . . 6
β’ ((π β β0
β§ (π Β· π΄) β β€ β§ 1 β
β€) β ((πΏβ(π Β· π΄)) = (πΏβ1) β π β₯ ((π Β· π΄) β 1))) |
48 | 44, 45, 46, 47 | syl3anc 1372 |
. . . . 5
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β ((πΏβ(π Β· π΄)) = (πΏβ1) β π β₯ ((π Β· π΄) β 1))) |
49 | 43, 48 | bitr3d 281 |
. . . 4
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β (((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ) β π β₯ ((π Β· π΄) β 1))) |
50 | 49 | rexbidva 3177 |
. . 3
β’ ((π β β0
β§ π΄ β β€)
β (βπ β
β€ ((πΏβπ)(.rβπ)(πΏβπ΄)) = (1rβπ) β βπ β β€ π β₯ ((π Β· π΄) β 1))) |
51 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β π΄ β β€) |
52 | | nn0z 12583 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β€) |
53 | 52 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β π β β€) |
54 | | gcddvds 16444 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π β β€) β ((π΄ gcd π) β₯ π΄ β§ (π΄ gcd π) β₯ π)) |
55 | 51, 53, 54 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β ((π΄ gcd π) β₯ π΄ β§ (π΄ gcd π) β₯ π)) |
56 | 55 | simpld 496 |
. . . . . . . 8
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β₯ π΄) |
57 | 51, 53 | gcdcld 16449 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β
β0) |
58 | 57 | nn0zd 12584 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β β€) |
59 | 34 | adantrr 716 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β π β β€) |
60 | | dvdsmultr2 16241 |
. . . . . . . . 9
β’ (((π΄ gcd π) β β€ β§ π β β€ β§ π΄ β β€) β ((π΄ gcd π) β₯ π΄ β (π΄ gcd π) β₯ (π Β· π΄))) |
61 | 58, 59, 51, 60 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β ((π΄ gcd π) β₯ π΄ β (π΄ gcd π) β₯ (π Β· π΄))) |
62 | 56, 61 | mpd 15 |
. . . . . . 7
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β₯ (π Β· π΄)) |
63 | 45 | adantrr 716 |
. . . . . . . 8
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π Β· π΄) β β€) |
64 | | 1zzd 12593 |
. . . . . . . 8
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β 1 β
β€) |
65 | | peano2zm 12605 |
. . . . . . . . . 10
β’ ((π Β· π΄) β β€ β ((π Β· π΄) β 1) β
β€) |
66 | 63, 65 | syl 17 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β ((π Β· π΄) β 1) β
β€) |
67 | 55 | simprd 497 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β₯ π) |
68 | | simprr 772 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β π β₯ ((π Β· π΄) β 1)) |
69 | 58, 53, 66, 67, 68 | dvdstrd 16238 |
. . . . . . . 8
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β₯ ((π Β· π΄) β 1)) |
70 | | dvdssub2 16244 |
. . . . . . . 8
β’ ((((π΄ gcd π) β β€ β§ (π Β· π΄) β β€ β§ 1 β β€)
β§ (π΄ gcd π) β₯ ((π Β· π΄) β 1)) β ((π΄ gcd π) β₯ (π Β· π΄) β (π΄ gcd π) β₯ 1)) |
71 | 58, 63, 64, 69, 70 | syl31anc 1374 |
. . . . . . 7
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β ((π΄ gcd π) β₯ (π Β· π΄) β (π΄ gcd π) β₯ 1)) |
72 | 62, 71 | mpbid 231 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) β₯ 1) |
73 | | dvds1 16262 |
. . . . . . 7
β’ ((π΄ gcd π) β β0 β ((π΄ gcd π) β₯ 1 β (π΄ gcd π) = 1)) |
74 | 57, 73 | syl 17 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β ((π΄ gcd π) β₯ 1 β (π΄ gcd π) = 1)) |
75 | 72, 74 | mpbid 231 |
. . . . 5
β’ (((π β β0
β§ π΄ β β€)
β§ (π β β€
β§ π β₯ ((π Β· π΄) β 1))) β (π΄ gcd π) = 1) |
76 | 75 | rexlimdvaa 3157 |
. . . 4
β’ ((π β β0
β§ π΄ β β€)
β (βπ β
β€ π β₯ ((π Β· π΄) β 1) β (π΄ gcd π) = 1)) |
77 | | simpr 486 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β€)
β π΄ β
β€) |
78 | 52 | adantr 482 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β€)
β π β
β€) |
79 | | bezout 16485 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€) β
βπ β β€
βπ β β€
(π΄ gcd π) = ((π΄ Β· π) + (π Β· π))) |
80 | 77, 78, 79 | syl2anc 585 |
. . . . . 6
β’ ((π β β0
β§ π΄ β β€)
β βπ β
β€ βπ β
β€ (π΄ gcd π) = ((π΄ Β· π) + (π Β· π))) |
81 | | eqeq1 2737 |
. . . . . . 7
β’ ((π΄ gcd π) = 1 β ((π΄ gcd π) = ((π΄ Β· π) + (π Β· π)) β 1 = ((π΄ Β· π) + (π Β· π)))) |
82 | 81 | 2rexbidv 3220 |
. . . . . 6
β’ ((π΄ gcd π) = 1 β (βπ β β€ βπ β β€ (π΄ gcd π) = ((π΄ Β· π) + (π Β· π)) β βπ β β€ βπ β β€ 1 = ((π΄ Β· π) + (π Β· π)))) |
83 | 80, 82 | syl5ibcom 244 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€)
β ((π΄ gcd π) = 1 β βπ β β€ βπ β β€ 1 = ((π΄ Β· π) + (π Β· π)))) |
84 | 52 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π β
β€) |
85 | | dvdsmul1 16221 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) |
86 | 84, 85 | sylancom 589 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π β₯ (π Β· π)) |
87 | | zmulcl 12611 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β (π Β· π) β β€) |
88 | 84, 87 | sylancom 589 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β (π Β· π) β
β€) |
89 | | dvdsnegb 16217 |
. . . . . . . . . . 11
β’ ((π β β€ β§ (π Β· π) β β€) β (π β₯ (π Β· π) β π β₯ -(π Β· π))) |
90 | 84, 88, 89 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β (π β₯ (π Β· π) β π β₯ -(π Β· π))) |
91 | 86, 90 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π β₯ -(π Β· π)) |
92 | 35 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π΄ β
β€) |
93 | 92 | zcnd 12667 |
. . . . . . . . . . . . . 14
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π΄ β
β) |
94 | | zcn 12563 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β π β
β) |
95 | 94 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π β
β) |
96 | 93, 95 | mulcomd 11235 |
. . . . . . . . . . . . 13
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β (π΄ Β· π) = (π Β· π΄)) |
97 | 96 | oveq1d 7424 |
. . . . . . . . . . . 12
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β ((π΄ Β· π) + (π Β· π)) = ((π Β· π΄) + (π Β· π))) |
98 | 95, 93 | mulcld 11234 |
. . . . . . . . . . . . 13
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β (π Β· π΄) β
β) |
99 | 88 | zcnd 12667 |
. . . . . . . . . . . . 13
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β (π Β· π) β
β) |
100 | 98, 99 | subnegd 11578 |
. . . . . . . . . . . 12
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β ((π Β· π΄) β -(π Β· π)) = ((π Β· π΄) + (π Β· π))) |
101 | 97, 100 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β ((π΄ Β· π) + (π Β· π)) = ((π Β· π΄) β -(π Β· π))) |
102 | 101 | oveq2d 7425 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β ((π Β· π΄) β ((π΄ Β· π) + (π Β· π))) = ((π Β· π΄) β ((π Β· π΄) β -(π Β· π)))) |
103 | 99 | negcld 11558 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β -(π Β· π) β
β) |
104 | 98, 103 | nncand 11576 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β ((π Β· π΄) β ((π Β· π΄) β -(π Β· π))) = -(π Β· π)) |
105 | 102, 104 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β ((π Β· π΄) β ((π΄ Β· π) + (π Β· π))) = -(π Β· π)) |
106 | 91, 105 | breqtrrd 5177 |
. . . . . . . 8
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β π β₯ ((π Β· π΄) β ((π΄ Β· π) + (π Β· π)))) |
107 | | oveq2 7417 |
. . . . . . . . 9
β’ (1 =
((π΄ Β· π) + (π Β· π)) β ((π Β· π΄) β 1) = ((π Β· π΄) β ((π΄ Β· π) + (π Β· π)))) |
108 | 107 | breq2d 5161 |
. . . . . . . 8
β’ (1 =
((π΄ Β· π) + (π Β· π)) β (π β₯ ((π Β· π΄) β 1) β π β₯ ((π Β· π΄) β ((π΄ Β· π) + (π Β· π))))) |
109 | 106, 108 | syl5ibrcom 246 |
. . . . . . 7
β’ ((((π β β0
β§ π΄ β β€)
β§ π β β€)
β§ π β β€)
β (1 = ((π΄ Β·
π) + (π Β· π)) β π β₯ ((π Β· π΄) β 1))) |
110 | 109 | rexlimdva 3156 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β€)
β§ π β β€)
β (βπ β
β€ 1 = ((π΄ Β·
π) + (π Β· π)) β π β₯ ((π Β· π΄) β 1))) |
111 | 110 | reximdva 3169 |
. . . . 5
β’ ((π β β0
β§ π΄ β β€)
β (βπ β
β€ βπ β
β€ 1 = ((π΄ Β·
π) + (π Β· π)) β βπ β β€ π β₯ ((π Β· π΄) β 1))) |
112 | 83, 111 | syld 47 |
. . . 4
β’ ((π β β0
β§ π΄ β β€)
β ((π΄ gcd π) = 1 β βπ β β€ π β₯ ((π Β· π΄) β 1))) |
113 | 76, 112 | impbid 211 |
. . 3
β’ ((π β β0
β§ π΄ β β€)
β (βπ β
β€ π β₯ ((π Β· π΄) β 1) β (π΄ gcd π) = 1)) |
114 | 28, 50, 113 | 3bitrd 305 |
. 2
β’ ((π β β0
β§ π΄ β β€)
β (βπ₯ β
(Baseβπ)(π₯(.rβπ)(πΏβπ΄)) = (1rβπ) β (π΄ gcd π) = 1)) |
115 | 8, 19, 114 | 3bitrd 305 |
1
β’ ((π β β0
β§ π΄ β β€)
β ((πΏβπ΄) β π β (π΄ gcd π) = 1)) |