Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . . 4
 
                           |
2 | | 4sq.2 |
. . . 4
   |
3 | | 4sq.3 |
. . . 4
       |
4 | | 4sq.4 |
. . . 4
   |
5 | | 4sqlem11.5 |
. . . 4
 
             |
6 | | 4sqlem11.6 |
. . . 4
       |
7 | 1, 2, 3, 4, 5, 6 | 4sqlem11 14978 |
. . 3
     |
8 | | n0 3732 |
. . 3
  
 
   |
9 | 7, 8 | sylib 201 |
. 2
      |
10 | | vex 3034 |
. . . . . . 7
 |
11 | | eqeq1 2475 |
. . . . . . . 8
       
         |
12 | 11 | rexbidv 2892 |
. . . . . . 7
  
          
               |
13 | 10, 12, 5 | elab2 3176 |
. . . . . 6

              |
14 | | abid 2459 |
. . . . . . . . 9
  
 
   
 
    |
15 | 5 | rexeqi 2978 |
. . . . . . . . 9
     
  
                   |
16 | | oveq1 6315 |
. . . . . . . . . . . . . 14
           |
17 | 16 | oveq1d 6323 |
. . . . . . . . . . . . 13
               |
18 | 17 | eqeq2d 2481 |
. . . . . . . . . . . 12
       
         |
19 | 18 | cbvrexv 3006 |
. . . . . . . . . . 11
            
              |
20 | | eqeq1 2475 |
. . . . . . . . . . . 12
       
         |
21 | 20 | rexbidv 2892 |
. . . . . . . . . . 11
  
          
               |
22 | 19, 21 | syl5bb 265 |
. . . . . . . . . 10
  
          
               |
23 | 22 | rexab 3189 |
. . . . . . . . 9
                    
                      |
24 | 14, 15, 23 | 3bitri 279 |
. . . . . . . 8
  
 
                         |
25 | 6 | rnmpt 5086 |
. . . . . . . . 9
 
      |
26 | 25 | eleq2i 2541 |
. . . . . . . 8

 
       |
27 | | rexcom4 3053 |
. . . . . . . . 9
               
    
  
           
 
     |
28 | | r19.41v 2928 |
. . . . . . . . . 10
             
 
                       |
29 | 28 | exbii 1726 |
. . . . . . . . 9
               
    
                      |
30 | 27, 29 | bitri 257 |
. . . . . . . 8
               
    
                      |
31 | 24, 26, 30 | 3bitr4i 285 |
. . . . . . 7

              
 
     |
32 | | ovex 6336 |
. . . . . . . . 9
       |
33 | | oveq2 6316 |
. . . . . . . . . 10
                       |
34 | 33 | eqeq2d 2481 |
. . . . . . . . 9
           
             |
35 | 32, 34 | ceqsexv 3070 |
. . . . . . . 8
         
    
            |
36 | 35 | rexbii 2881 |
. . . . . . 7
               
    
                  |
37 | 31, 36 | bitri 257 |
. . . . . 6

                  |
38 | 13, 37 | anbi12i 711 |
. . . . 5
 
                                 |
39 | | elin 3608 |
. . . . 5
  

   |
40 | | reeanv 2944 |
. . . . 5
                   
 
                                         |
41 | 38, 39, 40 | 3bitr4i 285 |
. . . 4
  
                  
             |
42 | | eqtr2 2491 |
. . . . . 6
       
 
                           |
43 | 4 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . 19
 
    
                     
  |
44 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . 19

  |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
    
                     
  |
46 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . . . . 18
 
   |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
    
                          |
48 | 47 | nn0red 10950 |
. . . . . . . . . . . . . . . 16
 
    
                          |
49 | 45 | nnrpd 11362 |
. . . . . . . . . . . . . . . 16
 
    
                     
  |
50 | 47 | nn0ge0d 10952 |
. . . . . . . . . . . . . . . 16
 
    
                     
    |
51 | 45 | nnred 10646 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
52 | 51 | ltm1d 10561 |
. . . . . . . . . . . . . . . 16
 
    
                          |
