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 ⊢ ( 𝜑 → 𝑋 = 𝑁 )