Step | Hyp | Ref
| Expression |
1 | | dvcvx.a |
. . 3
   |
2 | | dvcvx.c |
. . . 4
         |
3 | | dvcvx.t |
. . . . . . 7
       |
4 | | elioore 11691 |
. . . . . . 7
       |
5 | 3, 4 | syl 17 |
. . . . . 6
   |
6 | 5, 1 | remulcld 9689 |
. . . . 5
     |
7 | | 1re 9660 |
. . . . . . 7
 |
8 | | resubcl 9958 |
. . . . . . 7
 
     |
9 | 7, 5, 8 | sylancr 676 |
. . . . . 6
     |
10 | | dvcvx.b |
. . . . . 6
   |
11 | 9, 10 | remulcld 9689 |
. . . . 5
       |
12 | 6, 11 | readdcld 9688 |
. . . 4
           |
13 | 2, 12 | syl5eqel 2553 |
. . 3
   |
14 | | 1cnd 9677 |
. . . . . . . 8
   |
15 | 5 | recnd 9687 |
. . . . . . . 8
   |
16 | 1 | recnd 9687 |
. . . . . . . 8
   |
17 | 14, 15, 16 | subdird 10096 |
. . . . . . 7
             |
18 | 16 | mulid2d 9679 |
. . . . . . . 8
     |
19 | 18 | oveq1d 6323 |
. . . . . . 7
    
        |
20 | 17, 19 | eqtrd 2505 |
. . . . . 6
           |
21 | | dvcvx.l |
. . . . . . 7
   |
22 | | eliooord 11719 |
. . . . . . . . . . 11
     
   |
23 | 3, 22 | syl 17 |
. . . . . . . . . 10
 
   |
24 | 23 | simprd 470 |
. . . . . . . . 9
   |
25 | | posdif 10128 |
. . . . . . . . . 10
 
       |
26 | 5, 7, 25 | sylancl 675 |
. . . . . . . . 9
       |
27 | 24, 26 | mpbid 215 |
. . . . . . . 8
     |
28 | | ltmul2 10478 |
. . . . . . . 8
 
                   |
29 | 1, 10, 9, 27, 28 | syl112anc 1296 |
. . . . . . 7
             |
30 | 21, 29 | mpbid 215 |
. . . . . 6
    
      |
31 | 20, 30 | eqbrtrrd 4418 |
. . . . 5
  
 
      |
32 | 1, 6, 11 | ltsubadd2d 10232 |
. . . . 5
   
     
 
         |
33 | 31, 32 | mpbid 215 |
. . . 4
           |
34 | 33, 2 | syl6breqr 4436 |
. . 3
   |
35 | 1 | leidd 10201 |
. . . . 5

  |
36 | 10 | recnd 9687 |
. . . . . . . . . . 11
   |
37 | 14, 15, 36 | subdird 10096 |
. . . . . . . . . 10
             |
38 | 36 | mulid2d 9679 |
. . . . . . . . . . 11
     |
39 | 38 | oveq1d 6323 |
. . . . . . . . . 10
    
        |
40 | 37, 39 | eqtrd 2505 |
. . . . . . . . 9
           |
41 | 5, 10 | remulcld 9689 |
. . . . . . . . . 10
     |
42 | 23 | simpld 466 |
. . . . . . . . . . . 12
   |
43 | | ltmul2 10478 |
. . . . . . . . . . . 12
 

          |
44 | 1, 10, 5, 42, 43 | syl112anc 1296 |
. . . . . . . . . . 11
         |
45 | 21, 44 | mpbid 215 |
. . . . . . . . . 10
  
    |
46 | 6, 41, 10, 45 | ltsub2dd 10247 |
. . . . . . . . 9
  
 
      |
47 | 40, 46 | eqbrtrd 4416 |
. . . . . . . 8
    
      |
48 | 6, 11, 10 | ltaddsub2d 10235 |
. . . . . . . 8
               
     |
49 | 47, 48 | mpbird 240 |
. . . . . . 7
           |
50 | 2, 49 | syl5eqbr 4429 |
. . . . . 6
   |
51 | 13, 10, 50 | ltled 9800 |
. . . . 5

  |
52 | | iccss 11727 |
. . . . 5
         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
53 | 1, 10, 35, 51, 52 | syl22anc 1293 |
. . . 4
   ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    |
54 | | dvcvx.f |
. . . 4
    ![[,] [,]](_icc.gif)       |
55 | | rescncf 22007 |
. . . 4
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
56 | 53, 54, 55 | sylc 61 |
. . 3
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
57 | | ax-resscn 9614 |
. . . . . . . 8
 |
