Step | Hyp | Ref
| Expression |
1 | | areacirc.1 |
. . . 4
   
 
          
       |
2 | 1 | imaeq1i 5164 |
. . 3
                                    |
3 | | vex 3047 |
. . . 4
 |
4 | | imasng 5189 |
. . . 4
     
 
          
                                        |
5 | 3, 4 | ax-mp 5 |
. . 3
                                                         |
6 | | df-br 4402 |
. . . . 5
     
 
          
      
  
                         |
7 | | vex 3047 |
. . . . . 6
 |
8 | | eleq1 2516 |
. . . . . . . 8
 
   |
9 | 8 | anbi1d 710 |
. . . . . . 7
         |
10 | | oveq1 6295 |
. . . . . . . . 9
           |
11 | 10 | oveq1d 6303 |
. . . . . . . 8
                       |
12 | 11 | breq1d 4411 |
. . . . . . 7
           
   
                 |
13 | 9, 12 | anbi12d 716 |
. . . . . 6
                   
 
          
        |
14 | | eleq1 2516 |
. . . . . . . 8
 
   |
15 | 14 | anbi2d 709 |
. . . . . . 7
         |
16 | | oveq1 6295 |
. . . . . . . . 9
           |
17 | 16 | oveq2d 6304 |
. . . . . . . 8
                       |
18 | 17 | breq1d 4411 |
. . . . . . 7
           
   
                 |
19 | 15, 18 | anbi12d 716 |
. . . . . 6
                   
 
          
        |
20 | 3, 7, 13, 19 | opelopab 4722 |
. . . . 5
       
 
          
                          |
21 | | anass 654 |
. . . . 5
                              
        |
22 | 6, 20, 21 | 3bitri 275 |
. . . 4
     
 
          
      
                    |
23 | 22 | abbii 2566 |
. . 3
                           
 
         
        |
24 | 2, 5, 23 | 3eqtri 2476 |
. 2
                           |
25 | | simp3 1009 |
. . . . 5
     |
26 | 25 | biantrurd 511 |
. . . 4
              
                
         |
27 | 26 | abbidv 2568 |
. . 3
                     
 
         
         |
28 | | resqcl 12339 |
. . . . . . . . . . . 12
       |
29 | 28 | 3ad2ant1 1028 |
. . . . . . . . . . 11
         |
30 | | resqcl 12339 |
. . . . . . . . . . . 12
       |
31 | 30 | 3ad2ant3 1030 |
. . . . . . . . . . 11
         |
32 | 29, 31 | resubcld 10044 |
. . . . . . . . . 10
               |
33 | 32 | adantr 467 |
. . . . . . . . 9
  
    
             |
34 | | absresq 13358 |
. . . . . . . . . . . . 13
               |
35 | 34 | 3ad2ant3 1030 |
. . . . . . . . . . . 12
                 |
36 | 35 | breq1d 4411 |
. . . . . . . . . . 11
               
           |
37 | | recn 9626 |
. . . . . . . . . . . . . 14
   |
38 | 37 | abscld 13491 |
. . . . . . . . . . . . 13
       |
39 | 38 | 3ad2ant3 1030 |
. . . . . . . . . . . 12
         |
40 | | simp1 1007 |
. . . . . . . . . . . 12
     |
41 | 37 | absge0d 13499 |
. . . . . . . . . . . . 13
       |
42 | 41 | 3ad2ant3 1030 |
. . . . . . . . . . . 12
         |
43 | | simp2 1008 |
. . . . . . . . . . . 12
     |
44 | 39, 40, 42, 43 | le2sqd 12448 |
. . . . . . . . . . 11
       
               |
45 | 29, 31 | subge0d 10200 |
. . . . . . . . . . 11
   
         
           |
46 | 36, 44, 45 | 3bitr4d 289 |
. . . . . . . . . 10
       
             |
47 | 46 | biimpa 487 |
. . . . . . . . 9
  
    

            |
48 | 33, 47 | resqrtcld 13472 |
. . . . . . . 8
  
    
                 |
49 | 48 | renegcld 10043 |
. . . . . . 7
  
    
                  |
50 | 49 | rexrd 9687 |
. . . . . 6
  
    
                  |
51 | 48 | rexrd 9687 |
. . . . . 6
  
    
                 |
