Step | Hyp | Ref
| Expression |
1 | | lgsquad2.1 |
. . . 4
   |
2 | | 2nn 10790 |
. . . . 5
 |
3 | 2 | a1i 11 |
. . . 4
   |
4 | | lgsquad2.3 |
. . . 4
   |
5 | 1 | nnzd 11062 |
. . . . . 6
   |
6 | | 2z 10993 |
. . . . . 6
 |
7 | | gcdcom 14563 |
. . . . . 6
 
       |
8 | 5, 6, 7 | sylancl 675 |
. . . . 5
       |
9 | | lgsquad2.2 |
. . . . . 6
   |
10 | | 2prm 14719 |
. . . . . . 7
 |
11 | | coprm 14736 |
. . . . . . 7
   
     |
12 | 10, 5, 11 | sylancr 676 |
. . . . . 6
       |
13 | 9, 12 | mpbid 215 |
. . . . 5
     |
14 | 8, 13 | eqtrd 2505 |
. . . 4
     |
15 | | rpmulgcd 14602 |
. . . 4
  
            |
16 | 1, 3, 4, 14, 15 | syl31anc 1295 |
. . 3
         |
17 | | lgsquad2.5 |
. . 3
     |
18 | 16, 17 | eqtrd 2505 |
. 2
       |
19 | | oveq1 6315 |
. . . . . . . 8
           |
20 | | oveq2 6316 |
. . . . . . . 8
           |
21 | 19, 20 | oveq12d 6326 |
. . . . . . 7
                       |
22 | | oveq1 6315 |
. . . . . . . . . . . 12
       |
23 | | 1m1e0 10700 |
. . . . . . . . . . . 12
   |
24 | 22, 23 | syl6eq 2521 |
. . . . . . . . . . 11
     |
25 | 24 | oveq1d 6323 |
. . . . . . . . . 10
         |
26 | | 2cn 10702 |
. . . . . . . . . . 11
 |
27 | | 2ne0 10724 |
. . . . . . . . . . 11
 |
28 | 26, 27 | div0i 10363 |
. . . . . . . . . 10
   |
29 | 25, 28 | syl6eq 2521 |
. . . . . . . . 9
       |
30 | 29 | oveq1d 6323 |
. . . . . . . 8
                   |
31 | 30 | oveq2d 6324 |
. . . . . . 7
                             |
32 | 21, 31 | eqeq12d 2486 |
. . . . . 6
                          
                        |
33 | 32 | imbi2d 323 |
. . . . 5
                                                               |
34 | 33 | imbi2d 323 |
. . . 4
  
                               
                                |
35 | | oveq1 6315 |
. . . . . . 7
 
         |
36 | 35 | eqeq1d 2473 |
. . . . . 6
      
      |
37 | | oveq1 6315 |
. . . . . . . 8
           |
38 | | oveq2 6316 |
. . . . . . . 8
           |
39 | 37, 38 | oveq12d 6326 |
. . . . . . 7
                       |
40 | | oveq1 6315 |
. . . . . . . . . 10
       |
41 | 40 | oveq1d 6323 |
. . . . . . . . 9
           |
42 | 41 | oveq1d 6323 |
. . . . . . . 8
                       |
43 | 42 | oveq2d 6324 |
. . . . . . 7
                                 |
44 | 39, 43 | eqeq12d 2486 |
. . . . . 6
                          
                            |
45 | 36, 44 | imbi12d 327 |
. . . . 5
                                                                   |
46 | 45 | imbi2d 323 |
. . . 4
  
                               
                                    |
47 | | oveq1 6315 |
. . . . . . 7
 
         |
48 | 47 | eqeq1d 2473 |
. . . . . 6
      
      |
49 | | oveq1 6315 |
. . . . . . . 8
           |
50 | | oveq2 6316 |
. . . . . . . 8
           |
51 | 49, 50 | oveq12d 6326 |
. . . . . . 7
                       |
52 | | oveq1 6315 |
. . . . . . . . . 10
       |
53 | 52 | oveq1d 6323 |
. . . . . . . . 9
           |
54 | 53 | oveq1d 6323 |
. . . . . . . 8
                       |
55 | 54 | oveq2d 6324 |
. . . . . . 7
                                 |
56 | 51, 55 | eqeq12d 2486 |
. . . . . 6
                          
                            |
57 | 48, 56 | imbi12d 327 |
. . . . 5
                                                                   |
58 | 57 | imbi2d 323 |
. . . 4
  
                               
                                    |