58 | 57 | a1i 11 |
. . . . . . 7

  |
59 | | cncff 22003 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)      |
60 | 54, 59 | syl 17 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)      |
61 | | fss 5749 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)      |
62 | 60, 57, 61 | sylancl 675 |
. . . . . . 7
     ![[,] [,]](_icc.gif)      |
63 | | iccssre 11741 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
  |
64 | 1, 10, 63 | syl2anc 673 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
  |
65 | | iccssre 11741 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
  |
66 | 1, 13, 65 | syl2anc 673 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
  |
67 | | eqid 2471 |
. . . . . . . 8
  ℂfld   ℂfld |
68 | 67 | tgioo2 21899 |
. . . . . . . 8
       ℂfld
↾t   |
69 | 67, 68 | dvres 22945 |
. . . . . . 7
       ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)      |
70 | 58, 62, 64, 66, 69 | syl22anc 1293 |
. . . . . 6
     ![[,] [,]](_icc.gif)             
      ![[,] [,]](_icc.gif)      |
71 | | iccntr 21917 |
. . . . . . . 8
 
       
      ![[,] [,]](_icc.gif)         |
72 | 1, 13, 71 | syl2anc 673 |
. . . . . . 7
       
      ![[,] [,]](_icc.gif)         |
73 | 72 | reseq2d 5111 |
. . . . . 6
          
      ![[,] [,]](_icc.gif)              |
74 | 70, 73 | eqtrd 2505 |
. . . . 5
     ![[,] [,]](_icc.gif)              |
75 | 74 | dmeqd 5042 |
. . . 4
  
  ![[,] [,]](_icc.gif)              |
76 | | dmres 5131 |
. . . . 5
             
   |
77 | 10 | rexrd 9708 |
. . . . . . . 8
   |
78 | | iooss2 11697 |
. . . . . . . 8
             |
79 | 77, 51, 78 | syl2anc 673 |
. . . . . . 7
    
      |
80 | | dvcvx.d |
. . . . . . . 8
  
         |
81 | | isof1o 6234 |
. . . . . . . 8
                      |
82 | | f1odm 5832 |
. . . . . . . 8
          
        |
83 | 80, 81, 82 | 3syl 18 |
. . . . . . 7
         |
84 | 79, 83 | sseqtr4d 3455 |
. . . . . 6
    
    |
85 | | df-ss 3404 |
. . . . . 6
    
 
              |
86 | 84, 85 | sylib 201 |
. . . . 5
      
        |
87 | 76, 86 | syl5eq 2517 |
. . . 4
               |
88 | 75, 87 | eqtrd 2505 |
. . 3
  
  ![[,] [,]](_icc.gif)          |
89 | 1, 13, 34, 56, 88 | mvth 23023 |
. 2
         
  ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            |
90 | 1, 13, 34 | ltled 9800 |
. . . . 5

  |
91 | 10 | leidd 10201 |
. . . . 5

  |
92 | | iccss 11727 |
. . . . 5
         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
93 | 1, 10, 90, 91, 92 | syl22anc 1293 |
. . . 4
   ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    |
94 | | rescncf 22007 |
. . . 4
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)    
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
95 | 93, 54, 94 | sylc 61 |
. . 3
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
96 | | iccssre 11741 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
  |
97 | 13, 10, 96 | syl2anc 673 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
  |
98 | 67, 68 | dvres 22945 |
. . . . . . 7
       ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)      |
99 | 58, 62, 64, 97, 98 | syl22anc 1293 |
. . . . . 6
     ![[,] [,]](_icc.gif)             
      ![[,] [,]](_icc.gif)      |
100 | | iccntr 21917 |
. . . . . . . 8
 
       
      ![[,] [,]](_icc.gif)         |
101 | 13, 10, 100 | syl2anc 673 |
. . . . . . 7
       
      ![[,] [,]](_icc.gif)         |
102 | 101 | reseq2d 5111 |
. . . . . 6
          
      ![[,] [,]](_icc.gif)              |
103 | 99, 102 | eqtrd 2505 |
. . . . 5
     ![[,] [,]](_icc.gif)              |
104 | 103 | dmeqd 5042 |
. . . 4
  
  ![[,] [,]](_icc.gif)              |
105 | | dmres 5131 |
. . . . 5
             
   |
106 | 1 | rexrd 9708 |
. . . . . . . 8
   |
107 | | iooss1 11696 |
. . . . . . . 8
             |
108 | 106, 90, 107 | syl2anc 673 |
. . . . . . 7
    
      |
