Proof of Theorem scvxcvx
Step | Hyp | Ref
| Expression |
1 | | scvxcvx.1 |
. . . . . . . . 9

  |
2 | 1 | adantr 452 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)      |
3 | | simpr1 963 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)   
  |
4 | 2, 3 | sseldd 3313 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)   
  |
5 | 4 | adantr 452 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)           |
6 | | simpr2 964 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)   
  |
7 | 2, 6 | sseldd 3313 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)   
  |
8 | 7 | adantr 452 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)           |
9 | 5, 8 | lttri4d 9174 |
. . . . 5
   
  ![[,] [,]](_icc.gif)         
   |
10 | | simprl 733 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)          
      |
11 | 3 | adantr 452 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)          
  |
12 | 6 | adantr 452 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)          
  |
13 | 11, 12 | jca 519 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)           
   |
14 | | simprr 734 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)             |
15 | | simpll 731 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)             |
16 | | breq1 4179 |
. . . . . . . . . . . 12
 
   |
17 | | oveq2 6052 |
. . . . . . . . . . . . . . . . 17
       |
18 | 17 | oveq1d 6059 |
. . . . . . . . . . . . . . . 16
                   |
19 | 18 | fveq2d 5695 |
. . . . . . . . . . . . . . 15
                           |
20 | | fveq2 5691 |
. . . . . . . . . . . . . . . . 17
           |
21 | 20 | oveq2d 6060 |
. . . . . . . . . . . . . . . 16
               |
22 | 21 | oveq1d 6059 |
. . . . . . . . . . . . . . 15
                                   |
23 | 19, 22 | breq12d 4189 |
. . . . . . . . . . . . . 14
                             
                               |
24 | 23 | ralbidv 2690 |
. . . . . . . . . . . . 13
  
                                
                                     |
25 | 24 | imbi2d 308 |
. . . . . . . . . . . 12
  
                                                                          |
26 | 16, 25 | imbi12d 312 |
. . . . . . . . . . 11
                                       

                                        |
27 | | breq2 4180 |
. . . . . . . . . . . 12
 
   |
28 | | oveq2 6052 |
. . . . . . . . . . . . . . . . 17
           |
29 | 28 | oveq2d 6060 |
. . . . . . . . . . . . . . . 16
                   |
30 | 29 | fveq2d 5695 |
. . . . . . . . . . . . . . 15
                           |
31 | | fveq2 5691 |
. . . . . . . . . . . . . . . . 17
           |
32 | 31 | oveq2d 6060 |
. . . . . . . . . . . . . . . 16
                   |
33 | 32 | oveq2d 6060 |
. . . . . . . . . . . . . . 15
                                   |
34 | 30, 33 | breq12d 4189 |
. . . . . . . . . . . . . 14
                             
                               |
35 | 34 | ralbidv 2690 |
. . . . . . . . . . . . 13
  
                                
                                     |
36 | 35 | imbi2d 308 |
. . . . . . . . . . . 12
  
                                                                          |
37 | 27, 36 | imbi12d 312 |
. . . . . . . . . . 11
                                       

                                        |
38 | | scvxcvx.4 |
. . . . . . . . . . . . . . 15
 

                                    |
39 | 38 | 3expia 1155 |
. . . . . . . . . . . . . 14
 

                                      |
40 | 39 | ralrimiv 2752 |
. . . . . . . . . . . . 13
 

  
                                   |
41 | 40 | expcom 425 |
. . . . . . . . . . . 12
 
 
                                     |
42 | 41 | 3expia 1155 |
. . . . . . . . . . 11
 
                                         |
43 | 26, 37, 42 | vtocl2ga 2983 |
. . . . . . . . . 10
 
                                         |
44 | 13, 14, 15, 43 | syl3c 59 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)           
                                   |
45 | | oveq1 6051 |
. . . . . . . . . . . . 13
       |
46 | | oveq2 6052 |
. . . . . . . . . . . . . 14
       |
47 | 46 | oveq1d 6059 |
. . . . . . . . . . . . 13
           |
48 | 45, 47 | oveq12d 6062 |
. . . . . . . . . . . 12
                   |
49 | 48 | fveq2d 5695 |
. . . . . . . . . . 11
                           |
50 | | oveq1 6051 |
. . . . . . . . . . . 12
               |