53 | | modid 12154 |
. . . . . . . . . . . . . . . 16
       
             |
54 | 48, 49, 50, 52, 53 | syl22anc 1293 |
. . . . . . . . . . . . . . 15
 
    
                              |
55 | 54 | oveq1d 6323 |
. . . . . . . . . . . . . 14
 
    
                                              |
56 | | simp2r 1057 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
                     
      |
57 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . . . . 21
       |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                     
  |
59 | | zsqcl2 12390 |
. . . . . . . . . . . . . . . . . . . 20
       |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
    
                            |
61 | 60 | nn0red 10950 |
. . . . . . . . . . . . . . . . . 18
 
    
                            |
62 | | modlt 12140 |
. . . . . . . . . . . . . . . . . 18
     
      
  |
63 | 61, 49, 62 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
    
                           
  |
64 | | zsqcl 12383 |
. . . . . . . . . . . . . . . . . . . . 21
       |
65 | 58, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                            |
66 | 65, 45 | zmodcld 12150 |
. . . . . . . . . . . . . . . . . . 19
 
    
                              |
67 | 66 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . 18
 
    
                              |
68 | | prmz 14705 |
. . . . . . . . . . . . . . . . . . 19

  |
69 | 43, 68 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
    
                     
  |
70 | | zltlem1 11013 |
. . . . . . . . . . . . . . . . . 18
       
                   |
71 | 67, 69, 70 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
    
                                        |
72 | 63, 71 | mpbid 215 |
. . . . . . . . . . . . . . . 16
 
    
                           
    |
73 | 72, 54 | breqtrrd 4422 |
. . . . . . . . . . . . . . 15
 
    
                           
 
    |
74 | | modsubdir 12192 |
. . . . . . . . . . . . . . . 16
       
                                     |
75 | 48, 61, 49, 74 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
 
    
                                                          |
76 | 73, 75 | mpbid 215 |
. . . . . . . . . . . . . 14
 
    
                                              |
77 | | simp3 1032 |
. . . . . . . . . . . . . 14
 
    
                                        |
78 | 55, 76, 77 | 3eqtr4rd 2516 |
. . . . . . . . . . . . 13
 
    
                                        |
79 | | simp2l 1056 |
. . . . . . . . . . . . . . . 16
 
    
                     
      |
80 | | elfzelz 11826 |
. . . . . . . . . . . . . . . 16
       |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . 15
 
    
                     
  |
82 | | zsqcl 12383 |
. . . . . . . . . . . . . . 15
       |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
 
    
                            |
84 | 47 | nn0zd 11061 |
. . . . . . . . . . . . . . 15
 
    
                          |
85 | 84, 65 | zsubcld 11068 |
. . . . . . . . . . . . . 14
 
    
                                |
86 | | moddvds 14389 |
. . . . . . . . . . . . . 14
                               
                 |
87 | 45, 83, 85, 86 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
    
                                      
                 |
88 | 78, 87 | mpbid 215 |
. . . . . . . . . . . 12
 
    
                                      |
89 | | zsqcl2 12390 |
. . . . . . . . . . . . . . . 16
       |
90 | 81, 89 | syl 17 |
. . . . . . . . . . . . . . 15
 
    
                            |
91 | 90 | nn0cnd 10951 |
. . . . . . . . . . . . . 14
 
    
                            |
92 | 47 | nn0cnd 10951 |
. . . . . . . . . . . . . 14
 
    
                          |
93 | 60 | nn0cnd 10951 |
. . . . . . . . . . . . . 14
 
    
                            |
94 | 91, 92, 93 | subsub3d 10035 |
. . . . . . . . . . . . 13
 
    
                                                    |
95 | 90, 60 | nn0addcld 10953 |
. . . . . . . . . . . . . . 15
 
    
                                  |
96 | 95 | nn0cnd 10951 |
. . . . . . . . . . . . . 14
 
    
                                  |
97 | 45 | nncnd 10647 |
. . . . . . . . . . . . . 14
 
    
                     
  |
