Step | Hyp | Ref
| Expression |
1 | | 4sqlem11.1 |
. . . . . . 7
 
                           |
2 | | 4sq.2 |
. . . . . . 7
   |
3 | | 4sq.3 |
. . . . . . 7
       |
4 | | 4sq.4 |
. . . . . . 7
   |
5 | | 4sq.5 |
. . . . . . 7
      
  |
6 | | 4sq.6 |
. . . . . . 7
     |
7 | | 4sq.7 |
. . . . . . 7
inf    |
8 | | 4sq.m |
. . . . . . 7
       |
9 | | 4sq.a |
. . . . . . 7
   |
10 | | 4sq.b |
. . . . . . 7
   |
11 | | 4sq.c |
. . . . . . 7
   |
12 | | 4sq.d |
. . . . . . 7
   |
13 | | 4sq.e |
. . . . . . 7
           |
14 | | 4sq.f |
. . . . . . 7
           |
15 | | 4sq.g |
. . . . . . 7
           |
16 | | 4sq.h |
. . . . . . 7
           |
17 | | 4sq.r |
. . . . . . 7
                         |
18 | | 4sq.p |
. . . . . . 7
                           |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem16 12441 |
. . . . . 6
         
     |
20 | 19 | simpld 112 |
. . . . 5

  |
21 | 1, 2, 3, 4, 5, 6, 7 | 4sqlem13m 12438 |
. . . . . . . 8
      |
22 | 21 | simpld 112 |
. . . . . . 7
    |
23 | | 1zzd 9311 |
. . . . . . . 8
 
   |
24 | | nnuz 9595 |
. . . . . . . . . 10
     |
25 | 24 | rabeqi 2745 |
. . . . . . . . 9
             |
26 | 6, 25 | eqtri 2210 |
. . . . . . . 8
         |
27 | 6 | ssrab3 3256 |
. . . . . . . . . . . . . . . 16
 |
28 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
 
   |
29 | | elfznn 10086 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
30 | 29 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
31 | | prmnn 12145 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
32 | 4, 31 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
33 | 32 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
34 | 30, 33 | nnmulcld 8999 |
. . . . . . . . . . . . . . . . . . . . 21
             |
35 | 34 | nnnn0d 9260 |
. . . . . . . . . . . . . . . . . . . 20
             |
36 | 1 | 4sqlemsdc 12435 |
. . . . . . . . . . . . . . . . . . . 20
  
DECID     |
37 | 35, 36 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
        
DECID     |
38 | 23, 26, 28, 37 | infssuzcldc 11987 |
. . . . . . . . . . . . . . . . . 18
 
 inf     |
39 | 22, 38 | exlimddv 1910 |
. . . . . . . . . . . . . . . . 17
 inf     |
40 | 7, 39 | eqeltrid 2276 |
. . . . . . . . . . . . . . . 16
   |
41 | 27, 40 | sselid 3168 |
. . . . . . . . . . . . . . 15
   |
42 | 41 | nnred 8963 |
. . . . . . . . . . . . . 14
   |
43 | 21 | simprd 114 |
. . . . . . . . . . . . . 14
   |
44 | 42, 43 | ltned 8102 |
. . . . . . . . . . . . 13
   |
45 | 41 | nncnd 8964 |
. . . . . . . . . . . . . . . . 17
   |
46 | 45 | sqvald 10685 |
. . . . . . . . . . . . . . . 16
         |
47 | 46 | breq1d 4028 |
. . . . . . . . . . . . . . 15
      
        |
48 | 41 | nnzd 9405 |
. . . . . . . . . . . . . . . 16
   |
49 | | prmz 12146 |
. . . . . . . . . . . . . . . . 17

  |
50 | 4, 49 | syl 14 |
. . . . . . . . . . . . . . . 16
   |
51 | 41 | nnne0d 8995 |
. . . . . . . . . . . . . . . 16
   |
52 | | dvdscmulr 11862 |
. . . . . . . . . . . . . . . 16
 

     
    |
53 | 48, 50, 48, 51, 52 | syl112anc 1253 |
. . . . . . . . . . . . . . 15
    
    |
54 | | dvdsprm 12172 |
. . . . . . . . . . . . . . . 16
       
   |
55 | 8, 4, 54 | syl2anc 411 |
. . . . . . . . . . . . . . 15
     |
