Proof of Theorem 2sqmod
Step | Hyp | Ref
| Expression |
1 | | 2sqmod.6 |
. . . . . 6

  |
2 | 1 | adantr 472 |
. . . . 5
 
      
  |
3 | | 2sqmod.4 |
. . . . . . . 8
   |
4 | 3 | nn0red 10950 |
. . . . . . 7
   |
5 | 4 | adantr 472 |
. . . . . 6
 
      
  |
6 | | 2sqmod.3 |
. . . . . . . 8
   |
7 | 6 | nn0red 10950 |
. . . . . . 7
   |
8 | 7 | adantr 472 |
. . . . . 6
 
      
  |
9 | 3 | nn0ge0d 10952 |
. . . . . . 7

  |
10 | 9 | adantr 472 |
. . . . . 6
 
      
  |
11 | 6 | nn0ge0d 10952 |
. . . . . . 7

  |
12 | 11 | adantr 472 |
. . . . . 6
 
      
  |
13 | 3 | nn0cnd 10951 |
. . . . . . . . 9
   |
14 | 13 | sqcld 12452 |
. . . . . . . 8
       |
15 | 14 | adantr 472 |
. . . . . . 7
 
      
      |
16 | 6 | nn0cnd 10951 |
. . . . . . . . 9
   |
17 | 16 | sqcld 12452 |
. . . . . . . 8
       |
18 | 17 | adantr 472 |
. . . . . . 7
 
      
      |
19 | | 2sqmod.2 |
. . . . . . . . . . . . 13
   |
20 | 19 | nn0cnd 10951 |
. . . . . . . . . . . 12
   |
21 | 20 | sqcld 12452 |
. . . . . . . . . . 11
       |
22 | | 2sqmod.5 |
. . . . . . . . . . . . 13
   |
23 | 22 | nn0cnd 10951 |
. . . . . . . . . . . 12
   |
24 | 23 | sqcld 12452 |
. . . . . . . . . . 11
       |
25 | | 2sqmod.8 |
. . . . . . . . . . . 12
             |
26 | | 2sqmod.9 |
. . . . . . . . . . . 12
             |
27 | 25, 26 | eqtr4d 2508 |
. . . . . . . . . . 11
                       |
28 | 21, 17, 14, 24, 27 | addeqxfrd 28397 |
. . . . . . . . . 10
                       |
29 | 28 | adantr 472 |
. . . . . . . . 9
 
      
                      |
30 | 19 | nn0zd 11061 |
. . . . . . . . . . . . . . . 16
   |
31 | 3 | nn0zd 11061 |
. . . . . . . . . . . . . . . 16
   |
32 | | dvdsmul1 14401 |
. . . . . . . . . . . . . . . 16
 
     |
33 | 30, 31, 32 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     |
34 | 33 | adantr 472 |
. . . . . . . . . . . . . 14
 
      

   |
35 | 20, 13 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
     |
36 | 35 | adantr 472 |
. . . . . . . . . . . . . . 15
 
      
    |
37 | 16, 23 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
     |
38 | 37 | adantr 472 |
. . . . . . . . . . . . . . 15
 
      
    |
39 | 19 | nn0red 10950 |
. . . . . . . . . . . . . . . . . . . 20
   |
40 | 39, 4 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . 19
     |
41 | 22 | nn0red 10950 |
. . . . . . . . . . . . . . . . . . . 20
   |
42 | 7, 41 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . 19
     |
43 | 40, 42 | resubcld 10068 |
. . . . . . . . . . . . . . . . . 18
    
    |
44 | 43 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
    
    |
45 | 44 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
      
 
      |
46 | 43 | sqge0d 12481 |
. . . . . . . . . . . . . . . . . . . . . . 23

            |
