Step | Hyp | Ref
| Expression |
1 | | bndmet 32157 |
. . 3
    
      |
2 | | 0re 9668 |
. . . . . 6
 |
3 | 2 | ne0ii 3749 |
. . . . 5
 |
4 | | metf 21393 |
. . . . . . . . . 10
    
        |
5 | | ffn 5750 |
. . . . . . . . . 10
           |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
    

   |
7 | 1, 6 | syl 17 |
. . . . . . . 8
    

   |
8 | 7 | ad2antrr 737 |
. . . . . . 7
             |
9 | 1, 4 | syl 17 |
. . . . . . . . . . . 12
    
        |
10 | | fdm 5755 |
. . . . . . . . . . . 12
           |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
    
    |
12 | | xpeq2 4867 |
. . . . . . . . . . . 12

      |
13 | | xp0 5273 |
. . . . . . . . . . . 12
   |
14 | 12, 13 | syl6eq 2511 |
. . . . . . . . . . 11

    |
15 | 11, 14 | sylan9eq 2515 |
. . . . . . . . . 10
         |
16 | 15 | adantr 471 |
. . . . . . . . 9
        
  |
17 | | dm0rn0 5069 |
. . . . . . . . 9

  |
18 | 16, 17 | sylib 201 |
. . . . . . . 8
        
  |
19 | | 0ss 3774 |
. . . . . . . 8
  ![[,] [,]](_icc.gif)   |
20 | 18, 19 | syl6eqss 3493 |
. . . . . . 7
        
  ![[,] [,]](_icc.gif)    |
21 | | df-f 5604 |
. . . . . . 7
         ![[,] [,]](_icc.gif) 
  
  ![[,] [,]](_icc.gif)     |
22 | 8, 20, 21 | sylanbrc 675 |
. . . . . 6
                 ![[,] [,]](_icc.gif)    |
23 | 22 | ralrimiva 2813 |
. . . . 5
                ![[,] [,]](_icc.gif)    |
24 | | r19.2z 3869 |
. . . . 5
  
        ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    |
25 | 3, 23, 24 | sylancr 674 |
. . . 4
                ![[,] [,]](_icc.gif)    |
26 | | isbnd2 32159 |
. . . . . 6
      
      

           |
27 | 26 | simprbi 470 |
. . . . 5
       
           |
28 | | 2re 10706 |
. . . . . . . . . . 11
 |
29 | | simprlr 778 |
. . . . . . . . . . . 12
       

         
  |
30 | 29 | rpred 11369 |
. . . . . . . . . . 11
       

         
  |
31 | | remulcl 9649 |
. . . . . . . . . . 11
 
     |
32 | 28, 30, 31 | sylancr 674 |
. . . . . . . . . 10
       

         
    |
33 | 6 | adantr 471 |
. . . . . . . . . . 11
       

         

   |
34 | | simpll 765 |
. . . . . . . . . . . . . 14
                      
      |
35 | | simprl 769 |
. . . . . . . . . . . . . 14
                      
  |
36 | | simprr 771 |
. . . . . . . . . . . . . 14
                         |
37 | | metcl 21395 |
. . . . . . . . . . . . . 14
     
       |
38 | 34, 35, 36, 37 | syl3anc 1276 |
. . . . . . . . . . . . 13
                             |
39 | | metge0 21408 |
. . . . . . . . . . . . . 14
     
       |
40 | 34, 35, 36, 39 | syl3anc 1276 |
. . . . . . . . . . . . 13
                      
      |
41 | 32 | adantr 471 |
. . . . . . . . . . . . . 14
                           |
42 | | simprll 777 |
. . . . . . . . . . . . . . . . . 18
       

         
  |
43 | 42 | adantr 471 |
. . . . . . . . . . . . . . . . 17
                         |
44 | | metcl 21395 |
. . . . . . . . . . . . . . . . 17
     
       |
45 | 34, 43, 35, 44 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
                             |
46 | | metcl 21395 |
. . . . . . . . . . . . . . . . 17
     
       |
47 | 34, 43, 36, 46 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
                             |
48 | 45, 47 | readdcld 9695 |
. . . . . . . . . . . . . . 15
                                   |
49 | | mettri2 21404 |
. . . . . . . . . . . . . . . 16
      
 
                |
50 | 34, 43, 35, 36, 49 | syl13anc 1278 |
. . . . . . . . . . . . . . 15
                          
            |
51 | 30 | adantr 471 |
. . . . . . . . . . . . . . . . 17
                         |
52 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . 19
                      
          |
53 | 35, 52 | eleqtrd 2541 |
. . . . . . . . . . . . . . . . . 18
                      
          |