59 | | oveq1 6315 |
. . . . . . 7
   
           |
60 | 59 | eqeq1d 2473 |
. . . . . 6
          
      |
61 | | oveq1 6315 |
. . . . . . . 8
               |
62 | | oveq2 6316 |
. . . . . . . 8
               |
63 | 61, 62 | oveq12d 6326 |
. . . . . . 7
                             |
64 | | oveq1 6315 |
. . . . . . . . . 10
           |
65 | 64 | oveq1d 6323 |
. . . . . . . . 9
               |
66 | 65 | oveq1d 6323 |
. . . . . . . 8
                           |
67 | 66 | oveq2d 6324 |
. . . . . . 7
                                     |
68 | 63, 67 | eqeq12d 2486 |
. . . . . 6
                            
                                  |
69 | 60, 68 | imbi12d 327 |
. . . . 5
                                                                             |
70 | 69 | imbi2d 323 |
. . . 4
    
                               
                                            |
71 | | oveq1 6315 |
. . . . . . 7
 
         |
72 | 71 | eqeq1d 2473 |
. . . . . 6
             |
73 | | oveq1 6315 |
. . . . . . . 8
           |
74 | | oveq2 6316 |
. . . . . . . 8
           |
75 | 73, 74 | oveq12d 6326 |
. . . . . . 7
                       |
76 | | oveq1 6315 |
. . . . . . . . . 10
       |
77 | 76 | oveq1d 6323 |
. . . . . . . . 9
           |
78 | 77 | oveq1d 6323 |
. . . . . . . 8
                       |
79 | 78 | oveq2d 6324 |
. . . . . . 7
                                 |
80 | 75, 79 | eqeq12d 2486 |
. . . . . 6
                          
                            |
81 | 72, 80 | imbi12d 327 |
. . . . 5
                                                                   |
82 | 81 | imbi2d 323 |
. . . 4
  
                               
                                    |
83 | | 1t1e1 10780 |
. . . . . . 7
   |
84 | | neg1cn 10735 |
. . . . . . . 8
  |
85 | | exp0 12314 |
. . . . . . . 8
         |
86 | 84, 85 | ax-mp 5 |
. . . . . . 7
      |
87 | 83, 86 | eqtr4i 2496 |
. . . . . 6
        |
88 | | sq1 12407 |
. . . . . . . . 9
     |
89 | 88 | oveq1i 6318 |
. . . . . . . 8
             |
90 | | 1nn 10642 |
. . . . . . . . . 10
 |
91 | 90 | a1i 11 |
. . . . . . . . 9
   |
92 | 4 | nnzd 11062 |
. . . . . . . . 9
   |
93 | | 1gcd 14580 |
. . . . . . . . . 10
 
   |
94 | 92, 93 | syl 17 |
. . . . . . . . 9
     |
95 | | lgssq 24342 |
. . . . . . . . 9
 

            |
96 | 91, 92, 94, 95 | syl3anc 1292 |
. . . . . . . 8
           |
97 | 89, 96 | syl5eqr 2519 |
. . . . . . 7
       |
98 | 88 | oveq2i 6319 |
. . . . . . . 8
             |
99 | | gcd1 14575 |
. . . . . . . . . 10
     |
100 | 92, 99 | syl 17 |
. . . . . . . . 9
     |
101 | | lgssq2 24343 |
. . . . . . . . 9
 
             |
102 | 92, 91, 100, 101 | syl3anc 1292 |
. . . . . . . 8
           |
103 | 98, 102 | syl5eqr 2519 |
. . . . . . 7
       |
104 | 97, 103 | oveq12d 6326 |
. . . . . 6
               |
105 | | nnm1nn0 10935 |
. . . . . . . . . . 11
 
   |
106 | 4, 105 | syl 17 |
. . . . . . . . . 10
     |
107 | 106 | nn0cnd 10951 |
. . . . . . . . 9
     |
108 | 107 | halfcld 10880 |
. . . . . . . 8
       |
109 | 108 | mul02d 9849 |
. . . . . . 7
         |
110 | 109 | oveq2d 6324 |
. . . . . 6
                   |
111 | 87, 104, 110 | 3eqtr4a 2531 |
. . . . 5
                        |
112 | 111 | a1d 25 |
. . . 4
                              |
113 | | simprl 772 |
. . . . . . . . 9
 

        |
114 | | prmz 14705 |
. . . . . . . . . . . 12

  |
115 | 114 | ad2antrl 742 |
. . . . . . . . . . 11
 

        |
