Step | Hyp | Ref
| Expression |
1 | | brbtwn2 25785 |
. . 3
|
2 | | brbtwn2 25785 |
. . . . 5
|
3 | 2 | 3comr 1273 |
. . . 4
|
4 | | colinearalglem3 25788 |
. . . . . 6
|
5 | 4 | 3comr 1273 |
. . . . 5
|
6 | 5 | anbi2d 740 |
. . . 4
|
7 | 3, 6 | bitrd 268 |
. . 3
|
8 | | brbtwn2 25785 |
. . . . 5
|
9 | | colinearalglem2 25787 |
. . . . . 6
|
10 | 9 | anbi2d 740 |
. . . . 5
|
11 | 8, 10 | bitrd 268 |
. . . 4
|
12 | 11 | 3coml 1272 |
. . 3
|
13 | 1, 7, 12 | 3orbi123d 1398 |
. 2
|
14 | | fveecn 25782 |
. . . . . . . . . . . . 13
|
15 | | fveecn 25782 |
. . . . . . . . . . . . 13
|
16 | | subid 10300 |
. . . . . . . . . . . . . . . 16
|
17 | 16 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
18 | 17 | adantl 482 |
. . . . . . . . . . . . . 14
|
19 | | subcl 10280 |
. . . . . . . . . . . . . . 15
|
20 | 19 | mul01d 10235 |
. . . . . . . . . . . . . 14
|
21 | 18, 20 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
22 | 14, 15, 21 | syl2an 494 |
. . . . . . . . . . . 12
|
23 | 22 | anandirs 874 |
. . . . . . . . . . 11
|
24 | | 0le0 11110 |
. . . . . . . . . . 11
|
25 | 23, 24 | syl6eqbr 4692 |
. . . . . . . . . 10
|
26 | 25 | ralrimiva 2966 |
. . . . . . . . 9
|
27 | 26 | 3adant1 1079 |
. . . . . . . 8
|
28 | | fveq1 6190 |
. . . . . . . . . . . 12
|
29 | 28 | oveq2d 6666 |
. . . . . . . . . . 11
|
30 | 28 | oveq2d 6666 |
. . . . . . . . . . 11
|
31 | 29, 30 | oveq12d 6668 |
. . . . . . . . . 10
|
32 | 31 | breq1d 4663 |
. . . . . . . . 9
|
33 | 32 | ralbidv 2986 |
. . . . . . . 8
|
34 | 27, 33 | syl5ibcom 235 |
. . . . . . 7
|
35 | | 3mix1 1230 |
. . . . . . 7
|
36 | 34, 35 | syl6 35 |
. . . . . 6
|
37 | 36 | a1dd 50 |
. . . . 5
|
38 | | simp3 1063 |
. . . . . . . . 9
|
39 | | simp1 1061 |
. . . . . . . . 9
|
40 | | eqeefv 25783 |
. . . . . . . . 9
|
41 | 38, 39, 40 | syl2anc 693 |
. . . . . . . 8
|
42 | 41 | necon3abid 2830 |
. . . . . . 7
|
43 | | df-ne 2795 |
. . . . . . . . 9
|
44 | 43 | rexbii 3041 |
. . . . . . . 8
|
45 | | rexnal 2995 |
. . . . . . . 8
|
46 | 44, 45 | bitr2i 265 |
. . . . . . 7
|
47 | 42, 46 | syl6bb 276 |
. . . . . 6
|
48 | | ralcom 3098 |
. . . . . . . 8
|
49 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
50 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
51 | 49, 50 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
52 | 51 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
53 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
54 | 53, 50 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
55 | 54 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
56 | 52, 55 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
57 | 56 | ralbidv 2986 |
. . . . . . . . . . 11
|
58 | 57 | rspcv 3305 |
. . . . . . . . . 10
|
59 | 58 | ad2antrl 764 |
. . . . . . . . 9
|
60 | | fveere 25781 |
. . . . . . . . . . . . . 14
|
61 | 60 | 3ad2antl1 1223 |
. . . . . . . . . . . . 13
|
62 | | fveere 25781 |
. . . . . . . . . . . . . 14
|
63 | 62 | 3ad2antl2 1224 |
. . . . . . . . . . . . 13
|
64 | | fveere 25781 |
. . . . . . . . . . . . . 14
|
65 | 64 | 3ad2antl3 1225 |
. . . . . . . . . . . . 13
|
66 | 61, 63, 65 | 3jca 1242 |
. . . . . . . . . . . 12
|
67 | 66 | anim1i 592 |
. . . . . . . . . . 11
|
68 | 67 | anasss 679 |
. . . . . . . . . 10
|
69 | | fveecn 25782 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . 15
|
71 | 14 | 3ad2antl2 1224 |
. . . . . . . . . . . . . . 15
|
72 | 15 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . 15
|
73 | 70, 71, 72 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
74 | 73 | adantlr 751 |
. . . . . . . . . . . . 13
|
75 | | recn 10026 |
. . . . . . . . . . . . . . . 16
|
76 | | recn 10026 |
. . . . . . . . . . . . . . . 16
|
77 | | recn 10026 |
. . . . . . . . . . . . . . . 16
|
78 | 75, 76, 77 | 3anim123i 1247 |
. . . . . . . . . . . . . . 15
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . 14
|
80 | 79 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
81 | | simplrr 801 |
. . . . . . . . . . . . 13
|
82 | | eqcom 2629 |
. . . . . . . . . . . . . 14
|
83 | | simp12 1092 |
. . . . . . . . . . . . . . . 16
|
84 | | simp11 1091 |
. . . . . . . . . . . . . . . 16
|
85 | | simp22 1095 |
. . . . . . . . . . . . . . . . . . 19
|
86 | | simp21 1094 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 85, 86 | subcld 10392 |
. . . . . . . . . . . . . . . . . 18
|
88 | | simp23 1096 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 88, 86 | subcld 10392 |
. . . . . . . . . . . . . . . . . 18
|
90 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 90, 91 | subeq0ad 10402 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 92 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 93 | biimp3ar 1433 |
. . . . . . . . . . . . . . . . . 18
|
95 | 87, 89, 94 | divcld 10801 |
. . . . . . . . . . . . . . . . 17
|
96 | | simp13 1093 |
. . . . . . . . . . . . . . . . . 18
|
97 | 96, 84 | subcld 10392 |
. . . . . . . . . . . . . . . . 17
|
98 | 95, 97 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
99 | | subadd2 10285 |
. . . . . . . . . . . . . . . . 17
|
100 | 99 | bicomd 213 |
. . . . . . . . . . . . . . . 16
|
101 | 83, 84, 98, 100 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
102 | 87, 97, 89, 94 | div23d 10838 |
. . . . . . . . . . . . . . . 16
|
103 | 102 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
104 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
|
105 | 87, 97 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
106 | 83, 84 | subcld 10392 |
. . . . . . . . . . . . . . . . . 18
|
107 | 105, 89, 106, 94 | divmuld 10823 |
. . . . . . . . . . . . . . . . 17
|
108 | 89, 106 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
|
110 | 107, 109 | bitrd 268 |
. . . . . . . . . . . . . . . 16
|
111 | 104, 110 | syl5bb 272 |
. . . . . . . . . . . . . . 15
|
112 | 101, 103,
111 | 3bitr2d 296 |
. . . . . . . . . . . . . 14
|
113 | 82, 112 | syl5bb 272 |
. . . . . . . . . . . . 13
|
114 | 74, 80, 81, 113 | syl3anc 1326 |
. . . . . . . . . . . 12
|
115 | 114 | ralbidva 2985 |
. . . . . . . . . . 11
|
116 | | 3simpb 1059 |
. . . . . . . . . . . 12
|
117 | | simpl2 1065 |
. . . . . . . . . . . . . 14
|
118 | | simpl1 1064 |
. . . . . . . . . . . . . 14
|
119 | 117, 118 | resubcld 10458 |
. . . . . . . . . . . . 13
|
120 | | simpl3 1066 |
. . . . . . . . . . . . . 14
|
121 | 120, 118 | resubcld 10458 |
. . . . . . . . . . . . 13
|
122 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
|
123 | 122 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
124 | 75 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
125 | 123, 124 | subeq0ad 10402 |
. . . . . . . . . . . . . . 15
|
126 | 125 | necon3bid 2838 |
. . . . . . . . . . . . . 14
|
127 | 126 | biimpar 502 |
. . . . . . . . . . . . 13
|
128 | 119, 121,
127 | redivcld 10853 |
. . . . . . . . . . . 12
|
129 | | colinearalglem4 25789 |
. . . . . . . . . . . . 13
|
130 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
131 | 130 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
132 | 131 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
133 | 132 | ralimi 2952 |
. . . . . . . . . . . . . . 15
|
134 | | ralbi 3068 |
. . . . . . . . . . . . . . 15
|
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
|
136 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
137 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
138 | 136, 137 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
139 | 138 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
140 | 139 | ralimi 2952 |
. . . . . . . . . . . . . . 15
|
141 | | ralbi 3068 |
. . . . . . . . . . . . . . 15
|
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . 14
|
143 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
144 | 143 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
145 | 144 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
146 | 145 | ralimi 2952 |
. . . . . . . . . . . . . . 15
|
147 | | ralbi 3068 |
. . . . . . . . . . . . . . 15
|
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
|
149 | 135, 142,
148 | 3orbi123d 1398 |
. . . . . . . . . . . . 13
|
150 | 129, 149 | syl5ibrcom 237 |
. . . . . . . . . . . 12
|
151 | 116, 128,
150 | syl2an 494 |
. . . . . . . . . . 11
|
152 | 115, 151 | sylbird 250 |
. . . . . . . . . 10
|
153 | 68, 152 | syldan 487 |
. . . . . . . . 9
|
154 | 59, 153 | syld 47 |
. . . . . . . 8
|
155 | 48, 154 | syl5bi 232 |
. . . . . . 7
|
156 | 155 | rexlimdvaa 3032 |
. . . . . 6
|
157 | 47, 156 | sylbid 230 |
. . . . 5
|
158 | 37, 157 | pm2.61dne 2880 |
. . . 4
|
159 | 158 | pm4.71rd 667 |
. . 3
|
160 | | andir 912 |
. . . . 5
|
161 | 160 | orbi1i 542 |
. . . 4
|
162 | | df-3or 1038 |
. . . . . 6
|
163 | 162 | anbi1i 731 |
. . . . 5
|
164 | | andir 912 |
. . . . 5
|
165 | 163, 164 | bitri 264 |
. . . 4
|
166 | | df-3or 1038 |
. . . 4
|
167 | 161, 165,
166 | 3bitr4i 292 |
. . 3
|
168 | 159, 167 | syl6rbb 277 |
. 2
|
169 | 13, 168 | bitrd 268 |
1
|