Step | Hyp | Ref
| Expression |
1 | | pcmpt.3 |
. 2
|
2 | | fveq2 6191 |
. . . . . 6
|
3 | 2 | oveq2d 6666 |
. . . . 5
|
4 | | breq2 4657 |
. . . . . 6
|
5 | 4 | ifbid 4108 |
. . . . 5
|
6 | 3, 5 | eqeq12d 2637 |
. . . 4
|
7 | 6 | imbi2d 330 |
. . 3
|
8 | | fveq2 6191 |
. . . . . 6
|
9 | 8 | oveq2d 6666 |
. . . . 5
|
10 | | breq2 4657 |
. . . . . 6
|
11 | 10 | ifbid 4108 |
. . . . 5
|
12 | 9, 11 | eqeq12d 2637 |
. . . 4
|
13 | 12 | imbi2d 330 |
. . 3
|
14 | | fveq2 6191 |
. . . . . 6
|
15 | 14 | oveq2d 6666 |
. . . . 5
|
16 | | breq2 4657 |
. . . . . 6
|
17 | 16 | ifbid 4108 |
. . . . 5
|
18 | 15, 17 | eqeq12d 2637 |
. . . 4
|
19 | 18 | imbi2d 330 |
. . 3
|
20 | | fveq2 6191 |
. . . . . 6
|
21 | 20 | oveq2d 6666 |
. . . . 5
|
22 | | breq2 4657 |
. . . . . 6
|
23 | 22 | ifbid 4108 |
. . . . 5
|
24 | 21, 23 | eqeq12d 2637 |
. . . 4
|
25 | 24 | imbi2d 330 |
. . 3
|
26 | | pcmpt.4 |
. . . 4
|
27 | | 1z 11407 |
. . . . . . . . 9
|
28 | | seq1 12814 |
. . . . . . . . 9
|
29 | 27, 28 | ax-mp 5 |
. . . . . . . 8
|
30 | | 1nn 11031 |
. . . . . . . . 9
|
31 | | 1nprm 15392 |
. . . . . . . . . . . 12
|
32 | | eleq1 2689 |
. . . . . . . . . . . 12
|
33 | 31, 32 | mtbiri 317 |
. . . . . . . . . . 11
|
34 | 33 | iffalsed 4097 |
. . . . . . . . . 10
|
35 | | pcmpt.1 |
. . . . . . . . . 10
|
36 | | 1ex 10035 |
. . . . . . . . . 10
|
37 | 34, 35, 36 | fvmpt 6282 |
. . . . . . . . 9
|
38 | 30, 37 | ax-mp 5 |
. . . . . . . 8
|
39 | 29, 38 | eqtri 2644 |
. . . . . . 7
|
40 | 39 | oveq2i 6661 |
. . . . . 6
|
41 | | pc1 15560 |
. . . . . 6
|
42 | 40, 41 | syl5eq 2668 |
. . . . 5
|
43 | | prmgt1 15409 |
. . . . . . 7
|
44 | | 1re 10039 |
. . . . . . . 8
|
45 | | prmuz2 15408 |
. . . . . . . . 9
|
46 | | eluzelre 11698 |
. . . . . . . . 9
|
47 | 45, 46 | syl 17 |
. . . . . . . 8
|
48 | | ltnle 10117 |
. . . . . . . 8
|
49 | 44, 47, 48 | sylancr 695 |
. . . . . . 7
|
50 | 43, 49 | mpbid 222 |
. . . . . 6
|
51 | 50 | iffalsed 4097 |
. . . . 5
|
52 | 42, 51 | eqtr4d 2659 |
. . . 4
|
53 | 26, 52 | syl 17 |
. . 3
|
54 | 26 | adantr 481 |
. . . . . . . . . . . . 13
|
55 | | pcmpt.2 |
. . . . . . . . . . . . . . . . 17
|
56 | 35, 55 | pcmptcl 15595 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | simpld 475 |
. . . . . . . . . . . . . . 15
|
58 | | peano2nn 11032 |
. . . . . . . . . . . . . . 15
|
59 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
|
60 | 57, 58, 59 | syl2an 494 |
. . . . . . . . . . . . . 14
|
61 | 60 | adantrr 753 |
. . . . . . . . . . . . 13
|
62 | 54, 61 | pccld 15555 |
. . . . . . . . . . . 12
|
63 | 62 | nn0cnd 11353 |
. . . . . . . . . . 11
|
64 | 63 | addid2d 10237 |
. . . . . . . . . 10
|
65 | 58 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
66 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
67 | 66, 36 | ifex 4156 |
. . . . . . . . . . . . . 14
|
68 | 67 | csbex 4793 |
. . . . . . . . . . . . 13
|
69 | 35 | fvmpts 6285 |
. . . . . . . . . . . . . 14
|
70 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
71 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
72 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
73 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
74 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . 17
|
75 | 72, 73, 74 | nfov 6676 |
. . . . . . . . . . . . . . . 16
|
76 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
77 | 71, 75, 76 | nfif 4115 |
. . . . . . . . . . . . . . 15
|
78 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
79 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
80 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . 17
|
81 | 79, 80 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
82 | 78, 81 | ifbieq1d 4109 |
. . . . . . . . . . . . . . 15
|
83 | 70, 77, 82 | csbief 3558 |
. . . . . . . . . . . . . 14
|
84 | 69, 83 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
85 | 65, 68, 84 | sylancl 694 |
. . . . . . . . . . . 12
|
86 | | simprr 796 |
. . . . . . . . . . . . . 14
|
87 | 86, 54 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
88 | 87 | iftrued 4094 |
. . . . . . . . . . . 12
|
89 | 86 | csbeq1d 3540 |
. . . . . . . . . . . . . 14
|
90 | | nfcvd 2765 |
. . . . . . . . . . . . . . . 16
|
91 | | pcmpt.5 |
. . . . . . . . . . . . . . . 16
|
92 | 90, 91 | csbiegf 3557 |
. . . . . . . . . . . . . . 15
|
93 | 54, 92 | syl 17 |
. . . . . . . . . . . . . 14
|
94 | 89, 93 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
95 | 86, 94 | oveq12d 6668 |
. . . . . . . . . . . 12
|
96 | 85, 88, 95 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
97 | 96 | oveq2d 6666 |
. . . . . . . . . 10
|
98 | 91 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
99 | 98 | rspcv 3305 |
. . . . . . . . . . . . 13
|
100 | 26, 55, 99 | sylc 65 |
. . . . . . . . . . . 12
|
101 | 100 | adantr 481 |
. . . . . . . . . . 11
|
102 | | pcidlem 15576 |
. . . . . . . . . . 11
|
103 | 54, 101, 102 | syl2anc 693 |
. . . . . . . . . 10
|
104 | 64, 97, 103 | 3eqtrd 2660 |
. . . . . . . . 9
|
105 | | oveq1 6657 |
. . . . . . . . . 10
|
106 | 105 | eqeq1d 2624 |
. . . . . . . . 9
|
107 | 104, 106 | syl5ibrcom 237 |
. . . . . . . 8
|
108 | | nnre 11027 |
. . . . . . . . . . . . 13
|
109 | 108 | ad2antrl 764 |
. . . . . . . . . . . 12
|
110 | | ltp1 10861 |
. . . . . . . . . . . . 13
|
111 | | peano2re 10209 |
. . . . . . . . . . . . . 14
|
112 | | ltnle 10117 |
. . . . . . . . . . . . . 14
|
113 | 111, 112 | mpdan 702 |
. . . . . . . . . . . . 13
|
114 | 110, 113 | mpbid 222 |
. . . . . . . . . . . 12
|
115 | 109, 114 | syl 17 |
. . . . . . . . . . 11
|
116 | 86 | breq1d 4663 |
. . . . . . . . . . 11
|
117 | 115, 116 | mtbid 314 |
. . . . . . . . . 10
|
118 | 117 | iffalsed 4097 |
. . . . . . . . 9
|
119 | 118 | eqeq2d 2632 |
. . . . . . . 8
|
120 | | simpr 477 |
. . . . . . . . . . . . . 14
|
121 | | nnuz 11723 |
. . . . . . . . . . . . . 14
|
122 | 120, 121 | syl6eleq 2711 |
. . . . . . . . . . . . 13
|
123 | | seqp1 12816 |
. . . . . . . . . . . . 13
|
124 | 122, 123 | syl 17 |
. . . . . . . . . . . 12
|
125 | 124 | oveq2d 6666 |
. . . . . . . . . . 11
|
126 | 26 | adantr 481 |
. . . . . . . . . . . 12
|
127 | 56 | simprd 479 |
. . . . . . . . . . . . . 14
|
128 | 127 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
129 | | nnz 11399 |
. . . . . . . . . . . . . 14
|
130 | | nnne0 11053 |
. . . . . . . . . . . . . 14
|
131 | 129, 130 | jca 554 |
. . . . . . . . . . . . 13
|
132 | 128, 131 | syl 17 |
. . . . . . . . . . . 12
|
133 | | nnz 11399 |
. . . . . . . . . . . . . 14
|
134 | | nnne0 11053 |
. . . . . . . . . . . . . 14
|
135 | 133, 134 | jca 554 |
. . . . . . . . . . . . 13
|
136 | 60, 135 | syl 17 |
. . . . . . . . . . . 12
|
137 | | pcmul 15556 |
. . . . . . . . . . . 12
|
138 | 126, 132,
136, 137 | syl3anc 1326 |
. . . . . . . . . . 11
|
139 | 125, 138 | eqtrd 2656 |
. . . . . . . . . 10
|
140 | 139 | adantrr 753 |
. . . . . . . . 9
|
141 | | prmnn 15388 |
. . . . . . . . . . . . . . 15
|
142 | 26, 141 | syl 17 |
. . . . . . . . . . . . . 14
|
143 | 142 | nnred 11035 |
. . . . . . . . . . . . 13
|
144 | 143 | adantr 481 |
. . . . . . . . . . . 12
|
145 | 144 | leidd 10594 |
. . . . . . . . . . 11
|
146 | 145, 86 | breqtrrd 4681 |
. . . . . . . . . 10
|
147 | 146 | iftrued 4094 |
. . . . . . . . 9
|
148 | 140, 147 | eqeq12d 2637 |
. . . . . . . 8
|
149 | 107, 119,
148 | 3imtr4d 283 |
. . . . . . 7
|
150 | 149 | expr 643 |
. . . . . 6
|
151 | 139 | adantrr 753 |
. . . . . . . . . 10
|
152 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
153 | 152 | necomd 2849 |
. . . . . . . . . . . . . . 15
|
154 | 26 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
155 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
156 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
157 | 74 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . 19
|
158 | 80 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
159 | 157, 158 | rspc 3303 |
. . . . . . . . . . . . . . . . . 18
|
160 | 155, 156,
159 | sylc 65 |
. . . . . . . . . . . . . . . . 17
|
161 | | prmdvdsexpr 15429 |
. . . . . . . . . . . . . . . . 17
|
162 | 154, 155,
160, 161 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
163 | 162 | necon3ad 2807 |
. . . . . . . . . . . . . . 15
|
164 | 153, 163 | mpd 15 |
. . . . . . . . . . . . . 14
|
165 | 58 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
|
166 | 165, 68, 84 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
167 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
168 | 166, 167 | sylan9eq 2676 |
. . . . . . . . . . . . . . 15
|
169 | 168 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
170 | 164, 169 | mtbird 315 |
. . . . . . . . . . . . 13
|
171 | 57 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
172 | 171, 165,
59 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
173 | 172 | adantr 481 |
. . . . . . . . . . . . . 14
|
174 | | pceq0 15575 |
. . . . . . . . . . . . . 14
|
175 | 154, 173,
174 | syl2anc 693 |
. . . . . . . . . . . . 13
|
176 | 170, 175 | mpbird 247 |
. . . . . . . . . . . 12
|
177 | | iffalse 4095 |
. . . . . . . . . . . . . . 15
|
178 | 166, 177 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
|
179 | 178 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
180 | 26, 41 | syl 17 |
. . . . . . . . . . . . . 14
|
181 | 180 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
182 | 179, 181 | eqtrd 2656 |
. . . . . . . . . . . 12
|
183 | 176, 182 | pm2.61dan 832 |
. . . . . . . . . . 11
|
184 | 183 | oveq2d 6666 |
. . . . . . . . . 10
|
185 | 26 | adantr 481 |
. . . . . . . . . . . . 13
|
186 | 128 | adantrr 753 |
. . . . . . . . . . . . 13
|
187 | 185, 186 | pccld 15555 |
. . . . . . . . . . . 12
|
188 | 187 | nn0cnd 11353 |
. . . . . . . . . . 11
|
189 | 188 | addid1d 10236 |
. . . . . . . . . 10
|
190 | 151, 184,
189 | 3eqtrd 2660 |
. . . . . . . . 9
|
191 | 142 | adantr 481 |
. . . . . . . . . . . . 13
|
192 | 191 | nnred 11035 |
. . . . . . . . . . . 12
|
193 | 165 | nnred 11035 |
. . . . . . . . . . . 12
|
194 | 192, 193 | ltlend 10182 |
. . . . . . . . . . 11
|
195 | | simprl 794 |
. . . . . . . . . . . 12
|
196 | | nnleltp1 11432 |
. . . . . . . . . . . 12
|
197 | 191, 195,
196 | syl2anc 693 |
. . . . . . . . . . 11
|
198 | | simprr 796 |
. . . . . . . . . . . 12
|
199 | 198 | biantrud 528 |
. . . . . . . . . . 11
|
200 | 194, 197,
199 | 3bitr4rd 301 |
. . . . . . . . . 10
|
201 | 200 | ifbid 4108 |
. . . . . . . . 9
|
202 | 190, 201 | eqeq12d 2637 |
. . . . . . . 8
|
203 | 202 | biimprd 238 |
. . . . . . 7
|
204 | 203 | expr 643 |
. . . . . 6
|
205 | 150, 204 | pm2.61dne 2880 |
. . . . 5
|
206 | 205 | expcom 451 |
. . . 4
|
207 | 206 | a2d 29 |
. . 3
|
208 | 7, 13, 19, 25, 53, 207 | nnind 11038 |
. 2
|
209 | 1, 208 | mpcom 38 |
1
|