Step | Hyp | Ref
| Expression |
1 | | 0re 9668 |
. . . 4
 |
2 | 1 | ne0ii 3749 |
. . 3
 |
3 | | ral0 3885 |
. . . . 5
    ![[,] [,]](_icc.gif)                
         |
4 | | c1lip1.a |
. . . . . . . . 9
   |
5 | 4 | rexrd 9715 |
. . . . . . . 8
   |
6 | | c1lip1.b |
. . . . . . . . 9
   |
7 | 6 | rexrd 9715 |
. . . . . . . 8
   |
8 | | icc0 11712 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
   |
9 | 5, 7, 8 | syl2anc 671 |
. . . . . . 7
    ![[,] [,]](_icc.gif)     |
10 | 9 | biimpar 492 |
. . . . . 6
 

  ![[,] [,]](_icc.gif)    |
11 | 10 | raleqdv 3004 |
. . . . 5
 

 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
       
    ![[,] [,]](_icc.gif)                
           |
12 | 3, 11 | mpbiri 241 |
. . . 4
 

   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
          |
13 | 12 | ralrimivw 2814 |
. . 3
 

    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
          |
14 | | r19.2z 3869 |
. . 3
  
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
         
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                           |
15 | 2, 13, 14 | sylancr 674 |
. 2
 

    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
          |
16 | 4 | adantr 471 |
. . . . 5
 

  |
17 | 6 | adantr 471 |
. . . . 5
 

  |
18 | | simpr 467 |
. . . . 5
 

  |
19 | | c1lip1.f |
. . . . . 6
     |
20 | 19 | adantr 471 |
. . . . 5
 


   |
21 | | c1lip1.dv |
. . . . . 6
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
22 | 21 | adantr 471 |
. . . . 5
 

     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
23 | | c1lip1.cn |
. . . . . 6
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
24 | 23 | adantr 471 |
. . . . 5
 

   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
25 | | eqid 2461 |
. . . . 5
            ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)       |
26 | 16, 17, 18, 20, 22, 24, 25 | c1liplem1 22996 |
. . . 4
 

             ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)                 |
27 | | oveq1 6321 |
. . . . . . . 8
             ![[,] [,]](_icc.gif)                           ![[,] [,]](_icc.gif)               |
28 | 27 | breq2d 4427 |
. . . . . . 7
             ![[,] [,]](_icc.gif)                            
                           ![[,] [,]](_icc.gif)                |
29 | 28 | imbi2d 322 |
. . . . . 6
             ![[,] [,]](_icc.gif)                                             
             ![[,] [,]](_icc.gif)                 |
30 | 29 | 2ralbidv 2843 |
. . . . 5
             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                       
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)                 |
31 | 30 | rspcev 3161 |
. . . 4
              ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                           ![[,] [,]](_icc.gif)              
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                         |
32 | 26, 31 | syl 17 |
. . 3
 

    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                         |
33 | | breq1 4418 |
. . . . . . . . . 10
 
   |
34 | | fveq2 5887 |
. . . . . . . . . . . . 13
           |
35 | 34 | oveq2d 6330 |
. . . . . . . . . . . 12
                       |
36 | 35 | fveq2d 5891 |
. . . . . . . . . . 11
                               |
37 | | oveq2 6322 |
. . . . . . . . . . . . 13
       |
38 | 37 | fveq2d 5891 |
. . . . . . . . . . . 12
               |
39 | 38 | oveq2d 6330 |
. . . . . . . . . . 11
                   |
40 | 36, 39 | breq12d 4428 |
. . . . . . . . . 10
               
       
                         |
41 | 33, 40 | imbi12d 326 |
. . . . . . . . 9
                
        

                          |
42 | | breq2 4419 |
. . . . . . . . . 10
 
   |
43 | | fveq2 5887 |
. . . . . . . . . . . . 13
           |
44 | 43 | oveq1d 6329 |
. . . . . . . . . . . 12
                       |
45 | 44 | fveq2d 5891 |
. . . . . . . . . . 11
                               |
46 | | oveq1 6321 |
. . . . . . . . . . . . 13
       |
