Step | Hyp | Ref
| Expression |
1 | | simpll 760 |
. . . . . 6
       |
2 | | iccmbl 22519 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)    |
3 | 2 | adantll 720 |
. . . . . 6
       ![[,] [,]](_icc.gif)    |
4 | | inmbl 22495 |
. . . . . 6
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
5 | 1, 3, 4 | syl2anc 667 |
. . . . 5
        ![[,] [,]](_icc.gif)     |
6 | | mblvol 22484 |
. . . . 5
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
7 | 5, 6 | syl 17 |
. . . 4
           ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
8 | | inss2 3653 |
. . . . . 6
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
9 | 8 | a1i 11 |
. . . . 5
        ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
10 | | mblss 22485 |
. . . . . 6
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
11 | 3, 10 | syl 17 |
. . . . 5
       ![[,] [,]](_icc.gif)    |
12 | | mblvol 22484 |
. . . . . . 7
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     |
13 | 3, 12 | syl 17 |
. . . . . 6
          ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     |
14 | | iccvolcl 22520 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)     |
15 | 14 | adantll 720 |
. . . . . 6
          ![[,] [,]](_icc.gif)     |
16 | 13, 15 | eqeltrrd 2530 |
. . . . 5
           ![[,] [,]](_icc.gif)     |
17 | | ovolsscl 22439 |
. . . . 5
     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
18 | 9, 11, 16, 17 | syl3anc 1268 |
. . . 4
            ![[,] [,]](_icc.gif)      |
19 | 7, 18 | eqeltrd 2529 |
. . 3
           ![[,] [,]](_icc.gif)      |
20 | | volcn.1 |
. . 3
       ![[,] [,]](_icc.gif)      |
21 | 19, 20 | fmptd 6046 |
. 2
         |
22 | | simprr 766 |
. . . 4
         |
23 | | oveq12 6299 |
. . . . . . . . . . . . 13
 
       |
24 | 23 | ancoms 455 |
. . . . . . . . . . . 12
 
       |
25 | 24 | fveq2d 5869 |
. . . . . . . . . . 11
 
               |
26 | 25 | breq1d 4412 |
. . . . . . . . . 10
 
       
         |
27 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
28 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
29 | 27, 28 | oveqan12rd 6310 |
. . . . . . . . . . . 12
 
                       |
30 | 29 | fveq2d 5869 |
. . . . . . . . . . 11
 
                               |
31 | 30 | breq1d 4412 |
. . . . . . . . . 10
 
               
                 |
32 | 26, 31 | imbi12d 322 |
. . . . . . . . 9
 
                                                 |
33 | | oveq12 6299 |
. . . . . . . . . . . . 13
 
       |
34 | 33 | ancoms 455 |
. . . . . . . . . . . 12
 
       |
35 | 34 | fveq2d 5869 |
. . . . . . . . . . 11
 
               |
36 | 35 | breq1d 4412 |
. . . . . . . . . 10
 
       
         |
37 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
38 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
39 | 37, 38 | oveqan12rd 6310 |
. . . . . . . . . . . 12
 
                       |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . 11
 
                               |
41 | 40 | breq1d 4412 |
. . . . . . . . . 10
 
               
                 |
42 | 36, 41 | imbi12d 322 |
. . . . . . . . 9
 
                                                 |
43 | | ssid 3451 |
. . . . . . . . . 10
 |
44 | 43 | a1i 11 |
. . . . . . . . 9
       |
45 | | recn 9629 |
. . . . . . . . . . . . 13
   |
46 | | recn 9629 |
. . . . . . . . . . . . 13
   |
47 | | abssub 13389 |
. . . . . . . . . . . . 13
 
               |
48 | 45, 46, 47 | syl2anr 481 |
. . . . . . . . . . . 12
 
               |
49 | 48 | adantl 468 |
. . . . . . . . . . 11
      
 
              |
50 | 49 | breq1d 4412 |
. . . . . . . . . 10
      
 
                |
51 | 21 | adantr 467 |
. . . . . . . . . . . . 13
           |
52 | | ffvelrn 6020 |
. . . . . . . . . . . . . 14
     
       |
53 | | ffvelrn 6020 |
. . . . . . . . . . . . . 14
     
       |
54 | 52, 53 | anim12dan 848 |
. . . . . . . . . . . . 13
        
            |
55 | 51, 54 | sylan 474 |
. . . . . . . . . . . 12
      
 
            |
56 | | recn 9629 |
. . . . . . . . . . . . 13
           |
57 | | recn 9629 |
. . . . . . . . . . . . 13
           |
58 | | abssub 13389 |
. . . . . . . . . . . . 13
                                         |
59 | 56, 57, 58 | syl2anr 481 |
. . . . . . . . . . . 12
                                         |
60 | 55, 59 | syl 17 |
. . . . . . . . . . 11
      
 
                              |
61 | 60 | breq1d 4412 |
. . . . . . . . . 10
      
 
                                |
62 | 50, 61 | imbi12d 322 |
. . . . . . . . 9
      
 
                                                |
63 | | simpr2 1015 |
. . . . . . . . . . . . . . 15
      
    |
