Step | Hyp | Ref
| Expression |
1 | | elfz1end 12371 |
. . 3
|
2 | 1 | biimpi 206 |
. 2
|
3 | | oveq2 6658 |
. . . 4
|
4 | 3 | raleqdv 3144 |
. . 3
|
5 | | oveq2 6658 |
. . . 4
|
6 | 5 | raleqdv 3144 |
. . 3
|
7 | | oveq2 6658 |
. . . 4
|
8 | 7 | raleqdv 3144 |
. . 3
|
9 | | oveq2 6658 |
. . . 4
|
10 | 9 | raleqdv 3144 |
. . 3
|
11 | | prmind.6 |
. . . . 5
|
12 | | elfz1eq 12352 |
. . . . . 6
|
13 | | prmind.1 |
. . . . . 6
|
14 | 12, 13 | syl 17 |
. . . . 5
|
15 | 11, 14 | mpbiri 248 |
. . . 4
|
16 | 15 | rgen 2922 |
. . 3
|
17 | | peano2nn 11032 |
. . . . . . . . . . . . 13
|
18 | 17 | ad2antrr 762 |
. . . . . . . . . . . 12
|
19 | 18 | nncnd 11036 |
. . . . . . . . . . 11
|
20 | | elfzuz 12338 |
. . . . . . . . . . . . . 14
|
21 | 20 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
22 | | eluz2nn 11726 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
|
24 | 23 | nncnd 11036 |
. . . . . . . . . . 11
|
25 | 23 | nnne0d 11065 |
. . . . . . . . . . 11
|
26 | 19, 24, 25 | divcan2d 10803 |
. . . . . . . . . 10
|
27 | | simprr 796 |
. . . . . . . . . . . . 13
|
28 | 23 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
29 | 18 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
30 | | dvdsval2 14986 |
. . . . . . . . . . . . . 14
|
31 | 28, 25, 29, 30 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
32 | 27, 31 | mpbid 222 |
. . . . . . . . . . . 12
|
33 | 24 | mulid2d 10058 |
. . . . . . . . . . . . . 14
|
34 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . 17
|
35 | 34 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
|
36 | | nncn 11028 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
38 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
|
39 | | pncan 10287 |
. . . . . . . . . . . . . . . . 17
|
40 | 37, 38, 39 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
41 | 35, 40 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
|
42 | | nnz 11399 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
44 | | zleltp1 11428 |
. . . . . . . . . . . . . . . 16
|
45 | 28, 43, 44 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
46 | 41, 45 | mpbid 222 |
. . . . . . . . . . . . . 14
|
47 | 33, 46 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
48 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
49 | 18 | nnred 11035 |
. . . . . . . . . . . . . 14
|
50 | 23 | nnred 11035 |
. . . . . . . . . . . . . 14
|
51 | 23 | nngt0d 11064 |
. . . . . . . . . . . . . 14
|
52 | | ltmuldiv 10896 |
. . . . . . . . . . . . . 14
|
53 | 48, 49, 50, 51, 52 | syl112anc 1330 |
. . . . . . . . . . . . 13
|
54 | 47, 53 | mpbid 222 |
. . . . . . . . . . . 12
|
55 | | eluz2b1 11759 |
. . . . . . . . . . . 12
|
56 | 32, 54, 55 | sylanbrc 698 |
. . . . . . . . . . 11
|
57 | | fznn 12408 |
. . . . . . . . . . . . . . 15
|
58 | 43, 57 | syl 17 |
. . . . . . . . . . . . . 14
|
59 | 23, 41, 58 | mpbir2and 957 |
. . . . . . . . . . . . 13
|
60 | | simplr 792 |
. . . . . . . . . . . . 13
|
61 | | prmind.2 |
. . . . . . . . . . . . . 14
|
62 | 61 | rspcv 3305 |
. . . . . . . . . . . . 13
|
63 | 59, 60, 62 | sylc 65 |
. . . . . . . . . . . 12
|
64 | 18 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
|
65 | 23 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
|
66 | 64, 65 | rpdivcld 11889 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | rpgt0d 11875 |
. . . . . . . . . . . . . . 15
|
68 | | elnnz 11387 |
. . . . . . . . . . . . . . 15
|
69 | 32, 67, 68 | sylanbrc 698 |
. . . . . . . . . . . . . 14
|
70 | 18 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . 18
|
71 | 19, 70 | dividd 10799 |
. . . . . . . . . . . . . . . . 17
|
72 | | eluz2b2 11761 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 72 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
|
74 | 21, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
75 | 71, 74 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . 16
|
76 | 18 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
|
77 | | ltdiv23 10914 |
. . . . . . . . . . . . . . . . 17
|
78 | 49, 49, 76, 50, 51, 77 | syl122anc 1335 |
. . . . . . . . . . . . . . . 16
|
79 | 75, 78 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
80 | | zleltp1 11428 |
. . . . . . . . . . . . . . . 16
|
81 | 32, 43, 80 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
82 | 79, 81 | mpbird 247 |
. . . . . . . . . . . . . 14
|
83 | | fznn 12408 |
. . . . . . . . . . . . . . 15
|
84 | 43, 83 | syl 17 |
. . . . . . . . . . . . . 14
|
85 | 69, 82, 84 | mpbir2and 957 |
. . . . . . . . . . . . 13
|
86 | | prmind.3 |
. . . . . . . . . . . . . . 15
|
87 | 86 | cbvralv 3171 |
. . . . . . . . . . . . . 14
|
88 | 60, 87 | sylib 208 |
. . . . . . . . . . . . 13
|
89 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
90 | 89, 86 | sbcie 3470 |
. . . . . . . . . . . . . . 15
|
91 | | dfsbcq 3437 |
. . . . . . . . . . . . . . 15
|
92 | 90, 91 | syl5bbr 274 |
. . . . . . . . . . . . . 14
|
93 | 92 | rspcv 3305 |
. . . . . . . . . . . . 13
|
94 | 85, 88, 93 | sylc 65 |
. . . . . . . . . . . 12
|
95 | 63, 94 | jca 554 |
. . . . . . . . . . 11
|
96 | 92 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
97 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
98 | | prmind.4 |
. . . . . . . . . . . . . . . 16
|
99 | 97, 98 | sbcie 3470 |
. . . . . . . . . . . . . . 15
|
100 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | sbceq1d 3440 |
. . . . . . . . . . . . . . 15
|
102 | 99, 101 | syl5bbr 274 |
. . . . . . . . . . . . . 14
|
103 | 96, 102 | imbi12d 334 |
. . . . . . . . . . . . 13
|
104 | 103 | imbi2d 330 |
. . . . . . . . . . . 12
|
105 | | prmind2.8 |
. . . . . . . . . . . . 13
|
106 | 105 | expcom 451 |
. . . . . . . . . . . 12
|
107 | 104, 106 | vtoclga 3272 |
. . . . . . . . . . 11
|
108 | 56, 21, 95, 107 | syl3c 66 |
. . . . . . . . . 10
|
109 | 26, 108 | sbceq1dd 3441 |
. . . . . . . . 9
|
110 | 109 | rexlimdvaa 3032 |
. . . . . . . 8
|
111 | | ralnex 2992 |
. . . . . . . . 9
|
112 | | simpl 473 |
. . . . . . . . . . . . . 14
|
113 | | elnnuz 11724 |
. . . . . . . . . . . . . 14
|
114 | 112, 113 | sylib 208 |
. . . . . . . . . . . . 13
|
115 | | eluzp1p1 11713 |
. . . . . . . . . . . . 13
|
116 | 114, 115 | syl 17 |
. . . . . . . . . . . 12
|
117 | | df-2 11079 |
. . . . . . . . . . . . 13
|
118 | 117 | fveq2i 6194 |
. . . . . . . . . . . 12
|
119 | 116, 118 | syl6eleqr 2712 |
. . . . . . . . . . 11
|
120 | | isprm3 15396 |
. . . . . . . . . . . 12
|
121 | 120 | baibr 945 |
. . . . . . . . . . 11
|
122 | 119, 121 | syl 17 |
. . . . . . . . . 10
|
123 | | simpr 477 |
. . . . . . . . . . . . 13
|
124 | 61 | cbvralv 3171 |
. . . . . . . . . . . . 13
|
125 | 123, 124 | sylib 208 |
. . . . . . . . . . . 12
|
126 | 112 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
127 | 126, 38, 39 | sylancl 694 |
. . . . . . . . . . . . . 14
|
128 | 127 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
129 | 128 | raleqdv 3144 |
. . . . . . . . . . . 12
|
130 | 125, 129 | mpbird 247 |
. . . . . . . . . . 11
|
131 | | nfcv 2764 |
. . . . . . . . . . . 12
|
132 | | nfv 1843 |
. . . . . . . . . . . . 13
|
133 | | nfsbc1v 3455 |
. . . . . . . . . . . . 13
|
134 | 132, 133 | nfim 1825 |
. . . . . . . . . . . 12
|
135 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
136 | 135 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
137 | 136 | raleqdv 3144 |
. . . . . . . . . . . . 13
|
138 | | sbceq1a 3446 |
. . . . . . . . . . . . 13
|
139 | 137, 138 | imbi12d 334 |
. . . . . . . . . . . 12
|
140 | | prmind2.7 |
. . . . . . . . . . . . 13
|
141 | 140 | ex 450 |
. . . . . . . . . . . 12
|
142 | 131, 134,
139, 141 | vtoclgaf 3271 |
. . . . . . . . . . 11
|
143 | 130, 142 | syl5com 31 |
. . . . . . . . . 10
|
144 | 122, 143 | sylbid 230 |
. . . . . . . . 9
|
145 | 111, 144 | syl5bir 233 |
. . . . . . . 8
|
146 | 110, 145 | pm2.61d 170 |
. . . . . . 7
|
147 | 146 | ex 450 |
. . . . . 6
|
148 | | ralsnsg 4216 |
. . . . . . 7
|
149 | 17, 148 | syl 17 |
. . . . . 6
|
150 | 147, 149 | sylibrd 249 |
. . . . 5
|
151 | 150 | ancld 576 |
. . . 4
|
152 | | fzsuc 12388 |
. . . . . . 7
|
153 | 113, 152 | sylbi 207 |
. . . . . 6
|
154 | 153 | raleqdv 3144 |
. . . . 5
|
155 | | ralunb 3794 |
. . . . 5
|
156 | 154, 155 | syl6bb 276 |
. . . 4
|
157 | 151, 156 | sylibrd 249 |
. . 3
|
158 | 4, 6, 8, 10, 16, 157 | nnind 11038 |
. 2
|
159 | | prmind.5 |
. . 3
|
160 | 159 | rspcv 3305 |
. 2
|
161 | 2, 158, 160 | sylc 65 |
1
|