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 33714
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 11314 . . . . . . . 8 (𝜑𝑇 ∈ ℂ)
4 constrrtll.s . . . . . . . . . . . 12 (𝜑𝑆 ⊆ ℂ)
5 constrrtll.b . . . . . . . . . . . 12 (𝜑𝐵𝑆)
64, 5sseldd 4003 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
7 constrrtll.a . . . . . . . . . . . 12 (𝜑𝐴𝑆)
84, 7sseldd 4003 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
96, 8cjsubd 32747 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵𝐴)) = ((∗‘𝐵) − (∗‘𝐴)))
106, 8subcld 11643 . . . . . . . . . . 11 (𝜑 → (𝐵𝐴) ∈ ℂ)
1110cjcld 15241 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵𝐴)) ∈ ℂ)
129, 11eqeltrrd 2839 . . . . . . . . 9 (𝜑 → ((∗‘𝐵) − (∗‘𝐴)) ∈ ℂ)
13 constrrtll.d . . . . . . . . . . 11 (𝜑𝐷𝑆)
144, 13sseldd 4003 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
15 constrrtll.c . . . . . . . . . . 11 (𝜑𝐶𝑆)
164, 15sseldd 4003 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
1714, 16subcld 11643 . . . . . . . . 9 (𝜑 → (𝐷𝐶) ∈ ℂ)
1812, 17mulcld 11306 . . . . . . . 8 (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) ∈ ℂ)
1914, 16cjsubd 32747 . . . . . . . . . 10 (𝜑 → (∗‘(𝐷𝐶)) = ((∗‘𝐷) − (∗‘𝐶)))
2017cjcld 15241 . . . . . . . . . 10 (𝜑 → (∗‘(𝐷𝐶)) ∈ ℂ)
2119, 20eqeltrrd 2839 . . . . . . . . 9 (𝜑 → ((∗‘𝐷) − (∗‘𝐶)) ∈ ℂ)
2210, 21mulcld 11306 . . . . . . . 8 (𝜑 → ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))) ∈ ℂ)
233, 18, 22subdid 11742 . . . . . . 7 (𝜑 → (𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) − (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))))
241oveq1d 7460 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐶) = ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶))
25 constrrtll.r . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ ℝ)
2625recnd 11314 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ ℂ)
2726, 17mulcld 11306 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝐷𝐶)) ∈ ℂ)
28 constrrtll.2 . . . . . . . . . . . . . 14 (𝜑𝑋 = (𝐶 + (𝑅 · (𝐷𝐶))))
2916, 27, 28mvrladdd 11699 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐶) = (𝑅 · (𝐷𝐶)))
3024, 29eqtr3d 2776 . . . . . . . . . . . 12 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = (𝑅 · (𝐷𝐶)))
3130, 27eqeltrd 2838 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) ∈ ℂ)
32 constrrtll.3 . . . . . . . . . . . . . . 15 (𝜑 → (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ 0)
33 fveq2 6919 . . . . . . . . . . . . . . . . 17 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) = 0 → (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = (ℑ‘0))
34 im0 15198 . . . . . . . . . . . . . . . . 17 (ℑ‘0) = 0
3533, 34eqtrdi 2790 . . . . . . . . . . . . . . . 16 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) = 0 → (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = 0)
3635necon3i 2975 . . . . . . . . . . . . . . 15 ((ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ 0 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ≠ 0)
3732, 36syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ≠ 0)
3811, 17, 37mulne0bbd 11942 . . . . . . . . . . . . 13 (𝜑 → (𝐷𝐶) ≠ 0)
3931, 26, 17, 38divmul3d 12100 . . . . . . . . . . . 12 (𝜑 → ((((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = 𝑅 ↔ ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = (𝑅 · (𝐷𝐶))))
4030, 39mpbird 257 . . . . . . . . . . 11 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = 𝑅)
4140fveq2d 6923 . . . . . . . . . . . 12 (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶))) = (∗‘𝑅))
4231, 17, 38cjdivd 15268 . . . . . . . . . . . . 13 (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶))) = ((∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) / (∗‘(𝐷𝐶))))
433, 10mulcld 11306 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 · (𝐵𝐴)) ∈ ℂ)
448, 43addcld 11305 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 + (𝑇 · (𝐵𝐴))) ∈ ℂ)
4544, 16cjsubd 32747 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) = ((∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) − (∗‘𝐶)))
468, 43cjaddd 15265 . . . . . . . . . . . . . . . . 17 (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (∗‘(𝑇 · (𝐵𝐴)))))
473, 10cjmuld 15266 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∗‘(𝑇 · (𝐵𝐴))) = ((∗‘𝑇) · (∗‘(𝐵𝐴))))
482cjred 15271 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗‘𝑇) = 𝑇)
4948, 9oveq12d 7463 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((∗‘𝑇) · (∗‘(𝐵𝐴))) = (𝑇 · ((∗‘𝐵) − (∗‘𝐴))))
5047, 49eqtrd 2774 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝑇 · (𝐵𝐴))) = (𝑇 · ((∗‘𝐵) − (∗‘𝐴))))
5150oveq2d 7461 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∗‘𝐴) + (∗‘(𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))))
5246, 51eqtrd 2774 . . . . . . . . . . . . . . . 16 (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) = ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))))
5352oveq1d 7460 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘(𝐴 + (𝑇 · (𝐵𝐴)))) − (∗‘𝐶)) = (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)))
5445, 53eqtrd 2774 . . . . . . . . . . . . . 14 (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) = (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)))
5554, 19oveq12d 7463 . . . . . . . . . . . . 13 (𝜑 → ((∗‘((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶)) / (∗‘(𝐷𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
5642, 55eqtrd 2774 . . . . . . . . . . . 12 (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
5725cjred 15271 . . . . . . . . . . . 12 (𝜑 → (∗‘𝑅) = 𝑅)
5841, 56, 573eqtr3rd 2783 . . . . . . . . . . 11 (𝜑𝑅 = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
5940, 58eqtrd 2774 . . . . . . . . . 10 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))))
608cjcld 15241 . . . . . . . . . . . . 13 (𝜑 → (∗‘𝐴) ∈ ℂ)
613, 12mulcld 11306 . . . . . . . . . . . . 13 (𝜑 → (𝑇 · ((∗‘𝐵) − (∗‘𝐴))) ∈ ℂ)
6260, 61addcld 11305 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) ∈ ℂ)
6316cjcld 15241 . . . . . . . . . . . 12 (𝜑 → (∗‘𝐶) ∈ ℂ)
6462, 63subcld 11643 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) ∈ ℂ)
6517, 38cjne0d 15248 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐷𝐶)) ≠ 0)
6619, 65eqnetrrd 3011 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐷) − (∗‘𝐶)) ≠ 0)
6731, 17, 64, 21, 38, 66divmuleqd 12112 . . . . . . . . . 10 (𝜑 → ((((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) / (𝐷𝐶)) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))) ↔ (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶))))
6859, 67mpbid 232 . . . . . . . . 9 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶)))
698, 43, 16addsubassd 11663 . . . . . . . . . . . 12 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = (𝐴 + ((𝑇 · (𝐵𝐴)) − 𝐶)))
7043, 8, 16addsub12d 11666 . . . . . . . . . . . 12 (𝜑 → ((𝑇 · (𝐵𝐴)) + (𝐴𝐶)) = (𝐴 + ((𝑇 · (𝐵𝐴)) − 𝐶)))
7169, 70eqtr4d 2777 . . . . . . . . . . 11 (𝜑 → ((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) = ((𝑇 · (𝐵𝐴)) + (𝐴𝐶)))
7271oveq1d 7460 . . . . . . . . . 10 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = (((𝑇 · (𝐵𝐴)) + (𝐴𝐶)) · ((∗‘𝐷) − (∗‘𝐶))))
738, 16subcld 11643 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶) ∈ ℂ)
7443, 73, 21adddird 11311 . . . . . . . . . 10 (𝜑 → (((𝑇 · (𝐵𝐴)) + (𝐴𝐶)) · ((∗‘𝐷) − (∗‘𝐶))) = (((𝑇 · (𝐵𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))))
753, 10, 21mulassd 11309 . . . . . . . . . . 11 (𝜑 → ((𝑇 · (𝐵𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) = (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))))
7675oveq1d 7460 . . . . . . . . . 10 (𝜑 → (((𝑇 · (𝐵𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))))
7772, 74, 763eqtrd 2778 . . . . . . . . 9 (𝜑 → (((𝐴 + (𝑇 · (𝐵𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))))
7860, 61, 63addsubassd 11663 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) = ((∗‘𝐴) + ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) − (∗‘𝐶))))
7961, 60, 63addsub12d 11666 . . . . . . . . . . . 12 (𝜑 → ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) = ((∗‘𝐴) + ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) − (∗‘𝐶))))
8078, 79eqtr4d 2777 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) = ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))))
8180oveq1d 7460 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶)) = (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) · (𝐷𝐶)))
8260, 63subcld 11643 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) − (∗‘𝐶)) ∈ ℂ)
8361, 82, 17adddird 11311 . . . . . . . . . 10 (𝜑 → (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) · (𝐷𝐶)) = (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷𝐶)) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
843, 12, 17mulassd 11309 . . . . . . . . . . 11 (𝜑 → ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷𝐶)) = (𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))))
8584oveq1d 7460 . . . . . . . . . 10 (𝜑 → (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷𝐶)) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
8681, 83, 853eqtrd 2778 . . . . . . . . 9 (𝜑 → ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷𝐶)) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
8768, 77, 863eqtr3d 2782 . . . . . . . 8 (𝜑 → ((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
883, 22mulcld 11306 . . . . . . . . 9 (𝜑 → (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ∈ ℂ)
8973, 21mulcld 11306 . . . . . . . . 9 (𝜑 → ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) ∈ ℂ)
903, 18mulcld 11306 . . . . . . . . 9 (𝜑 → (𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) ∈ ℂ)
9182, 17mulcld 11306 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶)) ∈ ℂ)
9288, 89, 90, 91addsubeq4d 11694 . . . . . . . 8 (𝜑 → (((𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) ↔ ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) − (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶)))))
9387, 92mpbid 232 . . . . . . 7 (𝜑 → ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶))) − (𝑇 · ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
9423, 93eqtrd 2774 . . . . . 6 (𝜑 → (𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))))
9518, 22subcld 11643 . . . . . . 7 (𝜑 → ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ∈ ℂ)
9689, 91subcld 11643 . . . . . . 7 (𝜑 → (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) ∈ ℂ)
9711, 17mulcld 11306 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℂ)
98 reim0b 15164 . . . . . . . . . . . . . 14 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℂ → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = 0))
9997, 98syl 17 . . . . . . . . . . . . 13 (𝜑 → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = 0))
10099necon3bbid 2980 . . . . . . . . . . . 12 (𝜑 → (¬ ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (ℑ‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ 0))
10132, 100mpbird 257 . . . . . . . . . . 11 (𝜑 → ¬ ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
102 cjreb 15168 . . . . . . . . . . . . 13 (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℂ → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((∗‘(𝐵𝐴)) · (𝐷𝐶))))
10397, 102syl 17 . . . . . . . . . . . 12 (𝜑 → (((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((∗‘(𝐵𝐴)) · (𝐷𝐶))))
104103necon3bbid 2980 . . . . . . . . . . 11 (𝜑 → (¬ ((∗‘(𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ ↔ (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ ((∗‘(𝐵𝐴)) · (𝐷𝐶))))
105101, 104mpbid 232 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) ≠ ((∗‘(𝐵𝐴)) · (𝐷𝐶)))
10611, 17cjmuld 15266 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((∗‘(∗‘(𝐵𝐴))) · (∗‘(𝐷𝐶))))
10710cjcjd 15244 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘(𝐵𝐴))) = (𝐵𝐴))
108107, 19oveq12d 7463 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘(𝐵𝐴))) · (∗‘(𝐷𝐶))) = ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))
109106, 108eqtrd 2774 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘(𝐵𝐴)) · (𝐷𝐶))) = ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))
1109oveq1d 7460 . . . . . . . . . 10 (𝜑 → ((∗‘(𝐵𝐴)) · (𝐷𝐶)) = (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)))
111105, 109, 1103netr3d 3019 . . . . . . . . 9 (𝜑 → ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))) ≠ (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)))
112111necomd 2998 . . . . . . . 8 (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) ≠ ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))
11318, 22, 112subne0d 11652 . . . . . . 7 (𝜑 → ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ≠ 0)
1143, 95, 96, 113ldiv 12124 . . . . . 6 (𝜑 → ((𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) ↔ 𝑇 = ((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶)))))))
11594, 114mpbid 232 . . . . 5 (𝜑𝑇 = ((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))))
116115oveq1d 7460 . . . 4 (𝜑 → (𝑇 · (𝐵𝐴)) = (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴)))
117116oveq2d 7461 . . 3 (𝜑 → (𝐴 + (𝑇 · (𝐵𝐴))) = (𝐴 + (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴))))
1181, 117eqtrd 2774 . 2 (𝜑𝑋 = (𝐴 + (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴))))
119 constrrtll.n . 2 𝑁 = (𝐴 + (((((𝐴𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷𝐶)) − ((𝐵𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵𝐴)))
120118, 119eqtr4di 2792 1 (𝜑𝑋 = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1537  wcel 2103  wne 2942  wss 3970  cfv 6572  (class class class)co 7445  cc 11178  cr 11179  0cc0 11180   + caddc 11183   · cmul 11185  cmin 11516   / cdiv 11943  ccj 15141  cim 15143
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 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766  ax-resscn 11237  ax-1cn 11238  ax-icn 11239  ax-addcl 11240  ax-addrcl 11241  ax-mulcl 11242  ax-mulrcl 11243  ax-mulcom 11244  ax-addass 11245  ax-mulass 11246  ax-distr 11247  ax-i2m1 11248  ax-1ne0 11249  ax-1rid 11250  ax-rnegex 11251  ax-rrecex 11252  ax-cnre 11253  ax-pre-lttri 11254  ax-pre-lttrn 11255  ax-pre-ltadd 11256  ax-pre-mulgt0 11257
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 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-po 5611  df-so 5612  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-riota 7401  df-ov 7448  df-oprab 7449  df-mpo 7450  df-er 8759  df-en 9000  df-dom 9001  df-sdom 9002  df-pnf 11322  df-mnf 11323  df-xr 11324  df-ltxr 11325  df-le 11326  df-sub 11518  df-neg 11519  df-div 11944  df-2 12352  df-cj 15144  df-re 15145  df-im 15146
This theorem is referenced by:  constrfin  33728  constrelextdg2  33729
  Copyright terms: Public domain W3C validator