Step | Hyp | Ref
| Expression |
1 | | sqrlem1.1 |
. . 3
    
  |
2 | | sqrlem1.2 |
. . 3
   
 |
3 | | sqrlem5.3 |
. . 3
 

    |
4 | 1, 2, 3 | sqrlem6 12859 |
. 2
         |
5 | 1, 2 | sqrlem3 12856 |
. . . . 5
         |
6 | 5 | adantr 465 |
. . . 4
  
     
      |
7 | 1, 2 | sqrlem4 12857 |
. . . . . . . 8
   
   |
8 | 7 | adantr 465 |
. . . . . . 7
  
     
    |
9 | 8 | simpld 459 |
. . . . . 6
  
     
  |
10 | | rpre 11112 |
. . . . . . . . . . 11

  |
11 | 10 | adantr 465 |
. . . . . . . . . 10
     |
12 | | rpre 11112 |
. . . . . . . . . . . . 13

  |
13 | 12 | adantr 465 |
. . . . . . . . . . . 12
     |
14 | 7, 13 | syl 16 |
. . . . . . . . . . 11
     |
15 | 14 | resqcld 12155 |
. . . . . . . . . 10
         |
16 | 11, 15 | resubcld 9891 |
. . . . . . . . 9
   
       |
17 | 16 | adantr 465 |
. . . . . . . 8
  
     
        |
18 | 15, 11 | posdifd 10041 |
. . . . . . . . 9
       
         |
19 | 18 | biimpa 484 |
. . . . . . . 8
  
     
        |
20 | 17, 19 | elrpd 11140 |
. . . . . . 7
  
     
        |
21 | | 3re 10510 |
. . . . . . . 8
 |
22 | | 3pos 10530 |
. . . . . . . 8
 |
23 | 21, 22 | elrpii 11109 |
. . . . . . 7
 |
24 | | rpdivcl 11128 |
. . . . . . 7
       
           |
25 | 20, 23, 24 | sylancl 662 |
. . . . . 6
  
     
 
        |
26 | 9, 25 | rpaddcld 11157 |
. . . . 5
  
     
            |
27 | 14 | adantr 465 |
. . . . . . . . 9
  
     
  |
28 | 27 | recnd 9527 |
. . . . . . . 8
  
     
  |
29 | | 3nn 10595 |
. . . . . . . . . . 11
 |
30 | | nndivre 10472 |
. . . . . . . . . . 11
                   |
31 | 16, 29, 30 | sylancl 662 |
. . . . . . . . . 10
             |
32 | 31 | adantr 465 |
. . . . . . . . 9
  
     
 
        |
33 | 32 | recnd 9527 |
. . . . . . . 8
  
     
 
        |
34 | | binom2 12102 |
. . . . . . . 8
                                                           |
35 | 28, 33, 34 | syl2anc 661 |
. . . . . . 7
  
     
 
 
                 
 
                        |
36 | 15 | adantr 465 |
. . . . . . . . 9
  
     
      |
37 | 36 | recnd 9527 |
. . . . . . . 8
  
     
      |
38 | | 2re 10506 |
. . . . . . . . . 10
 |
39 | 27, 32 | remulcld 9529 |
. . . . . . . . . 10
  
     
            |
40 | | remulcl 9482 |
. . . . . . . . . 10
  
           
 
          |
41 | 38, 39, 40 | sylancr 663 |
. . . . . . . . 9
  
     
              |
42 | 41 | recnd 9527 |
. . . . . . . 8
  
     
              |
43 | 32 | resqcld 12155 |
. . . . . . . . 9
  
     
              |
44 | 43 | recnd 9527 |
. . . . . . . 8
  
     
              |
45 | 37, 42, 44 | addassd 9523 |
. . . . . . 7
  
     
                                                                  |
46 | 35, 45 | eqtrd 2495 |
. . . . . 6
  
     
 
 
                 
 
                        |
47 | | 2cn 10507 |
. . . . . . . . . . . . 13
 |
48 | | mulass 9485 |
. . . . . . . . . . . . 13
 
                                   |
49 | 47, 48 | mp3an1 1302 |
. . . . . . . . . . . 12
                                     |