109 | 108, 83 | sseqtr4d 3455 |
. . . . . 6
    
    |
110 | | df-ss 3404 |
. . . . . 6
    
 
              |
111 | 109, 110 | sylib 201 |
. . . . 5
      
        |
112 | 105, 111 | syl5eq 2517 |
. . . 4
               |
113 | 104, 112 | eqtrd 2505 |
. . 3
  
  ![[,] [,]](_icc.gif)          |
114 | 13, 10, 50, 95, 113 | mvth 23023 |
. 2
         
  ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            |
115 | | reeanv 2944 |
. . 3
                
  ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
  
 
          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)          
          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)             |
116 | 74 | fveq1d 5881 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                     |
117 | | fvres 5893 |
. . . . . . . . 9
                         |
118 | 117 | adantr 472 |
. . . . . . . 8
     
                         |
119 | 116, 118 | sylan9eq 2525 |
. . . . . . 7
 
    
           ![[,] [,]](_icc.gif)               |
120 | 13 | rexrd 9708 |
. . . . . . . . . . . 12
   |
121 | | ubicc2 11775 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    |
122 | 106, 120,
90, 121 | syl3anc 1292 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
123 | | fvres 5893 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
124 | 122, 123 | syl 17 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)            |
125 | | lbicc2 11774 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    |
126 | 106, 120,
90, 125 | syl3anc 1292 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
127 | | fvres 5893 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
128 | 126, 127 | syl 17 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)            |
129 | 124, 128 | oveq12d 6326 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                   |
130 | 129 | oveq1d 6323 |
. . . . . . . 8
    
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                          |
131 | 130 | adantr 472 |
. . . . . . 7
 
    
            ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                          |
132 | 119, 131 | eqeq12d 2486 |
. . . . . 6
 
    
         
  ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                                 |
133 | 103 | fveq1d 5881 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)                     |
134 | | fvres 5893 |
. . . . . . . . 9
                         |
135 | 134 | adantl 473 |
. . . . . . . 8
     
                         |
136 | 133, 135 | sylan9eq 2525 |
. . . . . . 7
 
    
           ![[,] [,]](_icc.gif)               |
137 | | ubicc2 11775 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    |
138 | 120, 77, 51, 137 | syl3anc 1292 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
139 | | fvres 5893 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
140 | 138, 139 | syl 17 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)            |
141 | | lbicc2 11774 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    |
142 | 120, 77, 51, 141 | syl3anc 1292 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
143 | | fvres 5893 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
144 | 142, 143 | syl 17 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)            |
145 | 140, 144 | oveq12d 6326 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                   |
146 | 145 | oveq1d 6323 |
. . . . . . . 8
    
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                          |
147 | 146 | adantr 472 |
. . . . . . 7
 
    
            ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)                          |
148 | 136, 147 | eqeq12d 2486 |
. . . . . 6
 
    
         
  ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                                 |
149 | 132, 148 | anbi12d 725 |
. . . . 5
 
    
             ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
 
     ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
  
                                             |
150 | | elioore 11691 |
. . . . . . . . . 10
       |
151 | 150 | ad2antrl 742 |
. . . . . . . . 9
 
    
        |
152 | 13 | adantr 472 |
. . . . . . . . 9
 
    
        |
153 | | elioore 11691 |
. . . . . . . . . 10
       |
154 | 153 | ad2antll 743 |
. . . . . . . . 9
 
    
        |
155 | | eliooord 11719 |
. . . . . . . . . . 11
         |
156 | 155 | ad2antrl 742 |
. . . . . . . . . 10
 
    
          |
157 | 156 | simprd 470 |
. . . . . . . . 9
 
    
        |
158 | | eliooord 11719 |
. . . . . . . . . . 11
         |
159 | 158 | ad2antll 743 |
. . . . . . . . . 10
 
    
          |
160 | 159 | simpld 466 |
. . . . . . . . 9
 
    
        |
161 | 151, 152,
154, 157, 160 | lttrd 9813 |
. . . . . . . 8
 
    
        |
162 | 80 | adantr 472 |
. . . . . . . . 9
 
    
                 |
163 | 79 | sselda 3418 |
. . . . . . . . . 10
 
    
      |
164 | 163 | adantrr 731 |
. . . . . . . . 9
 
    
            |
165 | 108 | sselda 3418 |
. . . . . . . . . 10
 
    
      |
166 | 165 | adantrl 730 |
. . . . . . . . 9
 
    
            |
167 | | isorel 6235 |
. . . . . . . . 9
   
           
      
               |