51 | 46 | oveq1d 6059 |
. . . . . . . . . . . 12
                   |
52 | 50, 51 | oveq12d 6062 |
. . . . . . . . . . 11
                                   |
53 | 49, 52 | breq12d 4189 |
. . . . . . . . . 10
                             
                               |
54 | 53 | rspcv 3012 |
. . . . . . . . 9
      
                                                                |
55 | 10, 44, 54 | sylc 58 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                                         |
56 | 55 | orcd 382 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)                                                                       |
57 | 56 | expr 599 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)                                                                       |
58 | | unitssre 11002 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)   |
59 | | simpr3 965 |
. . . . . . . . . . . . . . . 16
 

  ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
60 | 58, 59 | sseldi 3310 |
. . . . . . . . . . . . . . 15
 

  ![[,] [,]](_icc.gif)   
  |
61 | 60 | recnd 9074 |
. . . . . . . . . . . . . 14
 

  ![[,] [,]](_icc.gif)   
  |
62 | | ax-1cn 9008 |
. . . . . . . . . . . . . 14
 |
63 | | pncan3 9273 |
. . . . . . . . . . . . . 14
 
       |
64 | 61, 62, 63 | sylancl 644 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)          |
65 | 64 | oveq1d 6059 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)              |
66 | | subcl 9265 |
. . . . . . . . . . . . . 14
 
     |
67 | 62, 61, 66 | sylancr 645 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)        |
68 | 7 | recnd 9074 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)   
  |
69 | 61, 67, 68 | adddird 9073 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)                    |
70 | 68 | mulid2d 9066 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)        |
71 | 65, 69, 70 | 3eqtr3d 2448 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)              |
72 | 71 | fveq2d 5695 |
. . . . . . . . . 10
 

  ![[,] [,]](_icc.gif)                      |
73 | 64 | oveq1d 6059 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)                      |
74 | | scvxcvx.2 |
. . . . . . . . . . . . . . 15
       |
75 | 74 | adantr 452 |
. . . . . . . . . . . . . 14
 

  ![[,] [,]](_icc.gif)          |
76 | 75, 6 | ffvelrnd 5834 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)          |
77 | 76 | recnd 9074 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)          |
78 | 61, 67, 77 | adddird 9073 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)                                |
79 | 77 | mulid2d 9066 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)                |
80 | 73, 78, 79 | 3eqtr3d 2448 |
. . . . . . . . . 10
 

  ![[,] [,]](_icc.gif)                          |
81 | 72, 80 | eqtr4d 2443 |
. . . . . . . . 9
 

  ![[,] [,]](_icc.gif)                                  |
82 | 81 | adantr 452 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)             
                         |
83 | | oveq2 6052 |
. . . . . . . . . . 11
 
     |
84 | 83 | oveq1d 6059 |
. . . . . . . . . 10
                   |
85 | 84 | fveq2d 5695 |
. . . . . . . . 9
     
                     |
86 | | fveq2 5691 |
. . . . . . . . . . 11
           |
87 | 86 | oveq2d 6060 |
. . . . . . . . . 10
 
             |
88 | 87 | oveq1d 6059 |
. . . . . . . . 9
                                   |
89 | 85, 88 | eqeq12d 2422 |
. . . . . . . 8
                             
                               |
90 | 82, 89 | syl5ibrcom 214 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)         
                               |
91 | | olc 374 |
. . . . . . 7
                                                                                         |
92 | 90, 91 | syl6 31 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)         
                                                             |
93 | | 1re 9050 |
. . . . . . . . . . . . 13
 |
94 | | elioore 10906 |
. . . . . . . . . . . . 13
       |
95 | | resubcl 9325 |
. . . . . . . . . . . . 13
 
     |
96 | 93, 94, 95 | sylancr 645 |
. . . . . . . . . . . 12
         |
97 | | eliooord 10930 |
. . . . . . . . . . . . . 14
     
   |
98 | 97 | simprd 450 |
. . . . . . . . . . . . 13
       |
99 | | posdif 9481 |
. . . . . . . . . . . . . 14
 
       |
100 | 94, 93, 99 | sylancl 644 |
. . . . . . . . . . . . 13
     
     |
101 | 98, 100 | mpbid 202 |
. . . . . . . . . . . 12
         |
102 | 97 | simpld 446 |
. . . . . . . . . . . . 13
       |
