Step | Hyp | Ref
| Expression |
1 | | prmind.5 |
. 2
|
2 | | oveq2 5873 |
. . . 4
|
3 | 2 | raleqdv 2676 |
. . 3
|
4 | | oveq2 5873 |
. . . 4
|
5 | 4 | raleqdv 2676 |
. . 3
|
6 | | oveq2 5873 |
. . . 4
|
7 | 6 | raleqdv 2676 |
. . 3
|
8 | | oveq2 5873 |
. . . 4
|
9 | 8 | raleqdv 2676 |
. . 3
|
10 | | prmind.6 |
. . . . 5
|
11 | | elfz1eq 10005 |
. . . . . 6
|
12 | | prmind.1 |
. . . . . 6
|
13 | 11, 12 | syl 14 |
. . . . 5
|
14 | 10, 13 | mpbiri 168 |
. . . 4
|
15 | 14 | rgen 2528 |
. . 3
|
16 | | peano2nn 8904 |
. . . . . . . . . . . . 13
|
17 | 16 | ad2antrr 488 |
. . . . . . . . . . . 12
|
18 | 17 | nncnd 8906 |
. . . . . . . . . . 11
|
19 | | elfzuz 9991 |
. . . . . . . . . . . . . 14
|
20 | 19 | ad2antrl 490 |
. . . . . . . . . . . . 13
|
21 | | eluz2nn 9539 |
. . . . . . . . . . . . 13
|
22 | 20, 21 | syl 14 |
. . . . . . . . . . . 12
|
23 | 22 | nncnd 8906 |
. . . . . . . . . . 11
|
24 | 22 | nnap0d 8938 |
. . . . . . . . . . 11
# |
25 | 18, 23, 24 | divcanap2d 8722 |
. . . . . . . . . 10
|
26 | | simprr 531 |
. . . . . . . . . . . . 13
|
27 | 22 | nnzd 9347 |
. . . . . . . . . . . . . 14
|
28 | 22 | nnne0d 8937 |
. . . . . . . . . . . . . 14
|
29 | 17 | nnzd 9347 |
. . . . . . . . . . . . . 14
|
30 | | dvdsval2 11765 |
. . . . . . . . . . . . . 14
|
31 | 27, 28, 29, 30 | syl3anc 1238 |
. . . . . . . . . . . . 13
|
32 | 26, 31 | mpbid 147 |
. . . . . . . . . . . 12
|
33 | 23 | mulid2d 7950 |
. . . . . . . . . . . . . 14
|
34 | | elfzle2 9998 |
. . . . . . . . . . . . . . . . 17
|
35 | 34 | ad2antrl 490 |
. . . . . . . . . . . . . . . 16
|
36 | | nncn 8900 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
|
38 | | ax-1cn 7879 |
. . . . . . . . . . . . . . . . 17
|
39 | | pncan 8137 |
. . . . . . . . . . . . . . . . 17
|
40 | 37, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . . . 16
|
41 | 35, 40 | breqtrd 4024 |
. . . . . . . . . . . . . . 15
|
42 | | nnz 9245 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
|
44 | | zleltp1 9281 |
. . . . . . . . . . . . . . . 16
|
45 | 27, 43, 44 | syl2anc 411 |
. . . . . . . . . . . . . . 15
|
46 | 41, 45 | mpbid 147 |
. . . . . . . . . . . . . 14
|
47 | 33, 46 | eqbrtrd 4020 |
. . . . . . . . . . . . 13
|
48 | | 1red 7947 |
. . . . . . . . . . . . . 14
|
49 | 17 | nnred 8905 |
. . . . . . . . . . . . . 14
|
50 | 22 | nnred 8905 |
. . . . . . . . . . . . . 14
|
51 | 22 | nngt0d 8936 |
. . . . . . . . . . . . . 14
|
52 | | ltmuldiv 8804 |
. . . . . . . . . . . . . 14
|
53 | 48, 49, 50, 51, 52 | syl112anc 1242 |
. . . . . . . . . . . . 13
|
54 | 47, 53 | mpbid 147 |
. . . . . . . . . . . 12
|
55 | | eluz2b1 9574 |
. . . . . . . . . . . 12
|
56 | 32, 54, 55 | sylanbrc 417 |
. . . . . . . . . . 11
|
57 | | prmind.2 |
. . . . . . . . . . . . 13
|
58 | | simplr 528 |
. . . . . . . . . . . . 13
|
59 | | fznn 10059 |
. . . . . . . . . . . . . . 15
|
60 | 43, 59 | syl 14 |
. . . . . . . . . . . . . 14
|
61 | 22, 41, 60 | mpbir2and 944 |
. . . . . . . . . . . . 13
|
62 | 57, 58, 61 | rspcdva 2844 |
. . . . . . . . . . . 12
|
63 | | vex 2738 |
. . . . . . . . . . . . . . 15
|
64 | | prmind.3 |
. . . . . . . . . . . . . . 15
|
65 | 63, 64 | sbcie 2995 |
. . . . . . . . . . . . . 14
|
66 | | dfsbcq 2962 |
. . . . . . . . . . . . . 14
|
67 | 65, 66 | bitr3id 194 |
. . . . . . . . . . . . 13
|
68 | 64 | cbvralv 2701 |
. . . . . . . . . . . . . 14
|
69 | 58, 68 | sylib 122 |
. . . . . . . . . . . . 13
|
70 | 17 | nnrpd 9665 |
. . . . . . . . . . . . . . . . 17
|
71 | 22 | nnrpd 9665 |
. . . . . . . . . . . . . . . . 17
|
72 | 70, 71 | rpdivcld 9685 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | rpgt0d 9670 |
. . . . . . . . . . . . . . 15
|
74 | | elnnz 9236 |
. . . . . . . . . . . . . . 15
|
75 | 32, 73, 74 | sylanbrc 417 |
. . . . . . . . . . . . . 14
|
76 | 17 | nnap0d 8938 |
. . . . . . . . . . . . . . . . . 18
# |
77 | 18, 76 | dividapd 8716 |
. . . . . . . . . . . . . . . . 17
|
78 | | eluz2gt1 9575 |
. . . . . . . . . . . . . . . . . 18
|
79 | 20, 78 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
80 | 77, 79 | eqbrtrd 4020 |
. . . . . . . . . . . . . . . 16
|
81 | 17 | nngt0d 8936 |
. . . . . . . . . . . . . . . . 17
|
82 | | ltdiv23 8822 |
. . . . . . . . . . . . . . . . 17
|
83 | 49, 49, 81, 50, 51, 82 | syl122anc 1247 |
. . . . . . . . . . . . . . . 16
|
84 | 80, 83 | mpbid 147 |
. . . . . . . . . . . . . . 15
|
85 | | zleltp1 9281 |
. . . . . . . . . . . . . . . 16
|
86 | 32, 43, 85 | syl2anc 411 |
. . . . . . . . . . . . . . 15
|
87 | 84, 86 | mpbird 167 |
. . . . . . . . . . . . . 14
|
88 | | fznn 10059 |
. . . . . . . . . . . . . . 15
|
89 | 43, 88 | syl 14 |
. . . . . . . . . . . . . 14
|
90 | 75, 87, 89 | mpbir2and 944 |
. . . . . . . . . . . . 13
|
91 | 67, 69, 90 | rspcdva 2844 |
. . . . . . . . . . . 12
|
92 | 62, 91 | jca 306 |
. . . . . . . . . . 11
|
93 | 67 | anbi2d 464 |
. . . . . . . . . . . . . 14
|
94 | | oveq2 5873 |
. . . . . . . . . . . . . . 15
|
95 | 94 | sbceq1d 2965 |
. . . . . . . . . . . . . 14
|
96 | 93, 95 | imbi12d 234 |
. . . . . . . . . . . . 13
|
97 | 96 | imbi2d 230 |
. . . . . . . . . . . 12
|
98 | | prmind2.8 |
. . . . . . . . . . . . . . 15
|
99 | 98 | ancoms 268 |
. . . . . . . . . . . . . 14
|
100 | | eluzelz 9510 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | adantl 277 |
. . . . . . . . . . . . . . . 16
|
102 | | eluzelz 9510 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | adantr 276 |
. . . . . . . . . . . . . . . 16
|
104 | 101, 103 | zmulcld 9354 |
. . . . . . . . . . . . . . 15
|
105 | | prmind.4 |
. . . . . . . . . . . . . . . 16
|
106 | 105 | sbcieg 2993 |
. . . . . . . . . . . . . . 15
|
107 | 104, 106 | syl 14 |
. . . . . . . . . . . . . 14
|
108 | 99, 107 | sylibrd 169 |
. . . . . . . . . . . . 13
|
109 | 108 | ex 115 |
. . . . . . . . . . . 12
|
110 | 97, 109 | vtoclga 2801 |
. . . . . . . . . . 11
|
111 | 56, 20, 92, 110 | syl3c 63 |
. . . . . . . . . 10
|
112 | 25, 111 | sbceq1dd 2966 |
. . . . . . . . 9
|
113 | 112 | rexlimdvaa 2593 |
. . . . . . . 8
|
114 | | ralnex 2463 |
. . . . . . . . 9
|
115 | | simpl 109 |
. . . . . . . . . . . . . 14
|
116 | | elnnuz 9537 |
. . . . . . . . . . . . . 14
|
117 | 115, 116 | sylib 122 |
. . . . . . . . . . . . 13
|
118 | | eluzp1p1 9526 |
. . . . . . . . . . . . 13
|
119 | 117, 118 | syl 14 |
. . . . . . . . . . . 12
|
120 | | df-2 8951 |
. . . . . . . . . . . . 13
|
121 | 120 | fveq2i 5510 |
. . . . . . . . . . . 12
|
122 | 119, 121 | eleqtrrdi 2269 |
. . . . . . . . . . 11
|
123 | | isprm3 12085 |
. . . . . . . . . . . 12
|
124 | 123 | baibr 920 |
. . . . . . . . . . 11
|
125 | 122, 124 | syl 14 |
. . . . . . . . . 10
|
126 | | simpr 110 |
. . . . . . . . . . . . 13
|
127 | 57 | cbvralv 2701 |
. . . . . . . . . . . . 13
|
128 | 126, 127 | sylib 122 |
. . . . . . . . . . . 12
|
129 | 115 | nncnd 8906 |
. . . . . . . . . . . . . . 15
|
130 | 129, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . 14
|
131 | 130 | oveq2d 5881 |
. . . . . . . . . . . . 13
|
132 | 131 | raleqdv 2676 |
. . . . . . . . . . . 12
|
133 | 128, 132 | mpbird 167 |
. . . . . . . . . . 11
|
134 | | nfcv 2317 |
. . . . . . . . . . . 12
|
135 | | nfv 1526 |
. . . . . . . . . . . . 13
|
136 | | nfsbc1v 2979 |
. . . . . . . . . . . . 13
|
137 | 135, 136 | nfim 1570 |
. . . . . . . . . . . 12
|
138 | | oveq1 5872 |
. . . . . . . . . . . . . . 15
|
139 | 138 | oveq2d 5881 |
. . . . . . . . . . . . . 14
|
140 | 139 | raleqdv 2676 |
. . . . . . . . . . . . 13
|
141 | | sbceq1a 2970 |
. . . . . . . . . . . . 13
|
142 | 140, 141 | imbi12d 234 |
. . . . . . . . . . . 12
|
143 | | prmind2.7 |
. . . . . . . . . . . . 13
|
144 | 143 | ex 115 |
. . . . . . . . . . . 12
|
145 | 134, 137,
142, 144 | vtoclgaf 2800 |
. . . . . . . . . . 11
|
146 | 133, 145 | syl5com 29 |
. . . . . . . . . 10
|
147 | 125, 146 | sylbid 150 |
. . . . . . . . 9
|
148 | 114, 147 | syl5bir 153 |
. . . . . . . 8
|
149 | | 2z 9254 |
. . . . . . . . . . 11
|
150 | 149 | a1i 9 |
. . . . . . . . . 10
|
151 | 115 | nnzd 9347 |
. . . . . . . . . . . 12
|
152 | 151 | peano2zd 9351 |
. . . . . . . . . . 11
|
153 | | 1zzd 9253 |
. . . . . . . . . . 11
|
154 | 152, 153 | zsubcld 9353 |
. . . . . . . . . 10
|
155 | 19, 21 | syl 14 |
. . . . . . . . . . 11
|
156 | | dvdsdc 11773 |
. . . . . . . . . . 11
DECID
|
157 | 155, 152,
156 | syl2anr 290 |
. . . . . . . . . 10
DECID
|
158 | 150, 154,
157 | exfzdc 10210 |
. . . . . . . . 9
DECID
|
159 | | exmiddc 836 |
. . . . . . . . 9
DECID |
160 | 158, 159 | syl 14 |
. . . . . . . 8
|
161 | 113, 148,
160 | mpjaod 718 |
. . . . . . 7
|
162 | 161 | ex 115 |
. . . . . 6
|
163 | | ralsnsg 3626 |
. . . . . . 7
|
164 | 16, 163 | syl 14 |
. . . . . 6
|
165 | 162, 164 | sylibrd 169 |
. . . . 5
|
166 | 165 | ancld 325 |
. . . 4
|
167 | | fzsuc 10039 |
. . . . . . 7
|
168 | 116, 167 | sylbi 121 |
. . . . . 6
|
169 | 168 | raleqdv 2676 |
. . . . 5
|
170 | | ralunb 3314 |
. . . . 5
|
171 | 169, 170 | bitrdi 196 |
. . . 4
|
172 | 166, 171 | sylibrd 169 |
. . 3
|
173 | 3, 5, 7, 9, 15, 172 | nnind 8908 |
. 2
|
174 | | elfz1end 10025 |
. . 3
|
175 | 174 | biimpi 120 |
. 2
|
176 | 1, 173, 175 | rspcdva 2844 |
1
|