Proof of Theorem 4sqlem17
Step | Hyp | Ref
| Expression |
1 | | 4sq.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 14959 |
. . . . . 6
         
     |
20 | 19 | simpld 465 |
. . . . 5

  |
21 | | ssrab2 3526 |
. . . . . . . . 9
     |
22 | 6, 21 | eqsstri 3474 |
. . . . . . . 8
 |
23 | | nnuz 11223 |
. . . . . . . 8
     |
24 | 22, 23 | sseqtri 3476 |
. . . . . . 7
     |
25 | 1, 2, 3, 4, 5, 6, 7 | 4sqlem13 14956 |
. . . . . . . . . . . . . . . 16
     |
26 | 25 | simpld 465 |
. . . . . . . . . . . . . . 15
   |
27 | | infssuzcl 11274 |
. . . . . . . . . . . . . . 15
 
     inf     |
28 | 24, 26, 27 | sylancr 674 |
. . . . . . . . . . . . . 14
 inf     |
29 | 7, 28 | syl5eqel 2544 |
. . . . . . . . . . . . 13
   |
30 | 22, 29 | sseldi 3442 |
. . . . . . . . . . . 12
   |
31 | 30 | nnred 10652 |
. . . . . . . . . . 11
   |
32 | 25 | simprd 469 |
. . . . . . . . . . 11
   |
33 | 31, 32 | ltned 9797 |
. . . . . . . . . 10
   |
34 | 30 | nncnd 10653 |
. . . . . . . . . . . . . 14
   |
35 | 34 | sqvald 12445 |
. . . . . . . . . . . . 13
         |
36 | 35 | breq1d 4426 |
. . . . . . . . . . . 12
      
        |
37 | 30 | nnzd 11068 |
. . . . . . . . . . . . 13
   |
38 | | prmz 14675 |
. . . . . . . . . . . . . 14

  |
39 | 4, 38 | syl 17 |
. . . . . . . . . . . . 13
   |
40 | 30 | nnne0d 10682 |
. . . . . . . . . . . . 13
   |
41 | | dvdscmulr 14380 |
. . . . . . . . . . . . 13
 

     
    |
42 | 37, 39, 37, 40, 41 | syl112anc 1280 |
. . . . . . . . . . . 12
    
    |
43 | | dvdsprm 14696 |
. . . . . . . . . . . . 13
       
   |
44 | 8, 4, 43 | syl2anc 671 |
. . . . . . . . . . . 12
     |
45 | 36, 42, 44 | 3bitrd 287 |
. . . . . . . . . . 11
      
    |
46 | 45 | necon3bbid 2673 |
. . . . . . . . . 10
      

   |
47 | 33, 46 | mpbird 240 |
. . . . . . . . 9
     
   |
48 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem14 14957 |
. . . . . . . . . . . 12
   |
49 | | elnn0 10900 |
. . . . . . . . . . . 12

    |
50 | 48, 49 | sylib 201 |
. . . . . . . . . . 11
 
   |
51 | 50 | ord 383 |
. . . . . . . . . 10
 
   |
52 | | orc 391 |
. . . . . . . . . . 11
 
   |
53 | 19 | simprd 469 |
. . . . . . . . . . 11
        
    |
54 | 52, 53 | syl5 33 |
. . . . . . . . . 10
      
    |
55 | 51, 54 | syld 45 |
. . . . . . . . 9
 
    
    |
56 | 47, 55 | mt3d 130 |
. . . . . . . 8
   |
57 | | gzreim 14932 |
. . . . . . . . . . . . . . . . . . 19
 
        ![] ]](rbrack.gif)  |
58 | 9, 10, 57 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
        ![] ]](rbrack.gif)  |
59 | | gzcn 14925 |
. . . . . . . . . . . . . . . . . 18
       
      |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
61 | 60 | absvalsq2d 13554 |
. . . . . . . . . . . . . . . 16
     
             
          
          |
62 | 9 | zred 11069 |
. . . . . . . . . . . . . . . . . . 19
   |
63 | 10 | zred 11069 |
. . . . . . . . . . . . . . . . . . 19
   |
64 | 62, 63 | crred 13343 |
. . . . . . . . . . . . . . . . . 18
    
      |
65 | 64 | oveq1d 6330 |
. . . . . . . . . . . . . . . . 17
     

            |