50 | 28, 33, 49 | syl2anc 661 |
. . . . . . . . . . 11
  
     
             
 
          |
51 | 50 | eqcomd 2462 |
. . . . . . . . . 10
  
     
                          |
52 | 33 | sqvald 12126 |
. . . . . . . . . 10
  
     
                                |
53 | 51, 52 | oveq12d 6221 |
. . . . . . . . 9
  
     
                                                            |
54 | | remulcl 9482 |
. . . . . . . . . . . 12
 
     |
55 | 38, 27, 54 | sylancr 663 |
. . . . . . . . . . 11
  
     
    |
56 | 55 | recnd 9527 |
. . . . . . . . . 10
  
     
    |
57 | 56, 33, 33 | adddird 9526 |
. . . . . . . . 9
  
     
                                                        |
58 | 53, 57 | eqtr4d 2498 |
. . . . . . . 8
  
     
                                                  |
59 | 7 | simprd 463 |
. . . . . . . . . . . . . . 15
     |
60 | | 2pos 10528 |
. . . . . . . . . . . . . . . . 17
 |
61 | | 1re 9500 |
. . . . . . . . . . . . . . . . . 18
 |
62 | | lemul2 10297 |
. . . . . . . . . . . . . . . . . 18
 
           |
63 | 61, 62 | mp3an2 1303 |
. . . . . . . . . . . . . . . . 17
    
        |
64 | 38, 60, 63 | mpanr12 685 |
. . . . . . . . . . . . . . . 16
 
       |
65 | 14, 64 | syl 16 |
. . . . . . . . . . . . . . 15
   
       |
66 | 59, 65 | mpbid 210 |
. . . . . . . . . . . . . 14
         |
67 | 66 | adantr 465 |
. . . . . . . . . . . . 13
  
     
      |
68 | | 2t1e2 10585 |
. . . . . . . . . . . . 13
   |
69 | 67, 68 | syl6breq 4442 |
. . . . . . . . . . . 12
  
     
    |
70 | 11 | adantr 465 |
. . . . . . . . . . . . . . . 16
  
     
  |
71 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
  
     
  |
72 | 27 | sqge0d 12156 |
. . . . . . . . . . . . . . . . . 18
  
     
      |
73 | 70, 36 | addge01d 10042 |
. . . . . . . . . . . . . . . . . 18
  
     
    
         |
74 | 72, 73 | mpbid 210 |
. . . . . . . . . . . . . . . . 17
  
     
        |
75 | 70, 36, 70 | lesubaddd 10051 |
. . . . . . . . . . . . . . . . 17
  
     
 
    
         |
76 | 74, 75 | mpbird 232 |
. . . . . . . . . . . . . . . 16
  
     
        |
77 | | simplr 754 |
. . . . . . . . . . . . . . . 16
  
     
  |
78 | 17, 70, 71, 76, 77 | letrd 9643 |
. . . . . . . . . . . . . . 15
  
     
        |
79 | | 1le3 10653 |
. . . . . . . . . . . . . . . 16
 |
80 | | letr 9583 |
. . . . . . . . . . . . . . . . . 18
                
          |
81 | 61, 21, 80 | mp3an23 1307 |
. . . . . . . . . . . . . . . . 17
              
          |
82 | 17, 81 | syl 16 |
. . . . . . . . . . . . . . . 16
  
     
         
        |
83 | 79, 82 | mpan2i 677 |
. . . . . . . . . . . . . . 15
  
     
 
     
        |
84 | 78, 83 | mpd 15 |
. . . . . . . . . . . . . 14
  
     
        |
85 | | 3t1e3 10587 |
. . . . . . . . . . . . . 14
   |
86 | 84, 85 | syl6breqr 4443 |
. . . . . . . . . . . . 13
  
     
          |
87 | | ledivmul 10320 |
. . . . . . . . . . . . . . . 16
                               |
88 | 61, 87 | mp3an2 1303 |
. . . . . . . . . . . . . . 15
                         
     |
89 | 21, 22, 88 | mpanr12 685 |
. . . . . . . . . . . . . 14
               
           |