56 | 47, 53, 55 | 3bitrd 214 |
. . . . . . . . . . . . . 14
      
    |
57 | 56 | necon3bbid 2400 |
. . . . . . . . . . . . 13
      

   |
58 | 44, 57 | mpbird 167 |
. . . . . . . . . . . 12
     
   |
59 | | orc 713 |
. . . . . . . . . . . . 13
 
   |
60 | 19 | simprd 114 |
. . . . . . . . . . . . 13
        
    |
61 | 59, 60 | syl5 32 |
. . . . . . . . . . . 12
      
    |
62 | 58, 61 | mtod 664 |
. . . . . . . . . . 11
   |
63 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem14 12439 |
. . . . . . . . . . . 12
   |
64 | | elnn0 9209 |
. . . . . . . . . . . 12

    |
65 | 63, 64 | sylib 122 |
. . . . . . . . . . 11
 
   |
66 | 62, 65 | ecased 1360 |
. . . . . . . . . 10
   |
67 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . . 21
 
        ![] ]](rbrack.gif)  |
68 | 9, 10, 67 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
        ![] ]](rbrack.gif)  |
69 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . . 20
       
      |
70 | 68, 69 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
       |
71 | 70 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . . 18
     
             
          
          |
72 | 9 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
   |
73 | 10 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
   |
74 | 72, 73 | crred 11020 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
75 | 74 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
     

            |
76 | 72, 73 | crimd 11021 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
77 | 76 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
     

            |
78 | 75, 77 | oveq12d 5915 |
. . . . . . . . . . . . . . . . . 18
       
          
                    |
79 | 71, 78 | eqtrd 2222 |
. . . . . . . . . . . . . . . . 17
     
                   |
80 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . . 21
 
        ![] ]](rbrack.gif)  |
81 | 11, 12, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
        ![] ]](rbrack.gif)  |
82 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . . 20
       
      |
83 | 81, 82 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
       |
84 | 83 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . . 18
     
             
          
          |
85 | 11 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
   |
86 | 12 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
   |
87 | 85, 86 | crred 11020 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
88 | 87 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
     

            |
89 | 85, 86 | crimd 11021 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
90 | 89 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
     

            |
91 | 88, 90 | oveq12d 5915 |
. . . . . . . . . . . . . . . . . 18
       
          
                    |
92 | 84, 91 | eqtrd 2222 |
. . . . . . . . . . . . . . . . 17
     
                   |
93 | 79, 92 | oveq12d 5915 |
. . . . . . . . . . . . . . . 16
                                                   |
94 | 18, 93 | eqtr4d 2225 |
. . . . . . . . . . . . . . 15
        
           
          |
95 | 94 | oveq1d 5912 |
. . . . . . . . . . . . . 14
           
           
           |
96 | 32 | nncnd 8964 |
. . . . . . . . . . . . . . 15
   |
97 | 41 | nnap0d 8996 |
. . . . . . . . . . . . . . 15
 #   |
98 | 96, 45, 97 | divcanap3d 8783 |
. . . . . . . . . . . . . 14
       |
99 | 95, 98 | eqtr3d 2224 |
. . . . . . . . . . . . 13
                   
           |
100 | 9, 41, 13 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
         |
101 | 100 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
   |
102 | 10, 41, 14 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
         |
103 | 102 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
   |
104 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . 20
 
        ![] ]](rbrack.gif)  |
105 | 101, 103,
104 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
        ![] ]](rbrack.gif)  |
106 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . 19
       
      |
107 | 105, 106 | syl 14 |
. . . . . . . . . . . . . . . . . 18
       |
108 | 107 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . 17
     
             
          
          |
109 | 101 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
   |
110 | 103 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
   |
111 | 109, 110 | crred 11020 |
. . . . . . . . . . . . . . . . . . 19
    
      |
112 | 111 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
     

            |
113 | 109, 110 | crimd 11021 |
. . . . . . . . . . . . . . . . . . 19
    
      |
114 | 113 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
     

            |
115 | 112, 114 | oveq12d 5915 |
. . . . . . . . . . . . . . . . 17
       
          
                    |
116 | 108, 115 | eqtrd 2222 |
. . . . . . . . . . . . . . . 16
     
                   |
117 | 11, 41, 15 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
         |