66 | 62, 63 | crimd 13344 |
. . . . . . . . . . . . . . . . . 18
    
      |
67 | 66 | oveq1d 6330 |
. . . . . . . . . . . . . . . . 17
     

            |
68 | 65, 67 | oveq12d 6333 |
. . . . . . . . . . . . . . . 16
       
          
                    |
69 | 61, 68 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
     
                   |
70 | | gzreim 14932 |
. . . . . . . . . . . . . . . . . . 19
 
        ![] ]](rbrack.gif)  |
71 | 11, 12, 70 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
        ![] ]](rbrack.gif)  |
72 | | gzcn 14925 |
. . . . . . . . . . . . . . . . . 18
       
      |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
74 | 73 | absvalsq2d 13554 |
. . . . . . . . . . . . . . . 16
     
             
          
          |
75 | 11 | zred 11069 |
. . . . . . . . . . . . . . . . . . 19
   |
76 | 12 | zred 11069 |
. . . . . . . . . . . . . . . . . . 19
   |
77 | 75, 76 | crred 13343 |
. . . . . . . . . . . . . . . . . 18
    
      |
78 | 77 | oveq1d 6330 |
. . . . . . . . . . . . . . . . 17
     

            |
79 | 75, 76 | crimd 13344 |
. . . . . . . . . . . . . . . . . 18
    
      |
80 | 79 | oveq1d 6330 |
. . . . . . . . . . . . . . . . 17
     

            |
81 | 78, 80 | oveq12d 6333 |
. . . . . . . . . . . . . . . 16
       
          
                    |
82 | 74, 81 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
     
                   |
83 | 69, 82 | oveq12d 6333 |
. . . . . . . . . . . . . 14
                                                   |
84 | 18, 83 | eqtr4d 2499 |
. . . . . . . . . . . . 13
        
           
          |
85 | 84 | oveq1d 6330 |
. . . . . . . . . . . 12
           
           
           |
86 | | prmnn 14674 |
. . . . . . . . . . . . . . 15

  |
87 | 4, 86 | syl 17 |
. . . . . . . . . . . . . 14
   |
88 | 87 | nncnd 10653 |
. . . . . . . . . . . . 13
   |
89 | 88, 34, 40 | divcan3d 10416 |
. . . . . . . . . . . 12
       |
90 | 85, 89 | eqtr3d 2498 |
. . . . . . . . . . 11
                   
           |
91 | 9, 30, 13 | 4sqlem5 14935 |
. . . . . . . . . . . . . . . . . . 19
         |
92 | 91 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
   |
93 | 10, 30, 14 | 4sqlem5 14935 |
. . . . . . . . . . . . . . . . . . 19
         |
94 | 93 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
   |
95 | | gzreim 14932 |
. . . . . . . . . . . . . . . . . 18
 
        ![] ]](rbrack.gif)  |
96 | 92, 94, 95 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
        ![] ]](rbrack.gif)  |
97 | | gzcn 14925 |
. . . . . . . . . . . . . . . . 17
       
      |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
99 | 98 | absvalsq2d 13554 |
. . . . . . . . . . . . . . 15
     
             
          
          |
100 | 92 | zred 11069 |
. . . . . . . . . . . . . . . . . 18
   |
101 | 94 | zred 11069 |
. . . . . . . . . . . . . . . . . 18
   |
102 | 100, 101 | crred 13343 |
. . . . . . . . . . . . . . . . 17
    
      |
103 | 102 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
     

            |
104 | 100, 101 | crimd 13344 |
. . . . . . . . . . . . . . . . 17
    
      |
105 | 104 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
     

            |
106 | 103, 105 | oveq12d 6333 |
. . . . . . . . . . . . . . 15
       
          
                    |
107 | 99, 106 | eqtrd 2496 |
. . . . . . . . . . . . . 14
     
                   |
108 | 11, 30, 15 | 4sqlem5 14935 |
. . . . . . . . . . . . . . . . . . 19
         |
109 | 108 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
   |
110 | 12, 30, 16 | 4sqlem5 14935 |
. . . . . . . . . . . . . . . . . . 19
         |
111 | 110 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
   |
112 | | gzreim 14932 |
. . . . . . . . . . . . . . . . . 18
 
        ![] ]](rbrack.gif)  |
113 | 109, 111,
112 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
        ![] ]](rbrack.gif)  |