52 | | iccval 11672 |
. . . . . 6
                                                 ![[,] [,]](_icc.gif)                                
                  |
53 | 50, 51, 52 | syl2anc 666 |
. . . . 5
  
    
                  ![[,] [,]](_icc.gif)                
                                  |
54 | | iftrue 3886 |
. . . . . 6
          
                  ![[,] [,]](_icc.gif)                 
                 ![[,] [,]](_icc.gif)                  |
55 | 54 | adantl 468 |
. . . . 5
  
    
                         ![[,] [,]](_icc.gif)                 
                 ![[,] [,]](_icc.gif)                  |
56 | | absresq 13358 |
. . . . . . . . . . . 12
               |
57 | 32 | recnd 9666 |
. . . . . . . . . . . . . 14
               |
58 | 57 | adantr 467 |
. . . . . . . . . . . . 13
  
    
             |
59 | 58 | sqsqrtd 13494 |
. . . . . . . . . . . 12
  
    
                               |
60 | 56, 59 | breqan12rd 4418 |
. . . . . . . . . . 11
        

                               
             |
61 | | recn 9626 |
. . . . . . . . . . . . . 14
   |
62 | 61 | abscld 13491 |
. . . . . . . . . . . . 13
       |
63 | 62 | adantl 468 |
. . . . . . . . . . . 12
        

       |
64 | 48 | adantr 467 |
. . . . . . . . . . . 12
        

                 |
65 | 61 | absge0d 13499 |
. . . . . . . . . . . . 13
       |
66 | 65 | adantl 468 |
. . . . . . . . . . . 12
        

       |
67 | 33, 47 | sqrtge0d 13475 |
. . . . . . . . . . . . 13
  
    

                |
68 | 67 | adantr 467 |
. . . . . . . . . . . 12
        

                 |
69 | 63, 64, 66, 68 | le2sqd 12448 |
. . . . . . . . . . 11
        

                   
                             |
70 | 31 | adantr 467 |
. . . . . . . . . . . . 13
  

       |
71 | | resqcl 12339 |
. . . . . . . . . . . . . 14
       |
72 | 71 | adantl 468 |
. . . . . . . . . . . . 13
  

       |
73 | 29 | adantr 467 |
. . . . . . . . . . . . 13
  

       |
74 | 70, 72, 73 | leaddsub2d 10212 |
. . . . . . . . . . . 12
  

                                 |
75 | 74 | adantlr 720 |
. . . . . . . . . . 11
        

                                 |
76 | 60, 69, 75 | 3bitr4rd 290 |
. . . . . . . . . 10
        

                   
                 |
77 | | simpr 463 |
. . . . . . . . . . 11
        

   |
78 | 77, 64 | absled 13485 |
. . . . . . . . . 10
        

                   
                                  |
79 | | rexr 9683 |
. . . . . . . . . . . 12
   |
80 | 79 | adantl 468 |
. . . . . . . . . . 11
        

   |
81 | 80 | biantrurd 511 |
. . . . . . . . . 10
        

                                
                                    |
82 | 76, 78, 81 | 3bitrd 283 |
. . . . . . . . 9
        

                
                                   |
83 | 82 | pm5.32da 646 |
. . . . . . . 8
  
    
                 
 
               
                    |
84 | | simprl 763 |
. . . . . . . . . . 11
        
                 
                
  |
85 | 48 | adantr 467 |
. . . . . . . . . . 11
        
                 
                
                |
86 | | mnfxr 11411 |
. . . . . . . . . . . . 13
 |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
        
                 
                
  |
88 | 49 | adantr 467 |
. . . . . . . . . . . . 13
        
                 
                
                 |
89 | 88 | rexrd 9687 |
. . . . . . . . . . . 12
        
                 
                
                 |
90 | | mnflt 11422 |
. . . . . . . . . . . . . 14
                                 |
91 | 49, 90 | syl 17 |
. . . . . . . . . . . . 13
  
    

                 |
92 | 91 | adantr 467 |
. . . . . . . . . . . 12
        
                 
                
                 |
93 | | simprrl 773 |
. . . . . . . . . . . 12
        
                 
                
                 |
94 | 87, 89, 84, 92, 93 | xrltletrd 11455 |
. . . . . . . . . . 11
        
                 
                
  |