103 | | ltsubpos 9480 |
. . . . . . . . . . . . . 14
 
       |
104 | 94, 93, 103 | sylancl 644 |
. . . . . . . . . . . . 13
     
     |
105 | 102, 104 | mpbid 202 |
. . . . . . . . . . . 12
         |
106 | | 0xr 9091 |
. . . . . . . . . . . . 13
 |
107 | 93 | rexri 9097 |
. . . . . . . . . . . . 13
 |
108 | | elioo2 10917 |
. . . . . . . . . . . . 13
         
    
      |
109 | 106, 107,
108 | mp2an 654 |
. . . . . . . . . . . 12
      
    
     |
110 | 96, 101, 105, 109 | syl3anbrc 1138 |
. . . . . . . . . . 11
             |
111 | 110 | ad2antrl 709 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                   |
112 | 6 | adantr 452 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)          
  |
113 | 3 | adantr 452 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)          
  |
114 | 112, 113 | jca 519 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)           
   |
115 | | simprr 734 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)             |
116 | | simpll 731 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)             |
117 | | breq1 4179 |
. . . . . . . . . . . . 13
 
   |
118 | | oveq2 6052 |
. . . . . . . . . . . . . . . . . 18
       |
119 | 118 | oveq1d 6059 |
. . . . . . . . . . . . . . . . 17
                   |
120 | 119 | fveq2d 5695 |
. . . . . . . . . . . . . . . 16
                           |
121 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . 18
           |
122 | 121 | oveq2d 6060 |
. . . . . . . . . . . . . . . . 17
               |
123 | 122 | oveq1d 6059 |
. . . . . . . . . . . . . . . 16
                                   |
124 | 120, 123 | breq12d 4189 |
. . . . . . . . . . . . . . 15
                             
                               |
125 | 124 | ralbidv 2690 |
. . . . . . . . . . . . . 14
  
                                
                                     |
126 | 125 | imbi2d 308 |
. . . . . . . . . . . . 13
  
                                                                          |
127 | 117, 126 | imbi12d 312 |
. . . . . . . . . . . 12
                                       

                                        |
128 | | breq2 4180 |
. . . . . . . . . . . . 13
 
   |
129 | | oveq2 6052 |
. . . . . . . . . . . . . . . . . 18
           |
130 | 129 | oveq2d 6060 |
. . . . . . . . . . . . . . . . 17
                   |
131 | 130 | fveq2d 5695 |
. . . . . . . . . . . . . . . 16
                           |
132 | | fveq2 5691 |
. . . . . . . . . . . . . . . . . 18
           |
133 | 132 | oveq2d 6060 |
. . . . . . . . . . . . . . . . 17
                   |
134 | 133 | oveq2d 6060 |
. . . . . . . . . . . . . . . 16
                                   |
135 | 131, 134 | breq12d 4189 |
. . . . . . . . . . . . . . 15
                             
                               |
136 | 135 | ralbidv 2690 |
. . . . . . . . . . . . . 14
  
                                
                                     |
137 | 136 | imbi2d 308 |
. . . . . . . . . . . . 13
  
                                                                          |
138 | 128, 137 | imbi12d 312 |
. . . . . . . . . . . 12
                                       

                                        |
139 | 127, 138,
42 | vtocl2ga 2983 |
. . . . . . . . . . 11
 
                                         |
140 | 114, 115,
116, 139 | syl3c 59 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)           
                                   |
141 | | oveq1 6051 |
. . . . . . . . . . . . . 14
           |
142 | | oveq2 6052 |
. . . . . . . . . . . . . . 15
           |
143 | 142 | oveq1d 6059 |
. . . . . . . . . . . . . 14
               |
144 | 141, 143 | oveq12d 6062 |
. . . . . . . . . . . . 13
                         |
145 | 144 | fveq2d 5695 |
. . . . . . . . . . . 12
                                 |
146 | | oveq1 6051 |
. . . . . . . . . . . . 13
                   |
147 | 142 | oveq1d 6059 |
. . . . . . . . . . . . 13
                       |
148 | 146, 147 | oveq12d 6062 |
. . . . . . . . . . . 12
                                         |
149 | 145, 148 | breq12d 4189 |
. . . . . . . . . . 11
                               
                                       |
150 | 149 | rspcv 3012 |
. . . . . . . . . 10
        
                                                                        |
