Step | Hyp | Ref
| Expression |
1 | | gexexlem.3 |
. . 3
|
2 | | gexex.1 |
. . . 4
|
3 | | gexex.3 |
. . . 4
|
4 | 2, 3 | odcl 17955 |
. . 3
|
5 | 1, 4 | syl 17 |
. 2
|
6 | | gexexlem.2 |
. . 3
|
7 | 6 | nnnn0d 11351 |
. 2
|
8 | | gexexlem.1 |
. . . 4
|
9 | | ablgrp 18198 |
. . . 4
|
10 | 8, 9 | syl 17 |
. . 3
|
11 | | gexex.2 |
. . . 4
gEx |
12 | 2, 11, 3 | gexod 18001 |
. . 3
|
13 | 10, 1, 12 | syl2anc 693 |
. 2
|
14 | 8 | ad2antrr 762 |
. . . . . . . . . . . 12
|
15 | 10 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
16 | | prmnn 15388 |
. . . . . . . . . . . . . . . 16
|
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . 15
|
18 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
19 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
20 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
21 | 2, 11, 3 | gexnnod 18003 |
. . . . . . . . . . . . . . . . 17
|
22 | 15, 19, 20, 21 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
23 | 18, 22 | pccld 15555 |
. . . . . . . . . . . . . . 15
|
24 | 17, 23 | nnexpcld 13030 |
. . . . . . . . . . . . . 14
|
25 | 24 | nnzd 11481 |
. . . . . . . . . . . . 13
|
26 | | eqid 2622 |
. . . . . . . . . . . . . 14
.g .g |
27 | 2, 26 | mulgcl 17559 |
. . . . . . . . . . . . 13
.g |
28 | 15, 25, 20, 27 | syl3anc 1326 |
. . . . . . . . . . . 12
.g |
29 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
30 | 2, 11, 3 | gexnnod 18003 |
. . . . . . . . . . . . . . . . 17
|
31 | 15, 19, 29, 30 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
32 | | pcdvds 15568 |
. . . . . . . . . . . . . . . 16
|
33 | 18, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
34 | 18, 31 | pccld 15555 |
. . . . . . . . . . . . . . . . 17
|
35 | 17, 34 | nnexpcld 13030 |
. . . . . . . . . . . . . . . 16
|
36 | | nndivdvds 14989 |
. . . . . . . . . . . . . . . 16
|
37 | 31, 35, 36 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
38 | 33, 37 | mpbid 222 |
. . . . . . . . . . . . . 14
|
39 | 38 | nnzd 11481 |
. . . . . . . . . . . . 13
|
40 | 2, 26 | mulgcl 17559 |
. . . . . . . . . . . . 13
.g |
41 | 15, 39, 29, 40 | syl3anc 1326 |
. . . . . . . . . . . 12
.g |
42 | 2, 3, 26 | odmulg 17973 |
. . . . . . . . . . . . . . . . . 18
.g |
43 | 15, 20, 25, 42 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
.g |
44 | | pcdvds 15568 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | 18, 22, 44 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | gcdeq 15272 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 24, 22, 46 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 45, 47 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
.g .g |
50 | 43, 49 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
.g |
51 | 50 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
.g
|
52 | 2, 11, 3 | gexnnod 18003 |
. . . . . . . . . . . . . . . . . 18
.g .g |
53 | 15, 19, 28, 52 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
.g |
54 | 53 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
.g |
55 | 24 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
56 | 24 | nnne0d 11065 |
. . . . . . . . . . . . . . . 16
|
57 | 54, 55, 56 | divcan3d 10806 |
. . . . . . . . . . . . . . 15
.g
.g |
58 | 51, 57 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
.g |
59 | 2, 11, 3 | gexnnod 18003 |
. . . . . . . . . . . . . . . . 17
.g
.g |
60 | 15, 19, 41, 59 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
.g |
61 | 60 | nncnd 11036 |
. . . . . . . . . . . . . . 15
.g |
62 | 35 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
63 | 38 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
64 | 38 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
|
65 | 31 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
66 | 35 | nnne0d 11065 |
. . . . . . . . . . . . . . . . 17
|
67 | 65, 62, 66 | divcan1d 10802 |
. . . . . . . . . . . . . . . 16
|
68 | 2, 3, 26 | odmulg 17973 |
. . . . . . . . . . . . . . . . 17
.g |
69 | 15, 29, 39, 68 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
.g |
70 | 35 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 39, 70, 71 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 72, 67 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
|
74 | | gcdeq 15272 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 38, 31, 74 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
76 | 73, 75 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
.g
.g |
78 | 67, 69, 77 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . 15
.g |
79 | 61, 62, 63, 64, 78 | mulcanad 10662 |
. . . . . . . . . . . . . 14
.g |
80 | 58, 79 | oveq12d 6668 |
. . . . . . . . . . . . 13
.g .g |
81 | | nndivdvds 14989 |
. . . . . . . . . . . . . . . . 17
|
82 | 22, 24, 81 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
83 | 45, 82 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
84 | 83 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
85 | | gcdcom 15235 |
. . . . . . . . . . . . . 14
|
86 | 84, 70, 85 | syl2anc 693 |
. . . . . . . . . . . . 13
|
87 | | pcndvds2 15572 |
. . . . . . . . . . . . . . . 16
|
88 | 18, 22, 87 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
89 | | coprm 15423 |
. . . . . . . . . . . . . . . 16
|
90 | 18, 84, 89 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
91 | 88, 90 | mpbid 222 |
. . . . . . . . . . . . . 14
|
92 | | prmz 15389 |
. . . . . . . . . . . . . . . 16
|
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . 15
|
94 | | rpexp1i 15433 |
. . . . . . . . . . . . . . 15
|
95 | 93, 84, 34, 94 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
96 | 91, 95 | mpd 15 |
. . . . . . . . . . . . 13
|
97 | 80, 86, 96 | 3eqtrd 2660 |
. . . . . . . . . . . 12
.g .g |
98 | | eqid 2622 |
. . . . . . . . . . . . 13
|
99 | 3, 2, 98 | odadd 18253 |
. . . . . . . . . . . 12
.g .g .g
.g
.g .g
.g .g |
100 | 14, 28, 41, 97, 99 | syl31anc 1329 |
. . . . . . . . . . 11
.g .g
.g .g |
101 | 58, 79 | oveq12d 6668 |
. . . . . . . . . . 11
.g .g |
102 | 100, 101 | eqtrd 2656 |
. . . . . . . . . 10
.g .g |
103 | 2, 98 | grpcl 17430 |
. . . . . . . . . . . 12
.g .g .g
.g |
104 | 15, 28, 41, 103 | syl3anc 1326 |
. . . . . . . . . . 11
.g
.g |
105 | | gexexlem.4 |
. . . . . . . . . . . . 13
|
106 | 105 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
107 | 106 | ad2antrr 762 |
. . . . . . . . . . 11
|
108 | | fveq2 6191 |
. . . . . . . . . . . . 13
.g .g
.g .g |
109 | 108 | breq1d 4663 |
. . . . . . . . . . . 12
.g .g
.g
.g |
110 | 109 | rspcv 3305 |
. . . . . . . . . . 11
.g
.g .g
.g |
111 | 104, 107,
110 | sylc 65 |
. . . . . . . . . 10
.g .g |
112 | 102, 111 | eqbrtrrd 4677 |
. . . . . . . . 9
|
113 | 83 | nnred 11035 |
. . . . . . . . . 10
|
114 | 22 | nnred 11035 |
. . . . . . . . . 10
|
115 | 35 | nnrpd 11870 |
. . . . . . . . . 10
|
116 | 113, 114,
115 | lemuldivd 11921 |
. . . . . . . . 9
|
117 | 112, 116 | mpbid 222 |
. . . . . . . 8
|
118 | | nnrp 11842 |
. . . . . . . . . 10
|
119 | | nnrp 11842 |
. . . . . . . . . 10
|
120 | | nnrp 11842 |
. . . . . . . . . 10
|
121 | | rpregt0 11846 |
. . . . . . . . . . 11
|
122 | | rpregt0 11846 |
. . . . . . . . . . 11
|
123 | | rpregt0 11846 |
. . . . . . . . . . 11
|
124 | | lediv2 10913 |
. . . . . . . . . . 11
|
125 | 121, 122,
123, 124 | syl3an 1368 |
. . . . . . . . . 10
|
126 | 118, 119,
120, 125 | syl3an 1368 |
. . . . . . . . 9
|
127 | 35, 24, 22, 126 | syl3anc 1326 |
. . . . . . . 8
|
128 | 117, 127 | mpbird 247 |
. . . . . . 7
|
129 | 17 | nnred 11035 |
. . . . . . . 8
|
130 | 34 | nn0zd 11480 |
. . . . . . . 8
|
131 | 23 | nn0zd 11480 |
. . . . . . . 8
|
132 | | prmuz2 15408 |
. . . . . . . . . 10
|
133 | 132 | adantl 482 |
. . . . . . . . 9
|
134 | | eluz2b2 11761 |
. . . . . . . . . 10
|
135 | 134 | simprbi 480 |
. . . . . . . . 9
|
136 | 133, 135 | syl 17 |
. . . . . . . 8
|
137 | 129, 130,
131, 136 | leexp2d 13039 |
. . . . . . 7
|
138 | 128, 137 | mpbird 247 |
. . . . . 6
|
139 | 138 | ralrimiva 2966 |
. . . . 5
|
140 | 2, 3 | odcl 17955 |
. . . . . . . 8
|
141 | 140 | adantl 482 |
. . . . . . 7
|
142 | 141 | nn0zd 11480 |
. . . . . 6
|
143 | 5 | nn0zd 11480 |
. . . . . . 7
|
144 | 143 | adantr 481 |
. . . . . 6
|
145 | | pc2dvds 15583 |
. . . . . 6
|
146 | 142, 144,
145 | syl2anc 693 |
. . . . 5
|
147 | 139, 146 | mpbird 247 |
. . . 4
|
148 | 147 | ralrimiva 2966 |
. . 3
|
149 | 2, 11, 3 | gexdvds2 18000 |
. . . 4
|
150 | 10, 143, 149 | syl2anc 693 |
. . 3
|
151 | 148, 150 | mpbird 247 |
. 2
|
152 | | dvdseq 15036 |
. 2
|
153 | 5, 7, 13, 151, 152 | syl22anc 1327 |
1
|