54 | | metxmet 21397 |
. . . . . . . . . . . . . . . . . . . 20
    
       |
55 | 34, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                      
       |
56 | | rpxr 11337 |
. . . . . . . . . . . . . . . . . . . . 21

  |
57 | 56 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . 20
  

           |
58 | 57 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . 19
                         |
59 | | elbl2 21453 |
. . . . . . . . . . . . . . . . . . 19
       
            
       |
60 | 55, 58, 43, 35, 59 | syl22anc 1277 |
. . . . . . . . . . . . . . . . . 18
                               
       |
61 | 53, 60 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
                             |
62 | 36, 52 | eleqtrd 2541 |
. . . . . . . . . . . . . . . . . 18
                                 |
63 | | elbl2 21453 |
. . . . . . . . . . . . . . . . . . 19
       
            
       |
64 | 55, 58, 43, 36, 63 | syl22anc 1277 |
. . . . . . . . . . . . . . . . . 18
                               
       |
65 | 62, 64 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
                             |
66 | 45, 47, 51, 51, 61, 65 | lt2addd 10263 |
. . . . . . . . . . . . . . . 16
                                     |
67 | 51 | recnd 9694 |
. . . . . . . . . . . . . . . . 17
                         |
68 | 67 | 2timesd 10883 |
. . . . . . . . . . . . . . . 16
                             |
69 | 66, 68 | breqtrrd 4442 |
. . . . . . . . . . . . . . 15
                                     |
70 | 38, 48, 41, 50, 69 | lelttrd 9818 |
. . . . . . . . . . . . . 14
                               |
71 | 38, 41, 70 | ltled 9808 |
. . . . . . . . . . . . 13
                          
    |
72 | | elicc2 11727 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)                       |
73 | 2, 41, 72 | sylancr 674 |
. . . . . . . . . . . . 13
                              ![[,] [,]](_icc.gif)        
       
      |
74 | 38, 40, 71, 73 | mpbir3and 1197 |
. . . . . . . . . . . 12
                             ![[,] [,]](_icc.gif)      |
75 | 74 | ralrimivva 2820 |
. . . . . . . . . . 11
       

         


      ![[,] [,]](_icc.gif)      |
76 | | ffnov 6426 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)   
  


      ![[,] [,]](_icc.gif)       |
77 | 33, 75, 76 | sylanbrc 675 |
. . . . . . . . . 10
       

         
        ![[,] [,]](_icc.gif)      |
78 | | oveq2 6322 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
79 | 78 | feq3d 5737 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)       |
80 | 79 | rspcev 3161 |
. . . . . . . . . 10
            ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)    |
81 | 32, 77, 80 | syl2anc 671 |
. . . . . . . . 9
       

         
         ![[,] [,]](_icc.gif)    |
82 | 81 | expr 624 |
. . . . . . . 8
      
                    ![[,] [,]](_icc.gif)     |
83 | 82 | rexlimdvva 2897 |
. . . . . . 7
    
 

                 ![[,] [,]](_icc.gif)     |
84 | 1, 83 | syl 17 |
. . . . . 6
    
 

                 ![[,] [,]](_icc.gif)     |
85 | 84 | adantr 471 |
. . . . 5
        

                 ![[,] [,]](_icc.gif)     |
86 | 27, 85 | mpd 15 |
. . . 4
                ![[,] [,]](_icc.gif)    |
87 | 25, 86 | pm2.61dane 2722 |
. . 3
    
         ![[,] [,]](_icc.gif)    |
88 | 1, 87 | jca 539 |
. 2
    
    
         ![[,] [,]](_icc.gif)     |
89 | | simpll 765 |
. . . 4
                ![[,] [,]](_icc.gif)         |
90 | | simpllr 774 |
. . . . . . 7
       

        ![[,] [,]](_icc.gif)  
   |
91 | 89 | adantr 471 |
. . . . . . . . 9
       

        ![[,] [,]](_icc.gif)  
       |
92 | | simpr 467 |
. . . . . . . . 9
       

        ![[,] [,]](_icc.gif)  
   |
93 | | met0 21406 |
. . . . . . . . 9
             |
94 | 91, 92, 93 | syl2anc 671 |
. . . . . . . 8
       

        ![[,] [,]](_icc.gif)  
       |
95 | | simplr 767 |
. . . . . . . . . . 11
       

        ![[,] [,]](_icc.gif)  
         ![[,] [,]](_icc.gif)    |
96 | 95, 92, 92 | fovrnd 6467 |
. . . . . . . . . 10
       

        ![[,] [,]](_icc.gif)  
       ![[,] [,]](_icc.gif)    |
