Step | Hyp | Ref
| Expression |
1 | | c1liplem1.k |
. . 3
            ![[,] [,]](_icc.gif)       |
2 | | imassrn 5179 |
. . . . . 6
          ![[,] [,]](_icc.gif)     |
3 | | absf 13400 |
. . . . . . 7
     |
4 | | frn 5735 |
. . . . . . 7
       |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
 |
6 | 2, 5 | sstri 3441 |
. . . . 5
          ![[,] [,]](_icc.gif)     |
7 | 6 | a1i 11 |
. . . 4
           ![[,] [,]](_icc.gif)   
  |
8 | | dvf 22862 |
. . . . . . . 8
         |
9 | | ffun 5731 |
. . . . . . . 8
             |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
   |
11 | 10 | a1i 11 |
. . . . . 6
     |
12 | | c1liplem1.dv |
. . . . . . . 8
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
13 | | cncff 21925 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
14 | | fdm 5733 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
16 | | ssdmres 5126 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
 
     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
17 | 15, 16 | sylibr 216 |
. . . . . 6
   ![[,] [,]](_icc.gif) 
    |
18 | | c1liplem1.a |
. . . . . . . 8
   |
19 | 18 | rexrd 9690 |
. . . . . . 7
   |
20 | | c1liplem1.b |
. . . . . . . 8
   |
21 | 20 | rexrd 9690 |
. . . . . . 7
   |
22 | | c1liplem1.le |
. . . . . . 7

  |
23 | | lbicc2 11748 |
. . . . . . 7
     ![[,] [,]](_icc.gif)    |
24 | 19, 21, 22, 23 | syl3anc 1268 |
. . . . . 6
   ![[,] [,]](_icc.gif)    |
25 | | funfvima2 6141 |
. . . . . . 7
      ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)      |
26 | 25 | imp 431 |
. . . . . 6
       ![[,] [,]](_icc.gif) 
  
  ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)     |
27 | 11, 17, 24, 26 | syl21anc 1267 |
. . . . 5
              ![[,] [,]](_icc.gif)     |
28 | | ffun 5731 |
. . . . . . 7
       |
29 | 3, 28 | ax-mp 5 |
. . . . . 6
 |
30 | | imassrn 5179 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)      |
31 | | frn 5735 |
. . . . . . . . 9
             |
32 | 8, 31 | ax-mp 5 |
. . . . . . . 8
   |
33 | 30, 32 | sstri 3441 |
. . . . . . 7
       ![[,] [,]](_icc.gif)    |
34 | 3 | fdmi 5734 |
. . . . . . 7
 |
35 | 33, 34 | sseqtr4i 3465 |
. . . . . 6
       ![[,] [,]](_icc.gif)    |
36 | | funfvima2 6141 |
. . . . . 6
 
       ![[,] [,]](_icc.gif)  
               ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)       |
37 | 29, 35, 36 | mp2an 678 |
. . . . 5
              ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)      |
38 | | ne0i 3737 |
. . . . 5
                     ![[,] [,]](_icc.gif)   
          ![[,] [,]](_icc.gif)      |
39 | 27, 37, 38 | 3syl 18 |
. . . 4
           ![[,] [,]](_icc.gif)      |
40 | | ax-resscn 9596 |
. . . . . . . 8
 |
41 | | ssid 3451 |
. . . . . . . 8
 |
42 | | cncfss 21931 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
43 | 40, 41, 42 | mp2an 678 |
. . . . . . 7
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      |
44 | 43, 12 | sseldi 3430 |
. . . . . 6
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
45 | | cniccbdd 22412 |
. . . . . 6
 
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
46 | 18, 20, 44, 45 | syl3anc 1268 |
. . . . 5
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
47 | | fvelima 5917 |
. . . . . . . . . 10
 
          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
48 | 29, 47 | mpan 676 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif)   
        ![[,] [,]](_icc.gif)          |
49 | | fvelima 5917 |
. . . . . . . . . . . . . 14
           ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)           |
50 | 10, 49 | mpan 676 |
. . . . . . . . . . . . 13
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)           |
51 | | fvres 5879 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)              |
52 | 51 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)              |
53 | 52 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                   |
54 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
55 | 54 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
          ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)         |
56 | 55 | breq1d 4412 |
. . . . . . . . . . . . . . . . . 18
           ![[,] [,]](_icc.gif)      
         ![[,] [,]](_icc.gif)      
   |
57 | 56 | rspccva 3149 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
58 | 53, 57 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)               |
59 | 58 | adantll 720 |
. . . . . . . . . . . . . . 15
   
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)            
  |
60 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
      
                |
61 | 60 | breq1d 4412 |
. . . . . . . . . . . . . . 15
      
          
       |
62 | 59, 61 | syl5ibcom 224 |
. . . . . . . . . . . . . 14
   
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)             
   |
63 | 62 | rexlimdva 2879 |
. . . . . . . . . . . . 13
    
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      
     ![[,] [,]](_icc.gif)            
   |