47 | | 2sqmod.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
48 | 6 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
49 | 47, 30, 48, 25 | 2sqn0 28482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
50 | | elnnne0 10907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    |
51 | 19, 49, 50 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
52 | 22 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
53 | 24, 14 | addcomd 9853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                       |
54 | 53, 26 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             |
55 | 47, 52, 31, 54 | 2sqn0 28482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
56 | | elnnne0 10907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    |
57 | 22, 55, 56 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
58 | 51, 57 | nnmulcld 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
59 | 47, 31, 52, 26 | 2sqn0 28482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
60 | | elnnne0 10907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    |
61 | 3, 59, 60 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
62 | 17, 21 | addcomd 9853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                       |
63 | 62, 25 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             |
64 | 47, 48, 30, 63 | 2sqn0 28482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
65 | | elnnne0 10907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    |
66 | 6, 64, 65 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
67 | 61, 66 | nnmulcld 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
68 | 58, 67 | nnaddcld 10678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
69 | 68 | nnsqcld 12474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
70 | 69 | nnred 10646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
71 | 43 | resqcld 12480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
72 | 70, 71 | addge02d 10223 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
              
     
                   |
73 | 46, 72 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . 22
          
     
                  |
74 | 25, 26 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           |
75 | | bhmafibid1 28480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                  
                  |
76 | 39, 7, 4, 41, 75 | syl22anc 1293 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                            
                  |
77 | 74, 76 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
                  |
78 | | prmz 14705 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
79 | 47, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
80 | 79 | zcnd 11064 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
81 | 80 | sqvald 12451 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
82 | 13, 16 | mulcomd 9682 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
83 | 82 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
84 | 83 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
85 | 84 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . 23
                            
                  |
86 | 77, 81, 85 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . . . . . . . 22
          
                  |
87 | 73, 86 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . . . . . 21
          
      |
88 | 87 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
      
                |
89 | 30, 52 | zmulcld 11069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
90 | 31, 48 | zmulcld 11069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
91 | 89, 90 | zaddcld 11067 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
92 | | dvdssqim 14600 |
. . . . . . . . . . . . . . . . . . . . . . 23
               
                 |
93 | 79, 91, 92 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
94 | | zsqcl 12383 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
95 | 79, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
96 | | dvdsle 14427 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               
                 |
97 | 95, 69, 96 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 |
98 | 93, 97 | syld 44 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
99 | 98 | imp 436 |
. . . . . . . . . . . . . . . . . . . 20
 
      
                |
100 | 95 | zred 11063 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
101 | 70, 100 | letri3d 9794 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 |
102 | 101 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
      
              
                                 |
103 | 88, 99, 102 | mpbir2and 936 |
. . . . . . . . . . . . . . . . . . 19
 
      
                |
104 | 86 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
      
                            |
105 | 103, 104 | eqtr2d 2506 |
. . . . . . . . . . . . . . . . . 18
 
      
     
                            |
106 | 70 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
             |
107 | 71 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
108 | 106, 106,
107 | subadd2d 10024 |
. . . . . . . . . . . . . . . . . . 19
                            
                                        |
109 | 108 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
      
                                
     
                             |
110 | 105, 109 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
 
      
                          
       |
111 | 106 | subidd 9993 |
. . . . . . . . . . . . . . . . . 18
                         |
112 | 111 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
      
                        |
113 | 110, 112 | eqtr3d 2507 |
. . . . . . . . . . . . . . . 16
 
      
            |
114 | 45, 113 | sqeq0d 12453 |
. . . . . . . . . . . . . . 15
 
      
 
      |
115 | 36, 38, 114 | subeq0d 10013 |
. . . . . . . . . . . . . 14
 
      
      |
116 | 34, 115 | breqtrd 4420 |
. . . . . . . . . . . . 13
 
      

   |
117 | 47, 30, 48, 25 | 2sqcoprm 28483 |
. . . . . . . . . . . . . 14
     |
118 | 117 | adantr 472 |
. . . . . . . . . . . . 13
 
      
    |
119 | | coprmdvds 14738 |
. . . . . . . . . . . . . . 15
 
   
       |
120 | 30, 48, 52, 119 | syl3anc 1292 |
. . . . . . . . . . . . . 14
   

  
   |
121 | 120 | adantr 472 |
. . . . . . . . . . . . 13
 
      
          |
122 | 116, 118,
121 | mp2and 693 |
. . . . . . . . . . . 12
 
      
  |