98 | | 1cnd 9677 |
. . . . . . . . . . . . . 14
 
    
                        |
99 | 96, 97, 98 | subsub3d 10035 |
. . . . . . . . . . . . 13
 
    
                                 
                  |
100 | 94, 99 | eqtrd 2505 |
. . . . . . . . . . . 12
 
    
                                                    |
101 | 88, 100 | breqtrd 4420 |
. . . . . . . . . . 11
 
    
                                      |
102 | | nn0p1nn 10933 |
. . . . . . . . . . . . . 14
          
              |
103 | 95, 102 | syl 17 |
. . . . . . . . . . . . 13
 
    
                                    |
104 | 103 | nnzd 11062 |
. . . . . . . . . . . 12
 
    
                                    |
105 | | dvdssubr 14423 |
. . . . . . . . . . . 12
                           
                 |
106 | 69, 104, 105 | syl2anc 673 |
. . . . . . . . . . 11
 
    
                                  
                 |
107 | 101, 106 | mpbird 240 |
. . . . . . . . . 10
 
    
                                    |
108 | 45 | nnne0d 10676 |
. . . . . . . . . . 11
 
    
                        |
109 | | dvdsval2 14385 |
. . . . . . . . . . 11
                                             |
110 | 69, 108, 104, 109 | syl3anc 1292 |
. . . . . . . . . 10
 
    
                                                    |
111 | 107, 110 | mpbid 215 |
. . . . . . . . 9
 
    
                                      |
112 | | nnrp 11334 |
. . . . . . . . . . . . . 14
                           |
113 | | nnrp 11334 |
. . . . . . . . . . . . . 14
   |
114 | | rpdivcl 11348 |
. . . . . . . . . . . . . 14
                               |
115 | 112, 113,
114 | syl2an 485 |
. . . . . . . . . . . . 13
             
                 |
116 | 103, 45, 115 | syl2anc 673 |
. . . . . . . . . . . 12
 
    
                                      |
117 | 116 | rpgt0d 11367 |
. . . . . . . . . . 11
 
    
                     
                |
118 | | elnnz 10971 |
. . . . . . . . . . 11
              
                                |
119 | 111, 117,
118 | sylanbrc 677 |
. . . . . . . . . 10
 
    
                                      |
120 | 119 | nnge1d 10674 |
. . . . . . . . 9
 
    
                     
                |
121 | 95 | nn0red 10950 |
. . . . . . . . . . . 12
 
    
                                  |
122 | | 2nn 10790 |
. . . . . . . . . . . . . . . 16
 |
123 | 2 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . 16
 
    
                     
  |
124 | | nnmulcl 10654 |
. . . . . . . . . . . . . . . 16
 
     |
125 | 122, 123,
124 | sylancr 676 |
. . . . . . . . . . . . . . 15
 
    
                          |
126 | 125 | nnred 10646 |
. . . . . . . . . . . . . 14
 
    
                          |
127 | 126 | resqcld 12480 |
. . . . . . . . . . . . 13
 
    
                              |
128 | | nnmulcl 10654 |
. . . . . . . . . . . . . . 15
           |
129 | 122, 125,
128 | sylancr 676 |
. . . . . . . . . . . . . 14
 
    
                            |
130 | 129 | nnred 10646 |
. . . . . . . . . . . . 13
 
    
                            |
131 | 127, 130 | readdcld 9688 |
. . . . . . . . . . . 12
 
    
                                    |
132 | | 1red 9676 |
. . . . . . . . . . . 12
 
    
                        |
133 | 123 | nnsqcld 12474 |
. . . . . . . . . . . . . . . 16
 
    
                            |
134 | | nnmulcl 10654 |
. . . . . . . . . . . . . . . 16
               |
135 | 122, 133,
134 | sylancr 676 |
. . . . . . . . . . . . . . 15
 
    
                              |
136 | 135 | nnred 10646 |
. . . . . . . . . . . . . 14
 
    
                              |
137 | 90 | nn0red 10950 |
. . . . . . . . . . . . . . . 16
 
    
                            |