114 | | gzcn 14925 |
. . . . . . . . . . . . . . . . 17
       
      |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
116 | 115 | absvalsq2d 13554 |
. . . . . . . . . . . . . . 15
     
             
          
          |
117 | 109 | zred 11069 |
. . . . . . . . . . . . . . . . . 18
   |
118 | 111 | zred 11069 |
. . . . . . . . . . . . . . . . . 18
   |
119 | 117, 118 | crred 13343 |
. . . . . . . . . . . . . . . . 17
    
      |
120 | 119 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
     

            |
121 | 117, 118 | crimd 13344 |
. . . . . . . . . . . . . . . . 17
    
      |
122 | 121 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
     

            |
123 | 120, 122 | oveq12d 6333 |
. . . . . . . . . . . . . . 15
       
          
                    |
124 | 116, 123 | eqtrd 2496 |
. . . . . . . . . . . . . 14
     
                   |
125 | 107, 124 | oveq12d 6333 |
. . . . . . . . . . . . 13
                                                   |
126 | 125 | oveq1d 6330 |
. . . . . . . . . . . 12
                   
                                   |
127 | 126, 17 | syl6eqr 2514 |
. . . . . . . . . . 11
                   
           |
128 | 90, 127 | oveq12d 6333 |
. . . . . . . . . 10
        
           
                           
              |
129 | 56 | nncnd 10653 |
. . . . . . . . . . 11
   |
130 | 88, 129 | mulcomd 9690 |
. . . . . . . . . 10
       |
131 | 128, 130 | eqtrd 2496 |
. . . . . . . . 9
        
           
                           
              |
132 | | eqid 2462 |
. . . . . . . . . 10
     
           
                         
         |
133 | | eqid 2462 |
. . . . . . . . . 10
     
           
                         
         |
134 | 9 | zcnd 11070 |
. . . . . . . . . . . . . . 15
   |
135 | | ax-icn 9624 |
. . . . . . . . . . . . . . . 16
 |
136 | 10 | zcnd 11070 |
. . . . . . . . . . . . . . . 16
   |
137 | | mulcl 9649 |
. . . . . . . . . . . . . . . 16
 
     |
138 | 135, 136,
137 | sylancr 674 |
. . . . . . . . . . . . . . 15
     |
139 | 92 | zcnd 11070 |
. . . . . . . . . . . . . . 15
   |
140 | 94 | zcnd 11070 |
. . . . . . . . . . . . . . . 16
   |
141 | | mulcl 9649 |
. . . . . . . . . . . . . . . 16
 
     |
142 | 135, 140,
141 | sylancr 674 |
. . . . . . . . . . . . . . 15
     |
143 | 134, 138,
139, 142 | addsub4d 10059 |
. . . . . . . . . . . . . 14
   
  
          
     |
144 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
145 | 144, 136,
140 | subdid 10102 |
. . . . . . . . . . . . . . 15
  
          |
146 | 145 | oveq2d 6331 |
. . . . . . . . . . . . . 14
               
     |
147 | 143, 146 | eqtr4d 2499 |
. . . . . . . . . . . . 13
   
  
        
     |
148 | 147 | oveq1d 6330 |
. . . . . . . . . . . 12
       

                |
149 | 134, 139 | subcld 10012 |
. . . . . . . . . . . . 13
     |
150 | 136, 140 | subcld 10012 |
. . . . . . . . . . . . . 14
     |
151 | | mulcl 9649 |
. . . . . . . . . . . . . 14
  
   
    |
152 | 135, 150,
151 | sylancr 674 |
. . . . . . . . . . . . 13
  
    |
153 | 149, 152,
34, 40 | divdird 10449 |
. . . . . . . . . . . 12
      
                  |
154 | 144, 150,
34, 40 | divassd 10446 |
. . . . . . . . . . . . 13
   
           |
155 | 154 | oveq2d 6331 |
. . . . . . . . . . . 12
        
                  |
156 | 148, 153,
155 | 3eqtrd 2500 |
. . . . . . . . . . 11
       

                  |
157 | 91 | simprd 469 |
. . . . . . . . . . . 12
       |
158 | 93 | simprd 469 |
. . . . . . . . . . . 12
       |
159 | | gzreim 14932 |
. . . . . . . . . . . 12
                          ![] ]](rbrack.gif)  |
160 | 157, 158,
159 | syl2anc 671 |
. . . . . . . . . . 11
                ![] ]](rbrack.gif)  |