123 | | dvdsle 14427 |
. . . . . . . . . . . . . 14
 
 
   |
124 | 30, 57, 123 | syl2anc 673 |
. . . . . . . . . . . . 13
 
   |
125 | 124 | adantr 472 |
. . . . . . . . . . . 12
 
      

   |
126 | 122, 125 | mpd 15 |
. . . . . . . . . . 11
 
      
  |
127 | 51 | nnrpd 11362 |
. . . . . . . . . . . . . 14
   |
128 | 127 | rprege0d 11371 |
. . . . . . . . . . . . 13
 
   |
129 | 22 | nn0ge0d 10952 |
. . . . . . . . . . . . 13

  |
130 | | le2sq 12387 |
. . . . . . . . . . . . 13
  
 
 
            |
131 | 128, 41, 129, 130 | syl12anc 1290 |
. . . . . . . . . . . 12
             |
132 | 131 | adantr 472 |
. . . . . . . . . . 11
 
      
            |
133 | 126, 132 | mpbid 215 |
. . . . . . . . . 10
 
      
          |
134 | 51 | nnsqcld 12474 |
. . . . . . . . . . . . 13
       |
135 | 134 | nnred 10646 |
. . . . . . . . . . . 12
       |
136 | | zsqcl 12383 |
. . . . . . . . . . . . . 14
       |
137 | 52, 136 | syl 17 |
. . . . . . . . . . . . 13
       |
138 | 137 | zred 11063 |
. . . . . . . . . . . 12
       |
139 | 135, 138 | suble0d 10225 |
. . . . . . . . . . 11
           
           |
140 | 139 | adantr 472 |
. . . . . . . . . 10
 
      
          
           |
141 | 133, 140 | mpbird 240 |
. . . . . . . . 9
 
      
         
  |
142 | 29, 141 | eqbrtrrd 4418 |
. . . . . . . 8
 
      
         
  |
143 | | dvdsmul1 14401 |
. . . . . . . . . . . . . . 15
 
     |
144 | 48, 52, 143 | syl2anc 673 |
. . . . . . . . . . . . . 14
     |
145 | 144 | adantr 472 |
. . . . . . . . . . . . 13
 
      

   |
146 | 145, 115 | breqtrrd 4422 |
. . . . . . . . . . . 12
 
      

   |
147 | | gcdcom 14563 |
. . . . . . . . . . . . . . 15
 
       |
148 | 30, 48, 147 | syl2anc 673 |
. . . . . . . . . . . . . 14
       |
149 | 148, 117 | eqtr3d 2507 |
. . . . . . . . . . . . 13
     |
150 | 149 | adantr 472 |
. . . . . . . . . . . 12
 
      
    |
151 | | coprmdvds 14738 |
. . . . . . . . . . . . . 14
 
   
       |
152 | 48, 30, 31, 151 | syl3anc 1292 |
. . . . . . . . . . . . 13
   

  
   |
153 | 152 | adantr 472 |
. . . . . . . . . . . 12
 
      
          |
154 | 146, 150,
153 | mp2and 693 |
. . . . . . . . . . 11
 
      
  |
155 | | dvdsle 14427 |
. . . . . . . . . . . . 13
 
 
   |
156 | 48, 61, 155 | syl2anc 673 |
. . . . . . . . . . . 12
 
   |
157 | 156 | adantr 472 |
. . . . . . . . . . 11
 
      

   |
158 | 154, 157 | mpd 15 |
. . . . . . . . . 10
 
      
  |
159 | 7, 4, 11, 9 | le2sqd 12489 |
. . . . . . . . . . 11
             |
160 | 159 | adantr 472 |
. . . . . . . . . 10
 
      
            |
161 | 158, 160 | mpbid 215 |
. . . . . . . . 9
 
      
          |
162 | 4 | resqcld 12480 |
. . . . . . . . . . 11
       |
163 | | zsqcl 12383 |
. . . . . . . . . . . . 13
       |
164 | 48, 163 | syl 17 |
. . . . . . . . . . . 12
       |
165 | 164 | zred 11063 |
. . . . . . . . . . 11
       |
166 | 162, 165 | subge0d 10224 |
. . . . . . . . . 10
               
       |