151 | 111, 140,
150 | sylc 58 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                                                 |
152 | | nncan 9290 |
. . . . . . . . . . . . . . 15
 
       |
153 | 62, 61, 152 | sylancr 645 |
. . . . . . . . . . . . . 14
 

  ![[,] [,]](_icc.gif)          |
154 | 153 | oveq1d 6059 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)              |
155 | 154 | oveq2d 6060 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)                          |
156 | 93, 60, 95 | sylancr 645 |
. . . . . . . . . . . . . . 15
 

  ![[,] [,]](_icc.gif)        |
157 | 156, 7 | remulcld 9076 |
. . . . . . . . . . . . . 14
 

  ![[,] [,]](_icc.gif)          |
158 | 157 | recnd 9074 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)          |
159 | 60, 4 | remulcld 9076 |
. . . . . . . . . . . . . 14
 

  ![[,] [,]](_icc.gif)        |
160 | 159 | recnd 9074 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)        |
161 | 158, 160 | addcomd 9228 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)                      |
162 | 155, 161 | eqtrd 2440 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)                          |
163 | 162 | adantr 452 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                                 |
164 | 163 | fveq2d 5695 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                                         |
165 | 153 | oveq1d 6059 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)                      |
166 | 165 | oveq2d 6060 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)                                          |
167 | 156, 76 | remulcld 9076 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)              |
168 | 167 | recnd 9074 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)              |
169 | 75, 3 | ffvelrnd 5834 |
. . . . . . . . . . . . . 14
 

  ![[,] [,]](_icc.gif)          |
170 | 60, 169 | remulcld 9076 |
. . . . . . . . . . . . 13
 

  ![[,] [,]](_icc.gif)            |
171 | 170 | recnd 9074 |
. . . . . . . . . . . 12
 

  ![[,] [,]](_icc.gif)            |
172 | 168, 171 | addcomd 9228 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)                                      |
173 | 166, 172 | eqtrd 2440 |
. . . . . . . . . 10
 

  ![[,] [,]](_icc.gif)                                          |
174 | 173 | adantr 452 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)                                                 |
175 | 151, 164,
174 | 3brtr3d 4205 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                                         |
176 | 175 | orcd 382 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)                                                                       |
177 | 176 | expr 599 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)                                                                       |
178 | 57, 92, 177 | 3jaod 1248 |
. . . . 5
   
  ![[,] [,]](_icc.gif)          
                                                              |
179 | 9, 178 | mpd 15 |
. . . 4
   
  ![[,] [,]](_icc.gif)                                                                     |
180 | 179 | ex 424 |
. . 3
 

  ![[,] [,]](_icc.gif)                                                                      |
181 | | elpri 3798 |
. . . 4
    
   |
182 | 77 | addid2d 9227 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)                |
183 | 169 | recnd 9074 |
. . . . . . . . 9
 

  ![[,] [,]](_icc.gif)          |
184 | 183 | mul02d 9224 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)            |
185 | 184, 79 | oveq12d 6062 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)                          |
186 | 4 | recnd 9074 |
. . . . . . . . . . 11
 

  ![[,] [,]](_icc.gif)   
  |
187 | 186 | mul02d 9224 |
. . . . . . . . . 10
 

  ![[,] [,]](_icc.gif)        |
188 | 187, 70 | oveq12d 6062 |
. . . . . . . . 9
 

  ![[,] [,]](_icc.gif)              |
189 | 68 | addid2d 9227 |
. . . . . . . . 9
 

  ![[,] [,]](_icc.gif)        |
190 | 188, 189 | eqtrd 2440 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)            |
191 | 190 | fveq2d 5695 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)                    |
192 | 182, 185,
191 | 3eqtr4rd 2451 |
. . . . . 6
 

  ![[,] [,]](_icc.gif)                              |
193 | | oveq1 6051 |
. . . . . . . . 9
 
     |
194 | | oveq2 6052 |
. . . . . . . . . . 11
       |
195 | 62 | subid1i 9332 |
. . . . . . . . . . 11
   |
196 | 194, 195 | syl6eq 2456 |
. . . . . . . . . 10
     |
197 | 196 | oveq1d 6059 |
. . . . . . . . 9
         |
198 | 193, 197 | oveq12d 6062 |
. . . . . . . 8
                 |
