Step | Hyp | Ref
| Expression |
1 | | brbtwn2 25014 |
. . 3
     
                                                                                                      |
2 | | brbtwn2 25014 |
. . . . 5
     
                                                                                                      |
3 | 2 | 3comr 1239 |
. . . 4
     
                                                                                                      |
4 | | colinearalglem3 25017 |
. . . . . 6
     
          
     
                                                
                                                           |
5 | 4 | 3comr 1239 |
. . . . 5
     
          
     
                                                
                                                           |
6 | 5 | anbi2d 718 |
. . . 4
     
                                                                                               
 
                           
     
                                                     |
7 | 3, 6 | bitrd 261 |
. . 3
     
                                                                                                      |
8 | | brbtwn2 25014 |
. . . . 5
     
                                                                                                      |
9 | | colinearalglem2 25016 |
. . . . . 6
     
          
     
                                                
                                                           |
10 | 9 | anbi2d 718 |
. . . . 5
     
                                                                                               
 
                           
     
                                                     |
11 | 8, 10 | bitrd 261 |
. . . 4
     
                                                                                                      |
12 | 11 | 3coml 1238 |
. . 3
     
                                                                                                      |
13 | 1, 7, 12 | 3orbi123d 1364 |
. 2
     
               

   
  
                           
     
                                                                                                                                                                                                                                  |
14 | | fveecn 25011 |
. . . . . . . . . . . . 13
     
           |
15 | | fveecn 25011 |
. . . . . . . . . . . . 13
     
           |
16 | | subid 9913 |
. . . . . . . . . . . . . . . 16
                 |
17 | 16 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                                         |
18 | 17 | adantl 473 |
. . . . . . . . . . . . . 14
                                               |
19 | | subcl 9894 |
. . . . . . . . . . . . . . 15
                       |
20 | 19 | mul01d 9850 |
. . . . . . . . . . . . . 14
                         |
21 | 18, 20 | eqtrd 2505 |
. . . . . . . . . . . . 13
                                   |
22 | 14, 15, 21 | syl2an 485 |
. . . . . . . . . . . 12
                                               |
23 | 22 | anandirs 847 |
. . . . . . . . . . 11
                                         |
24 | | 0le0 10721 |
. . . . . . . . . . 11
 |
25 | 23, 24 | syl6eqbr 4433 |
. . . . . . . . . 10
                                         |
26 | 25 | ralrimiva 2809 |
. . . . . . . . 9
     
     
                             |
27 | 26 | 3adant1 1048 |
. . . . . . . 8
     
                                       |
28 | | fveq1 5878 |
. . . . . . . . . . . 12
           |
29 | 28 | oveq2d 6324 |
. . . . . . . . . . 11
                       |
30 | 28 | oveq2d 6324 |
. . . . . . . . . . 11
                       |
31 | 29, 30 | oveq12d 6326 |
. . . . . . . . . 10
                                               |
32 | 31 | breq1d 4405 |
. . . . . . . . 9
                       
                         |
33 | 32 | ralbidv 2829 |
. . . . . . . 8
  
                          
                               |
34 | 27, 33 | syl5ibcom 228 |
. . . . . . 7
     
         
                               |
35 | | 3mix1 1199 |
. . . . . . 7
 
                            
                           
                           
                              |
36 | 34, 35 | syl6 33 |
. . . . . 6
     
         
                             
                           
                               |
37 | 36 | a1dd 46 |
. . . . 5
     
         
                                                          
                           
                           
                                |
38 | | simp3 1032 |
. . . . . . . . 9
     
               |
39 | | simp1 1030 |
. . . . . . . . 9
     
               |
40 | | eqeefv 25012 |
. . . . . . . . 9
     
      
                |
41 | 38, 39, 40 | syl2anc 673 |
. . . . . . . 8
     
         
                 |
42 | 41 | necon3abid 2679 |
. . . . . . 7
     
         
                 |
43 | | df-ne 2643 |
. . . . . . . . 9
        
          |
44 | 43 | rexbii 2881 |
. . . . . . . 8
              
               |
45 | | rexnal 2836 |
. . . . . . . 8
             
                |
46 | 44, 45 | bitr2i 258 |
. . . . . . 7
              
                |
47 | 42, 46 | syl6bb 269 |
. . . . . 6
     
         
                 |
48 | | ralcom 2937 |
. . . . . . . 8
 
     
                                                
                                                          |
49 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
50 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
51 | 49, 50 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                       |
52 | 51 | oveq2d 6324 |
. . . . . . . . . . . . 13
                                               |
53 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
54 | 53, 50 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                       |
55 | 54 | oveq1d 6323 |
. . . . . . . . . . . . 13
                                               |