95 | | simprrr 774 |
. . . . . . . . . . 11
        
                 
                
                |
96 | | xrre 11461 |
. . . . . . . . . . 11
                                 
  |
97 | 84, 85, 94, 95, 96 | syl22anc 1268 |
. . . . . . . . . 10
        
                 
                
  |
98 | 97 | ex 436 |
. . . . . . . . 9
  
    
  
                               
   |
99 | 98 | pm4.71rd 640 |
. . . . . . . 8
  
    
  
                                 
               
                    |
100 | 83, 99 | bitr4d 260 |
. . . . . . 7
  
    
                 
                                    |
101 | 100 | abbidv 2568 |
. . . . . 6
  
    
            
       
                                   |
102 | | df-rab 2745 |
. . . . . 6
                                 
                
                  |
103 | 101, 102 | syl6eqr 2502 |
. . . . 5
  
    
            
                                         |
104 | 53, 55, 103 | 3eqtr4rd 2495 |
. . . 4
  
    
            
           
                  ![[,] [,]](_icc.gif)                    |
105 | 40, 39 | ltnled 9779 |
. . . . . . . 8
       
       |
106 | 105 | biimprd 227 |
. . . . . . 7
       
       |
107 | 106 | imdistani 695 |
. . . . . 6
  
    
           |
108 | | df-rab 2745 |
. . . . . . 7
                                   |
109 | 29 | 3ad2ant1 1028 |
. . . . . . . . . . . 12
  

           |
110 | 31 | 3ad2ant1 1028 |
. . . . . . . . . . . 12
  

           |
111 | 71 | 3ad2ant3 1030 |
. . . . . . . . . . . . 13
  

           |
112 | 110, 111 | readdcld 9667 |
. . . . . . . . . . . 12
  

                 |
113 | 40, 39, 43, 42 | lt2sqd 12447 |
. . . . . . . . . . . . . . 15
                       |
114 | 35 | breq2d 4413 |
. . . . . . . . . . . . . . 15
               
           |
115 | 113, 114 | bitrd 257 |
. . . . . . . . . . . . . 14
                   |
116 | 115 | biimpa 487 |
. . . . . . . . . . . . 13
  

               |
117 | 116 | 3adant3 1027 |
. . . . . . . . . . . 12
  

               |
118 | | sqge0 12348 |
. . . . . . . . . . . . . 14
       |
119 | 118 | 3ad2ant3 1030 |
. . . . . . . . . . . . 13
  

           |
120 | 110, 111 | addge01d 10198 |
. . . . . . . . . . . . 13
  

     
   
                 |
121 | 119, 120 | mpbid 214 |
. . . . . . . . . . . 12
  

                     |
122 | 109, 110,
112, 117, 121 | ltletrd 9792 |
. . . . . . . . . . 11
  

                     |
123 | 109, 112 | ltnled 9779 |
. . . . . . . . . . 11
  

                   
                 |
124 | 122, 123 | mpbid 214 |
. . . . . . . . . 10
  

              
      |
125 | 124 | 3expa 1207 |
. . . . . . . . 9
          
                |
126 | 125 | ralrimiva 2801 |
. . . . . . . 8
  

     
         
      |
127 | | rabeq0 3753 |
. . . . . . . 8
           
    
          
      |
128 | 126, 127 | sylibr 216 |
. . . . . . 7
  

     
                 |
129 | 108, 128 | syl5eqr 2498 |
. . . . . 6
  

     
          
        |
130 | 107, 129 | syl 17 |
. . . . 5
  
    
            
        |
131 | | iffalse 3889 |
. . . . . 6
    
     
                  ![[,] [,]](_icc.gif)                 
  |
132 | 131 | adantl 468 |
. . . . 5
  
    
                         ![[,] [,]](_icc.gif)                 
  |
133 | 130, 132 | eqtr4d 2487 |
. . . 4
  
    
            
           
                  ![[,] [,]](_icc.gif)                    |
134 | 104, 133 | pm2.61dan 799 |
. . 3
                          
                  ![[,] [,]](_icc.gif)                    |
135 | 27, 134 | eqtr3d 2486 |
. 2
                            
                  ![[,] [,]](_icc.gif)                    |
136 | 24, 135 | syl5eq 2496 |
1
              
                  ![[,] [,]](_icc.gif)                    |