97 | | elicc2 11727 |
. . . . . . . . . . 11
 
        ![[,] [,]](_icc.gif)      
       
    |
98 | 2, 90, 97 | sylancr 674 |
. . . . . . . . . 10
       

        ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)      
       
    |
99 | 96, 98 | mpbid 215 |
. . . . . . . . 9
       

        ![[,] [,]](_icc.gif)  
     
       
   |
100 | 99 | simp3d 1028 |
. . . . . . . 8
       

        ![[,] [,]](_icc.gif)  
    
  |
101 | 94, 100 | eqbrtrrd 4438 |
. . . . . . 7
       

        ![[,] [,]](_icc.gif)  

  |
102 | 90, 101 | ge0p1rpd 11396 |
. . . . . 6
       

        ![[,] [,]](_icc.gif)  
     |
103 | | fovrn 6465 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif) 

      ![[,] [,]](_icc.gif)    |
104 | 103 | 3expa 1215 |
. . . . . . . . . . . . 13
           ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)    |
105 | 104 | adantlll 729 |
. . . . . . . . . . . 12
        

        ![[,] [,]](_icc.gif)  


      ![[,] [,]](_icc.gif)    |
106 | | elicc2 11727 |
. . . . . . . . . . . . . 14
 
        ![[,] [,]](_icc.gif)      
       
    |
107 | 2, 90, 106 | sylancr 674 |
. . . . . . . . . . . . 13
       

        ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)      
       
    |
108 | 107 | adantr 471 |
. . . . . . . . . . . 12
        

        ![[,] [,]](_icc.gif)  


       ![[,] [,]](_icc.gif) 
                 |
109 | 105, 108 | mpbid 215 |
. . . . . . . . . . 11
        

        ![[,] [,]](_icc.gif)  


                |
110 | 109 | simp1d 1026 |
. . . . . . . . . 10
        

        ![[,] [,]](_icc.gif)  


      |
111 | 90 | adantr 471 |
. . . . . . . . . 10
        

        ![[,] [,]](_icc.gif)  


  |
112 | | peano2re 9831 |
. . . . . . . . . . . 12
     |
113 | 90, 112 | syl 17 |
. . . . . . . . . . 11
       

        ![[,] [,]](_icc.gif)  
     |
114 | 113 | adantr 471 |
. . . . . . . . . 10
        

        ![[,] [,]](_icc.gif)  


    |
115 | 109 | simp3d 1028 |
. . . . . . . . . 10
        

        ![[,] [,]](_icc.gif)  


      |
116 | 111 | ltp1d 10564 |
. . . . . . . . . 10
        

        ![[,] [,]](_icc.gif)  


    |
117 | 110, 111,
114, 115, 116 | lelttrd 9818 |
. . . . . . . . 9
        

        ![[,] [,]](_icc.gif)  


        |
118 | 117 | ralrimiva 2813 |
. . . . . . . 8
       

        ![[,] [,]](_icc.gif)  
          |
119 | | rabid2 2979 |
. . . . . . . 8
        

        |
120 | 118, 119 | sylibr 217 |
. . . . . . 7
       

        ![[,] [,]](_icc.gif)  
           |
121 | 91, 54 | syl 17 |
. . . . . . . 8
       

        ![[,] [,]](_icc.gif)  
        |
122 | 113 | rexrd 9715 |
. . . . . . . 8
       

        ![[,] [,]](_icc.gif)  
     |
123 | | blval 21449 |
. . . . . . . 8
                              |
124 | 121, 92, 122, 123 | syl3anc 1276 |
. . . . . . 7
       

        ![[,] [,]](_icc.gif)  
                     |
125 | 120, 124 | eqtr4d 2498 |
. . . . . 6
       

        ![[,] [,]](_icc.gif)  
             |
126 | | oveq2 6322 |
. . . . . . . 8
                       |
127 | 126 | eqeq2d 2471 |
. . . . . . 7
   
       
             |
128 | 127 | rspcev 3161 |
. . . . . 6
               
          |
129 | 102, 125,
128 | syl2anc 671 |
. . . . 5
       

        ![[,] [,]](_icc.gif)  
            |
130 | 129 | ralrimiva 2813 |
. . . 4
                ![[,] [,]](_icc.gif)   
           |
131 | | isbnd 32156 |
. . . 4
         

            |
132 | 89, 130, 131 | sylanbrc 675 |
. . 3
                ![[,] [,]](_icc.gif)         |
133 | 132 | r19.29an 2942 |
. 2
      
        ![[,] [,]](_icc.gif)         |
134 | 88, 133 | impbii 192 |
1
         
         ![[,] [,]](_icc.gif)     |