56 | 52, 55 | eqeq12d 2486 |
. . . . . . . . . . . 12
                                             
                                               |
57 | 56 | ralbidv 2829 |
. . . . . . . . . . 11
  
                                                
                                                     |
58 | 57 | rspcv 3132 |
. . . . . . . . . 10
      
     
                                                                                                      |
59 | 58 | ad2antrl 742 |
. . . . . . . . 9
                                                                                                                                             |
60 | | fveere 25010 |
. . . . . . . . . . . . . 14
     
           |
61 | 60 | 3ad2antl1 1192 |
. . . . . . . . . . . . 13
                           |
62 | | fveere 25010 |
. . . . . . . . . . . . . 14
     
           |
63 | 62 | 3ad2antl2 1193 |
. . . . . . . . . . . . 13
                           |
64 | | fveere 25010 |
. . . . . . . . . . . . . 14
     
           |
65 | 64 | 3ad2antl3 1194 |
. . . . . . . . . . . . 13
                           |
66 | 61, 63, 65 | 3jca 1210 |
. . . . . . . . . . . 12
                                     |
67 | 66 | anim1i 578 |
. . . . . . . . . . 11
       
                                                 |
68 | 67 | anasss 659 |
. . . . . . . . . 10
                                                         |
69 | | fveecn 25011 |
. . . . . . . . . . . . . . . 16
     
           |
70 | 69 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . 15
                           |
71 | 14 | 3ad2antl2 1193 |
. . . . . . . . . . . . . . 15
                           |
72 | 15 | 3ad2antl3 1194 |
. . . . . . . . . . . . . . 15
                           |
73 | 70, 71, 72 | 3jca 1210 |
. . . . . . . . . . . . . 14
                                     |
74 | 73 | adantlr 729 |
. . . . . . . . . . . . 13
       
                                 
                     |
75 | | recn 9647 |
. . . . . . . . . . . . . . . 16
           |
76 | | recn 9647 |
. . . . . . . . . . . . . . . 16
           |
77 | | recn 9647 |
. . . . . . . . . . . . . . . 16
           |
78 | 75, 76, 77 | 3anim123i 1215 |
. . . . . . . . . . . . . . 15
                               |
79 | 78 | adantr 472 |
. . . . . . . . . . . . . 14
                                         |
80 | 79 | ad2antlr 741 |
. . . . . . . . . . . . 13
       
                                 
                     |
81 | | simplrr 779 |
. . . . . . . . . . . . 13
       
                                 
               |
82 | | eqcom 2478 |
. . . . . . . . . . . . . 14
                                                                                           |
83 | | simp12 1061 |
. . . . . . . . . . . . . . . 16
                                             |
84 | | simp11 1060 |
. . . . . . . . . . . . . . . 16
                                             |
85 | | simp22 1064 |
. . . . . . . . . . . . . . . . . . 19
                                             |
86 | | simp21 1063 |
. . . . . . . . . . . . . . . . . . 19
                                             |
87 | 85, 86 | subcld 10005 |
. . . . . . . . . . . . . . . . . 18
                                                   |
88 | | simp23 1065 |
. . . . . . . . . . . . . . . . . . 19
                                             |
89 | 88, 86 | subcld 10005 |
. . . . . . . . . . . . . . . . . 18
                                                   |
90 | | simpr3 1038 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
91 | | simpr1 1036 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
92 | 90, 91 | subeq0ad 10015 |
. . . . . . . . . . . . . . . . . . . 20
                                                     |
93 | 92 | necon3bid 2687 |
. . . . . . . . . . . . . . . . . . 19
                                                     |
94 | 93 | biimp3ar 1398 |
. . . . . . . . . . . . . . . . . 18
                                                   |
95 | 87, 89, 94 | divcld 10405 |
. . . . . . . . . . . . . . . . 17
                                                               |
96 | | simp13 1062 |
. . . . . . . . . . . . . . . . . 18
                                             |
97 | 96, 84 | subcld 10005 |
. . . . . . . . . . . . . . . . 17
                                                   |
98 | 95, 97 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
                                                                           |
99 | | subadd2 9899 |
. . . . . . . . . . . . . . . . 17
                                                                                                                                         |
100 | 99 | bicomd 206 |
. . . . . . . . . . . . . . . 16
                                                                                         
                                               |
101 | 83, 84, 98, 100 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
                                                                                   
                                               |
102 | 87, 97, 89, 94 | div23d 10442 |
. . . . . . . . . . . . . . . 16
                                                                                                             |
103 | 102 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
                                                                                   
                                               |