168 | 162, 164,
166, 167 | syl12anc 1290 |
. . . . . . . 8
 
    
      
               |
169 | 161, 168 | mpbid 215 |
. . . . . . 7
 
    
                    |
170 | | breq12 4400 |
. . . . . . 7
                                                                                       |
171 | 169, 170 | syl5ibcom 228 |
. . . . . 6
 
    
                                                
                               |
172 | 53, 122 | sseldd 3419 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
173 | 60, 172 | ffvelrnd 6038 |
. . . . . . . . . . 11
       |
174 | 53, 126 | sseldd 3419 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
175 | 60, 174 | ffvelrnd 6038 |
. . . . . . . . . . 11
       |
176 | 173, 175 | resubcld 10068 |
. . . . . . . . . 10
             |
177 | 27 | gt0ne0d 10199 |
. . . . . . . . . 10
     |
178 | 176, 9, 177 | redivcld 10457 |
. . . . . . . . 9
                 |
179 | 93, 138 | sseldd 3419 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
180 | 60, 179 | ffvelrnd 6038 |
. . . . . . . . . . 11
       |
181 | 180, 173 | resubcld 10068 |
. . . . . . . . . 10
             |
182 | 42 | gt0ne0d 10199 |
. . . . . . . . . 10
   |
183 | 181, 5, 182 | redivcld 10457 |
. . . . . . . . 9
               |
184 | 10, 1 | resubcld 10068 |
. . . . . . . . 9
     |
185 | 1, 10 | posdifd 10221 |
. . . . . . . . . 10
       |
186 | 21, 185 | mpbid 215 |
. . . . . . . . 9
     |
187 | | ltdiv1 10491 |
. . . . . . . . 9
                                                                             
 
                   |
188 | 178, 183,
184, 186, 187 | syl112anc 1296 |
. . . . . . . 8
                                           
 
                   |
189 | 176 | recnd 9687 |
. . . . . . . . . . . 12
             |
190 | 189, 15 | mulcomd 9682 |
. . . . . . . . . . 11
                           |
191 | 173 | recnd 9687 |
. . . . . . . . . . . 12
       |
192 | 175 | recnd 9687 |
. . . . . . . . . . . 12
       |
193 | 15, 191, 192 | subdid 10095 |
. . . . . . . . . . 11
                             |
194 | 190, 193 | eqtrd 2505 |
. . . . . . . . . 10
                    
        |
195 | 181 | recnd 9687 |
. . . . . . . . . . . 12
             |
196 | 9 | recnd 9687 |
. . . . . . . . . . . 12
     |
197 | 195, 196 | mulcomd 9682 |
. . . . . . . . . . 11
                               |
198 | 180 | recnd 9687 |
. . . . . . . . . . . 12
       |
199 | 196, 198,
191 | subdid 10095 |
. . . . . . . . . . 11
                                   |
200 | 197, 199 | eqtrd 2505 |
. . . . . . . . . 10
                                   |
201 | 194, 200 | breq12d 4408 |
. . . . . . . . 9
                                                               |
202 | 5, 42 | jca 541 |
. . . . . . . . . 10
     |
203 | 9, 27 | jca 541 |
. . . . . . . . . 10
         |
204 | | lt2mul2div 10505 |
. . . . . . . . . 10
             
                    
                          
                             |
205 | 176, 202,
181, 203, 204 | syl22anc 1293 |
. . . . . . . . 9
                                                         |
206 | 5, 173 | remulcld 9689 |
. . . . . . . . . . . . . 14
         |
207 | 206 | recnd 9687 |
. . . . . . . . . . . . 13
         |
208 | 9, 173 | remulcld 9689 |
. . . . . . . . . . . . . 14
           |
209 | 208 | recnd 9687 |
. . . . . . . . . . . . 13
           |
210 | 5, 175 | remulcld 9689 |
. . . . . . . . . . . . . 14
         |
211 | 210 | recnd 9687 |
. . . . . . . . . . . . 13
         |
212 | 207, 209,
211 | addsubd 10026 |
. . . . . . . . . . . 12
                  
                                |
213 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . 16
 |
214 | | pncan3 9903 |
. . . . . . . . . . . . . . . 16
 
       |
215 | 15, 213, 214 | sylancl 675 |
. . . . . . . . . . . . . . 15
       |
216 | 215 | oveq1d 6323 |
. . . . . . . . . . . . . 14
                   |
217 | 15, 196, 191 | adddird 9686 |
. . . . . . . . . . . . . 14
                             |
218 | 191 | mulid2d 9679 |
. . . . . . . . . . . . . 14
             |