90 | 17, 89 | syl 16 |
. . . . . . . . . . . . 13
  
     
              
     |
91 | 86, 90 | mpbird 232 |
. . . . . . . . . . . 12
  
     
 
        |
92 | | le2add 9936 |
. . . . . . . . . . . . . 14
                
   
                          |
93 | 38, 61, 92 | mpanr12 685 |
. . . . . . . . . . . . 13
                
 
                        |
94 | 55, 32, 93 | syl2anc 661 |
. . . . . . . . . . . 12
  
     
   
                          |
95 | 69, 91, 94 | mp2and 679 |
. . . . . . . . . . 11
  
     
                |
96 | | df-3 10496 |
. . . . . . . . . . 11
   |
97 | 95, 96 | syl6breqr 4443 |
. . . . . . . . . 10
  
     
              |
98 | 55, 32 | readdcld 9528 |
. . . . . . . . . . 11
  
     
              |
99 | 21 | a1i 11 |
. . . . . . . . . . 11
  
     
  |
100 | 98, 99, 25 | lemul1d 11181 |
. . . . . . . . . 10
  
     
            
                                   |
101 | 97, 100 | mpbid 210 |
. . . . . . . . 9
  
     
                                  |
102 | 17 | recnd 9527 |
. . . . . . . . . 10
  
     
        |
103 | | 3cn 10511 |
. . . . . . . . . . 11
 |
104 | | 3ne0 10531 |
. . . . . . . . . . 11
 |
105 | | divcan2 10117 |
. . . . . . . . . . 11
                           |
106 | 103, 104,
105 | mp3an23 1307 |
. . . . . . . . . 10
                         |
107 | 102, 106 | syl 16 |
. . . . . . . . 9
  
     
                  |
108 | 101, 107 | breqtrd 4427 |
. . . . . . . 8
  
     
                              |
109 | 58, 108 | eqbrtrd 4423 |
. . . . . . 7
  
     
                                  |
110 | 41, 43 | readdcld 9528 |
. . . . . . . 8
  
     
                            |
111 | 36, 110, 70 | leaddsub2d 10056 |
. . . . . . 7
  
     
                                
                                   |
112 | 109, 111 | mpbird 232 |
. . . . . 6
  
     
                                  |
113 | 46, 112 | eqbrtrd 4423 |
. . . . 5
  
     
 
 
            |
114 | | oveq1 6210 |
. . . . . . 7
          
                    |
115 | 114 | breq1d 4413 |
. . . . . 6
          
    
 
 
             |
116 | | oveq1 6210 |
. . . . . . . . 9
           |
117 | 116 | breq1d 4413 |
. . . . . . . 8
     
       |
118 | 117 | cbvrabv 3077 |
. . . . . . 7
     
       |
119 | 1, 118 | eqtri 2483 |
. . . . . 6
    
  |
120 | 115, 119 | elrab2 3226 |
. . . . 5
          
 
 
      
                 |
121 | 26, 113, 120 | sylanbrc 664 |
. . . 4
  
     
            |
122 | | suprub 10406 |
. . . . 5
   

            
 
          
  |
123 | 122, 2 | syl6breqr 4443 |
. . . 4
   

            
 
         |
124 | 6, 121, 123 | syl2anc 661 |
. . 3
  
     
            |
125 | 25 | rpgt0d 11145 |
. . . 4
  
     
          |
126 | 31, 14 | ltaddposd 10038 |
. . . . . 6
   
 
     
             |
127 | 14, 31 | readdcld 9528 |
. . . . . . 7
   
 
         |
128 | 14, 127 | ltnled 9636 |
. . . . . 6
             
             |
129 | 126, 128 | bitrd 253 |
. . . . 5
   
 
     

 
          |
130 | 129 | biimpa 484 |
. . . 4
  
         
            |
131 | 125, 130 | syldan 470 |
. . 3
  
     

 
         |
132 | 124, 131 | pm2.65da 576 |
. 2
         |
133 | 15, 11 | eqleltd 9633 |
. 2
       
             |
134 | 4, 132, 133 | mpbir2and 913 |
1
         |