Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
|
2 | | lgseisen.1 |
. . . . 5
|
3 | | lgseisen.3 |
. . . . . 6
|
4 | 3 | necomd 2849 |
. . . . 5
|
5 | | lgsquad.5 |
. . . . 5
|
6 | | lgsquad.4 |
. . . . 5
|
7 | | eleq1 2689 |
. . . . . . . . . 10
|
8 | | eleq1 2689 |
. . . . . . . . . 10
|
9 | 7, 8 | bi2anan9 917 |
. . . . . . . . 9
|
10 | | ancom 466 |
. . . . . . . . 9
|
11 | 9, 10 | syl6bb 276 |
. . . . . . . 8
|
12 | | oveq1 6657 |
. . . . . . . . 9
|
13 | | oveq1 6657 |
. . . . . . . . 9
|
14 | 12, 13 | breqan12d 4669 |
. . . . . . . 8
|
15 | 11, 14 | anbi12d 747 |
. . . . . . 7
|
16 | 15 | ancoms 469 |
. . . . . 6
|
17 | 16 | cbvopabv 4722 |
. . . . 5
|
18 | 1, 2, 4, 5, 6, 17 | lgsquadlem2 25106 |
. . . 4
|
19 | | relopab 5247 |
. . . . . . . 8
|
20 | | fzfid 12772 |
. . . . . . . . . 10
|
21 | | fzfid 12772 |
. . . . . . . . . 10
|
22 | | xpfi 8231 |
. . . . . . . . . 10
|
23 | 20, 21, 22 | syl2anc 693 |
. . . . . . . . 9
|
24 | | opabssxp 5193 |
. . . . . . . . 9
|
25 | | ssfi 8180 |
. . . . . . . . 9
|
26 | 23, 24, 25 | sylancl 694 |
. . . . . . . 8
|
27 | | cnven 8032 |
. . . . . . . 8
|
28 | 19, 26, 27 | sylancr 695 |
. . . . . . 7
|
29 | | cnvopab 5533 |
. . . . . . 7
|
30 | 28, 29 | syl6breq 4694 |
. . . . . 6
|
31 | | hasheni 13136 |
. . . . . 6
|
32 | 30, 31 | syl 17 |
. . . . 5
|
33 | 32 | oveq2d 6666 |
. . . 4
|
34 | 18, 33 | eqtr4d 2659 |
. . 3
|
35 | | lgsquad.6 |
. . . 4
|
36 | 2, 1, 3, 6, 5, 35 | lgsquadlem2 25106 |
. . 3
|
37 | 34, 36 | oveq12d 6668 |
. 2
|
38 | | neg1cn 11124 |
. . . 4
|
39 | 38 | a1i 11 |
. . 3
|
40 | | opabssxp 5193 |
. . . . . 6
|
41 | 35, 40 | eqsstri 3635 |
. . . . 5
|
42 | | ssfi 8180 |
. . . . 5
|
43 | 23, 41, 42 | sylancl 694 |
. . . 4
|
44 | | hashcl 13147 |
. . . 4
|
45 | 43, 44 | syl 17 |
. . 3
|
46 | | hashcl 13147 |
. . . 4
|
47 | 26, 46 | syl 17 |
. . 3
|
48 | 39, 45, 47 | expaddd 13010 |
. 2
|
49 | 1 | eldifad 3586 |
. . . . . . . . . . . . . . . . 17
|
50 | 49 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
51 | | prmnn 15388 |
. . . . . . . . . . . . . . . 16
|
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
|
53 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
55 | 5, 54 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 56 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
58 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
60 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
62 | 56 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 61 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
|
64 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
65 | 50, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | | uz2m1nn 11763 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 67 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 5, 70 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 62, 63, 71 | ltled 10185 |
. . . . . . . . . . . . . . . . . 18
|
73 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . 18
|
74 | 57, 61, 72, 73 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . 17
|
75 | | fzss2 12381 |
. . . . . . . . . . . . . . . . 17
|
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
|
77 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
78 | 76, 77 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
79 | | fzm1ndvds 15044 |
. . . . . . . . . . . . . . 15
|
80 | 52, 78, 79 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
81 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
82 | 2 | eldifad 3586 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
84 | | prmrp 15424 |
. . . . . . . . . . . . . . . . 17
|
85 | 50, 83, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
86 | 81, 85 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
87 | | prmz 15389 |
. . . . . . . . . . . . . . . . 17
|
88 | 83, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
|
89 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . 17
|
90 | 89 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
|
91 | | coprmdvds 15366 |
. . . . . . . . . . . . . . . 16
|
92 | 59, 88, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
93 | 86, 92 | mpan2d 710 |
. . . . . . . . . . . . . 14
|
94 | 80, 93 | mtod 189 |
. . . . . . . . . . . . 13
|
95 | | prmnn 15388 |
. . . . . . . . . . . . . . . . 17
|
96 | 83, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
|
97 | 96 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
98 | | elfznn 12370 |
. . . . . . . . . . . . . . . . 17
|
99 | 98 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
101 | 97, 100 | mulcomd 10061 |
. . . . . . . . . . . . . 14
|
102 | 101 | breq2d 4665 |
. . . . . . . . . . . . 13
|
103 | 94, 102 | mtbid 314 |
. . . . . . . . . . . 12
|
104 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
|
105 | 104 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
|
106 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . 15
|
107 | 105, 59, 106 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
108 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
109 | 107, 108 | syl5ibcom 235 |
. . . . . . . . . . . . 13
|
110 | 109 | necon3bd 2808 |
. . . . . . . . . . . 12
|
111 | 103, 110 | mpd 15 |
. . . . . . . . . . 11
|
112 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
|
113 | 112 | ad2antrl 764 |
. . . . . . . . . . . . . 14
|
114 | 113, 52 | nnmulcld 11068 |
. . . . . . . . . . . . 13
|
115 | 114 | nnred 11035 |
. . . . . . . . . . . 12
|
116 | 99, 96 | nnmulcld 11068 |
. . . . . . . . . . . . 13
|
117 | 116 | nnred 11035 |
. . . . . . . . . . . 12
|
118 | 115, 117 | lttri2d 10176 |
. . . . . . . . . . 11
|
119 | 111, 118 | mpbid 222 |
. . . . . . . . . 10
|
120 | 119 | ex 450 |
. . . . . . . . 9
|
121 | 120 | pm4.71rd 667 |
. . . . . . . 8
|
122 | | ancom 466 |
. . . . . . . 8
|
123 | 121, 122 | syl6rbb 277 |
. . . . . . 7
|
124 | 123 | opabbidv 4716 |
. . . . . 6
|
125 | | unopab 4728 |
. . . . . . 7
|
126 | 35 | uneq2i 3764 |
. . . . . . 7
|
127 | | andi 911 |
. . . . . . . 8
|
128 | 127 | opabbii 4717 |
. . . . . . 7
|
129 | 125, 126,
128 | 3eqtr4i 2654 |
. . . . . 6
|
130 | | df-xp 5120 |
. . . . . 6
|
131 | 124, 129,
130 | 3eqtr4g 2681 |
. . . . 5
|
132 | 131 | fveq2d 6195 |
. . . 4
|
133 | | inopab 5252 |
. . . . . . 7
|
134 | 35 | ineq2i 3811 |
. . . . . . 7
|
135 | | anandi 871 |
. . . . . . . 8
|
136 | 135 | opabbii 4717 |
. . . . . . 7
|
137 | 133, 134,
136 | 3eqtr4i 2654 |
. . . . . 6
|
138 | | ltnsym2 10136 |
. . . . . . . . . . . 12
|
139 | 115, 117,
138 | syl2anc 693 |
. . . . . . . . . . 11
|
140 | 139 | ex 450 |
. . . . . . . . . 10
|
141 | | imnan 438 |
. . . . . . . . . 10
|
142 | 140, 141 | sylib 208 |
. . . . . . . . 9
|
143 | 142 | nexdv 1864 |
. . . . . . . 8
|
144 | 143 | nexdv 1864 |
. . . . . . 7
|
145 | | opabn0 5006 |
. . . . . . . 8
|
146 | 145 | necon1bbii 2843 |
. . . . . . 7
|
147 | 144, 146 | sylib 208 |
. . . . . 6
|
148 | 137, 147 | syl5eq 2668 |
. . . . 5
|
149 | | hashun 13171 |
. . . . 5
|
150 | 26, 43, 148, 149 | syl3anc 1326 |
. . . 4
|
151 | | hashxp 13221 |
. . . . . 6
|
152 | 20, 21, 151 | syl2anc 693 |
. . . . 5
|
153 | | oddprm 15515 |
. . . . . . . . . 10
|
154 | 2, 153 | syl 17 |
. . . . . . . . 9
|
155 | 6, 154 | syl5eqel 2705 |
. . . . . . . 8
|
156 | 155 | nnnn0d 11351 |
. . . . . . 7
|
157 | | hashfz1 13134 |
. . . . . . 7
|
158 | 156, 157 | syl 17 |
. . . . . 6
|
159 | 55 | nnnn0d 11351 |
. . . . . . 7
|
160 | | hashfz1 13134 |
. . . . . . 7
|
161 | 159, 160 | syl 17 |
. . . . . 6
|
162 | 158, 161 | oveq12d 6668 |
. . . . 5
|
163 | 152, 162 | eqtrd 2656 |
. . . 4
|
164 | 132, 150,
163 | 3eqtr3d 2664 |
. . 3
|
165 | 164 | oveq2d 6666 |
. 2
|
166 | 37, 48, 165 | 3eqtr2d 2662 |
1
|