Proof of Theorem pc2dvds
Step | Hyp | Ref
| Expression |
1 | | pcdvdstr 12235 |
. . . . 5
|
2 | 1 | ancoms 266 |
. . . 4
|
3 | 2 | ralrimiva 2537 |
. . 3
|
4 | 3 | 3expia 1194 |
. 2
|
5 | | 2prm 12038 |
. . . . . . . 8
|
6 | | elex2 2737 |
. . . . . . . 8
|
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
|
8 | | r19.2m 3490 |
. . . . . . 7
|
9 | 7, 8 | mpan 421 |
. . . . . 6
|
10 | | id 19 |
. . . . . . . . . . . . 13
|
11 | | zq 9555 |
. . . . . . . . . . . . . 14
|
12 | 11 | adantl 275 |
. . . . . . . . . . . . 13
|
13 | | pcxcl 12220 |
. . . . . . . . . . . . 13
|
14 | 10, 12, 13 | syl2anr 288 |
. . . . . . . . . . . 12
|
15 | | pnfge 9716 |
. . . . . . . . . . . 12
|
16 | 14, 15 | syl 14 |
. . . . . . . . . . 11
|
17 | 16 | biantrurd 303 |
. . . . . . . . . 10
|
18 | | pc0 12213 |
. . . . . . . . . . . 12
|
19 | 18 | adantl 275 |
. . . . . . . . . . 11
|
20 | 19 | breq1d 3986 |
. . . . . . . . . 10
|
21 | | pnfxr 7942 |
. . . . . . . . . . 11
|
22 | | xrletri3 9731 |
. . . . . . . . . . 11
|
23 | 14, 21, 22 | sylancl 410 |
. . . . . . . . . 10
|
24 | 17, 20, 23 | 3bitr4d 219 |
. . . . . . . . 9
|
25 | | pnfnre 7931 |
. . . . . . . . . . . 12
|
26 | 25 | neli 2431 |
. . . . . . . . . . 11
|
27 | | eleq1 2227 |
. . . . . . . . . . 11
|
28 | 26, 27 | mtbiri 665 |
. . . . . . . . . 10
|
29 | | simplr 520 |
. . . . . . . . . . . 12
|
30 | | 0zd 9194 |
. . . . . . . . . . . 12
|
31 | | zdceq 9257 |
. . . . . . . . . . . 12
DECID |
32 | 29, 30, 31 | syl2anc 409 |
. . . . . . . . . . 11
DECID |
33 | | pczcl 12207 |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | nn0red 9159 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | adantll 468 |
. . . . . . . . . . . . . . 15
|
36 | 35 | an4s 578 |
. . . . . . . . . . . . . 14
|
37 | 36 | expr 373 |
. . . . . . . . . . . . 13
|
38 | 37 | a1d 22 |
. . . . . . . . . . . 12
DECID |
39 | 38 | necon1bddc 2411 |
. . . . . . . . . . 11
DECID |
40 | 32, 39 | mpd 13 |
. . . . . . . . . 10
|
41 | 28, 40 | syl5 32 |
. . . . . . . . 9
|
42 | 24, 41 | sylbid 149 |
. . . . . . . 8
|
43 | 42 | rexlimdva 2581 |
. . . . . . 7
|
44 | | 0dvds 11737 |
. . . . . . . 8
|
45 | 44 | adantl 275 |
. . . . . . 7
|
46 | 43, 45 | sylibrd 168 |
. . . . . 6
|
47 | 9, 46 | syl5 32 |
. . . . 5
|
48 | 47 | adantr 274 |
. . . 4
|
49 | | oveq2 5844 |
. . . . . . . 8
|
50 | 49 | breq1d 3986 |
. . . . . . 7
|
51 | 50 | ralbidv 2464 |
. . . . . 6
|
52 | | breq1 3979 |
. . . . . 6
|
53 | 51, 52 | imbi12d 233 |
. . . . 5
|
54 | 53 | adantl 275 |
. . . 4
|
55 | 48, 54 | mpbird 166 |
. . 3
|
56 | | zdvdsdc 11738 |
. . . . 5
DECID |
57 | 56 | adantr 274 |
. . . 4
DECID
|
58 | | gcddvds 11881 |
. . . . . . . . . . . 12
|
59 | 58 | simpld 111 |
. . . . . . . . . . 11
|
60 | | gcdcl 11884 |
. . . . . . . . . . . . 13
|
61 | 60 | nn0zd 9302 |
. . . . . . . . . . . 12
|
62 | | simpl 108 |
. . . . . . . . . . . 12
|
63 | | dvdsabsb 11736 |
. . . . . . . . . . . 12
|
64 | 61, 62, 63 | syl2anc 409 |
. . . . . . . . . . 11
|
65 | 59, 64 | mpbid 146 |
. . . . . . . . . 10
|
66 | 65 | adantr 274 |
. . . . . . . . 9
|
67 | | simpl 108 |
. . . . . . . . . . . . 13
|
68 | 67 | necon3ai 2383 |
. . . . . . . . . . . 12
|
69 | | gcdn0cl 11880 |
. . . . . . . . . . . 12
|
70 | 68, 69 | sylan2 284 |
. . . . . . . . . . 11
|
71 | 70 | nnzd 9303 |
. . . . . . . . . 10
|
72 | 70 | nnne0d 8893 |
. . . . . . . . . 10
|
73 | | nnabscl 11028 |
. . . . . . . . . . . 12
|
74 | 73 | adantlr 469 |
. . . . . . . . . . 11
|
75 | 74 | nnzd 9303 |
. . . . . . . . . 10
|
76 | | dvdsval2 11716 |
. . . . . . . . . 10
|
77 | 71, 72, 75, 76 | syl3anc 1227 |
. . . . . . . . 9
|
78 | 66, 77 | mpbid 146 |
. . . . . . . 8
|
79 | | nnre 8855 |
. . . . . . . . . . 11
|
80 | | nngt0 8873 |
. . . . . . . . . . 11
|
81 | 79, 80 | jca 304 |
. . . . . . . . . 10
|
82 | | nnre 8855 |
. . . . . . . . . . 11
|
83 | | nngt0 8873 |
. . . . . . . . . . 11
|
84 | 82, 83 | jca 304 |
. . . . . . . . . 10
|
85 | | divgt0 8758 |
. . . . . . . . . 10
|
86 | 81, 84, 85 | syl2an 287 |
. . . . . . . . 9
|
87 | 74, 70, 86 | syl2anc 409 |
. . . . . . . 8
|
88 | | elnnz 9192 |
. . . . . . . 8
|
89 | 78, 87, 88 | sylanbrc 414 |
. . . . . . 7
|
90 | | elnn1uz2 9536 |
. . . . . . 7
|
91 | 89, 90 | sylib 121 |
. . . . . 6
|
92 | 58 | simprd 113 |
. . . . . . . . . 10
|
93 | 92 | adantr 274 |
. . . . . . . . 9
|
94 | | breq1 3979 |
. . . . . . . . 9
|
95 | 93, 94 | syl5ibcom 154 |
. . . . . . . 8
|
96 | 74 | nncnd 8862 |
. . . . . . . . . 10
|
97 | 70 | nncnd 8862 |
. . . . . . . . . 10
|
98 | | 1cnd 7906 |
. . . . . . . . . 10
|
99 | 70 | nnap0d 8894 |
. . . . . . . . . 10
# |
100 | 96, 97, 98, 99 | divmulapd 8699 |
. . . . . . . . 9
|
101 | 97 | mulid1d 7907 |
. . . . . . . . . 10
|
102 | 101 | eqeq1d 2173 |
. . . . . . . . 9
|
103 | 100, 102 | bitrd 187 |
. . . . . . . 8
|
104 | | absdvdsb 11735 |
. . . . . . . . 9
|
105 | 104 | adantr 274 |
. . . . . . . 8
|
106 | 95, 103, 105 | 3imtr4d 202 |
. . . . . . 7
|
107 | | exprmfct 12049 |
. . . . . . . 8
|
108 | | simprl 521 |
. . . . . . . . . . . . . . . 16
|
109 | 74 | adantr 274 |
. . . . . . . . . . . . . . . . 17
|
110 | 109 | nnzd 9303 |
. . . . . . . . . . . . . . . 16
|
111 | 109 | nnne0d 8893 |
. . . . . . . . . . . . . . . 16
|
112 | 70 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
113 | | pcdiv 12211 |
. . . . . . . . . . . . . . . 16
|
114 | 108, 110,
111, 112, 113 | syl121anc 1232 |
. . . . . . . . . . . . . . 15
|
115 | | simplll 523 |
. . . . . . . . . . . . . . . . . 18
|
116 | | zq 9555 |
. . . . . . . . . . . . . . . . . 18
|
117 | 115, 116 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
118 | | pcabs 12234 |
. . . . . . . . . . . . . . . . 17
|
119 | 108, 117,
118 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | oveq1d 5851 |
. . . . . . . . . . . . . . 15
|
121 | 114, 120 | eqtrd 2197 |
. . . . . . . . . . . . . 14
|
122 | | simprr 522 |
. . . . . . . . . . . . . . 15
|
123 | 89 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
124 | | pcelnn 12229 |
. . . . . . . . . . . . . . . 16
|
125 | 108, 123,
124 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
126 | 122, 125 | mpbird 166 |
. . . . . . . . . . . . . 14
|
127 | 121, 126 | eqeltrrd 2242 |
. . . . . . . . . . . . 13
|
128 | 108, 112 | pccld 12209 |
. . . . . . . . . . . . . . 15
|
129 | 128 | nn0zd 9302 |
. . . . . . . . . . . . . 14
|
130 | | simplr 520 |
. . . . . . . . . . . . . . . 16
|
131 | | pczcl 12207 |
. . . . . . . . . . . . . . . 16
|
132 | 108, 115,
130, 131 | syl12anc 1225 |
. . . . . . . . . . . . . . 15
|
133 | 132 | nn0zd 9302 |
. . . . . . . . . . . . . 14
|
134 | | znnsub 9233 |
. . . . . . . . . . . . . 14
|
135 | 129, 133,
134 | syl2anc 409 |
. . . . . . . . . . . . 13
|
136 | 127, 135 | mpbird 166 |
. . . . . . . . . . . 12
|
137 | | zltnle 9228 |
. . . . . . . . . . . . 13
|
138 | 129, 133,
137 | syl2anc 409 |
. . . . . . . . . . . 12
|
139 | 136, 138 | mpbid 146 |
. . . . . . . . . . 11
|
140 | 132 | nn0red 9159 |
. . . . . . . . . . . . 13
|
141 | | simpllr 524 |
. . . . . . . . . . . . . . 15
|
142 | | nprmdvds1 12051 |
. . . . . . . . . . . . . . . . . 18
|
143 | 142 | ad2antrl 482 |
. . . . . . . . . . . . . . . . 17
|
144 | | gcdid0 11898 |
. . . . . . . . . . . . . . . . . . . . 21
|
145 | 115, 144 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
146 | 145 | oveq2d 5852 |
. . . . . . . . . . . . . . . . . . 19
|
147 | 96 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
|
148 | 109 | nnap0d 8894 |
. . . . . . . . . . . . . . . . . . . 20
# |
149 | 147, 148 | dividapd 8673 |
. . . . . . . . . . . . . . . . . . 19
|
150 | 146, 149 | eqtrd 2197 |
. . . . . . . . . . . . . . . . . 18
|
151 | 150 | breq2d 3988 |
. . . . . . . . . . . . . . . . 17
|
152 | 143, 151 | mtbird 663 |
. . . . . . . . . . . . . . . 16
|
153 | | oveq2 5844 |
. . . . . . . . . . . . . . . . . . . 20
|
154 | 153 | oveq2d 5852 |
. . . . . . . . . . . . . . . . . . 19
|
155 | 154 | breq2d 3988 |
. . . . . . . . . . . . . . . . . 18
|
156 | 122, 155 | syl5ibcom 154 |
. . . . . . . . . . . . . . . . 17
|
157 | 156 | necon3bd 2377 |
. . . . . . . . . . . . . . . 16
|
158 | 152, 157 | mpd 13 |
. . . . . . . . . . . . . . 15
|
159 | 108, 141,
158, 33 | syl12anc 1225 |
. . . . . . . . . . . . . 14
|
160 | 159 | nn0red 9159 |
. . . . . . . . . . . . 13
|
161 | | lemininf 11161 |
. . . . . . . . . . . . 13
inf
|
162 | 140, 140,
160, 161 | syl3anc 1227 |
. . . . . . . . . . . 12
inf
|
163 | | pcgcd 12237 |
. . . . . . . . . . . . . . 15
|
164 | 108, 115,
141, 163 | syl3anc 1227 |
. . . . . . . . . . . . . 14
|
165 | 159 | nn0zd 9302 |
. . . . . . . . . . . . . . 15
|
166 | | 2zinfmin 11170 |
. . . . . . . . . . . . . . 15
inf
|
167 | 133, 165,
166 | syl2anc 409 |
. . . . . . . . . . . . . 14
inf
|
168 | 164, 167 | eqtr4d 2200 |
. . . . . . . . . . . . 13
inf
|
169 | 168 | breq2d 3988 |
. . . . . . . . . . . 12
inf
|
170 | 140 | leidd 8403 |
. . . . . . . . . . . . 13
|
171 | 170 | biantrurd 303 |
. . . . . . . . . . . 12
|
172 | 162, 169,
171 | 3bitr4rd 220 |
. . . . . . . . . . 11
|
173 | 139, 172 | mtbird 663 |
. . . . . . . . . 10
|
174 | 173 | expr 373 |
. . . . . . . . 9
|
175 | 174 | reximdva 2566 |
. . . . . . . 8
|
176 | | rexnalim 2453 |
. . . . . . . 8
|
177 | 107, 175,
176 | syl56 34 |
. . . . . . 7
|
178 | 106, 177 | orim12d 776 |
. . . . . 6
|
179 | 91, 178 | mpd 13 |
. . . . 5
|
180 | 179 | ord 714 |
. . . 4
|
181 | | condc 843 |
. . . 4
DECID
|
182 | 57, 180, 181 | sylc 62 |
. . 3
|
183 | | 0zd 9194 |
. . . . 5
|
184 | | zdceq 9257 |
. . . . 5
DECID |
185 | 62, 183, 184 | syl2anc 409 |
. . . 4
DECID |
186 | | dcne 2345 |
. . . 4
DECID |
187 | 185, 186 | sylib 121 |
. . 3
|
188 | 55, 182, 187 | mpjaodan 788 |
. 2
|
189 | 4, 188 | impbid 128 |
1
|