64 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
65 | 64 | ineq2d 3634 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
66 | 65 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      |
67 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)     |
68 | 66, 20, 67 | fvmpt 5948 |
. . . . . . . . . . . . . . 15
           ![[,] [,]](_icc.gif)      |
69 | 63, 68 | syl 17 |
. . . . . . . . . . . . . 14
      
            ![[,] [,]](_icc.gif)      |
70 | | simplll 768 |
. . . . . . . . . . . . . . . 16
      
 
  |
71 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
       |
72 | 71 | adantr 467 |
. . . . . . . . . . . . . . . . 17
      
 
  |
73 | | iccmbl 22519 |
. . . . . . . . . . . . . . . . 17
 
   ![[,] [,]](_icc.gif)    |
74 | 72, 63, 73 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
      
    ![[,] [,]](_icc.gif)    |
75 | | inmbl 22495 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
76 | 70, 74, 75 | syl2anc 667 |
. . . . . . . . . . . . . . 15
      
     ![[,] [,]](_icc.gif)     |
77 | | mblvol 22484 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . 14
      
        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
79 | 69, 78 | eqtrd 2485 |
. . . . . . . . . . . . 13
      
             ![[,] [,]](_icc.gif)      |
80 | | simpr1 1014 |
. . . . . . . . . . . . . . 15
      
    |
81 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
82 | 81 | ineq2d 3634 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
83 | 82 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      |
84 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)     |
85 | 83, 20, 84 | fvmpt 5948 |
. . . . . . . . . . . . . . 15
           ![[,] [,]](_icc.gif)      |
86 | 80, 85 | syl 17 |
. . . . . . . . . . . . . 14
      
            ![[,] [,]](_icc.gif)      |
87 | | simp1 1008 |
. . . . . . . . . . . . . . . . 17
 
   |
88 | | iccmbl 22519 |
. . . . . . . . . . . . . . . . 17
 
   ![[,] [,]](_icc.gif)    |
89 | 71, 87, 88 | syl2an 480 |
. . . . . . . . . . . . . . . 16
      
    ![[,] [,]](_icc.gif)    |
90 | | inmbl 22495 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
91 | 70, 89, 90 | syl2anc 667 |
. . . . . . . . . . . . . . 15
      
     ![[,] [,]](_icc.gif)     |
92 | | mblvol 22484 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . 14
      
        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)      |
94 | 86, 93 | eqtrd 2485 |
. . . . . . . . . . . . 13
      
             ![[,] [,]](_icc.gif)      |
95 | 79, 94 | oveq12d 6308 |
. . . . . . . . . . . 12
      
                    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)       |
96 | 51 | adantr 467 |
. . . . . . . . . . . . . . . 16
      
        |
97 | 96, 63 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
      
        |
98 | 79, 97 | eqeltrrd 2530 |
. . . . . . . . . . . . . 14
      
      
  ![[,] [,]](_icc.gif)      |
99 | 72 | leidd 10180 |
. . . . . . . . . . . . . . . . . . 19
      
    |
100 | | simpr3 1016 |
. . . . . . . . . . . . . . . . . . 19
      
 
  |
101 | | iccss 11702 |
. . . . . . . . . . . . . . . . . . 19
         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
102 | 72, 63, 99, 100, 101 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . 18
      
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    |
103 | | sslin 3658 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
      
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
105 | | mblss 22485 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
106 | 76, 105 | syl 17 |
. . . . . . . . . . . . . . . . 17
      
     ![[,] [,]](_icc.gif)     |
107 | 104, 106 | sstrd 3442 |
. . . . . . . . . . . . . . . 16
      
     ![[,] [,]](_icc.gif)     |
108 | | iccssre 11716 |
. . . . . . . . . . . . . . . . 17
 
   ![[,] [,]](_icc.gif) 
  |
109 | 80, 63, 108 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
      
    ![[,] [,]](_icc.gif) 
  |
110 | 107, 109 | unssd 3610 |
. . . . . . . . . . . . . . 15
      
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
111 | 96, 80 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . 17
      
        |
112 | 94, 111 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . 16
      
      
  ![[,] [,]](_icc.gif)      |
113 | 63, 80 | resubcld 10047 |
. . . . . . . . . . . . . . . 16
      
      |
114 | 112, 113 | readdcld 9670 |
. . . . . . . . . . . . . . 15
      
          ![[,] [,]](_icc.gif)         |
115 | | ovolicc 22477 |
. . . . . . . . . . . . . . . . . . 19
 
       ![[,] [,]](_icc.gif)       |
116 | 115 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
      
        ![[,] [,]](_icc.gif)       |
117 | 116, 113 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . 17
      
        ![[,] [,]](_icc.gif)     |
118 | | ovolun 22452 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif)  
       ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      |
119 | 107, 112,
109, 117, 118 | syl22anc 1269 |
. . . . . . . . . . . . . . . 16
      
          ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      |
120 | 116 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
      
          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
121 | 119, 120 | breqtrd 4427 |
. . . . . . . . . . . . . . 15
      
          ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
        ![[,] [,]](_icc.gif)         |
122 | | ovollecl 22436 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)  
     
  ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