138 | 133 | nnred 10646 |
. . . . . . . . . . . . . . . 16
 
    
                            |
139 | 81 | zred 11063 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
140 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . 18
       |
141 | 79, 140 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
142 | 123 | nnred 10646 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
143 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . 18
       |
144 | 79, 143 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
    
                        |
145 | | le2sq2 12388 |
. . . . . . . . . . . . . . . . 17
  
 
 
          |
146 | 139, 141,
142, 144, 145 | syl22anc 1293 |
. . . . . . . . . . . . . . . 16
 
    
                         
      |
147 | 58 | zred 11063 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
148 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . 18
       |
149 | 56, 148 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
150 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . 18
       |
151 | 56, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
    
                        |
152 | | le2sq2 12388 |
. . . . . . . . . . . . . . . . 17
  
 
 
          |
153 | 147, 149,
142, 151, 152 | syl22anc 1293 |
. . . . . . . . . . . . . . . 16
 
    
                         
      |
154 | 137, 61, 138, 138, 146, 153 | le2addd 10253 |
. . . . . . . . . . . . . . 15
 
    
                               
            |
155 | 133 | nncnd 10647 |
. . . . . . . . . . . . . . . 16
 
    
                            |
156 | 155 | 2timesd 10878 |
. . . . . . . . . . . . . . 15
 
    
                                        |
157 | 154, 156 | breqtrrd 4422 |
. . . . . . . . . . . . . 14
 
    
                               
        |
158 | | 2lt4 10803 |
. . . . . . . . . . . . . . . 16
 |
159 | | 2re 10701 |
. . . . . . . . . . . . . . . . . 18
 |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
    
                        |
161 | | 4re 10708 |
. . . . . . . . . . . . . . . . . 18
 |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
    
                        |
163 | 133 | nngt0d 10675 |
. . . . . . . . . . . . . . . . 17
 
    
                     
      |
164 | | ltmul1 10477 |
. . . . . . . . . . . . . . . . 17
 
                           |
165 | 160, 162,
138, 163, 164 | syl112anc 1296 |
. . . . . . . . . . . . . . . 16
 
    
                                      |
166 | 158, 165 | mpbii 216 |
. . . . . . . . . . . . . . 15
 
    
                                    |
167 | | 2cn 10702 |
. . . . . . . . . . . . . . . . 17
 |
168 | 123 | nncnd 10647 |
. . . . . . . . . . . . . . . . 17
 
    
                     
  |
169 | | sqmul 12376 |
. . . . . . . . . . . . . . . . 17
 
                   |
170 | 167, 168,
169 | sylancr 676 |
. . . . . . . . . . . . . . . 16
 
    
                                        |
171 | | sq2 12409 |
. . . . . . . . . . . . . . . . 17
     |
172 | 171 | oveq1i 6318 |
. . . . . . . . . . . . . . . 16
                 |
173 | 170, 172 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
 
    
                                    |
174 | 166, 173 | breqtrrd 4422 |
. . . . . . . . . . . . . 14
 
    
                                    |
175 | 121, 136,
127, 157, 174 | lelttrd 9810 |
. . . . . . . . . . . . 13
 
    
                                        |
176 | 129 | nnrpd 11362 |
. . . . . . . . . . . . . 14
 
    
                            |
177 | 127, 176 | ltaddrpd 11394 |
. . . . . . . . . . . . 13
 
    
                                          |
178 | 121, 127,
131, 175, 177 | lttrd 9813 |
. . . . . . . . . . . 12
 
    
                                              |
179 | 121, 131,
132, 178 | ltadd1dd 10245 |
. . . . . . . . . . 11
 
    
                                                  |
180 | 3 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
 
    
                     
      |
181 | 180 | oveq1d 6323 |
. . . . . . . . . . . 12
 
    
                                    |
182 | 97 | sqvald 12451 |
. . . . . . . . . . . 12
 
    
                              |
183 | 125 | nncnd 10647 |
. . . . . . . . . . . . 13
 
    
                          |
184 | | binom21 12428 |
. . . . . . . . . . . . 13
                           |