104 | | eqcom 2478 |
. . . . . . . . . . . . . . . 16
                                                                                           |
105 | 87, 97 | mulcld 9681 |
. . . . . . . . . . . . . . . . . 18
                                                               |
106 | 83, 84 | subcld 10005 |
. . . . . . . . . . . . . . . . . 18
                                                   |
107 | 105, 89, 106, 94 | divmuld 10427 |
. . . . . . . . . . . . . . . . 17
                                                                                   
                                               |
108 | 89, 106 | mulcomd 9682 |
. . . . . . . . . . . . . . . . . 18
                                                                                     |
109 | 108 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . 17
                                                                                                                                   |
110 | 107, 109 | bitrd 261 |
. . . . . . . . . . . . . . . 16
                                                                                   
                                               |
111 | 104, 110 | syl5bb 265 |
. . . . . . . . . . . . . . 15
                                                                                   
                                               |
112 | 101, 103,
111 | 3bitr2d 289 |
. . . . . . . . . . . . . 14
                                                                                   
                                               |
113 | 82, 112 | syl5bb 265 |
. . . . . . . . . . . . 13
                                                                                                                                   |
114 | 74, 80, 81, 113 | syl3anc 1292 |
. . . . . . . . . . . 12
       
                                 
                                                                                                 |
115 | 114 | ralbidva 2828 |
. . . . . . . . . . 11
                                                                                            
                                                    |
116 | | 3simpb 1028 |
. . . . . . . . . . . 12
     
         
           |
117 | | simpl2 1034 |
. . . . . . . . . . . . . 14
                               |
118 | | simpl1 1033 |
. . . . . . . . . . . . . 14
                               |
119 | 117, 118 | resubcld 10068 |
. . . . . . . . . . . . 13
                                     |
120 | | simpl3 1035 |
. . . . . . . . . . . . . 14
                               |
121 | 120, 118 | resubcld 10068 |
. . . . . . . . . . . . 13
                                     |
122 | | simp3 1032 |
. . . . . . . . . . . . . . . . 17
                     |
123 | 122 | recnd 9687 |
. . . . . . . . . . . . . . . 16
                     |
124 | 75 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . 16
                     |
125 | 123, 124 | subeq0ad 10015 |
. . . . . . . . . . . . . . 15
                                     |
126 | 125 | necon3bid 2687 |
. . . . . . . . . . . . . 14
                                     |
127 | 126 | biimpar 493 |
. . . . . . . . . . . . 13
                                     |
128 | 119, 121,
127 | redivcld 10457 |
. . . . . . . . . . . 12
                                                 |
129 | | colinearalglem4 25018 |
. . . . . . . . . . . . 13
                                                                                                                                                                                                                                                                       
   |
130 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
                                            
                                                          |
131 | 130 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                                            
                                                                                  |
132 | 131 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
                                            
                      
                                                             |
133 | 132 | ralimi 2796 |
. . . . . . . . . . . . . . 15
 
                                                
                                                                                          |
134 | | ralbi 2908 |
. . . . . . . . . . . . . . 15
 
                           
                                                          
 
                          
                                                                   |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
 
                                                
 
                          
                                                                   |
136 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                                            
                                                          |
137 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                                            
                                                          |
138 | 136, 137 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
                                            
                                                                                                                      |
139 | 138 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
                                            
                      
                                                                                                 |
140 | 139 | ralimi 2796 |
. . . . . . . . . . . . . . 15
 
                                                
                                                                                                                              |
141 | | ralbi 2908 |
. . . . . . . . . . . . . . 15
 
                           
                                                                                                
                          
                                                                                                       |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . 14
 
                                                
 
                          
                                                                                                       |
143 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
                                            
                                                          |
144 | 143 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                                            
                                                                                  |
145 | 144 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
                                            
                      
                                                         
   |
146 | 145 | ralimi 2796 |
. . . . . . . . . . . . . . 15
 
                                                
                                                                                          |
147 | | ralbi 2908 |
. . . . . . . . . . . . . . 15
 
                           
                                                         
                                                                                                 |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
 
                                                
 
                          
                                                               
   |
149 | 135, 142,
148 | 3orbi123d 1364 |
. . . . . . . . . . . . 13
 
                                                
  
                           
                           
                           
 
                                                                                                                                                                                                                                  
    |
150 | 129, 149 | syl5ibrcom 230 |
. . . . . . . . . . . 12
                                                                                                                                               
                               |
151 | 116, 128,
150 | syl2an 485 |
. . . . . . . . . . 11
                                                                                                                                                     
                               |
152 | 115, 151 | sylbird 243 |
. . . . . . . . . 10
                                                                      ![]() |