161 | 156, 160 | eqeltrd 2540 |
. . . . . . . . . 10
       

       ![] ]](rbrack.gif)  |
162 | 11 | zcnd 11070 |
. . . . . . . . . . . . . . 15
   |
163 | 12 | zcnd 11070 |
. . . . . . . . . . . . . . . 16
   |
164 | | mulcl 9649 |
. . . . . . . . . . . . . . . 16
 
     |
165 | 135, 163,
164 | sylancr 674 |
. . . . . . . . . . . . . . 15
     |
166 | 109 | zcnd 11070 |
. . . . . . . . . . . . . . 15
   |
167 | 111 | zcnd 11070 |
. . . . . . . . . . . . . . . 16
   |
168 | | mulcl 9649 |
. . . . . . . . . . . . . . . 16
 
     |
169 | 135, 167,
168 | sylancr 674 |
. . . . . . . . . . . . . . 15
     |
170 | 162, 165,
166, 169 | addsub4d 10059 |
. . . . . . . . . . . . . 14
   
  
          
     |
171 | 144, 163,
167 | subdid 10102 |
. . . . . . . . . . . . . . 15
  
          |
172 | 171 | oveq2d 6331 |
. . . . . . . . . . . . . 14
               
     |
173 | 170, 172 | eqtr4d 2499 |
. . . . . . . . . . . . 13
   
  
        
     |
174 | 173 | oveq1d 6330 |
. . . . . . . . . . . 12
       

                |
175 | 162, 166 | subcld 10012 |
. . . . . . . . . . . . 13
     |
176 | 163, 167 | subcld 10012 |
. . . . . . . . . . . . . 14
     |
177 | | mulcl 9649 |
. . . . . . . . . . . . . 14
  
   
    |
178 | 135, 176,
177 | sylancr 674 |
. . . . . . . . . . . . 13
  
    |
179 | 175, 178,
34, 40 | divdird 10449 |
. . . . . . . . . . . 12
      
                  |
180 | 144, 176,
34, 40 | divassd 10446 |
. . . . . . . . . . . . 13
   
           |
181 | 180 | oveq2d 6331 |
. . . . . . . . . . . 12
        
                  |
182 | 174, 179,
181 | 3eqtrd 2500 |
. . . . . . . . . . 11
       

                  |
183 | 108 | simprd 469 |
. . . . . . . . . . . 12
       |
184 | 110 | simprd 469 |
. . . . . . . . . . . 12
       |
185 | | gzreim 14932 |
. . . . . . . . . . . 12
                          ![] ]](rbrack.gif)  |
186 | 183, 184,
185 | syl2anc 671 |
. . . . . . . . . . 11
                ![] ]](rbrack.gif)  |
187 | 182, 186 | eqeltrd 2540 |
. . . . . . . . . 10
       

       ![] ]](rbrack.gif)  |
188 | 87 | nnnn0d 10954 |
. . . . . . . . . . 11
   |
189 | 90, 188 | eqeltrd 2540 |
. . . . . . . . . 10
                   
           |
190 | 1, 58, 71, 96, 113, 132, 133, 30, 161, 187, 189 | mul4sqlem 14946 |
. . . . . . . . 9
        
           
                           
            |
191 | 131, 190 | eqeltrrd 2541 |
. . . . . . . 8
     |
192 | | oveq1 6322 |
. . . . . . . . . 10
       |
193 | 192 | eleq1d 2524 |
. . . . . . . . 9
   
     |
194 | 193, 6 | elrab2 3210 |
. . . . . . . 8

      |
195 | 56, 191, 194 | sylanbrc 675 |
. . . . . . 7
   |
196 | | infssuzle 11273 |
. . . . . . 7
 
     inf     |
197 | 24, 195, 196 | sylancr 674 |
. . . . . 6
 inf     |
198 | 7, 197 | syl5eqbr 4450 |
. . . . 5

  |
199 | 56 | nnred 10652 |
. . . . . 6
   |
200 | 199, 31 | letri3d 9803 |
. . . . 5
  
    |
201 | 20, 198, 200 | mpbir2and 938 |
. . . 4
   |
202 | 201 | olcd 399 |
. . 3
     |
203 | 202, 53 | mpd 15 |
. 2
         |
204 | 203, 47 | pm2.65i 178 |
1
 |