47 | 46 | fveq2d 5891 |
. . . . . . . . . . . 12
               |
48 | 47 | oveq2d 6330 |
. . . . . . . . . . 11
                   |
49 | 45, 48 | breq12d 4428 |
. . . . . . . . . 10
               
       
                         |
50 | 42, 49 | imbi12d 326 |
. . . . . . . . 9
                
        

                          |
51 | 41, 50 | rspc2v 3170 |
. . . . . . . 8
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                       
                          |
52 | 51 | ad2antlr 738 |
. . . . . . 7
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                           
                          |
53 | | pm2.27 40 |
. . . . . . . 8
                
                      
           |
54 | 53 | adantl 472 |
. . . . . . 7
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                    
                      
           |
55 | 52, 54 | syld 45 |
. . . . . 6
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                                        
           |
56 | | 0le0 10726 |
. . . . . . . . . 10
 |
57 | | fvres 5901 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
58 | 57 | ad2antrl 739 |
. . . . . . . . . . . . . . 15
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)            |
59 | | cncff 21973 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
60 | 23, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
61 | 60 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
62 | | simpl 463 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
63 | | ffvelrn 6042 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
64 | 61, 62, 63 | syl2an 484 |
. . . . . . . . . . . . . . 15
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
65 | 58, 64 | eqeltrrd 2540 |
. . . . . . . . . . . . . 14
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)          |
66 | 65 | recnd 9694 |
. . . . . . . . . . . . 13
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)          |
67 | 66 | subidd 9999 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                |
68 | 67 | abs00bd 13402 |
. . . . . . . . . . 11
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                    |
69 | | iccssre 11744 |
. . . . . . . . . . . . . . . . . . 19
 
   ![[,] [,]](_icc.gif) 
  |
70 | 4, 6, 69 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif) 
  |
71 | 70 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . 17
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
72 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
73 | 71, 72 | sseldd 3444 |
. . . . . . . . . . . . . . . 16
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
74 | 73 | recnd 9694 |
. . . . . . . . . . . . . . 15
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
75 | 74 | subidd 9999 |
. . . . . . . . . . . . . 14
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        |
76 | 75 | abs00bd 13402 |
. . . . . . . . . . . . 13
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)            |
77 | 76 | oveq2d 6330 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                |
78 | | simplr 767 |
. . . . . . . . . . . . . 14
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
79 | 78 | recnd 9694 |
. . . . . . . . . . . . 13
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
80 | 79 | mul01d 9857 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        |
81 | 77, 80 | eqtrd 2495 |
. . . . . . . . . . 11
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)              |
82 | 68, 81 | breq12d 4428 |
. . . . . . . . . 10
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                  
       
   |
83 | 56, 82 | mpbiri 241 |
. . . . . . . . 9
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                            |
84 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
85 | 84 | oveq1d 6329 |
. . . . . . . . . . 11
                       |
86 | 85 | fveq2d 5891 |
. . . . . . . . . 10
                               |
87 | | oveq1 6321 |
. . . . . . . . . . . 12
       |
88 | 87 | fveq2d 5891 |
. . . . . . . . . . 11
               |
89 | 88 | oveq2d 6330 |
. . . . . . . . . 10
                   |
90 | 86, 89 | breq12d 4428 |
. . . . . . . . 9
               
       
                         |
91 | 83, 90 | syl5ibcom 228 |
. . . . . . . 8
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                  
           |
92 | 91 | imp 435 |
. . . . . . 7
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                  
          |
93 | 92 | a1d 26 |
. . . . . 6
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                                    
           |
94 | | breq1 4418 |
. . . . . . . . . . 11
 
   |
95 | | fveq2 5887 |
. . . . . . . . . . . . . 14
           |
96 | 95 | oveq2d 6330 |
. . . . . . . . . . . . 13
                       |
97 | 96 | fveq2d 5891 |
. . . . . . . . . . . 12
                               |
98 | | oveq2 6322 |
. . . . . . . . . . . . . 14
       |
99 | 98 | fveq2d 5891 |
. . . . . . . . . . . . 13
               |
