Metamath Proof Explorer


Theorem constrrtlc1

Description: In the construction of constructible numbers, line-circle intersections are roots of a quadratic equation, non-degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses constrrtlc.s φ S
constrrtlc.a φ A S
constrrtlc.b φ B S
constrrtlc.c φ C S
constrrtlc.e φ E S
constrrtlc.f φ F S
constrrtlc.t φ T
constrrtlc.1 φ X = A + T B A
constrrtlc.2 φ X C = E F
constrrtlc.q Q = B A B A
constrrtlc.m M = A A Q - C - C Q Q
constrrtlc.n N = C A - A Q - C + E F E F Q
constrrtlc1.1 φ A B
Assertion constrrtlc1 φ X 2 + M X + N = 0 Q 0

Proof

Step Hyp Ref Expression
1 constrrtlc.s φ S
2 constrrtlc.a φ A S
3 constrrtlc.b φ B S
4 constrrtlc.c φ C S
5 constrrtlc.e φ E S
6 constrrtlc.f φ F S
7 constrrtlc.t φ T
8 constrrtlc.1 φ X = A + T B A
9 constrrtlc.2 φ X C = E F
10 constrrtlc.q Q = B A B A
11 constrrtlc.m M = A A Q - C - C Q Q
12 constrrtlc.n N = C A - A Q - C + E F E F Q
13 constrrtlc1.1 φ A B
14 1 2 sseldd φ A
15 14 cjcld φ A
16 1 3 sseldd φ B
17 16 cjcld φ B
18 17 15 subcld φ B A
19 16 14 subcld φ B A
20 13 necomd φ B A
21 16 14 20 subne0d φ B A 0
22 18 19 21 divcld φ B A B A
23 10 22 eqeltrid φ Q
24 14 23 mulcld φ A Q
25 15 24 subcld φ A A Q
26 1 4 sseldd φ C
27 26 cjcld φ C
28 25 27 subcld φ A - A Q - C
29 26 23 mulcld φ C Q
30 28 29 subcld φ A A Q - C - C Q
31 16 14 cjsubd φ B A = B A
32 19 21 cjne0d φ B A 0
33 31 32 eqnetrrd φ B A 0
34 18 19 33 21 divne0d φ B A B A 0
35 10 neeq1i Q 0 B A B A 0
36 34 35 sylibr φ Q 0
37 30 23 36 divcld φ A A Q - C - C Q Q
38 7 recnd φ T
39 38 19 mulcld φ T B A
40 14 39 addcld φ A + T B A
41 8 40 eqeltrd φ X
42 37 41 mulcomd φ A A Q - C - C Q Q X = X A A Q - C - C Q Q
43 11 a1i φ M = A A Q - C - C Q Q
44 43 oveq1d φ M X = A A Q - C - C Q Q X
45 41 30 23 36 divassd φ X A A Q - C - C Q Q = X A A Q - C - C Q Q
46 42 44 45 3eqtr4d φ M X = X A A Q - C - C Q Q
47 12 a1i φ N = C A - A Q - C + E F E F Q
48 46 47 oveq12d φ M X + N = X A A Q - C - C Q Q + C A - A Q - C + E F E F Q
49 41 30 mulcld φ X A A Q - C - C Q
50 26 28 mulcld φ C A - A Q - C
51 41 sqvald φ X 2 = X X
52 51 oveq1d φ X 2 Q = X X Q
53 41 41 23 mulassd φ X X Q = X X Q
54 52 53 eqtrd φ X 2 Q = X X Q
55 41 23 mulcld φ X Q
56 41 55 mulcld φ X X Q
57 54 56 eqeltrd φ X 2 Q
58 57 49 50 addsubd φ X 2 Q + X A A Q - C - C Q - C A - A Q - C = X 2 Q - C A - A Q - C + X A A Q - C - C Q
59 54 oveq1d φ X 2 Q C A - A Q - C = X X Q C A - A Q - C
60 41 28 29 subdid φ X A A Q - C - C Q = X A - A Q - C X C Q
61 59 60 oveq12d φ X 2 Q - C A - A Q - C + X A A Q - C - C Q = X X Q C A - A Q - C + X A - A Q - C - X C Q
62 41 28 mulcld φ X A - A Q - C
63 41 29 mulcld φ X C Q
64 56 62 50 63 addsub4d φ X X Q + X A - A Q - C - C A - A Q - C + X C Q = X X Q C A - A Q - C + X A - A Q - C - X C Q
65 41 26 55 28 submuladdd φ X C X Q + A A Q - C = X X Q + X A - A Q - C - C X Q + C A - A Q - C
66 9 oveq1d φ X C 2 = E F 2
67 41 26 subcld φ X C
68 67 absvalsqd φ X C 2 = X C X C
69 1 5 sseldd φ E
70 1 6 sseldd φ F
71 69 70 subcld φ E F
72 71 absvalsqd φ E F 2 = E F E F
73 66 68 72 3eqtr3d φ X C X C = E F E F
74 8 fvoveq1d φ X C = A + T B A - C
75 40 26 cjsubd φ A + T B A - C = A + T B A C
76 14 39 cjaddd φ A + T B A = A + T B A
77 38 19 cjmuld φ T B A = T B A
78 7 cjred φ T = T
79 14 39 8 mvrladdd φ X A = T B A
80 79 39 eqeltrd φ X A
81 80 38 19 21 divmul3d φ X A B A = T X A = T B A
82 79 81 mpbird φ X A B A = T
83 78 82 eqtr4d φ T = X A B A
84 83 31 oveq12d φ T B A = X A B A B A
85 80 19 18 21 div32d φ X A B A B A = X A B A B A
86 10 oveq2i X A Q = X A B A B A
87 85 86 eqtr4di φ X A B A B A = X A Q
88 41 14 23 subdird φ X A Q = X Q A Q
89 84 87 88 3eqtrd φ T B A = X Q A Q
90 77 89 eqtrd φ T B A = X Q A Q
91 90 oveq2d φ A + T B A = A + X Q - A Q
92 15 55 24 addsub12d φ A + X Q - A Q = X Q + A - A Q
93 76 91 92 3eqtrd φ A + T B A = X Q + A - A Q
94 93 oveq1d φ A + T B A C = X Q + A A Q - C
95 55 25 27 addsubassd φ X Q + A A Q - C = X Q + A A Q - C
96 75 94 95 3eqtrd φ A + T B A - C = X Q + A A Q - C
97 74 96 eqtrd φ X C = X Q + A A Q - C
98 97 oveq2d φ X C X C = X C X Q + A A Q - C
99 69 70 cjsubd φ E F = E F
100 99 oveq2d φ E F E F = E F E F
101 73 98 100 3eqtr3d φ X C X Q + A A Q - C = E F E F
102 26 41 23 mul12d φ C X Q = X C Q
103 102 oveq1d φ C X Q + C A - A Q - C = X C Q + C A - A Q - C
104 63 50 103 comraddd φ C X Q + C A - A Q - C = C A - A Q - C + X C Q
105 104 oveq2d φ X X Q + X A - A Q - C - C X Q + C A - A Q - C = X X Q + X A - A Q - C - C A - A Q - C + X C Q
106 65 101 105 3eqtr3rd φ X X Q + X A - A Q - C - C A - A Q - C + X C Q = E F E F
107 61 64 106 3eqtr2d φ X 2 Q - C A - A Q - C + X A A Q - C - C Q = E F E F
108 58 107 eqtrd φ X 2 Q + X A A Q - C - C Q - C A - A Q - C = E F E F
109 57 49 addcld φ X 2 Q + X A A Q - C - C Q
110 109 50 subcld φ X 2 Q + X A A Q - C - C Q - C A - A Q - C
111 108 110 eqeltrrd φ E F E F
112 50 111 addcld φ C A - A Q - C + E F E F
113 112 negcld φ C A - A Q - C + E F E F
114 49 113 23 36 divdird φ X A A Q - C - C Q + C A - A Q - C + E F E F Q = X A A Q - C - C Q Q + C A - A Q - C + E F E F Q
115 48 114 eqtr4d φ M X + N = X A A Q - C - C Q + C A - A Q - C + E F E F Q
116 115 oveq2d φ X 2 + M X + N = X 2 + X A A Q - C - C Q + C A - A Q - C + E F E F Q
117 41 sqcld φ X 2
118 49 113 addcld φ X A A Q - C - C Q + C A - A Q - C + E F E F
119 117 23 118 36 muldivdid φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F Q = X 2 + X A A Q - C - C Q + C A - A Q - C + E F E F Q
120 57 49 113 addassd φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F = X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F
121 109 112 negsubd φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F = X 2 Q + X A A Q - C - C Q - C A - A Q - C + E F E F
122 109 50 111 subsub4d φ X 2 Q + X A A Q - C - C Q - C A - A Q - C - E F E F = X 2 Q + X A A Q - C - C Q - C A - A Q - C + E F E F
123 110 108 subeq0bd φ X 2 Q + X A A Q - C - C Q - C A - A Q - C - E F E F = 0
124 121 122 123 3eqtr2d φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F = 0
125 120 124 eqtr3d φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F = 0
126 57 118 addcld φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F
127 126 23 36 diveq0ad φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F Q = 0 X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F = 0
128 125 127 mpbird φ X 2 Q + X A A Q - C - C Q + C A - A Q - C + E F E F Q = 0
129 116 119 128 3eqtr2d φ X 2 + M X + N = 0
130 129 36 jca φ X 2 + M X + N = 0 Q 0