Metamath Proof Explorer


Theorem constrrtll

Description: In the construction of constructible numbers, line-line intersections are solutions of linear equations, and can therefore be completely constructed. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses constrrtll.s φ S
constrrtll.a φ A S
constrrtll.b φ B S
constrrtll.c φ C S
constrrtll.d φ D S
constrrtll.t φ T
constrrtll.r φ R
constrrtll.1 φ X = A + T B A
constrrtll.2 φ X = C + R D C
constrrtll.3 φ B A D C 0
constrrtll.n N = A + A C D C A C D C B A D C B A D C B A
Assertion constrrtll φ X = N

Proof

Step Hyp Ref Expression
1 constrrtll.s φ S
2 constrrtll.a φ A S
3 constrrtll.b φ B S
4 constrrtll.c φ C S
5 constrrtll.d φ D S
6 constrrtll.t φ T
7 constrrtll.r φ R
8 constrrtll.1 φ X = A + T B A
9 constrrtll.2 φ X = C + R D C
10 constrrtll.3 φ B A D C 0
11 constrrtll.n N = A + A C D C A C D C B A D C B A D C B A
12 6 recnd φ T
13 1 3 sseldd φ B
14 1 2 sseldd φ A
15 13 14 cjsubd φ B A = B A
16 13 14 subcld φ B A
17 16 cjcld φ B A
18 15 17 eqeltrrd φ B A
19 1 5 sseldd φ D
20 1 4 sseldd φ C
21 19 20 subcld φ D C
22 18 21 mulcld φ B A D C
23 19 20 cjsubd φ D C = D C
24 21 cjcld φ D C
25 23 24 eqeltrrd φ D C
26 16 25 mulcld φ B A D C
27 12 22 26 subdid φ T B A D C B A D C = T B A D C T B A D C
28 8 oveq1d φ X C = A + T B A - C
29 7 recnd φ R
30 29 21 mulcld φ R D C
31 20 30 9 mvrladdd φ X C = R D C
32 28 31 eqtr3d φ A + T B A - C = R D C
33 32 30 eqeltrd φ A + T B A - C
34 fveq2 B A D C = 0 B A D C = 0
35 im0 0 = 0
36 34 35 eqtrdi B A D C = 0 B A D C = 0
37 36 necon3i B A D C 0 B A D C 0
38 10 37 syl φ B A D C 0
39 17 21 38 mulne0bbd φ D C 0
40 33 29 21 39 divmul3d φ A + T B A - C D C = R A + T B A - C = R D C
41 32 40 mpbird φ A + T B A - C D C = R
42 41 fveq2d φ A + T B A - C D C = R
43 33 21 39 cjdivd φ A + T B A - C D C = A + T B A - C D C
44 12 16 mulcld φ T B A
45 14 44 addcld φ A + T B A
46 45 20 cjsubd φ A + T B A - C = A + T B A C
47 14 44 cjaddd φ A + T B A = A + T B A
48 12 16 cjmuld φ T B A = T B A
49 6 cjred φ T = T
50 49 15 oveq12d φ T B A = T B A
51 48 50 eqtrd φ T B A = T B A
52 51 oveq2d φ A + T B A = A + T B A
53 47 52 eqtrd φ A + T B A = A + T B A
54 53 oveq1d φ A + T B A C = A + T B A - C
55 46 54 eqtrd φ A + T B A - C = A + T B A - C
56 55 23 oveq12d φ A + T B A - C D C = A + T B A - C D C
57 43 56 eqtrd φ A + T B A - C D C = A + T B A - C D C
58 7 cjred φ R = R
59 42 57 58 3eqtr3rd φ R = A + T B A - C D C
60 41 59 eqtrd φ A + T B A - C D C = A + T B A - C D C
61 14 cjcld φ A
62 12 18 mulcld φ T B A
63 61 62 addcld φ A + T B A
64 20 cjcld φ C
65 63 64 subcld φ A + T B A - C
66 21 39 cjne0d φ D C 0
67 23 66 eqnetrrd φ D C 0
68 33 21 65 25 39 67 divmuleqd φ A + T B A - C D C = A + T B A - C D C A + T B A - C D C = A + T B A - C D C
69 60 68 mpbid φ A + T B A - C D C = A + T B A - C D C
70 14 44 20 addsubassd φ A + T B A - C = A + T B A - C
71 44 14 20 addsub12d φ T B A + A - C = A + T B A - C
72 70 71 eqtr4d φ A + T B A - C = T B A + A - C
73 72 oveq1d φ A + T B A - C D C = T B A + A - C D C
74 14 20 subcld φ A C
75 44 74 25 adddird φ T B A + A - C D C = T B A D C + A C D C
76 12 16 25 mulassd φ T B A D C = T B A D C
77 76 oveq1d φ T B A D C + A C D C = T B A D C + A C D C
78 73 75 77 3eqtrd φ A + T B A - C D C = T B A D C + A C D C
79 61 62 64 addsubassd φ A + T B A - C = A + T B A - C
80 62 61 64 addsub12d φ T B A + A - C = A + T B A - C
81 79 80 eqtr4d φ A + T B A - C = T B A + A - C
82 81 oveq1d φ A + T B A - C D C = T B A + A - C D C
83 61 64 subcld φ A C
84 62 83 21 adddird φ T B A + A - C D C = T B A D C + A C D C
85 12 18 21 mulassd φ T B A D C = T B A D C
86 85 oveq1d φ T B A D C + A C D C = T B A D C + A C D C
87 82 84 86 3eqtrd φ A + T B A - C D C = T B A D C + A C D C
88 69 78 87 3eqtr3d φ T B A D C + A C D C = T B A D C + A C D C
89 12 26 mulcld φ T B A D C
90 74 25 mulcld φ A C D C
91 12 22 mulcld φ T B A D C
92 83 21 mulcld φ A C D C
93 89 90 91 92 addsubeq4d φ T B A D C + A C D C = T B A D C + A C D C T B A D C T B A D C = A C D C A C D C
94 88 93 mpbid φ T B A D C T B A D C = A C D C A C D C
95 27 94 eqtrd φ T B A D C B A D C = A C D C A C D C
96 22 26 subcld φ B A D C B A D C
97 90 92 subcld φ A C D C A C D C
98 17 21 mulcld φ B A D C
99 reim0b B A D C B A D C B A D C = 0
100 98 99 syl φ B A D C B A D C = 0
101 100 necon3bbid φ ¬ B A D C B A D C 0
102 10 101 mpbird φ ¬ B A D C
103 cjreb B A D C B A D C B A D C = B A D C
104 98 103 syl φ B A D C B A D C = B A D C
105 104 necon3bbid φ ¬ B A D C B A D C B A D C
106 102 105 mpbid φ B A D C B A D C
107 17 21 cjmuld φ B A D C = B A D C
108 16 cjcjd φ B A = B A
109 108 23 oveq12d φ B A D C = B A D C
110 107 109 eqtrd φ B A D C = B A D C
111 15 oveq1d φ B A D C = B A D C
112 106 110 111 3netr3d φ B A D C B A D C
113 112 necomd φ B A D C B A D C
114 22 26 113 subne0d φ B A D C B A D C 0
115 12 96 97 114 ldiv φ T B A D C B A D C = A C D C A C D C T = A C D C A C D C B A D C B A D C
116 95 115 mpbid φ T = A C D C A C D C B A D C B A D C
117 116 oveq1d φ T B A = A C D C A C D C B A D C B A D C B A
118 117 oveq2d φ A + T B A = A + A C D C A C D C B A D C B A D C B A
119 8 118 eqtrd φ X = A + A C D C A C D C B A D C B A D C B A
120 119 11 eqtr4di φ X = N