116 | 6 | a1i 11 |
. . . . . . . . . . 11
 

        |
117 | 4 | adantr 472 |
. . . . . . . . . . . . 13
 

        |
118 | 117 | nnzd 11062 |
. . . . . . . . . . . 12
 

        |
119 | | zmulcl 11009 |
. . . . . . . . . . . 12
 
     |
120 | 6, 118, 119 | sylancr 676 |
. . . . . . . . . . 11
 

          |
121 | | simprr 774 |
. . . . . . . . . . 11
 

      
     |
122 | | dvdsmul1 14401 |
. . . . . . . . . . . 12
 
     |
123 | 6, 118, 122 | sylancr 676 |
. . . . . . . . . . 11
 

          |
124 | | rpdvds 14755 |
. . . . . . . . . . 11
                   |
125 | 115, 116,
120, 121, 123, 124 | syl32anc 1300 |
. . . . . . . . . 10
 

      
   |
126 | | prmrp 14737 |
. . . . . . . . . . 11
         |
127 | 113, 10, 126 | sylancl 675 |
. . . . . . . . . 10
 

            |
128 | 125, 127 | mpbid 215 |
. . . . . . . . 9
 

        |
129 | | eldifsn 4088 |
. . . . . . . . 9
    

   |
130 | 113, 128,
129 | sylanbrc 677 |
. . . . . . . 8
 

      
     |
131 | | prmnn 14704 |
. . . . . . . . . . 11

  |
132 | 131 | ad2antrl 742 |
. . . . . . . . . 10
 

        |
133 | 2 | a1i 11 |
. . . . . . . . . 10
 

        |
134 | | rpmulgcd 14602 |
. . . . . . . . . 10
  
            |
135 | 132, 133,
117, 125, 134 | syl31anc 1295 |
. . . . . . . . 9
 

      
       |
136 | 135, 121 | eqtr3d 2507 |
. . . . . . . 8
 

      
   |
137 | 130, 136 | jca 541 |
. . . . . . 7
 

                |
138 | | lgsquad2lem2.f |
. . . . . . 7
 
 
   
                              |
139 | 137, 138 | syldan 478 |
. . . . . 6
 

                                 |
140 | 139 | exp32 616 |
. . . . 5
                                    |
141 | 140 | com12 31 |
. . . 4

                                   |
142 | | jcab 880 |
. . . . 5
                                                                  
      
                                
                              |
143 | | simplrl 778 |
. . . . . . . . . . . 12
                          
                                                                  |
144 | | eluz2nn 11221 |
. . . . . . . . . . . 12
    
  |
145 | 143, 144 | syl 17 |
. . . . . . . . . . 11
                          
                                                              |
146 | | simplrr 779 |
. . . . . . . . . . . 12
                          
                                                                  |
147 | | eluz2nn 11221 |
. . . . . . . . . . . 12
    
  |
148 | 146, 147 | syl 17 |
. . . . . . . . . . 11
                          
                                                              |
149 | 145, 148 | nnmulcld 10679 |
. . . . . . . . . 10
                          
                                                                |
150 | | n2dvds1 14431 |
. . . . . . . . . . . 12
 |
151 | 92 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
                
   
  |
152 | 6, 151, 122 | sylancr 676 |
. . . . . . . . . . . . . 14
                
   
    |
153 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
                
      |
154 | | eluzelz 11192 |
. . . . . . . . . . . . . . . . . 18
    
  |
155 | | eluzelz 11192 |
. . . . . . . . . . . . . . . . . 18
    
  |
156 | 154, 155 | anim12i 576 |
. . . . . . . . . . . . . . . . 17
          
    |
157 | 156 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
                
        |
158 | | zmulcl 11009 |
. . . . . . . . . . . . . . . 16
 
     |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . 15
                
        |
160 | 6, 151, 119 | sylancr 676 |
. . . . . . . . . . . . . . 15
                
        |
161 | | dvdsgcd 14590 |
. . . . . . . . . . . . . . 15
  
                    |
162 | 153, 159,
160, 161 | syl3anc 1292 |
. . . . . . . . . . . . . 14
                
      

            |
163 | 152, 162 | mpan2d 688 |
. . . . . . . . . . . . 13
                
         
      |
164 | | simpr 468 |
. . . . . . . . . . . . . 14
                
            |
165 | 164 | breq2d 4407 |
. . . . . . . . . . . . 13
                
       
      |
166 | 163, 165 | sylibd 222 |
. . . . . . . . . . . 12
                
          |