167 | 166 | adantr 472 |
. . . . . . . . 9
 
      
                      |
168 | 161, 167 | mpbird 240 |
. . . . . . . 8
 
      
            |
169 | 135, 138 | resubcld 10068 |
. . . . . . . . . . 11
             |
170 | 28, 169 | eqeltrrd 2550 |
. . . . . . . . . 10
             |
171 | | 0red 9662 |
. . . . . . . . . 10
   |
172 | 170, 171 | letri3d 9794 |
. . . . . . . . 9
                                     |
173 | 172 | adantr 472 |
. . . . . . . 8
 
      
          
                         |
174 | 142, 168,
173 | mpbir2and 936 |
. . . . . . 7
 
      
            |
175 | 15, 18, 174 | subeq0d 10013 |
. . . . . 6
 
      
          |
176 | 5, 8, 10, 12, 175 | sq11d 12490 |
. . . . 5
 
      
  |
177 | 2, 176 | breqtrrd 4422 |
. . . 4
 
      
  |
178 | | 2sqmod.7 |
. . . . . 6

  |
179 | 178 | adantr 472 |
. . . . 5
 
      
  |
180 | 39 | adantr 472 |
. . . . . 6
 
      
  |
181 | 41 | adantr 472 |
. . . . . 6
 
      
  |
182 | 19 | nn0ge0d 10952 |
. . . . . . 7

  |
183 | 182 | adantr 472 |
. . . . . 6
 
      
  |
184 | 129 | adantr 472 |
. . . . . 6
 
      
  |
185 | 21 | adantr 472 |
. . . . . . 7
 
      
      |
186 | 24 | adantr 472 |
. . . . . . 7
 
      
      |
187 | 168, 29 | breqtrrd 4422 |
. . . . . . . 8
 
      
            |
188 | 169, 171 | letri3d 9794 |
. . . . . . . . 9
                                     |
189 | 188 | adantr 472 |
. . . . . . . 8
 
      
          
                         |
190 | 141, 187,
189 | mpbir2and 936 |
. . . . . . 7
 
      
            |
191 | 185, 186,
190 | subeq0d 10013 |
. . . . . 6
 
      
          |
192 | 180, 181,
183, 184, 191 | sq11d 12490 |
. . . . 5
 
      
  |
193 | 179, 192 | breqtrrd 4422 |
. . . 4
 
      
  |
194 | 39, 4 | letri3d 9794 |
. . . . 5
  
    |
195 | 194 | adantr 472 |
. . . 4
 
      

     |
196 | 177, 193,
195 | mpbir2and 936 |
. . 3
 
      
  |
197 | 20 | adantr 472 |
. . . 4
 
      
  |
198 | 13 | adantr 472 |
. . . 4
 
      
  |
199 | 16 | adantr 472 |
. . . 4
 
      
  |
200 | 64 | adantr 472 |
. . . 4
 
      
  |
201 | 41 | adantr 472 |
. . . . . . 7
 
      
  |
202 | 7 | adantr 472 |
. . . . . . 7
 
      
  |
203 | 129 | adantr 472 |
. . . . . . 7
 
      
  |
204 | 11 | adantr 472 |
. . . . . . 7
 
      
  |
205 | 24 | adantr 472 |
. . . . . . . 8
 
      
      |
206 | 17 | adantr 472 |
. . . . . . . 8
 
      
      |
207 | | prmnn 14704 |
. . . . . . . . . . . . 13

  |
208 | 47, 207 | syl 17 |
. . . . . . . . . . . 12
   |
209 | 208 | nnne0d 10676 |
. . . . . . . . . . 11
   |
210 | 209 | neneqd 2648 |
. . . . . . . . . 10
   |
211 | 210 | adantr 472 |
. . . . . . . . 9
 
      
  |
212 | 80, 24, 17 | subdid 10095 |
. . . . . . . . . . . . . . 15
                             |
213 | 80, 24 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
         |
214 | 21, 24 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
             |
215 | 80, 17 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
         |
216 | 14, 17 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
             |