118 | 117 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
   |
119 | 12, 41, 16 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
         |
120 | 119 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
   |
121 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . 20
 
        ![] ]](rbrack.gif)  |
122 | 118, 120,
121 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
        ![] ]](rbrack.gif)  |
123 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . 19
       
      |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . . . . . . 18
       |
125 | 124 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . 17
     
             
          
          |
126 | 118 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
   |
127 | 120 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
   |
128 | 126, 127 | crred 11020 |
. . . . . . . . . . . . . . . . . . 19
    
      |
129 | 128 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
     

            |
130 | 126, 127 | crimd 11021 |
. . . . . . . . . . . . . . . . . . 19
    
      |
131 | 130 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
     

            |
132 | 129, 131 | oveq12d 5915 |
. . . . . . . . . . . . . . . . 17
       
          
                    |
133 | 125, 132 | eqtrd 2222 |
. . . . . . . . . . . . . . . 16
     
                   |
134 | 116, 133 | oveq12d 5915 |
. . . . . . . . . . . . . . 15
                                                   |
135 | 134 | oveq1d 5912 |
. . . . . . . . . . . . . 14
                   
                                   |
136 | 135, 17 | eqtr4di 2240 |
. . . . . . . . . . . . 13
                   
           |
137 | 99, 136 | oveq12d 5915 |
. . . . . . . . . . . 12
        
           
                           
              |
138 | 66 | nncnd 8964 |
. . . . . . . . . . . . 13
   |
139 | 96, 138 | mulcomd 8010 |
. . . . . . . . . . . 12
       |
140 | 137, 139 | eqtrd 2222 |
. . . . . . . . . . 11
        
           
                           
              |
141 | | eqid 2189 |
. . . . . . . . . . . 12
     
           
                         
         |
142 | | eqid 2189 |
. . . . . . . . . . . 12
     
           
                         
         |
143 | 9 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
   |
144 | | ax-icn 7937 |
. . . . . . . . . . . . . . . . . 18
 |
145 | 10 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
   |
146 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
 
     |
147 | 144, 145,
146 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
     |
148 | 101 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
   |
149 | 103 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
   |
150 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
 
     |
151 | 144, 149,
150 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
     |
152 | 143, 147,
148, 151 | addsub4d 8346 |
. . . . . . . . . . . . . . . 16
   
  
          
     |
153 | 144 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
   |
154 | 153, 145,
149 | subdid 8402 |
. . . . . . . . . . . . . . . . 17
  
          |
155 | 154 | oveq2d 5913 |
. . . . . . . . . . . . . . . 16
               
     |
156 | 152, 155 | eqtr4d 2225 |
. . . . . . . . . . . . . . 15
   
  
        
     |
157 | 156 | oveq1d 5912 |
. . . . . . . . . . . . . 14
       

                |
158 | 143, 148 | subcld 8299 |
. . . . . . . . . . . . . . 15
     |
159 | 145, 149 | subcld 8299 |
. . . . . . . . . . . . . . . 16
     |
160 | | mulcl 7969 |
. . . . . . . . . . . . . . . 16
  
   
    |
161 | 144, 159,
160 | sylancr 414 |
. . . . . . . . . . . . . . 15
  
    |
162 | 158, 161,
45, 97 | divdirapd 8817 |
. . . . . . . . . . . . . 14
      
                  |
163 | 153, 159,
45, 97 | divassapd 8814 |
. . . . . . . . . . . . . . 15
   
           |
164 | 163 | oveq2d 5913 |
. . . . . . . . . . . . . 14
        
                  |
165 | 157, 162,
164 | 3eqtrd 2226 |
. . . . . . . . . . . . 13
       

                  |
166 | 100 | simprd 114 |
. . . . . . . . . . . . . 14
       |
167 | 102 | simprd 114 |
. . . . . . . . . . . . . 14
       |
168 | | gzreim 12414 |
. . . . . . . . . . . . . 14
                          ![] ]](rbrack.gif)  |
169 | 166, 167,
168 | syl2anc 411 |
. . . . . . . . . . . . 13
                ![] ]](rbrack.gif)  |
170 | 165, 169 | eqeltrd 2266 |
. . . . . . . . . . . 12
       

       ![] ]](rbrack.gif)  |
171 | 11 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
   |
