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 ( 𝜑𝑆 ⊆ ℂ )
constrrtll.a ( 𝜑𝐴𝑆 )
constrrtll.b ( 𝜑𝐵𝑆 )
constrrtll.c ( 𝜑𝐶𝑆 )
constrrtll.d ( 𝜑𝐷𝑆 )
constrrtll.t ( 𝜑𝑇 ∈ ℝ )
constrrtll.r ( 𝜑𝑅 ∈ ℝ )
constrrtll.1 ( 𝜑𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵𝐴 ) ) ) )
constrrtll.2 ( 𝜑𝑋 = ( 𝐶 + ( 𝑅 · ( 𝐷𝐶 ) ) ) )
constrrtll.3 ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐷𝐶 ) ) ) ≠ 0 )
constrrtll.n 𝑁 = ( 𝐴 + ( ( ( ( ( 𝐴𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷𝐶 ) ) − ( ( 𝐵𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) · ( 𝐵𝐴 ) ) )
Assertion constrrtll ( 𝜑𝑋 = 𝑁 )

Proof

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