217 | 17, 24 | mulcomd 9682 |
. . . . . . . . . . . . . . . . . 18
                       |
218 | 25 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . 20
                         |
219 | 21, 17 | pncan2d 10007 |
. . . . . . . . . . . . . . . . . . . 20
                       |
220 | 218, 219 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . 19
             |
221 | 220 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
                         |
222 | 26 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . 20
                         |
223 | 14, 24 | pncan2d 10007 |
. . . . . . . . . . . . . . . . . . . 20
                       |
224 | 222, 223 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . 19
             |
225 | 224 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
                         |
226 | 217, 221,
225 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . . 17
                           |
227 | 80, 21, 24 | subdird 10096 |
. . . . . . . . . . . . . . . . 17
                                 |
228 | 80, 14, 17 | subdird 10096 |
. . . . . . . . . . . . . . . . 17
                                 |
229 | 226, 227,
228 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . . 16
                                       |
230 | 213, 214,
215, 216, 229 | subeqxfrd 28396 |
. . . . . . . . . . . . . . 15
                                       |
231 | 212, 230 | eqtrd 2505 |
. . . . . . . . . . . . . 14
                                     |
232 | 20, 23 | sqmuld 12466 |
. . . . . . . . . . . . . . 15
                   |
233 | 13, 16 | sqmuld 12466 |
. . . . . . . . . . . . . . 15
                   |
234 | 232, 233 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                                       |
235 | 20, 23 | mulcld 9681 |
. . . . . . . . . . . . . . 15
     |
236 | 13, 16 | mulcld 9681 |
. . . . . . . . . . . . . . 15
     |
237 | | subsq 12420 |
. . . . . . . . . . . . . . 15
    
                                |
238 | 235, 236,
237 | syl2anc 673 |
. . . . . . . . . . . . . 14
                         
     |
239 | 231, 234,
238 | 3eqtr2d 2511 |
. . . . . . . . . . . . 13
                       
     |
240 | 239 | adantr 472 |
. . . . . . . . . . . 12
 
      
                      
     |
241 | 235 | adantr 472 |
. . . . . . . . . . . . . 14
 
      
    |
242 | | simpll 768 |
. . . . . . . . . . . . . . . 16
      
   
      |
243 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
      
   
   
      |
244 | 243 | neqned 2650 |
. . . . . . . . . . . . . . . 16
      
   
      
   |
245 | 89, 90 | zsubcld 11068 |
. . . . . . . . . . . . . . . . . . 19
    
    |
246 | | dvdssqim 14600 |
. . . . . . . . . . . . . . . . . . 19
     
       
 
        
        |
247 | 79, 245, 246 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
                
        |
248 | 247 | imp 436 |
. . . . . . . . . . . . . . . . 17
 
      
        
       |
249 | 248 | adantr 472 |
. . . . . . . . . . . . . . . 16
      
   
            
       |
250 | 95 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
  
 
      |
251 | 245 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
  
 
 
      |
252 | 235 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 
    |
253 | 236 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 
    |
254 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
 
  
 
  
   |
255 | 252, 253,
254 | subne0d 10014 |
. . . . . . . . . . . . . . . . . . 19
 
  
 
 
      |
256 | 251, 255 | znsqcld 28398 |
. . . . . . . . . . . . . . . . . 18
 
  
 
            |
257 | | dvdsle 14427 |
. . . . . . . . . . . . . . . . . 18
          
               
    
        
        |
258 | 250, 256,
257 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
  
 
         
    
        
        |
259 | 258 | imp 436 |
. . . . . . . . . . . . . . . 16
   
            
              
       |
260 | 242, 244,
249, 259 | syl21anc 1291 |
. . . . . . . . . . . . . . 15
      
   
            
       |
261 | 39, 41 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
262 | 4, 7 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
263 | 261, 262 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . . 21
    
    |
264 | 263 | resqcld 12480 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
265 | 61 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
266 | 127, 265 | rpmulcld 11380 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
267 | 66 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
268 | 57 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
269 | 267, 268 | rpmulcld 11380 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
270 | 266, 269 | rpaddcld 11379 |
. . . . . . . . . . . . . . . . . . . . 21
         |