167 | 150, 166 | mtoi 183 |
. . . . . . . . . . 11
                
   
    |
168 | 167 | adantrr 731 |
. . . . . . . . . 10
                          
                                                           

   |
169 | 4 | ad2antrr 740 |
. . . . . . . . . 10
                          
                                                              |
170 | | lgsquad2.4 |
. . . . . . . . . . 11
   |
171 | 170 | ad2antrr 740 |
. . . . . . . . . 10
                          
                                                           
  |
172 | | dvdsmul2 14402 |
. . . . . . . . . . . . 13
 
     |
173 | 6, 151, 172 | sylancr 676 |
. . . . . . . . . . . 12
                
        |
174 | | rpdvds 14755 |
. . . . . . . . . . . 12
                         |
175 | 159, 151,
160, 164, 173, 174 | syl32anc 1300 |
. . . . . . . . . . 11
                
          |
176 | 175 | adantrr 731 |
. . . . . . . . . 10
                          
                                                                  |
177 | | eqidd 2472 |
. . . . . . . . . 10
                          
                                                                  |
178 | 157 | simpld 466 |
. . . . . . . . . . . . . 14
                
   
  |
179 | | gcdcom 14563 |
. . . . . . . . . . . . . 14
           
   |
180 | 178, 160,
179 | syl2anc 673 |
. . . . . . . . . . . . 13
                
              |
181 | | gcdcom 14563 |
. . . . . . . . . . . . . . . 16
    
          
     |
182 | 160, 159,
181 | syl2anc 673 |
. . . . . . . . . . . . . . 15
                
                  |
183 | 182, 164 | eqtrd 2505 |
. . . . . . . . . . . . . 14
                
            |
184 | | dvdsmul1 14401 |
. . . . . . . . . . . . . . 15
 
     |
185 | 157, 184 | syl 17 |
. . . . . . . . . . . . . 14
                
        |
186 | | rpdvds 14755 |
. . . . . . . . . . . . . 14
     
         
         |
187 | 160, 178,
159, 183, 185, 186 | syl32anc 1300 |
. . . . . . . . . . . . 13
                
          |
188 | 180, 187 | eqtrd 2505 |
. . . . . . . . . . . 12
                
          |
189 | 188 | adantrr 731 |
. . . . . . . . . . 11
                          
                                                                  |
190 | | simprrl 782 |
. . . . . . . . . . 11
                          
                                                                
                            |
191 | 189, 190 | mpd 15 |
. . . . . . . . . 10
                          
                                                                                       |
192 | 157 | simprd 470 |
. . . . . . . . . . . . . 14
                
      |
193 | | gcdcom 14563 |
. . . . . . . . . . . . . 14
           
   |
194 | 192, 160,
193 | syl2anc 673 |
. . . . . . . . . . . . 13
                
              |
195 | | dvdsmul2 14402 |
. . . . . . . . . . . . . . 15
 
     |
196 | 157, 195 | syl 17 |
. . . . . . . . . . . . . 14
                
   
    |
197 | | rpdvds 14755 |
. . . . . . . . . . . . . 14
     
         
         |
198 | 160, 192,
159, 183, 196, 197 | syl32anc 1300 |
. . . . . . . . . . . . 13
                
          |
199 | 194, 198 | eqtrd 2505 |
. . . . . . . . . . . 12
                
          |
200 | 199 | adantrr 731 |
. . . . . . . . . . 11
                          
                                                                  |
201 | | simprrr 783 |
. . . . . . . . . . 11
                          
                                                                
                            |
202 | 200, 201 | mpd 15 |
. . . . . . . . . 10
                          
                                                                                       |
203 | 149, 168,
169, 171, 176, 145, 148, 177, 191, 202 | lgsquad2lem1 24365 |
. . . . . . . . 9
                          
                                                                                             |
204 | 203 | exp32 616 |
. . . . . . . 8
 
    
     
   
         
                                                                                             |
205 | 204 | com23 80 |
. . . . . . 7
 
    
     
                                     
                                                                     |
206 | 205 | expcom 442 |
. . . . . 6
          
                                                                                                             |
207 | 206 | a2d 28 |
. . . . 5
          
                                                                   
   
                                       |
208 | 142, 207 | syl5bir 226 |
. . . 4
          
  
                                     
                            
   
                                       |
209 | 34, 46, 58, 70, 82, 112, 141, 208 | prmind 14715 |
. . 3
      
                             |
210 | 1, 209 | mpcom 36 |
. 2
                                  |
211 | 18, 210 | mpd 15 |
1
                            |