199 | 198 | fveq2d 5695 |
. . . . . . 7
     
                   |
200 | | oveq1 6051 |
. . . . . . . 8
 
             |
201 | 196 | oveq1d 6059 |
. . . . . . . 8
                 |
202 | 200, 201 | oveq12d 6062 |
. . . . . . 7
                                 |
203 | 199, 202 | eqeq12d 2422 |
. . . . . 6
                             
                           |
204 | 192, 203 | syl5ibrcom 214 |
. . . . 5
 

  ![[,] [,]](_icc.gif)                                    |
205 | 183 | addid1d 9226 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)                |
206 | 183 | mulid2d 9066 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)                |
207 | 77 | mul02d 9224 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)            |
208 | 206, 207 | oveq12d 6062 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)                          |
209 | 186 | mulid2d 9066 |
. . . . . . . . . 10
 

  ![[,] [,]](_icc.gif)        |
210 | 68 | mul02d 9224 |
. . . . . . . . . 10
 

  ![[,] [,]](_icc.gif)        |
211 | 209, 210 | oveq12d 6062 |
. . . . . . . . 9
 

  ![[,] [,]](_icc.gif)              |
212 | 186 | addid1d 9226 |
. . . . . . . . 9
 

  ![[,] [,]](_icc.gif)        |
213 | 211, 212 | eqtrd 2440 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)            |
214 | 213 | fveq2d 5695 |
. . . . . . 7
 

  ![[,] [,]](_icc.gif)                    |
215 | 205, 208,
214 | 3eqtr4rd 2451 |
. . . . . 6
 

  ![[,] [,]](_icc.gif)                              |
216 | | oveq1 6051 |
. . . . . . . . 9
 
     |
217 | | oveq2 6052 |
. . . . . . . . . . 11
       |
218 | | 1m1e0 10028 |
. . . . . . . . . . 11
   |
219 | 217, 218 | syl6eq 2456 |
. . . . . . . . . 10
     |
220 | 219 | oveq1d 6059 |
. . . . . . . . 9
         |
221 | 216, 220 | oveq12d 6062 |
. . . . . . . 8
                 |
222 | 221 | fveq2d 5695 |
. . . . . . 7
     
                   |
223 | | oveq1 6051 |
. . . . . . . 8
 
             |
224 | 219 | oveq1d 6059 |
. . . . . . . 8
                 |
225 | 223, 224 | oveq12d 6062 |
. . . . . . 7
                                 |
226 | 222, 225 | eqeq12d 2422 |
. . . . . 6
                             
                           |
227 | 215, 226 | syl5ibrcom 214 |
. . . . 5
 

  ![[,] [,]](_icc.gif)                                    |
228 | 204, 227 | jaod 370 |
. . . 4
 

  ![[,] [,]](_icc.gif)           
                          |
229 | 181, 228,
91 | syl56 32 |
. . 3
 

  ![[,] [,]](_icc.gif)                                                                     |
230 | | 0le1 9511 |
. . . . . 6
 |
231 | | prunioo 10985 |
. . . . . 6
              ![[,] [,]](_icc.gif)    |
232 | 106, 107,
230, 231 | mp3an 1279 |
. . . . 5
           ![[,] [,]](_icc.gif)   |
233 | 59, 232 | syl6eleqr 2499 |
. . . 4
 

  ![[,] [,]](_icc.gif)   
           |
234 | | elun 3452 |
. . . 4
         
           |
235 | 233, 234 | sylib 189 |
. . 3
 

  ![[,] [,]](_icc.gif)               |
236 | 180, 229,
235 | mpjaod 371 |
. 2
 

  ![[,] [,]](_icc.gif)                                                                |
237 | | scvxcvx.3 |
. . . . 5
 

    ![[,] [,]](_icc.gif) 
  |
238 | 1, 237 | cvxcl 20780 |
. . . 4
 

  ![[,] [,]](_icc.gif)              |
239 | 75, 238 | ffvelrnd 5834 |
. . 3
 

  ![[,] [,]](_icc.gif)                  |
240 | 170, 167 | readdcld 9075 |
. . 3
 

  ![[,] [,]](_icc.gif)                      |
241 | 239, 240 | leloed 9176 |
. 2
 

  ![[,] [,]](_icc.gif)                                                                                              |
242 | 236, 241 | mpbird 224 |
1
 

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