123 | 110, 114,
121, 122 | syl3anc 1268 |
. . . . . . . . . . . . . 14
      
          ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
124 | 72 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  |
125 | 63 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  |
126 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
  |
127 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
  |
128 | 100 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
  |
129 | | simp2 1009 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
130 | | elicc2 11699 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    ![[,] [,]](_icc.gif)  
    |
131 | 71, 129, 130 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . 22
      
     ![[,] [,]](_icc.gif)  
    |
132 | 131 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
   ![[,] [,]](_icc.gif)  
    |
133 | 126, 127,
128, 132 | mpbir3and 1191 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  ![[,] [,]](_icc.gif)    |
134 | | iccsplit 11765 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
135 | 124, 125,
133, 134 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
    

    
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
136 | | eqimss 3484 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    

    
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
138 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  |
139 | 63 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  |
140 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  |
141 | 139 | leidd 10180 |
. . . . . . . . . . . . . . . . . . . 20
    

    
  |
142 | | iccss 11702 |
. . . . . . . . . . . . . . . . . . . 20
         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
143 | 138, 139,
140, 141, 142 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . 19
    

    
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
144 | | ssun4 3600 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    

    
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
146 | 72, 80, 137, 145 | lecasei 9740 |
. . . . . . . . . . . . . . . . 17
      
    ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
147 | | sslin 3658 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . 16
      
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
149 | | indi 3689 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
150 | | inss2 3653 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
151 | | unss2 3605 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
153 | 149, 152 | eqsstri 3462 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
154 | 148, 153 | syl6ss 3444 |
. . . . . . . . . . . . . . 15
      
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)     |
155 | | ovolss 22438 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
156 | 154, 110,
155 | syl2anc 667 |
. . . . . . . . . . . . . 14
      
      
  ![[,] [,]](_icc.gif)   
        ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)      |
157 | 98, 123, 114, 156, 121 | letrd 9792 |
. . . . . . . . . . . . 13
      
      
  ![[,] [,]](_icc.gif)   
        ![[,] [,]](_icc.gif)         |
158 | 98, 112, 113 | lesubadd2d 10212 |
. . . . . . . . . . . . 13
      
           ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    
 
       ![[,] [,]](_icc.gif)         
  ![[,] [,]](_icc.gif)          |
159 | 157, 158 | mpbird 236 |
. . . . . . . . . . . 12
      
          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)         |
160 | 95, 159 | eqbrtrd 4423 |
. . . . . . . . . . 11
      
           
    |
161 | 97, 111 | resubcld 10047 |
. . . . . . . . . . . 12
      
              |
162 | | simplr 762 |
. . . . . . . . . . . . 13
      
    |
163 | 162 | rpred 11341 |
. . . . . . . . . . . 12
      
    |
164 | | lelttr 9724 |
. . . . . . . . . . . 12
             
              
                |
165 | 161, 113,
163, 164 | syl3anc 1268 |
. . . . . . . . . . 11
      
               
                |
166 | 160, 165 | mpand 681 |
. . . . . . . . . 10
      
              
   |
167 | | abssubge0 13390 |
. . . . . . . . . . . 12
 
           |
168 | 167 | adantl 468 |
. . . . . . . . . . 11
      
            |
169 | 168 | breq1d 4412 |
. . . . . . . . . 10
      
        
     |
170 | | ovolss 22438 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
       ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)      |
171 | 104, 106,
170 | syl2anc 667 |
. . . . . . . . . . . . 13
      
      
  ![[,] [,]](_icc.gif)   
       ![[,] [,]](_icc.gif)      |
172 | 171, 94, 79 | 3brtr4d 4433 |
. . . . . . . . . . . 12
      
     
      |
173 | 111, 97, 172 | abssubge0d 13493 |
. . . . . . . . . . 11
      
                            |
174 | 173 | breq1d 4412 |
. . . . . . . . . 10
      
                
             |
175 | 166, 169,
174 | 3imtr4d 272 |
. . . . . . . . 9
      
                          |
176 | 32, 42, 44, 62, 175 | wlogle 10147 |
. . . . . . . 8
      
 
      
                 |
177 | 176 | anassrs 654 |
. . . . . . 7
    


                          |
178 | 177 | ralrimiva 2802 |
. . . . . 6
                                |
179 | 178 | anasss 653 |
. . . . 5
                                |
180 | 179 | ancom2s 811 |
. . . 4
                                |
181 | | breq2 4406 |
. . . . . . 7
       
         |
182 | 181 | imbi1d 319 |
. . . . . 6
                                                 |
183 | 182 | ralbidv 2827 |
. . . . 5
  
                      
                         |
184 | 183 | rspcev 3150 |
. . . 4
  
                      
                          |
185 | 22, 180, 184 | syl2anc 667 |
. . 3
                                 |
186 | 185 | ralrimivva 2809 |
. 2
                               |
187 | | ax-resscn 9596 |
. . 3
 |
188 | | elcncf2 21922 |
. . 3
 
 
                                       |
189 | 187, 187,
188 | mp2an 678 |
. 2
                                       |
190 | 21, 186, 189 | sylanbrc 670 |
1
         |