64 | 50, 63 | syl5 33 |
. . . . . . . . . . . 12
    
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      
         ![[,] [,]](_icc.gif)      
   |
65 | 64 | imp 431 |
. . . . . . . . . . 11
   
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       
       ![[,] [,]](_icc.gif)       
  |
66 | | breq1 4405 |
. . . . . . . . . . 11
         
   |
67 | 65, 66 | syl5ibcom 224 |
. . . . . . . . . 10
   
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       
       ![[,] [,]](_icc.gif)        
   |
68 | 67 | rexlimdva 2879 |
. . . . . . . . 9
    
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      
          ![[,] [,]](_icc.gif)       
   |
69 | 48, 68 | syl5 33 |
. . . . . . . 8
    
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      
            ![[,] [,]](_icc.gif)       |
70 | 69 | ralrimiv 2800 |
. . . . . . 7
    
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      
            ![[,] [,]](_icc.gif)    
  |
71 | 70 | ex 436 |
. . . . . 6
 

 
  ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      
           ![[,] [,]](_icc.gif)        |
72 | 71 | reximdva 2862 |
. . . . 5
      ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)        |
73 | 46, 72 | mpd 15 |
. . . 4
             ![[,] [,]](_icc.gif)       |
74 | | suprcl 10569 |
. . . 4
            ![[,] [,]](_icc.gif)   
          ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)     
            ![[,] [,]](_icc.gif)        |
75 | 7, 39, 73, 74 | syl3anc 1268 |
. . 3
             ![[,] [,]](_icc.gif)        |
76 | 1, 75 | syl5eqel 2533 |
. 2
   |
77 | | simplrr 771 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    |
78 | | fvres 5879 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
79 | 77, 78 | syl 17 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)            |
80 | | c1liplem1.cn |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
81 | | cncff 21925 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
83 | 82 | ad2antrr 732 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
84 | 83, 77 | ffvelrnd 6023 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)        |
85 | 84 | recnd 9669 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)        |
86 | 79, 85 | eqeltrrd 2530 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      |
87 | | simplrl 770 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    |
88 | | fvres 5879 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
89 | 87, 88 | syl 17 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)            |
90 | 83, 87 | ffvelrnd 6023 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)        |
91 | 90 | recnd 9669 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)        |
92 | 89, 91 | eqeltrrd 2530 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      |
93 | 86, 92 | subcld 9986 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
            |
94 | | iccssre 11716 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif) 
  |
95 | 18, 20, 94 | syl2anc 667 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 
  |
96 | 95 | ad2antrr 732 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    |
97 | 96, 77 | sseldd 3433 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
98 | 96, 87 | sseldd 3433 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
99 | 97, 98 | resubcld 10047 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    |
100 | 99 | recnd 9669 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    |
101 | | simpr 463 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
102 | | difrp 11337 |
. . . . . . . . . . 11
 
       |
103 | 98, 97, 102 | syl2anc 667 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      |
104 | 101, 103 | mpbid 214 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    |
105 | 104 | rpne0d 11346 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    |
106 | 93, 100, 105 | absdivd 13517 |
. . . . . . 7
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                          |
107 | 6 | a1i 11 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
          ![[,] [,]](_icc.gif)   
  |
108 | 39 | ad2antrr 732 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
          ![[,] [,]](_icc.gif)      |
109 | 73 | ad2antrr 732 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
            ![[,] [,]](_icc.gif)       |
110 | 29 | a1i 11 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
111 | 93, 100, 105 | divcld 10383 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                |
112 | 111, 34 | syl6eleqr 2540 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                |
113 | 98 | rexrd 9690 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
114 | 97 | rexrd 9690 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
115 | 98, 97, 101 | ltled 9783 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
116 | | ubicc2 11749 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)    |
117 | 113, 114,
115, 116 | syl3anc 1268 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    |
118 | | fvres 5879 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)            |
120 | | lbicc2 11748 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)    |
121 | 113, 114,
115, 120 | syl3anc 1268 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    |
122 | | fvres 5879 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)            |
124 | 119, 123 | oveq12d 6308 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                   |
125 | 124 | oveq1d 6305 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                          |
126 | | iccss2 11705 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    |
127 | 126 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
128 | 127 | resabs1d 5134 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     |
129 | 80 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
130 | | rescncf 21929 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
131 | 127, 129,
130 | sylc 62 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
132 | 128, 131 | eqeltrrd 2530 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
133 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
134 | | c1liplem1.f |
. . . . . . . . . . . . . . . . . . 19
     |
135 | 134 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    

   |
136 | | cnex 9620 |
. . . . . . . . . . . . . . . . . . . 20
 |
137 | | reex 9630 |
. . . . . . . . . . . . . . . . . . . 20
 |
138 | 136, 137 | elpm2 7503 |
. . . . . . . . . . . . . . . . . . 19
           |
139 | 138 | simplbi 462 |
. . . . . . . . . . . . . . . . . 18
  
      |
