Step | Hyp | Ref
| Expression |
1 | | cygctb.1 |
. . . . . . 7
|
2 | 1 | grpbn0 17451 |
. . . . . 6
|
3 | 2 | adantr 481 |
. . . . 5
|
4 | | 6re 11101 |
. . . . . . . 8
|
5 | | rexr 10085 |
. . . . . . . 8
|
6 | | pnfnlt 11962 |
. . . . . . . 8
|
7 | 4, 5, 6 | mp2b 10 |
. . . . . . 7
|
8 | | fvex 6201 |
. . . . . . . . . . . . 13
|
9 | 1, 8 | eqeltri 2697 |
. . . . . . . . . . . 12
|
10 | 9 | a1i 11 |
. . . . . . . . . . 11
|
11 | | hashinf 13122 |
. . . . . . . . . . 11
|
12 | 10, 11 | sylan 488 |
. . . . . . . . . 10
|
13 | 12 | breq1d 4663 |
. . . . . . . . 9
|
14 | 13 | biimpd 219 |
. . . . . . . 8
|
15 | 14 | impancom 456 |
. . . . . . 7
|
16 | 7, 15 | mt3i 141 |
. . . . . 6
|
17 | | hashnncl 13157 |
. . . . . 6
|
18 | 16, 17 | syl 17 |
. . . . 5
|
19 | 3, 18 | mpbird 247 |
. . . 4
|
20 | | nnuz 11723 |
. . . 4
|
21 | 19, 20 | syl6eleq 2711 |
. . 3
|
22 | | 6nn 11189 |
. . . . 5
|
23 | 22 | nnzi 11401 |
. . . 4
|
24 | 23 | a1i 11 |
. . 3
|
25 | | simpr 477 |
. . 3
|
26 | | elfzo2 12473 |
. . 3
..^ |
27 | 21, 24, 25, 26 | syl3anbrc 1246 |
. 2
..^ |
28 | | df-6 11083 |
. . . . . . 7
|
29 | 28 | oveq2i 6661 |
. . . . . 6
..^ ..^ |
30 | 29 | eleq2i 2693 |
. . . . 5
..^ ..^ |
31 | | 5nn 11188 |
. . . . . . 7
|
32 | 31, 20 | eleqtri 2699 |
. . . . . 6
|
33 | | fzosplitsni 12579 |
. . . . . 6
..^ ..^ |
34 | 32, 33 | ax-mp 5 |
. . . . 5
..^ ..^ |
35 | 30, 34 | bitri 264 |
. . . 4
..^ ..^ |
36 | | df-5 11082 |
. . . . . . . . 9
|
37 | 36 | oveq2i 6661 |
. . . . . . . 8
..^ ..^ |
38 | 37 | eleq2i 2693 |
. . . . . . 7
..^ ..^ |
39 | | 4nn 11187 |
. . . . . . . . 9
|
40 | 39, 20 | eleqtri 2699 |
. . . . . . . 8
|
41 | | fzosplitsni 12579 |
. . . . . . . 8
..^ ..^ |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
..^ ..^ |
43 | 38, 42 | bitri 264 |
. . . . . 6
..^ ..^ |
44 | | df-4 11081 |
. . . . . . . . . . 11
|
45 | 44 | oveq2i 6661 |
. . . . . . . . . 10
..^ ..^ |
46 | 45 | eleq2i 2693 |
. . . . . . . . 9
..^ ..^ |
47 | | 3nn 11186 |
. . . . . . . . . . 11
|
48 | 47, 20 | eleqtri 2699 |
. . . . . . . . . 10
|
49 | | fzosplitsni 12579 |
. . . . . . . . . 10
..^ ..^ |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . 9
..^ ..^ |
51 | 46, 50 | bitri 264 |
. . . . . . . 8
..^ ..^ |
52 | | df-3 11080 |
. . . . . . . . . . . . 13
|
53 | 52 | oveq2i 6661 |
. . . . . . . . . . . 12
..^ ..^ |
54 | 53 | eleq2i 2693 |
. . . . . . . . . . 11
..^ ..^ |
55 | | 2eluzge1 11734 |
. . . . . . . . . . . 12
|
56 | | fzosplitsni 12579 |
. . . . . . . . . . . 12
..^ ..^ |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . 11
..^ ..^ |
58 | 54, 57 | bitri 264 |
. . . . . . . . . 10
..^ ..^ |
59 | | elsni 4194 |
. . . . . . . . . . . . . . . . 17
|
60 | | fzo12sn 12551 |
. . . . . . . . . . . . . . . . 17
..^ |
61 | 59, 60 | eleq2s 2719 |
. . . . . . . . . . . . . . . 16
..^ |
62 | 61 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ |
63 | | hash1 13192 |
. . . . . . . . . . . . . . 15
|
64 | 62, 63 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
..^ |
65 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . 17
|
66 | 62, 65 | syl6eqel 2709 |
. . . . . . . . . . . . . . . 16
..^ |
67 | | hashclb 13149 |
. . . . . . . . . . . . . . . . 17
|
68 | 9, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
69 | 66, 68 | sylibr 224 |
. . . . . . . . . . . . . . 15
..^ |
70 | | 1onn 7719 |
. . . . . . . . . . . . . . . 16
|
71 | | nnfi 8153 |
. . . . . . . . . . . . . . . 16
|
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
73 | | hashen 13135 |
. . . . . . . . . . . . . . 15
|
74 | 69, 72, 73 | sylancl 694 |
. . . . . . . . . . . . . 14
..^ |
75 | 64, 74 | mpbid 222 |
. . . . . . . . . . . . 13
..^ |
76 | 1 | 0cyg 18294 |
. . . . . . . . . . . . . 14
CycGrp |
77 | | cygabl 18292 |
. . . . . . . . . . . . . 14
CycGrp |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . 13
|
79 | 75, 78 | syldan 487 |
. . . . . . . . . . . 12
..^ |
80 | 79 | ex 450 |
. . . . . . . . . . 11
..^
|
81 | | id 22 |
. . . . . . . . . . . . 13
|
82 | | 2prm 15405 |
. . . . . . . . . . . . 13
|
83 | 81, 82 | syl6eqel 2709 |
. . . . . . . . . . . 12
|
84 | 1 | prmcyg 18295 |
. . . . . . . . . . . . . 14
CycGrp |
85 | 84, 77 | syl 17 |
. . . . . . . . . . . . 13
|
86 | 85 | ex 450 |
. . . . . . . . . . . 12
|
87 | 83, 86 | syl5 34 |
. . . . . . . . . . 11
|
88 | 80, 87 | jaod 395 |
. . . . . . . . . 10
..^ |
89 | 58, 88 | syl5bi 232 |
. . . . . . . . 9
..^
|
90 | | id 22 |
. . . . . . . . . . 11
|
91 | | 3prm 15406 |
. . . . . . . . . . 11
|
92 | 90, 91 | syl6eqel 2709 |
. . . . . . . . . 10
|
93 | 92, 86 | syl5 34 |
. . . . . . . . 9
|
94 | 89, 93 | jaod 395 |
. . . . . . . 8
..^ |
95 | 51, 94 | syl5bi 232 |
. . . . . . 7
..^
|
96 | | simpl 473 |
. . . . . . . . . . 11
|
97 | | 2z 11409 |
. . . . . . . . . . 11
|
98 | | eqid 2622 |
. . . . . . . . . . . 12
gEx gEx |
99 | | eqid 2622 |
. . . . . . . . . . . 12
|
100 | 1, 98, 99 | gexdvds2 18000 |
. . . . . . . . . . 11
gEx
|
101 | 96, 97, 100 | sylancl 694 |
. . . . . . . . . 10
gEx
|
102 | 1, 98 | gex2abl 18254 |
. . . . . . . . . . . 12
gEx |
103 | 102 | ex 450 |
. . . . . . . . . . 11
gEx
|
104 | 103 | adantr 481 |
. . . . . . . . . 10
gEx
|
105 | 101, 104 | sylbird 250 |
. . . . . . . . 9
|
106 | | rexnal 2995 |
. . . . . . . . . 10
|
107 | 96 | adantr 481 |
. . . . . . . . . . . . 13
|
108 | | simprl 794 |
. . . . . . . . . . . . 13
|
109 | 1, 99 | odcl 17955 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
|
111 | | 4nn0 11311 |
. . . . . . . . . . . . . . . 16
|
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . 15
|
113 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
114 | 113, 111 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 114, 68 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
117 | 1, 99 | oddvds2 17983 |
. . . . . . . . . . . . . . . . 17
|
118 | 107, 116,
108, 117 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
119 | 113 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
120 | 118, 119 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
|
121 | | sq2 12960 |
. . . . . . . . . . . . . . . . 17
|
122 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
123 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
125 | 1, 99 | odcl2 17982 |
. . . . . . . . . . . . . . . . . . . . . 22
|
126 | 107, 116,
108, 125 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
|
127 | | pccl 15554 |
. . . . . . . . . . . . . . . . . . . . 21
|
128 | 82, 126, 127 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 128 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
|
130 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . . 20
|
131 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
132 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
133 | 132 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
134 | 97, 128, 133 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
135 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
136 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
137 | 129, 135,
136 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
138 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
139 | 138, 121 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
140 | 139 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
141 | 140 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
142 | 123, 120,
141 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
143 | | pcprmpw2 15586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
144 | 82, 126, 143 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
145 | 142, 144 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
146 | 145 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
147 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
148 | | exp1 12866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
149 | 147, 148 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
150 | 149 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
151 | 146, 150 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
152 | 134, 137,
151 | 3imtr3d 282 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
153 | 131, 152 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . 22
|
154 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
155 | 128 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
156 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
157 | 154, 155,
156 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
|
158 | 153, 157 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
|
159 | | nn0ltp1le 11435 |
. . . . . . . . . . . . . . . . . . . . . 22
|
160 | 65, 128, 159 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
|
161 | 158, 160 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
162 | 130, 161 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . 19
|
163 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
|
164 | 122, 129,
162, 163 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
|
165 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . 18
|
166 | 122, 124,
164, 165 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
167 | 121, 166 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . 16
|
168 | 167, 145 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
|
169 | | dvdseq 15036 |
. . . . . . . . . . . . . . 15
|
170 | 110, 112,
120, 168, 169 | syl22anc 1327 |
. . . . . . . . . . . . . 14
|
171 | 170, 119 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
172 | 1, 99, 107, 108, 171 | iscygodd 18290 |
. . . . . . . . . . . 12
CycGrp |
173 | 172, 77 | syl 17 |
. . . . . . . . . . 11
|
174 | 173 | rexlimdvaa 3032 |
. . . . . . . . . 10
|
175 | 106, 174 | syl5bir 233 |
. . . . . . . . 9
|
176 | 105, 175 | pm2.61d 170 |
. . . . . . . 8
|
177 | 176 | ex 450 |
. . . . . . 7
|
178 | 95, 177 | jaod 395 |
. . . . . 6
..^ |
179 | 43, 178 | syl5bi 232 |
. . . . 5
..^
|
180 | | id 22 |
. . . . . . 7
|
181 | | 5prm 15815 |
. . . . . . 7
|
182 | 180, 181 | syl6eqel 2709 |
. . . . . 6
|
183 | 182, 86 | syl5 34 |
. . . . 5
|
184 | 179, 183 | jaod 395 |
. . . 4
..^ |
185 | 35, 184 | syl5bi 232 |
. . 3
..^
|
186 | 185 | imp 445 |
. 2
..^ |
187 | 27, 186 | syldan 487 |
1
|