185 | 183, 184 | syl 17 |
. . . . . . . . . . . 12
 
    
                                              |
186 | 181, 182,
185 | 3eqtr3d 2513 |
. . . . . . . . . . 11
 
    
                                        |
187 | 179, 186 | breqtrrd 4422 |
. . . . . . . . . 10
 
    
                                      |
188 | 103 | nnred 10646 |
. . . . . . . . . . 11
 
    
                                    |
189 | 45 | nngt0d 10675 |
. . . . . . . . . . 11
 
    
                     
  |
190 | | ltdivmul 10502 |
. . . . . . . . . . 11
             

                                  |
191 | 188, 51, 51, 189, 190 | syl112anc 1296 |
. . . . . . . . . 10
 
    
                                                      |
192 | 187, 191 | mpbird 240 |
. . . . . . . . 9
 
    
                                   
  |
193 | | 1z 10991 |
. . . . . . . . . 10
 |
194 | | elfzm11 11891 |
. . . . . . . . . 10
 
                                    
                           
    |
195 | 193, 69, 194 | sylancr 676 |
. . . . . . . . 9
 
    
                                                         
                           
    |
196 | 111, 120,
192, 195 | mpbir3and 1213 |
. . . . . . . 8
 
    
                                            |
197 | | gzreim 14962 |
. . . . . . . . 9
 
        ![] ]](rbrack.gif)  |
198 | 81, 58, 197 | syl2anc 673 |
. . . . . . . 8
 
    
                             ![] ]](rbrack.gif)  |
199 | | gzcn 14955 |
. . . . . . . . . . . . 13
       
      |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . 12
 
    
                            |
201 | 200 | absvalsq2d 13582 |
. . . . . . . . . . 11
 
    
                                                   

         |
202 | 139, 147 | crred 13371 |
. . . . . . . . . . . . 13
 
    
                                |
203 | 202 | oveq1d 6323 |
. . . . . . . . . . . 12
 
    
                          

            |
204 | 139, 147 | crimd 13372 |
. . . . . . . . . . . . 13
 
    
                                |
205 | 204 | oveq1d 6323 |
. . . . . . . . . . . 12
 
    
                          

            |
206 | 203, 205 | oveq12d 6326 |
. . . . . . . . . . 11
 
    
                            
                               |
207 | 201, 206 | eqtrd 2505 |
. . . . . . . . . 10
 
    
                                              |
208 | 207 | oveq1d 6323 |
. . . . . . . . 9
 
    
                                                  |
209 | 103 | nncnd 10647 |
. . . . . . . . . 10
 
    
                                    |
210 | 209, 97, 108 | divcan1d 10406 |
. . . . . . . . 9
 
    
                                                    |
211 | 208, 210 | eqtr4d 2508 |
. . . . . . . 8
 
    
                                                      |
212 | | oveq1 6315 |
. . . . . . . . . 10
                                   |
213 | 212 | eqeq2d 2481 |
. . . . . . . . 9
                           
                             |
214 | | fveq2 5879 |
. . . . . . . . . . . 12
  
                |
215 | 214 | oveq1d 6323 |
. . . . . . . . . . 11
  
                        |
216 | 215 | oveq1d 6323 |
. . . . . . . . . 10
  
                            |
217 | 216 | eqeq1d 2473 |
. . . . . . . . 9
  
                            
                                 |
218 | 213, 217 | rspc2ev 3149 |
. . . . . . . 8
                      

    
                                   
                     |
219 | 196, 198,
211, 218 | syl3anc 1292 |
. . . . . . 7
 
    
                      
          
              |
220 | 219 | 3expia 1233 |
. . . . . 6
 
    
                                                  |
221 | 42, 220 | syl5 32 |
. . . . 5
 
    
             
               
                      |
222 | 221 | rexlimdvva 2878 |
. . . 4
                    
               
                      |
223 | 41, 222 | syl5bi 225 |
. . 3
   
    
                      |
224 | 223 | exlimdv 1787 |
. 2
         
                      |
225 | 9, 224 | mpd 15 |
1
                           |