140 | 135, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      |
141 | 138 | simprbi 466 |
. . . . . . . . . . . . . . . . . 18
  
  |
142 | 135, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
143 | | iccssre 11716 |
. . . . . . . . . . . . . . . . . 18
 
   ![[,] [,]](_icc.gif) 
  |
144 | 98, 97, 143 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)    |
145 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
  ℂfld   ℂfld |
146 | 145 | tgioo2 21821 |
. . . . . . . . . . . . . . . . . 18
       ℂfld
↾t   |
147 | 145, 146 | dvres 22866 |
. . . . . . . . . . . . . . . . 17
       

  ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)             
      ![[,] [,]](_icc.gif)      |
148 | 133, 140,
142, 144, 147 | syl22anc 1269 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)      |
149 | | iccntr 21839 |
. . . . . . . . . . . . . . . . . 18
 
       
      ![[,] [,]](_icc.gif)         |
150 | 98, 97, 149 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
             ![[,] [,]](_icc.gif)         |
151 | 150 | reseq2d 5105 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
         
      ![[,] [,]](_icc.gif)              |
152 | 148, 151 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)              |
153 | 152 | dmeqd 5037 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)              |
154 | | ioossicc 11720 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif)   |
155 | 154, 127 | syl5ss 3443 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      ![[,] [,]](_icc.gif)    |
156 | 17 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  ![[,] [,]](_icc.gif)  
   |
157 | 155, 156 | sstrd 3442 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    
   |
158 | | ssdmres 5126 |
. . . . . . . . . . . . . . 15
    
 
              |
159 | 157, 158 | sylib 200 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
              |
160 | 153, 159 | eqtrd 2485 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)          |
161 | 98, 97, 101, 132, 160 | mvth 22944 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
           ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)            |
162 | 152 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
     ![[,] [,]](_icc.gif)                     |
163 | 162 | adantrr 723 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        
  ![[,] [,]](_icc.gif)                     |
164 | | fvres 5879 |
. . . . . . . . . . . . . . . . . 18
                         |
165 | 164 | ad2antll 735 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                          |
166 | 163, 165 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        
  ![[,] [,]](_icc.gif)               |
167 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
          |
168 | 17 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        ![[,] [,]](_icc.gif) 
    |
169 | 155 | sseld 3431 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    
  ![[,] [,]](_icc.gif)     |
170 | 169 | impr 625 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        ![[,] [,]](_icc.gif)    |
171 | | funfvima2 6141 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)      |
172 | 171 | imp 431 |
. . . . . . . . . . . . . . . . 17
       ![[,] [,]](_icc.gif) 
  
  ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)     |
173 | 167, 168,
170, 172 | syl21anc 1267 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                   ![[,] [,]](_icc.gif)     |
174 | 166, 173 | eqeltrd 2529 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        
  ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     |
175 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)      |
176 | 174, 175 | syl5ibcom 224 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
            ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)      |
177 | 176 | expr 620 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
    
      ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)       |
178 | 177 | rexlimdv 2877 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
 
          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)      |
179 | 161, 178 | mpd 15 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
      ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)     |
180 | 125, 179 | eqeltrrd 2530 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)     |
181 | | funfvima 6140 |
. . . . . . . . . . 11
 
                                     ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)       |
182 | 181 | imp 431 |
. . . . . . . . . 10
                                       ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)      |
183 | 110, 112,
180, 182 | syl21anc 1267 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                            ![[,] [,]](_icc.gif)      |
184 | | suprub 10570 |
. . . . . . . . 9
             ![[,] [,]](_icc.gif)   
          ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)     
                            ![[,] [,]](_icc.gif)                      
            ![[,] [,]](_icc.gif)        |
185 | 107, 108,
109, 183, 184 | syl31anc 1271 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                 
            ![[,] [,]](_icc.gif)        |
186 | 185, 1 | syl6breqr 4443 |
. . . . . . 7
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                 
  |
187 | 106, 186 | eqbrtrrd 4425 |
. . . . . 6
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                        |
188 | 93 | abscld 13498 |
. . . . . . 7
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                |
189 | 76 | ad2antrr 732 |
. . . . . . 7
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
190 | 100, 105 | absrpcld 13510 |
. . . . . . 7
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        |
191 | 188, 189,
190 | ledivmuld 11391 |
. . . . . 6
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                                    
           |
192 | 187, 191 | mpbid 214 |
. . . . 5
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                        |
193 | 190 | rpcnd 11343 |
. . . . . 6
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
        |
194 | 189 | recnd 9669 |
. . . . . 6
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
  |
195 | 193, 194 | mulcomd 9664 |
. . . . 5
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                  |
196 | 192, 195 | breqtrd 4427 |
. . . 4
      ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
              
         |
197 | 196 | ex 436 |
. . 3
 
   ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    
                         |
198 | 197 | ralrimivva 2809 |
. 2
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                 
           |
199 | 76, 198 | jca 535 |
1
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                 
            |