271 | | 2z 10993 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
272 | 271 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
273 | 270, 272 | rpexpcld 12477 |
. . . . . . . . . . . . . . . . . . . 20
             |
274 | 264, 273 | ltaddrp2d 11395 |
. . . . . . . . . . . . . . . . . . 19
     
                             |
275 | | bhmafibid2 28481 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                     |
276 | 39, 7, 4, 41, 275 | syl22anc 1293 |
. . . . . . . . . . . . . . . . . . . . 21
                                               |
277 | 74, 276 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . . 20
                           |
278 | 82 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . 22
    
          |
279 | 278 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . 21
     
                 |
280 | 279 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . 20
                
                              |
281 | 277, 280 | eqtr4d 2508 |
. . . . . . . . . . . . . . . . . . 19
                           |
282 | 274, 281 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . . 18
     
         |
283 | 282, 81 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . 17
     
           |
284 | 242, 283 | syl 17 |
. . . . . . . . . . . . . . . 16
      
   
                    |
285 | 264, 100 | ltnled 9799 |
. . . . . . . . . . . . . . . . 17
               
        
        |
286 | 242, 285 | syl 17 |
. . . . . . . . . . . . . . . 16
      
   
                  
        
        |
287 | 284, 286 | mpbid 215 |
. . . . . . . . . . . . . . 15
      
   
   
        
       |
288 | 260, 287 | condan 811 |
. . . . . . . . . . . . . 14
 
      
      |
289 | 241, 288 | subeq0bd 10066 |
. . . . . . . . . . . . 13
 
      
 
      |
290 | 289 | oveq2d 6324 |
. . . . . . . . . . . 12
 
      
          
             |
291 | 235, 236 | addcld 9680 |
. . . . . . . . . . . . . 14
         |
292 | 291 | mul01d 9850 |
. . . . . . . . . . . . 13
           |
293 | 292 | adantr 472 |
. . . . . . . . . . . 12
 
      
          |
294 | 240, 290,
293 | 3eqtrd 2509 |
. . . . . . . . . . 11
 
      
              |
295 | 24, 17 | subcld 10005 |
. . . . . . . . . . . . 13
             |
296 | 80, 295 | mul0ord 10284 |
. . . . . . . . . . . 12
              
              |
297 | 296 | adantr 472 |
. . . . . . . . . . 11
 
      
 
                          |
298 | 294, 297 | mpbid 215 |
. . . . . . . . . 10
 
      
              |
299 | 298 | ord 384 |
. . . . . . . . 9
 
      

             |
300 | 211, 299 | mpd 15 |
. . . . . . . 8
 
      
            |
301 | 205, 206,
300 | subeq0d 10013 |
. . . . . . 7
 
      
          |
302 | 201, 202,
203, 204, 301 | sq11d 12490 |
. . . . . 6
 
      
  |
303 | 302 | oveq2d 6324 |
. . . . 5
 
      
      |
304 | 303, 288 | eqtr3d 2507 |
. . . 4
 
      
      |
305 | 197, 198,
199, 200, 304 | mulcan2ad 10270 |
. . 3
 
      
  |
306 | 137, 164 | zsubcld 11068 |
. . . . . 6
             |
307 | | dvdsmul1 14401 |
. . . . . 6
                           |
308 | 79, 306, 307 | syl2anc 673 |
. . . . 5
               |
309 | 308, 239 | breqtrd 4420 |
. . . 4
           
     |
310 | | euclemma 14744 |
. . . . 5
                                               |
311 | 47, 91, 245, 310 | syl3anc 1292 |
. . . 4
                                 |
312 | 309, 311 | mpbid 215 |
. . 3
                 |
313 | 196, 305,
312 | mpjaodan 803 |
. 2
   |
314 | 313 | oveq1d 6323 |
. . . . 5
           |
315 | 314 | oveq2d 6324 |
. . . 4
               |
316 | 315, 220,
224 | 3eqtr3d 2513 |
. . 3
           |
317 | 7, 41, 11, 129, 316 | sq11d 12490 |
. 2
   |
318 | 313, 317 | jca 541 |
1
     |