Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  constrrtll Structured version   Visualization version   GIF version

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

Proof of Theorem constrrtll
StepHypRef Expression
1 constrrtll.1 . . 3 (𝜑𝑋 = (𝐴 + (𝑇 · (𝐵𝐴))))
2 constrrtll.t . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
32recnd 11320 . . . . . . . 8 (𝜑𝑇 ∈ ℂ)
4 constrrtll.s . . . . . . . . . . . 12 (𝜑𝑆 ⊆ ℂ)
5 constrrtll.b . . . . . . . . . . . 12 (𝜑𝐵𝑆)
64, 5sseldd 4009 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
7 constrrtll.a . . . . . . . . . . . 12 (𝜑𝐴𝑆)
84, 7sseldd 4009 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
96, 8cjsubd 32757 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵𝐴)) = ((∗‘𝐵) − (∗‘𝐴)))
106, 8subcld 11649 . . . . . . . . . . 11 (𝜑 → (𝐵𝐴) ∈ ℂ)
1110cjcld 15247 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵𝐴)) ∈ ℂ)
129, 11eqeltrrd 2845 . . . . . . . . 9 (𝜑 → ((∗‘𝐵) − (∗‘𝐴)) ∈ ℂ)
13 constrrtll.d . . . . . . . . . . 11 (𝜑𝐷𝑆)
144, 13sseldd 4009 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
15 constrrtll.c . . . . . . . . . . 11 (𝜑𝐶𝑆)
164, 15sseldd 4009 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
1714, 16subcld 11649 . . . . . . . . 9 (𝜑 → (𝐷𝐶) ∈ ℂ)
1812, 17mulcld 11312 . . . . . . . 8 (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) ∈ ℂ)
1914, 16cjsubd 32757 . . . . . . . . . 10 (𝜑 → (∗‘(𝐷𝐶)) = ((∗‘𝐷) − (∗‘𝐶)))
2017cjcld 15247 . . . . . . . . . 10 (𝜑 → (∗‘(𝐷𝐶)) ∈ ℂ)
2119, 20eqeltrrd 2845 . . . . . . . . 9 (𝜑 → ((∗‘𝐷) − (∗‘𝐶)) ∈ ℂ)
2210, 21mulcld 11312 . . . . . . . 8 (𝜑 → ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))) ∈ ℂ)
233, 18, 22subdid 11748 . . . . . . 7 (𝜑 → (𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) − (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))))
241oveq1d 7465 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐶) = ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶))
25 constrrtll.r . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ ℝ)
2625recnd 11320 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ ℂ)
2726, 17mulcld 11312 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝐷𝐶)) ∈ ℂ)
28 constrrtll.2 . . . . . . . . . . . . . 14 (𝜑𝑋 = (𝐶 + (𝑅 · (𝐷𝐶))))
2916, 27, 28mvrladdd 11705 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐶) = (𝑅 · (𝐷𝐶)))
3024, 29eqtr3d 2782 . . . . . . . . . . . 12 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = (𝑅 · (𝐷𝐶)))
3130, 27eqeltrd 2844 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) ∈ ℂ)
32 constrrtll.3 . . . . . . . . . . . . . . 15 (𝜑 → (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ 0)
33 fveq2 6922 . . . . . . . . . . . . . . . . 17 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) = 0 → (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = (ℑ‘0))
34 im0 15204 . . . . . . . . . . . . . . . . 17 (ℑ‘0) = 0
3533, 34eqtrdi 2796 . . . . . . . . . . . . . . . 16 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) = 0 → (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = 0)
3635necon3i 2979 . . . . . . . . . . . . . . 15 ((ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ 0 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ≠ 0)
3732, 36syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ≠ 0)
3811, 17, 37mulne0bbd 11948 . . . . . . . . . . . . 13 (𝜑 → (𝐷𝐶) ≠ 0)
3931, 26, 17, 38divmul3d 12106 . . . . . . . . . . . 12 (𝜑 → ((((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = 𝑅 ↔ ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = (𝑅 · (𝐷𝐶))))
4030, 39mpbird 257 . . . . . . . . . . 11 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = 𝑅)
4140fveq2d 6926 . . . . . . . . . . . 12 (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶))) = (∗‘𝑅))
4231, 17, 38cjdivd 15274 . . . . . . . . . . . . 13 (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶))) = ((∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) / (∗‘(𝐷𝐶))))
433, 10mulcld 11312 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 · (𝐵𝐴)) ∈ ℂ)
448, 43addcld 11311 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 + (𝑇 · (𝐵𝐴))) ∈ ℂ)
4544, 16cjsubd 32757 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) = ((∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) − (∗‘𝐶)))
468, 43cjaddd 15271 . . . . . . . . . . . . . . . . 17 (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (∗‘(𝑇 · (𝐵𝐴)))))
473, 10cjmuld 15272 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∗‘(𝑇 · (𝐵𝐴))) = ((∗‘𝑇) · (∗‘(𝐵𝐴))))
482cjred 15277 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗‘𝑇) = 𝑇)
4948, 9oveq12d 7468 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((∗‘𝑇) · (∗‘(𝐵𝐴))) = (𝑇 · ((∗‘𝐵) − (∗‘𝐴))))
5047, 49eqtrd 2780 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝑇 · (𝐵𝐴))) = (𝑇 · ((∗‘𝐵) − (∗‘𝐴))))
5150oveq2d 7466 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∗‘𝐴) + (∗‘(𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))))
5246, 51eqtrd 2780 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))))
5352oveq1d 7465 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) − (∗‘𝐶)) = (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)))
5445, 53eqtrd 2780 . . . . . . . . . . . . . 14 (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) = (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)))
5554, 19oveq12d 7468 . . . . . . . . . . . . 13 (𝜑 → ((∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) / (∗‘(𝐷𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
5642, 55eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
5725cjred 15277 . . . . . . . . . . . 12 (𝜑 → (∗‘𝑅) = 𝑅)
5841, 56, 573eqtr3rd 2789 . . . . . . . . . . 11 (𝜑𝑅 = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
5940, 58eqtrd 2780 . . . . . . . . . 10 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
608cjcld 15247 . . . . . . . . . . . . 13 (𝜑 → (∗‘𝐴) ∈ ℂ)
613, 12mulcld 11312 . . . . . . . . . . . . 13 (𝜑 → (𝑇 · ((∗‘𝐵) − (∗‘𝐴))) ∈ ℂ)
6260, 61addcld 11311 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) ∈ ℂ)
6316cjcld 15247 . . . . . . . . . . . 12 (𝜑 → (∗‘𝐶) ∈ ℂ)
6462, 63subcld 11649 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) ∈ ℂ)
6517, 38cjne0d 15254 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐷𝐶)) ≠ 0)
6619, 65eqnetrrd 3015 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐷) − (∗‘𝐶)) ≠ 0)
6731, 17, 64, 21, 38, 66divmuleqd 12118 . . . . . . . . . 10 (𝜑 → ((((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))) ↔ (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶))))
6859, 67mpbid 232 . . . . . . . . 9 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶)))
698, 43, 16addsubassd 11669 . . . . . . . . . . . 12 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = (𝐴 + ((𝑇 · (𝐵𝐴)) − 𝐶)))
7043, 8, 16addsub12d 11672 . . . . . . . . . . . 12 (𝜑 → ((𝑇 · (𝐵𝐴)) + (𝐴𝐶)) = (𝐴 + ((𝑇 · (𝐵𝐴)) − 𝐶)))
7169, 70eqtr4d 2783 . . . . . . . . . . 11 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = ((𝑇 · (𝐵𝐴)) + (𝐴𝐶)))
7271oveq1d 7465 . . . . . . . . . 10 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = (((𝑇 · (𝐵𝐴)) + (𝐴𝐶)) · ((∗‘𝐷) − (∗‘𝐶))))
738, 16subcld 11649 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶) ∈ ℂ)
7443, 73, 21adddird 11317 . . . . . . . . . 10 (𝜑 → (((𝑇 · (𝐵𝐴)) + (𝐴𝐶)) · ((∗‘𝐷) − (∗‘𝐶))) = (((𝑇 · (𝐵𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))))
753, 10, 21mulassd 11315 . . . . . . . . . . 11 (𝜑 → ((𝑇 · (𝐵𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) = (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))))
7675oveq1d 7465 . . . . . . . . . 10 (𝜑 → (((𝑇 · (𝐵𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))))
7772, 74, 763eqtrd 2784 . . . . . . . . 9 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))))
7860, 61, 63addsubassd 11669 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) = ((∗‘𝐴) + ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) − (∗‘𝐶))))
7961, 60, 63addsub12d 11672 . . . . . . . . . . . 12 (𝜑 → ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) = ((∗‘𝐴) + ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) − (∗‘𝐶))))
8078, 79eqtr4d 2783 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) = ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))))
8180oveq1d 7465 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶)) = (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) · (𝐷𝐶)))
8260, 63subcld 11649 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) − (∗‘𝐶)) ∈ ℂ)
8361, 82, 17adddird 11317 . . . . . . . . . 10 (𝜑 → (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) · (𝐷𝐶)) = (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷𝐶)) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
843, 12, 17mulassd 11315 . . . . . . . . . . 11 (𝜑 → ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷𝐶)) = (𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))))
8584oveq1d 7465 . . . . . . . . . 10 (𝜑 → (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷𝐶)) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
8681, 83, 853eqtrd 2784 . . . . . . . . 9 (𝜑 → ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶)) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
8768, 77, 863eqtr3d 2788 . . . . . . . 8 (𝜑 → ((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
883, 22mulcld 11312 . . . . . . . . 9 (𝜑 → (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ∈ ℂ)
8973, 21mulcld 11312 . . . . . . . . 9 (𝜑 → ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) ∈ ℂ)
903, 18mulcld 11312 . . . . . . . . 9 (𝜑 → (𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) ∈ ℂ)
9182, 17mulcld 11312 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶)) ∈ ℂ)
9288, 89, 90, 91addsubeq4d 11700 . . . . . . . 8 (𝜑 → (((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) ↔ ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) − (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶)))))
9387, 92mpbid 232 . . . . . . 7 (𝜑 → ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) − (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
9423, 93eqtrd 2780 . . . . . 6 (𝜑 → (𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
9518, 22subcld 11649 . . . . . . 7 (𝜑 → ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ∈ ℂ)
9689, 91subcld 11649 . . . . . . 7 (𝜑 → (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) ∈ ℂ)
9711, 17mulcld 11312 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℂ)
98 reim0b 15170 . . . . . . . . . . . . . 14 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℂ → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = 0))
9997, 98syl 17 . . . . . . . . . . . . 13 (𝜑 → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = 0))
10099necon3bbid 2984 . . . . . . . . . . . 12 (𝜑 → (¬ ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ 0))
10132, 100mpbird 257 . . . . . . . . . . 11 (𝜑 → ¬ ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
102 cjreb 15174 . . . . . . . . . . . . 13 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℂ → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((∗‘(𝐵𝐴)) · (𝐷𝐶))))
10397, 102syl 17 . . . . . . . . . . . 12 (𝜑 → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((∗‘(𝐵𝐴)) · (𝐷𝐶))))
104103necon3bbid 2984 . . . . . . . . . . 11 (𝜑 → (¬ ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ ((∗‘(𝐵𝐴)) · (𝐷𝐶))))
105101, 104mpbid 232 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ ((∗‘(𝐵𝐴)) · (𝐷𝐶)))
10611, 17cjmuld 15272 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((∗‘(∗‘(𝐵𝐴))) · (∗‘(𝐷𝐶))))
10710cjcjd 15250 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘(𝐵𝐴))) = (𝐵𝐴))
108107, 19oveq12d 7468 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘(𝐵𝐴))) · (∗‘(𝐷𝐶))) = ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))
109106, 108eqtrd 2780 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))
1109oveq1d 7465 . . . . . . . . . 10 (𝜑 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) = (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)))
111105, 109, 1103netr3d 3023 . . . . . . . . 9 (𝜑 → ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))) ≠ (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)))
112111necomd 3002 . . . . . . . 8 (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) ≠ ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))
11318, 22, 112subne0d 11658 . . . . . . 7 (𝜑 → ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ≠ 0)
1143, 95, 96, 113ldiv 12130 . . . . . 6 (𝜑 → ((𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) ↔ 𝑇 = ((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))))))
11594, 114mpbid 232 . . . . 5 (𝜑𝑇 = ((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))))
116115oveq1d 7465 . . . 4 (𝜑 → (𝑇 · (𝐵𝐴)) = (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴)))
117116oveq2d 7466 . . 3 (𝜑 → (𝐴 + (𝑇 · (𝐵𝐴))) = (𝐴 + (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴))))
1181, 117eqtrd 2780 . 2 (𝜑𝑋 = (𝐴 + (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴))))
119 constrrtll.n . 2 𝑁 = (𝐴 + (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴)))
120118, 119eqtr4di 2798 1 (𝜑𝑋 = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1537  wcel 2108  wne 2946  wss 3976  cfv 6575  (class class class)co 7450  cc 11184  cr 11185  0cc0 11186   + caddc 11189   · cmul 11191  cmin 11522   / cdiv 11949  ccj 15147  cim 15149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772  ax-resscn 11243  ax-1cn 11244  ax-icn 11245  ax-addcl 11246  ax-addrcl 11247  ax-mulcl 11248  ax-mulrcl 11249  ax-mulcom 11250  ax-addass 11251  ax-mulass 11252  ax-distr 11253  ax-i2m1 11254  ax-1ne0 11255  ax-1rid 11256  ax-rnegex 11257  ax-rrecex 11258  ax-cnre 11259  ax-pre-lttri 11260  ax-pre-lttrn 11261  ax-pre-ltadd 11262  ax-pre-mulgt0 11263
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-riota 7406  df-ov 7453  df-oprab 7454  df-mpo 7455  df-er 8765  df-en 9006  df-dom 9007  df-sdom 9008  df-pnf 11328  df-mnf 11329  df-xr 11330  df-ltxr 11331  df-le 11332  df-sub 11524  df-neg 11525  df-div 11950  df-2 12358  df-cj 15150  df-re 15151  df-im 15152
This theorem is referenced by:  constrfin  33738  constrelextdg2  33739
  Copyright terms: Public domain W3C validator