Metamath Proof Explorer


Theorem colinearalglem4

Description: Lemma for colinearalg . Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013)

Ref Expression
Assertion colinearalglem4 A𝔼NC𝔼NKi1NKCiAi+Ai-AiCiAi0i1NCiKCiAi+AiAiKCiAi+Ai0i1NAiCiKCiAi+Ai-Ci0

Proof

Step Hyp Ref Expression
1 relin01 KK00KK11K
2 1 adantl A𝔼NC𝔼NKK00KK11K
3 fveere A𝔼Ni1NAi
4 3 adantlr A𝔼NC𝔼Ni1NAi
5 fveere C𝔼Ni1NCi
6 5 adantll A𝔼NC𝔼Ni1NCi
7 4 6 jca A𝔼NC𝔼Ni1NAiCi
8 simprl AiCiKK0K
9 8 recnd AiCiKK0K
10 resubcl CiAiCiAi
11 10 ancoms AiCiCiAi
12 11 adantr AiCiKK0CiAi
13 12 recnd AiCiKK0CiAi
14 9 13 13 mulassd AiCiKK0KCiAiCiAi=KCiAiCiAi
15 8 12 remulcld AiCiKK0KCiAi
16 15 recnd AiCiKK0KCiAi
17 recn AiAi
18 17 ad2antrr AiCiKK0Ai
19 16 18 pncand AiCiKK0KCiAi+Ai-Ai=KCiAi
20 19 oveq1d AiCiKK0KCiAi+Ai-AiCiAi=KCiAiCiAi
21 13 sqvald AiCiKK0CiAi2=CiAiCiAi
22 21 oveq2d AiCiKK0KCiAi2=KCiAiCiAi
23 14 20 22 3eqtr4d AiCiKK0KCiAi+Ai-AiCiAi=KCiAi2
24 simprr AiCiKK0K0
25 12 sqge0d AiCiKK00CiAi2
26 24 25 jca AiCiKK0K00CiAi2
27 26 orcd AiCiKK0K00CiAi20KCiAi20
28 12 resqcld AiCiKK0CiAi2
29 mulle0b KCiAi2KCiAi20K00CiAi20KCiAi20
30 8 28 29 syl2anc AiCiKK0KCiAi20K00CiAi20KCiAi20
31 27 30 mpbird AiCiKK0KCiAi20
32 23 31 eqbrtrd AiCiKK0KCiAi+Ai-AiCiAi0
33 7 32 sylan A𝔼NC𝔼Ni1NKK0KCiAi+Ai-AiCiAi0
34 33 an32s A𝔼NC𝔼NKK0i1NKCiAi+Ai-AiCiAi0
35 34 ralrimiva A𝔼NC𝔼NKK0i1NKCiAi+Ai-AiCiAi0
36 35 expr A𝔼NC𝔼NKK0i1NKCiAi+Ai-AiCiAi0
37 recn CiCi
38 37 ad2antlr AiCiK0KK1Ci
39 17 ad2antrr AiCiK0KK1Ai
40 simprl AiCiK0KK1K
41 11 adantr AiCiK0KK1CiAi
42 40 41 remulcld AiCiK0KK1KCiAi
43 42 recnd AiCiK0KK1KCiAi
44 38 39 43 sub32d AiCiK0KK1Ci-Ai-KCiAi=Ci-KCiAi-Ai
45 ax-1cn 1
46 40 recnd AiCiK0KK1K
47 41 recnd AiCiK0KK1CiAi
48 subdir 1KCiAi1KCiAi=1CiAiKCiAi
49 45 46 47 48 mp3an2i AiCiK0KK11KCiAi=1CiAiKCiAi
50 47 mullidd AiCiK0KK11CiAi=CiAi
51 50 oveq1d AiCiK0KK11CiAiKCiAi=Ci-Ai-KCiAi
52 49 51 eqtr2d AiCiK0KK1Ci-Ai-KCiAi=1KCiAi
53 38 43 39 subsub4d AiCiK0KK1Ci-KCiAi-Ai=CiKCiAi+Ai
54 44 52 53 3eqtr3rd AiCiK0KK1CiKCiAi+Ai=1KCiAi
55 39 39 43 sub32d AiCiK0KK1Ai-Ai-KCiAi=Ai-KCiAi-Ai
56 39 subidd AiCiK0KK1AiAi=0
57 56 oveq1d AiCiK0KK1Ai-Ai-KCiAi=0KCiAi
58 df-neg KCiAi=0KCiAi
59 57 58 eqtr4di AiCiK0KK1Ai-Ai-KCiAi=KCiAi
60 39 43 39 subsub4d AiCiK0KK1Ai-KCiAi-Ai=AiKCiAi+Ai
61 55 59 60 3eqtr3rd AiCiK0KK1AiKCiAi+Ai=KCiAi
62 54 61 oveq12d AiCiK0KK1CiKCiAi+AiAiKCiAi+Ai=1KCiAiKCiAi
63 1re 1
64 resubcl 1K1K
65 63 64 mpan K1K
66 65 ad2antrl AiCiK0KK11K
67 66 41 remulcld AiCiK0KK11KCiAi
68 67 recnd AiCiK0KK11KCiAi
69 68 43 mulneg2d AiCiK0KK11KCiAiKCiAi=1KCiAiKCiAi
70 66 recnd AiCiK0KK11K
71 70 47 46 47 mul4d AiCiK0KK11KCiAiKCiAi=1KKCiAiCiAi
72 71 negeqd AiCiK0KK11KCiAiKCiAi=1KKCiAiCiAi
73 62 69 72 3eqtrd AiCiK0KK1CiKCiAi+AiAiKCiAi+Ai=1KKCiAiCiAi
74 66 40 remulcld AiCiK0KK11KK
75 41 resqcld AiCiK0KK1CiAi2
76 simpl K0KK1K
77 63 76 64 sylancr K0KK11K
78 subge0 1K01KK1
79 63 78 mpan K01KK1
80 79 biimpar KK101K
81 80 adantrl K0KK101K
82 simprl K0KK10K
83 77 76 81 82 mulge0d K0KK101KK
84 83 adantl AiCiK0KK101KK
85 41 sqge0d AiCiK0KK10CiAi2
86 74 75 84 85 mulge0d AiCiK0KK101KKCiAi2
87 47 sqvald AiCiK0KK1CiAi2=CiAiCiAi
88 87 oveq2d AiCiK0KK11KKCiAi2=1KKCiAiCiAi
89 86 88 breqtrd AiCiK0KK101KKCiAiCiAi
90 41 41 remulcld AiCiK0KK1CiAiCiAi
91 74 90 remulcld AiCiK0KK11KKCiAiCiAi
92 91 le0neg2d AiCiK0KK101KKCiAiCiAi1KKCiAiCiAi0
93 89 92 mpbid AiCiK0KK11KKCiAiCiAi0
94 73 93 eqbrtrd AiCiK0KK1CiKCiAi+AiAiKCiAi+Ai0
95 7 94 sylan A𝔼NC𝔼Ni1NK0KK1CiKCiAi+AiAiKCiAi+Ai0
96 95 an32s A𝔼NC𝔼NK0KK1i1NCiKCiAi+AiAiKCiAi+Ai0
97 96 ralrimiva A𝔼NC𝔼NK0KK1i1NCiKCiAi+AiAiKCiAi+Ai0
98 97 expr A𝔼NC𝔼NK0KK1i1NCiKCiAi+AiAiKCiAi+Ai0
99 37 ad2antlr AiCiK1KCi
100 17 ad2antrr AiCiK1KAi
101 99 100 negsubdi2d AiCiK1KCiAi=AiCi
102 101 oveq1d AiCiK1KCiAiK1CiAi=AiCiK1CiAi
103 simplr AiCiK1KCi
104 simpll AiCiK1KAi
105 103 104 10 syl2anc AiCiK1KCiAi
106 105 recnd AiCiK1KCiAi
107 peano2rem KK1
108 107 ad2antrl AiCiK1KK1
109 108 105 remulcld AiCiK1KK1CiAi
110 109 recnd AiCiK1KK1CiAi
111 106 110 mulneg1d AiCiK1KCiAiK1CiAi=CiAiK1CiAi
112 108 recnd AiCiK1KK1
113 106 112 106 mul12d AiCiK1KCiAiK1CiAi=K1CiAiCiAi
114 106 sqvald AiCiK1KCiAi2=CiAiCiAi
115 114 oveq2d AiCiK1KK1CiAi2=K1CiAiCiAi
116 113 115 eqtr4d AiCiK1KCiAiK1CiAi=K1CiAi2
117 116 negeqd AiCiK1KCiAiK1CiAi=K1CiAi2
118 111 117 eqtrd AiCiK1KCiAiK1CiAi=K1CiAi2
119 simprl AiCiK1KK
120 119 recnd AiCiK1KK
121 subdir K1CiAiK1CiAi=KCiAi1CiAi
122 45 121 mp3an2 KCiAiK1CiAi=KCiAi1CiAi
123 120 106 122 syl2anc AiCiK1KK1CiAi=KCiAi1CiAi
124 106 mullidd AiCiK1K1CiAi=CiAi
125 124 oveq2d AiCiK1KKCiAi1CiAi=KCiAiCiAi
126 119 105 remulcld AiCiK1KKCiAi
127 126 recnd AiCiK1KKCiAi
128 127 99 100 subsub3d AiCiK1KKCiAiCiAi=KCiAi+Ai-Ci
129 123 125 128 3eqtrd AiCiK1KK1CiAi=KCiAi+Ai-Ci
130 129 oveq2d AiCiK1KAiCiK1CiAi=AiCiKCiAi+Ai-Ci
131 102 118 130 3eqtr3rd AiCiK1KAiCiKCiAi+Ai-Ci=K1CiAi2
132 105 resqcld AiCiK1KCiAi2
133 simprr AiCiK1K1K
134 subge0 K10K11K
135 63 134 mpan2 K0K11K
136 135 ad2antrl AiCiK1K0K11K
137 133 136 mpbird AiCiK1K0K1
138 105 sqge0d AiCiK1K0CiAi2
139 108 132 137 138 mulge0d AiCiK1K0K1CiAi2
140 108 132 remulcld AiCiK1KK1CiAi2
141 140 le0neg2d AiCiK1K0K1CiAi2K1CiAi20
142 139 141 mpbid AiCiK1KK1CiAi20
143 131 142 eqbrtrd AiCiK1KAiCiKCiAi+Ai-Ci0
144 7 143 sylan A𝔼NC𝔼Ni1NK1KAiCiKCiAi+Ai-Ci0
145 144 an32s A𝔼NC𝔼NK1Ki1NAiCiKCiAi+Ai-Ci0
146 145 ralrimiva A𝔼NC𝔼NK1Ki1NAiCiKCiAi+Ai-Ci0
147 146 expr A𝔼NC𝔼NK1Ki1NAiCiKCiAi+Ai-Ci0
148 36 98 147 3orim123d A𝔼NC𝔼NKK00KK11Ki1NKCiAi+Ai-AiCiAi0i1NCiKCiAi+AiAiKCiAi+Ai0i1NAiCiKCiAi+Ai-Ci0
149 2 148 mpd A𝔼NC𝔼NKi1NKCiAi+Ai-AiCiAi0i1NCiKCiAi+AiAiKCiAi+Ai0i1NAiCiKCiAi+Ai-Ci0