Step | Hyp | Ref
| Expression |
1 | | ablfacrp.k |
. . . . . 6
โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} |
2 | | ablfacrp.l |
. . . . . 6
โข ๐ฟ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} |
3 | 1, 2 | ineq12i 4175 |
. . . . 5
โข (๐พ โฉ ๐ฟ) = ({๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โฉ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐}) |
4 | | inrab 4271 |
. . . . 5
โข ({๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โฉ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐}) = {๐ฅ โ ๐ต โฃ ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)} |
5 | 3, 4 | eqtri 2765 |
. . . 4
โข (๐พ โฉ ๐ฟ) = {๐ฅ โ ๐ต โฃ ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)} |
6 | | ablfacrp.b |
. . . . . . . . . . . . . 14
โข ๐ต = (Baseโ๐บ) |
7 | | ablfacrp.o |
. . . . . . . . . . . . . 14
โข ๐ = (odโ๐บ) |
8 | 6, 7 | odcl 19325 |
. . . . . . . . . . . . 13
โข (๐ฅ โ ๐ต โ (๐โ๐ฅ) โ
โ0) |
9 | 8 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐โ๐ฅ) โ
โ0) |
10 | 9 | nn0zd 12532 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐โ๐ฅ) โ โค) |
11 | | ablfacrp.m |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
12 | 11 | nnzd 12533 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ โ โค) |
14 | | ablfacrp.n |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
15 | 14 | nnzd 12533 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ โ โค) |
17 | | dvdsgcd 16432 |
. . . . . . . . . . 11
โข (((๐โ๐ฅ) โ โค โง ๐ โ โค โง ๐ โ โค) โ (((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐) โ (๐โ๐ฅ) โฅ (๐ gcd ๐))) |
18 | 10, 13, 16, 17 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ต) โ (((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐) โ (๐โ๐ฅ) โฅ (๐ gcd ๐))) |
19 | 18 | 3impia 1118 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ (๐โ๐ฅ) โฅ (๐ gcd ๐)) |
20 | | ablfacrp.1 |
. . . . . . . . . 10
โข (๐ โ (๐ gcd ๐) = 1) |
21 | 20 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ (๐ gcd ๐) = 1) |
22 | 19, 21 | breqtrd 5136 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ (๐โ๐ฅ) โฅ 1) |
23 | | simp2 1138 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ ๐ฅ โ ๐ต) |
24 | | dvds1 16208 |
. . . . . . . . 9
โข ((๐โ๐ฅ) โ โ0 โ ((๐โ๐ฅ) โฅ 1 โ (๐โ๐ฅ) = 1)) |
25 | 23, 8, 24 | 3syl 18 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ ((๐โ๐ฅ) โฅ 1 โ (๐โ๐ฅ) = 1)) |
26 | 22, 25 | mpbid 231 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ (๐โ๐ฅ) = 1) |
27 | | ablfacrp.g |
. . . . . . . . . 10
โข (๐ โ ๐บ โ Abel) |
28 | | ablgrp 19574 |
. . . . . . . . . 10
โข (๐บ โ Abel โ ๐บ โ Grp) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐บ โ Grp) |
30 | 29 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ ๐บ โ Grp) |
31 | | ablfacrp.z |
. . . . . . . . 9
โข 0 =
(0gโ๐บ) |
32 | 7, 31, 6 | odeq1 19349 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ฅ โ ๐ต) โ ((๐โ๐ฅ) = 1 โ ๐ฅ = 0 )) |
33 | 30, 23, 32 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ ((๐โ๐ฅ) = 1 โ ๐ฅ = 0 )) |
34 | 26, 33 | mpbid 231 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ ๐ฅ = 0 ) |
35 | | velsn 4607 |
. . . . . 6
โข (๐ฅ โ { 0 } โ ๐ฅ = 0 ) |
36 | 34, 35 | sylibr 233 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต โง ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)) โ ๐ฅ โ { 0 }) |
37 | 36 | rabssdv 4037 |
. . . 4
โข (๐ โ {๐ฅ โ ๐ต โฃ ((๐โ๐ฅ) โฅ ๐ โง (๐โ๐ฅ) โฅ ๐)} โ { 0 }) |
38 | 5, 37 | eqsstrid 3997 |
. . 3
โข (๐ โ (๐พ โฉ ๐ฟ) โ { 0 }) |
39 | 7, 6 | oddvdssubg 19640 |
. . . . . . . 8
โข ((๐บ โ Abel โง ๐ โ โค) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
40 | 27, 12, 39 | syl2anc 585 |
. . . . . . 7
โข (๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
41 | 1, 40 | eqeltrid 2842 |
. . . . . 6
โข (๐ โ ๐พ โ (SubGrpโ๐บ)) |
42 | 31 | subg0cl 18943 |
. . . . . 6
โข (๐พ โ (SubGrpโ๐บ) โ 0 โ ๐พ) |
43 | 41, 42 | syl 17 |
. . . . 5
โข (๐ โ 0 โ ๐พ) |
44 | 7, 6 | oddvdssubg 19640 |
. . . . . . . 8
โข ((๐บ โ Abel โง ๐ โ โค) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
45 | 27, 15, 44 | syl2anc 585 |
. . . . . . 7
โข (๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
46 | 2, 45 | eqeltrid 2842 |
. . . . . 6
โข (๐ โ ๐ฟ โ (SubGrpโ๐บ)) |
47 | 31 | subg0cl 18943 |
. . . . . 6
โข (๐ฟ โ (SubGrpโ๐บ) โ 0 โ ๐ฟ) |
48 | 46, 47 | syl 17 |
. . . . 5
โข (๐ โ 0 โ ๐ฟ) |
49 | 43, 48 | elind 4159 |
. . . 4
โข (๐ โ 0 โ (๐พ โฉ ๐ฟ)) |
50 | 49 | snssd 4774 |
. . 3
โข (๐ โ { 0 } โ (๐พ โฉ ๐ฟ)) |
51 | 38, 50 | eqssd 3966 |
. 2
โข (๐ โ (๐พ โฉ ๐ฟ) = { 0 }) |
52 | | ablfacrp.s |
. . . . . 6
โข โ =
(LSSumโ๐บ) |
53 | 52 | lsmsubg2 19644 |
. . . . 5
โข ((๐บ โ Abel โง ๐พ โ (SubGrpโ๐บ) โง ๐ฟ โ (SubGrpโ๐บ)) โ (๐พ โ ๐ฟ) โ (SubGrpโ๐บ)) |
54 | 27, 41, 46, 53 | syl3anc 1372 |
. . . 4
โข (๐ โ (๐พ โ ๐ฟ) โ (SubGrpโ๐บ)) |
55 | 6 | subgss 18936 |
. . . 4
โข ((๐พ โ ๐ฟ) โ (SubGrpโ๐บ) โ (๐พ โ ๐ฟ) โ ๐ต) |
56 | 54, 55 | syl 17 |
. . 3
โข (๐ โ (๐พ โ ๐ฟ) โ ๐ต) |
57 | | eqid 2737 |
. . . . . 6
โข
(.gโ๐บ) = (.gโ๐บ) |
58 | 6, 57 | mulg1 18890 |
. . . . 5
โข (๐ โ ๐ต โ (1(.gโ๐บ)๐) = ๐) |
59 | 58 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ ๐ต) โ (1(.gโ๐บ)๐) = ๐) |
60 | | bezout 16431 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ โ โค
โ๐ โ โค
(๐ gcd ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
61 | 12, 15, 60 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ๐ โ โค โ๐ โ โค (๐ gcd ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
62 | 61 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ ๐ต) โ โ๐ โ โค โ๐ โ โค (๐ gcd ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
63 | 20 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐ gcd ๐) = 1) |
64 | 63 | eqeq1d 2739 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐) + (๐ ยท ๐)) โ 1 = ((๐ ยท ๐) + (๐ ยท ๐)))) |
65 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
66 | | simprl 770 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
67 | 65, 66 | zmulcld 12620 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐ ยท ๐) โ โค) |
68 | 67 | zcnd 12615 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐ ยท ๐) โ โ) |
69 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
70 | | simprr 772 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
71 | 69, 70 | zmulcld 12620 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐ ยท ๐) โ โค) |
72 | 71 | zcnd 12615 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐ ยท ๐) โ โ) |
73 | 68, 72 | addcomd 11364 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
74 | 73 | oveq1d 7377 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐) = (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐)) |
75 | 29 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐บ โ Grp) |
76 | | simplr 768 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ ๐ต) |
77 | | eqid 2737 |
. . . . . . . . . . . 12
โข
(+gโ๐บ) = (+gโ๐บ) |
78 | 6, 57, 77 | mulgdir 18915 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง ((๐ ยท ๐) โ โค โง (๐ ยท ๐) โ โค โง ๐ โ ๐ต)) โ (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐) = (((๐ ยท ๐)(.gโ๐บ)๐)(+gโ๐บ)((๐ ยท ๐)(.gโ๐บ)๐))) |
79 | 75, 71, 67, 76, 78 | syl13anc 1373 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐) = (((๐ ยท ๐)(.gโ๐บ)๐)(+gโ๐บ)((๐ ยท ๐)(.gโ๐บ)๐))) |
80 | 74, 79 | eqtrd 2777 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐) = (((๐ ยท ๐)(.gโ๐บ)๐)(+gโ๐บ)((๐ ยท ๐)(.gโ๐บ)๐))) |
81 | 41 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐พ โ (SubGrpโ๐บ)) |
82 | 46 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ฟ โ (SubGrpโ๐บ)) |
83 | 6, 57 | mulgcl 18900 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง (๐ ยท ๐) โ โค โง ๐ โ ๐ต) โ ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ต) |
84 | 75, 71, 76, 83 | syl3anc 1372 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ต) |
85 | 6, 7 | odcl 19325 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ (๐โ๐) โ
โ0) |
86 | 85 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โ
โ0) |
87 | 86 | nn0zd 12532 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โ โค) |
88 | 65, 69 | zmulcld 12620 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐ ยท ๐) โ โค) |
89 | | ablfacrp.2 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) |
90 | 11, 14 | nnmulcld 12213 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ ยท ๐) โ โ) |
91 | 90 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ ยท ๐) โ
โ0) |
92 | 89, 91 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โฏโ๐ต) โ
โ0) |
93 | 6 | fvexi 6861 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ต โ V |
94 | | hashclb 14265 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ต โ V โ (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0)) |
95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0) |
96 | 92, 95 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ Fin) |
97 | 96 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ต โ Fin) |
98 | 6, 7 | oddvds2 19355 |
. . . . . . . . . . . . . . . 16
โข ((๐บ โ Grp โง ๐ต โ Fin โง ๐ โ ๐ต) โ (๐โ๐) โฅ (โฏโ๐ต)) |
99 | 75, 97, 76, 98 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โฅ (โฏโ๐ต)) |
100 | 89 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (โฏโ๐ต) = (๐ ยท ๐)) |
101 | 99, 100 | breqtrd 5136 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โฅ (๐ ยท ๐)) |
102 | 87, 88, 70, 101 | dvdsmultr1d 16186 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โฅ ((๐ ยท ๐) ยท ๐)) |
103 | 65 | zcnd 12615 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
104 | 69 | zcnd 12615 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
105 | 70 | zcnd 12615 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
106 | 103, 104,
105 | mulassd 11185 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
107 | 102, 106 | breqtrd 5136 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โฅ (๐ ยท (๐ ยท ๐))) |
108 | 6, 7, 57 | odmulgid 19343 |
. . . . . . . . . . . . 13
โข (((๐บ โ Grp โง ๐ โ ๐ต โง (๐ ยท ๐) โ โค) โง ๐ โ โค) โ ((๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐ โ (๐โ๐) โฅ (๐ ยท (๐ ยท ๐)))) |
109 | 75, 76, 71, 65, 108 | syl31anc 1374 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐ โ (๐โ๐) โฅ (๐ ยท (๐ ยท ๐)))) |
110 | 107, 109 | mpbird 257 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐) |
111 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ฅ = ((๐ ยท ๐)(.gโ๐บ)๐) โ (๐โ๐ฅ) = (๐โ((๐ ยท ๐)(.gโ๐บ)๐))) |
112 | 111 | breq1d 5120 |
. . . . . . . . . . . 12
โข (๐ฅ = ((๐ ยท ๐)(.gโ๐บ)๐) โ ((๐โ๐ฅ) โฅ ๐ โ (๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐)) |
113 | 112, 1 | elrab2 3653 |
. . . . . . . . . . 11
โข (((๐ ยท ๐)(.gโ๐บ)๐) โ ๐พ โ (((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ต โง (๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐)) |
114 | 84, 110, 113 | sylanbrc 584 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐พ) |
115 | 6, 57 | mulgcl 18900 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง (๐ ยท ๐) โ โค โง ๐ โ ๐ต) โ ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ต) |
116 | 75, 67, 76, 115 | syl3anc 1372 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ต) |
117 | 87, 88, 66, 101 | dvdsmultr1d 16186 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โฅ ((๐ ยท ๐) ยท ๐)) |
118 | | zcn 12511 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ๐ โ
โ) |
119 | 118 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
120 | | mulass 11146 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
121 | | mul12 11327 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ ยท ๐)) = (๐ ยท (๐ ยท ๐))) |
122 | 120, 121 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
123 | 103, 104,
119, 122 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
124 | 117, 123 | breqtrd 5136 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ๐) โฅ (๐ ยท (๐ ยท ๐))) |
125 | 6, 7, 57 | odmulgid 19343 |
. . . . . . . . . . . . 13
โข (((๐บ โ Grp โง ๐ โ ๐ต โง (๐ ยท ๐) โ โค) โง ๐ โ โค) โ ((๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐ โ (๐โ๐) โฅ (๐ ยท (๐ ยท ๐)))) |
126 | 75, 76, 67, 69, 125 | syl31anc 1374 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐ โ (๐โ๐) โฅ (๐ ยท (๐ ยท ๐)))) |
127 | 124, 126 | mpbird 257 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐) |
128 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ฅ = ((๐ ยท ๐)(.gโ๐บ)๐) โ (๐โ๐ฅ) = (๐โ((๐ ยท ๐)(.gโ๐บ)๐))) |
129 | 128 | breq1d 5120 |
. . . . . . . . . . . 12
โข (๐ฅ = ((๐ ยท ๐)(.gโ๐บ)๐) โ ((๐โ๐ฅ) โฅ ๐ โ (๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐)) |
130 | 129, 2 | elrab2 3653 |
. . . . . . . . . . 11
โข (((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ฟ โ (((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ต โง (๐โ((๐ ยท ๐)(.gโ๐บ)๐)) โฅ ๐)) |
131 | 116, 127,
130 | sylanbrc 584 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ฟ) |
132 | 77, 52 | lsmelvali 19439 |
. . . . . . . . . 10
โข (((๐พ โ (SubGrpโ๐บ) โง ๐ฟ โ (SubGrpโ๐บ)) โง (((๐ ยท ๐)(.gโ๐บ)๐) โ ๐พ โง ((๐ ยท ๐)(.gโ๐บ)๐) โ ๐ฟ)) โ (((๐ ยท ๐)(.gโ๐บ)๐)(+gโ๐บ)((๐ ยท ๐)(.gโ๐บ)๐)) โ (๐พ โ ๐ฟ)) |
133 | 81, 82, 114, 131, 132 | syl22anc 838 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (((๐ ยท ๐)(.gโ๐บ)๐)(+gโ๐บ)((๐ ยท ๐)(.gโ๐บ)๐)) โ (๐พ โ ๐ฟ)) |
134 | 80, 133 | eqeltrd 2838 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐) โ (๐พ โ ๐ฟ)) |
135 | | oveq1 7369 |
. . . . . . . . 9
โข (1 =
((๐ ยท ๐) + (๐ ยท ๐)) โ (1(.gโ๐บ)๐) = (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐)) |
136 | 135 | eleq1d 2823 |
. . . . . . . 8
โข (1 =
((๐ ยท ๐) + (๐ ยท ๐)) โ ((1(.gโ๐บ)๐) โ (๐พ โ ๐ฟ) โ (((๐ ยท ๐) + (๐ ยท ๐))(.gโ๐บ)๐) โ (๐พ โ ๐ฟ))) |
137 | 134, 136 | syl5ibrcom 247 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ (1 = ((๐ ยท ๐) + (๐ ยท ๐)) โ (1(.gโ๐บ)๐) โ (๐พ โ ๐ฟ))) |
138 | 64, 137 | sylbid 239 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ต) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐) + (๐ ยท ๐)) โ (1(.gโ๐บ)๐) โ (๐พ โ ๐ฟ))) |
139 | 138 | rexlimdvva 3206 |
. . . . 5
โข ((๐ โง ๐ โ ๐ต) โ (โ๐ โ โค โ๐ โ โค (๐ gcd ๐) = ((๐ ยท ๐) + (๐ ยท ๐)) โ (1(.gโ๐บ)๐) โ (๐พ โ ๐ฟ))) |
140 | 62, 139 | mpd 15 |
. . . 4
โข ((๐ โง ๐ โ ๐ต) โ (1(.gโ๐บ)๐) โ (๐พ โ ๐ฟ)) |
141 | 59, 140 | eqeltrrd 2839 |
. . 3
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ (๐พ โ ๐ฟ)) |
142 | 56, 141 | eqelssd 3970 |
. 2
โข (๐ โ (๐พ โ ๐ฟ) = ๐ต) |
143 | 51, 142 | jca 513 |
1
โข (๐ โ ((๐พ โฉ ๐ฟ) = { 0 } โง (๐พ โ ๐ฟ) = ๐ต)) |