100 | 99 | oveq2d 6330 |
. . . . . . . . . . . 12
                   |
101 | 97, 100 | breq12d 4428 |
. . . . . . . . . . 11
               
       
                         |
102 | 94, 101 | imbi12d 326 |
. . . . . . . . . 10
                
        

                          |
103 | | breq2 4419 |
. . . . . . . . . . 11
 
   |
104 | | fveq2 5887 |
. . . . . . . . . . . . . 14
           |
105 | 104 | oveq1d 6329 |
. . . . . . . . . . . . 13
                       |
106 | 105 | fveq2d 5891 |
. . . . . . . . . . . 12
                               |
107 | | oveq1 6321 |
. . . . . . . . . . . . . 14
       |
108 | 107 | fveq2d 5891 |
. . . . . . . . . . . . 13
               |
109 | 108 | oveq2d 6330 |
. . . . . . . . . . . 12
                   |
110 | 106, 109 | breq12d 4428 |
. . . . . . . . . . 11
               
       
                         |
111 | 103, 110 | imbi12d 326 |
. . . . . . . . . 10
                
        

                          |
112 | 102, 111 | rspc2v 3170 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                       
                          |
113 | 112 | ancoms 459 |
. . . . . . . 8
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                       
                          |
114 | 113 | ad2antlr 738 |
. . . . . . 7
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                           
                          |
115 | | simpr 467 |
. . . . . . . 8
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)       |
116 | | fvres 5901 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
117 | 116 | ad2antll 740 |
. . . . . . . . . . . . . 14
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)            |
118 | | simpr 467 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
119 | | ffvelrn 6042 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
120 | 61, 118, 119 | syl2an 484 |
. . . . . . . . . . . . . 14
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
121 | 117, 120 | eqeltrrd 2540 |
. . . . . . . . . . . . 13
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)          |
122 | 121 | recnd 9694 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)          |
123 | 66, 122 | abssubd 13563 |
. . . . . . . . . . 11
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                  |
124 | 123 | adantr 471 |
. . . . . . . . . 10
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                                   |
125 | 70 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
       ![[,] [,]](_icc.gif)    |
126 | 125 | sseld 3442 |
. . . . . . . . . . . . . . 15
        ![[,] [,]](_icc.gif) 
   |
127 | 125 | sseld 3442 |
. . . . . . . . . . . . . . 15
        ![[,] [,]](_icc.gif)     |
128 | 126, 127 | anim12d 570 |
. . . . . . . . . . . . . 14
         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     |
129 | 128 | imp 435 |
. . . . . . . . . . . . 13
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
   |
130 | | recn 9654 |
. . . . . . . . . . . . . 14
   |
131 | | recn 9654 |
. . . . . . . . . . . . . 14
   |
132 | | abssub 13437 |
. . . . . . . . . . . . . 14
 
               |
133 | 130, 131,
132 | syl2an 484 |
. . . . . . . . . . . . 13
 
               |
134 | 129, 133 | syl 17 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                  |
135 | 134 | adantr 471 |
. . . . . . . . . . 11
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                   |
136 | 135 | oveq2d 6330 |
. . . . . . . . . 10
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                       |
137 | 124, 136 | breq12d 4428 |
. . . . . . . . 9
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                   
       
                         |
138 | 137 | biimpd 212 |
. . . . . . . 8
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                   
                                 |
139 | 115, 138 | embantd 56 |
. . . . . . 7
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)                    
                      
           |
140 | 114, 139 | syld 45 |
. . . . . 6
    

    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                                        
           |
141 | | lttri4 9743 |
. . . . . . 7
 
 
   |
142 | 129, 141 | syl 17 |
. . . . . 6
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
   |
143 | 55, 93, 140, 142 | mpjao3dan 1344 |
. . . . 5
    
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                                        
           |
144 | 143 | ralrimdvva 2823 |
. . . 4
      
  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
           |
145 | 144 | reximdva 2873 |
. . 3
 

 
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
                           ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                            |
146 | 32, 145 | mpd 15 |
. 2
 

    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                
          |
147 | 15, 146, 6, 4 | ltlecasei 9767 |
1
     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                           |