172 | 12 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
   |
173 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
 
     |
174 | 144, 172,
173 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
     |
175 | 118 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
   |
176 | 120 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
   |
177 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
 
     |
178 | 144, 176,
177 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
     |
179 | 171, 174,
175, 178 | addsub4d 8346 |
. . . . . . . . . . . . . . . 16
   
  
          
     |
180 | 153, 172,
176 | subdid 8402 |
. . . . . . . . . . . . . . . . 17
  
          |
181 | 180 | oveq2d 5913 |
. . . . . . . . . . . . . . . 16
               
     |
182 | 179, 181 | eqtr4d 2225 |
. . . . . . . . . . . . . . 15
   
  
        
     |
183 | 182 | oveq1d 5912 |
. . . . . . . . . . . . . 14
       

                |
184 | 171, 175 | subcld 8299 |
. . . . . . . . . . . . . . 15
     |
185 | 172, 176 | subcld 8299 |
. . . . . . . . . . . . . . . 16
     |
186 | | mulcl 7969 |
. . . . . . . . . . . . . . . 16
  
   
    |
187 | 144, 185,
186 | sylancr 414 |
. . . . . . . . . . . . . . 15
  
    |
188 | 184, 187,
45, 97 | divdirapd 8817 |
. . . . . . . . . . . . . 14
      
                  |
189 | 153, 185,
45, 97 | divassapd 8814 |
. . . . . . . . . . . . . . 15
   
           |
190 | 189 | oveq2d 5913 |
. . . . . . . . . . . . . 14
        
                  |
191 | 183, 188,
190 | 3eqtrd 2226 |
. . . . . . . . . . . . 13
       

                  |
192 | 117 | simprd 114 |
. . . . . . . . . . . . . 14
       |
193 | 119 | simprd 114 |
. . . . . . . . . . . . . 14
       |
194 | | gzreim 12414 |
. . . . . . . . . . . . . 14
                          ![] ]](rbrack.gif)  |
195 | 192, 193,
194 | syl2anc 411 |
. . . . . . . . . . . . 13
                ![] ]](rbrack.gif)  |
196 | 191, 195 | eqeltrd 2266 |
. . . . . . . . . . . 12
       

       ![] ]](rbrack.gif)  |
197 | 32 | nnnn0d 9260 |
. . . . . . . . . . . . 13
   |
198 | 99, 197 | eqeltrd 2266 |
. . . . . . . . . . . 12
                   
           |
199 | 1, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198 | mul4sqlem 12428 |
. . . . . . . . . . 11
        
           
                           
            |
200 | 140, 199 | eqeltrrd 2267 |
. . . . . . . . . 10
     |
201 | | oveq1 5904 |
. . . . . . . . . . . 12
       |
202 | 201 | eleq1d 2258 |
. . . . . . . . . . 11
   
     |
203 | 202, 6 | elrab2 2911 |
. . . . . . . . . 10

      |
204 | 66, 200, 203 | sylanbrc 417 |
. . . . . . . . 9
   |
205 | 204 | adantr 276 |
. . . . . . . 8
 
   |
206 | | elfznn 10086 |
. . . . . . . . . . . 12
       |
207 | 206 | adantl 277 |
. . . . . . . . . . 11
           |
208 | 32 | ad2antrr 488 |
. . . . . . . . . . 11
           |
209 | 207, 208 | nnmulcld 8999 |
. . . . . . . . . 10
             |
210 | 209 | nnnn0d 9260 |
. . . . . . . . 9
             |
211 | 210, 36 | syl 14 |
. . . . . . . 8
        
DECID     |
212 | 23, 26, 205, 211 | infssuzledc 11986 |
. . . . . . 7
 
 inf     |
213 | 22, 212 | exlimddv 1910 |
. . . . . 6
 inf     |
214 | 7, 213 | eqbrtrid 4053 |
. . . . 5

  |
215 | 66 | nnred 8963 |
. . . . . 6
   |
216 | 215, 42 | letri3d 8104 |
. . . . 5
  
    |
217 | 20, 214, 216 | mpbir2and 946 |
. . . 4
   |
218 | 217 | olcd 735 |
. . 3
     |
219 | 218, 60 | mpd 13 |
. 2
         |
220 | 219, 58 | pm2.65i 640 |
1
 |