219 | 216, 217,
218 | 3eqtr3d 2513 |
. . . . . . . . . . . . 13
                       |
220 | 219 | oveq1d 6323 |
. . . . . . . . . . . 12
                  
           
        |
221 | 212, 220 | eqtr3d 2507 |
. . . . . . . . . . 11
         
                             |
222 | 221 | breq1d 4405 |
. . . . . . . . . 10
                                 
                       |
223 | 206, 210 | resubcld 10068 |
. . . . . . . . . . 11
                 |
224 | 9, 180 | remulcld 9689 |
. . . . . . . . . . 11
           |
225 | 223, 208,
224 | ltaddsubd 10234 |
. . . . . . . . . 10
                                 
 
     
                           |
226 | 173, 210,
224 | ltsubadd2d 10232 |
. . . . . . . . . 10
       
                 
 
                 |
227 | 222, 225,
226 | 3bitr3d 291 |
. . . . . . . . 9
         
                           
 
                 |
228 | 201, 205,
227 | 3bitr3d 291 |
. . . . . . . 8
                               
 
                 |
229 | 184 | recnd 9687 |
. . . . . . . . . . 11
     |
230 | 186 | gt0ne0d 10199 |
. . . . . . . . . . 11
     |
231 | 189, 196,
229, 177, 230 | divdiv1d 10436 |
. . . . . . . . . 10
                
                      |
232 | 20 | oveq2d 6324 |
. . . . . . . . . . . . 13
                 
     |
233 | 11 | recnd 9687 |
. . . . . . . . . . . . . 14
       |
234 | 6 | recnd 9687 |
. . . . . . . . . . . . . 14
     |
235 | 233, 16, 234 | subsub3d 10035 |
. . . . . . . . . . . . 13
      
                |
236 | 232, 235 | eqtrd 2505 |
. . . . . . . . . . . 12
                       |
237 | 196, 36, 16 | subdid 10095 |
. . . . . . . . . . . 12
    
              |
238 | 234, 233 | addcomd 9853 |
. . . . . . . . . . . . . 14
                   |
239 | 2, 238 | syl5eq 2517 |
. . . . . . . . . . . . 13
           |
240 | 239 | oveq1d 6323 |
. . . . . . . . . . . 12
               |
241 | 236, 237,
240 | 3eqtr4d 2515 |
. . . . . . . . . . 11
    
      |
242 | 241 | oveq2d 6324 |
. . . . . . . . . 10
                                   |
243 | 231, 242 | eqtrd 2505 |
. . . . . . . . 9
                
                  |
244 | 195, 15, 229, 182, 230 | divdiv1d 10436 |
. . . . . . . . . 10
              
              
     |
245 | 36, 233, 234 | subsub4d 10036 |
. . . . . . . . . . . . 13
        
              |
246 | 40 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
         
     |
247 | 41 | recnd 9687 |
. . . . . . . . . . . . . . . 16
     |
248 | 36, 247 | nncand 10010 |
. . . . . . . . . . . . . . 15
  
        |
249 | 246, 248 | eqtrd 2505 |
. . . . . . . . . . . . . 14
           |
250 | 249 | oveq1d 6323 |
. . . . . . . . . . . . 13
        
          |
251 | 245, 250 | eqtr3d 2507 |
. . . . . . . . . . . 12
                   |
252 | 239 | oveq2d 6324 |
. . . . . . . . . . . 12
               |
253 | 15, 36, 16 | subdid 10095 |
. . . . . . . . . . . 12
  
          |
254 | 251, 252,
253 | 3eqtr4d 2515 |
. . . . . . . . . . 11
         |
255 | 254 | oveq2d 6324 |
. . . . . . . . . 10
                           
     |
256 | 244, 255 | eqtr4d 2508 |
. . . . . . . . 9
              
                  |
257 | 243, 256 | breq12d 4408 |
. . . . . . . 8
                                   
                               |
258 | 188, 228,
257 | 3bitr3rd 292 |
. . . . . . 7
                                 
 
                 |
259 | 258 | adantr 472 |
. . . . . 6
 
    
                                  
                       |
260 | 171, 259 | sylibd 222 |
. . . . 5
 
    
                                                
                       |
261 | 149, 260 | sylbid 223 |
. . . 4
 
    
             ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
 
     ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
                          |
262 | 261 | rexlimdvva 2878 |
. . 3
                    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                                  |
263 | 115, 262 | syl5bir 226 |
. 2
              ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
 
           ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
                          |
264 | 89, 114, 263 | mp2and 693 |
1
    
 
                |