constrrtcclem - Mathbox for Thierry Arnoux

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

Theorem constrrtcclem 33897

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

**Hypotheses**
Ref	Expression
constrrtcc.s	⊢ (𝜑 → 𝑆 ⊆ ℂ)
constrrtcc.a	⊢ (𝜑 → 𝐴 ∈ 𝑆)
constrrtcc.b	⊢ (𝜑 → 𝐵 ∈ 𝑆)
constrrtcc.c	⊢ (𝜑 → 𝐶 ∈ 𝑆)
constrrtcc.d	⊢ (𝜑 → 𝐷 ∈ 𝑆)
constrrtcc.e	⊢ (𝜑 → 𝐸 ∈ 𝑆)
constrrtcc.f	⊢ (𝜑 → 𝐹 ∈ 𝑆)
constrrtcc.x	⊢ (𝜑 → 𝑋 ∈ ℂ)
constrrtcc.1	⊢ (𝜑 → 𝐴 ≠ 𝐷)
constrrtcc.2	⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
constrrtcc.3	⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
constrrtcc.4	⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
constrrtcc.5	⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
constrrtcc.m	⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
constrrtcc.n	⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
constrrtcclem.1	⊢ (𝜑 → 𝐵 ≠ 𝐶)
constrrtcclem.2	⊢ (𝜑 → 𝐸 ≠ 𝐹)

**Assertion**
Ref	Expression
constrrtcclem	⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

**Proof of Theorem constrrtcclem**
Step	Hyp	Ref	Expression
1		constrrtcc.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
2	1	sqcld 14100	. . 3 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
3		constrrtcc.m	. . . . 5 ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
4		constrrtcc.5	. . . . . . . . 9 ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
5		constrrtcc.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		constrrtcc.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ 𝑆)
7	5, 6	sseldd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
8		constrrtcc.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
9	5, 8	sseldd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
10	7, 9	subcld 11499	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ)
11	10	cjcld 15152	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
12	10, 11	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) ∈ ℂ)
13	4, 12	eqeltrid 2841	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℂ)
14		constrrtcc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑆)
15	5, 14	sseldd 3923	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
16	15	cjcld 15152	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
17		constrrtcc.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	5, 17	sseldd 3923	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
19	15, 18	addcld 11158	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
20	16, 19	mulcld 11159	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
21	13, 20	subcld 11499	. . . . . . 7 ⊢ (𝜑 → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) ∈ ℂ)
22		constrrtcc.4	. . . . . . . . 9 ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
23		constrrtcc.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
24	5, 23	sseldd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
25		constrrtcc.c	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
26	5, 25	sseldd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
27	24, 26	subcld 11499	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
28	27	cjcld 15152	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
29	27, 28	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) ∈ ℂ)
30	22, 29	eqeltrid 2841	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
31	18	cjcld 15152	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
32	31, 19	mulcld 11159	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
33	30, 32	subcld 11499	. . . . . . 7 ⊢ (𝜑 → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) ∈ ℂ)
34	21, 33	subcld 11499	. . . . . 6 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) ∈ ℂ)
35	16, 31	subcld 11499	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ∈ ℂ)
36	15, 18	cjsubd 32833	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
37	15, 18	subcld 11499	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
38		constrrtcc.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
39	38	necomd 2988	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐴)
40	15, 18, 39	subne0d 11508	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0)
41	37, 40	cjne0d 15159	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0)
42	36, 41	eqnetrrd 3001	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ≠ 0)
43	34, 35, 42	divcld 11925	. . . . 5 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
44	3, 43	eqeltrid 2841	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℂ)
45	44, 1	mulcld 11159	. . 3 ⊢ (𝜑 → (𝑀 · 𝑋) ∈ ℂ)
46		constrrtcc.n	. . . 4 ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
47	15, 18	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
48	31, 47	mulcld 11159	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
49	30, 15	mulcld 11159	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · 𝐷) ∈ ℂ)
50	48, 49	subcld 11499	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) ∈ ℂ)
51	16, 47	mulcld 11159	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
52	13, 18	mulcld 11159	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · 𝐴) ∈ ℂ)
53	51, 52	subcld 11499	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) ∈ ℂ)
54	50, 53	subcld 11499	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ∈ ℂ)
55	54, 35, 42	divcld 11925	. . . . 5 ⊢ (𝜑 → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
56	55	negcld 11486	. . . 4 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
57	46, 56	eqeltrid 2841	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℂ)
58	2, 45, 57	addassd 11161	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)))
59	35, 2	mulcld 11159	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) ∈ ℂ)
60	34, 1	mulcld 11159	. . . . . . 7 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) ∈ ℂ)
61	16, 31, 2	subdird 11601	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))))
62	21, 33, 1	subdird 11601	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
63	61, 62	oveq12d 7379	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
64	16, 2	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋↑2)) ∈ ℂ)
65	21, 1	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
66	31, 2	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋↑2)) ∈ ℂ)
67	33, 1	mulcld 11159	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
68	64, 65, 66, 67	addsub4d 11546	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
69	1, 18	subcld 11499	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ)
70	1, 15	subcld 11499	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ)
71	69, 70	mulcomd 11160	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = ((𝑋 − 𝐷) · (𝑋 − 𝐴)))
72	71	oveq2d 7377	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
73	69	cjcld 15152	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) ∈ ℂ)
74		constrrtcc.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
75		constrrtcclem.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
76	24, 26, 75	subne0d 11508	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
77	27, 76	absne0d 15406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ≠ 0)
78	74, 77	eqnetrd 3000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) ≠ 0)
79	69	abs00ad 15246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) = 0 ↔ (𝑋 − 𝐴) = 0))
80	79	necon3bid 2977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) ≠ 0 ↔ (𝑋 − 𝐴) ≠ 0))
81	78, 80	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐴) ≠ 0)
82	74	oveq1d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((abs‘(𝐵 − 𝐶))↑2))
83	69	absvalsqd 15401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))))
84	27	absvalsqd 15401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
85	82, 83, 84	3eqtr3d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
86	85, 22	eqtr4di 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = 𝑃)
87	69, 73, 81, 86	mvllmuld 11981	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = (𝑃 / (𝑋 − 𝐴)))
88	87, 73	eqeltrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 / (𝑋 − 𝐴)) ∈ ℂ)
89	31, 88	addcld 11158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) ∈ ℂ)
90	89, 69, 70	mulassd 11162	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
91	30, 69, 81	divcan1d 11926	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴)) = 𝑃)
92	91	oveq2d 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) + ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴))) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
93	31, 69, 88, 92	joinlmuladdmuld 11166	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
94	93	oveq1d 7376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)))
95	31, 69	mulcld 11159	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 − 𝐴)) ∈ ℂ)
96	95, 30, 70	adddird 11164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))))
97	31, 69, 70	mulassd 11162	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
98	1, 18, 1, 15	mulsubd 11603	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
99	1	sqvald 14099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑋↑2) = (𝑋 · 𝑋))
100	99	oveq1d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋↑2) + (𝐷 · 𝐴)) = ((𝑋 · 𝑋) + (𝐷 · 𝐴)))
101	1, 15, 18	adddid 11163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) = ((𝑋 · 𝐷) + (𝑋 · 𝐴)))
102	100, 101	oveq12d 7379	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
103	1, 19	mulcld 11159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) ∈ ℂ)
104	2, 47, 103	addsubd 11520	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
105	98, 102, 104	3eqtr2d 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
106	105	oveq2d 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
107	2, 103	subcld 11499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) ∈ ℂ)
108	31, 107, 47	adddid 11163	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
109	97, 106, 108	3eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
110	30, 1, 15	subdid 11600	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 · (𝑋 − 𝐷)) = ((𝑃 · 𝑋) − (𝑃 · 𝐷)))
111	109, 110	oveq12d 7379	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
112	94, 96, 111	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
113	1, 18	cjsubd 32833	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = ((∗‘𝑋) − (∗‘𝐴)))
114	113, 87	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)))
115	1	cjcld 15152	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝑋) ∈ ℂ)
116	115, 31, 88	subaddd 11517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)) ↔ ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋)))
117	114, 116	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋))
118	117	oveq1d 7376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
119	90, 112, 118	3eqtr3rd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
120	31, 107	mulcld 11159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
121	120, 48	addcld 11158	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) ∈ ℂ)
122	30, 1	mulcld 11159	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · 𝑋) ∈ ℂ)
123	121, 122, 49	addsubassd 11519	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
124	120, 48, 122	add32d 11368	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))))
125	124	oveq1d 7376	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
126	119, 123, 125	3eqtr2d 2778	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
127	120, 122	addcld 11158	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) ∈ ℂ)
128	127, 48, 49	addsubassd 11519	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
129	32, 1	mulcld 11159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
130	66, 129, 122	subadd23d 11521	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
131	31, 2, 103	subdid 11600	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))))
132	31, 1, 19	mul12d 11349	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))))
133	1, 32	mulcomd 11160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
134	132, 133	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
135	134	oveq2d 7377	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
136	131, 135	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
137	136	oveq1d 7376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)))
138	30, 32, 1	subdird 11601	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) = ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
139	138	oveq2d 7377	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
140	130, 137, 139	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
141	140	oveq1d 7376	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
142	126, 128, 141	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
143	70	cjcld 15152	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) ∈ ℂ)
144		constrrtcc.3	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
145		constrrtcclem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ≠ 𝐹)
146	7, 9, 145	subne0d 11508	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 − 𝐹) ≠ 0)
147	10, 146	absne0d 15406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐸 − 𝐹)) ≠ 0)
148	144, 147	eqnetrd 3000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) ≠ 0)
149	70	abs00ad 15246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) = 0 ↔ (𝑋 − 𝐷) = 0))
150	149	necon3bid 2977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) ≠ 0 ↔ (𝑋 − 𝐷) ≠ 0))
151	148, 150	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐷) ≠ 0)
152	144	oveq1d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((abs‘(𝐸 − 𝐹))↑2))
153	70	absvalsqd 15401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))))
154	10	absvalsqd 15401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
155	152, 153, 154	3eqtr3d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
156	155, 4	eqtr4di 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = 𝑄)
157	70, 143, 151, 156	mvllmuld 11981	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = (𝑄 / (𝑋 − 𝐷)))
158	157, 143	eqeltrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 / (𝑋 − 𝐷)) ∈ ℂ)
159	16, 158	addcld 11158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) ∈ ℂ)
160	159, 70, 69	mulassd 11162	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
161	13, 70, 151	divcan1d 11926	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷)) = 𝑄)
162	161	oveq2d 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) + ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷))) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
163	16, 70, 158, 162	joinlmuladdmuld 11166	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
164	163	oveq1d 7376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)))
165	16, 70	mulcld 11159	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 − 𝐷)) ∈ ℂ)
166	165, 13, 69	adddird 11164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))))
167	16, 70, 69	mulassd 11162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
168	71	oveq2d 7377	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
169	167, 168	eqtr4d 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
170	105	oveq2d 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
171	16, 107, 47	adddid 11163	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
172	169, 170, 171	3eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
173	13, 1, 18	subdid 11600	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 · (𝑋 − 𝐴)) = ((𝑄 · 𝑋) − (𝑄 · 𝐴)))
174	172, 173	oveq12d 7379	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
175	164, 166, 174	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
176	1, 15	cjsubd 32833	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = ((∗‘𝑋) − (∗‘𝐷)))
177	176, 157	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)))
178	115, 16, 158	subaddd 11517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)) ↔ ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋)))
179	177, 178	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋))
180	179	oveq1d 7376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
181	160, 175, 180	3eqtr3rd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
182	16, 107	mulcld 11159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
183	182, 51	addcld 11158	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) ∈ ℂ)
184	13, 1	mulcld 11159	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
185	183, 184, 52	addsubassd 11519	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
186	182, 51, 184	add32d 11368	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))))
187	186	oveq1d 7376	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
188	181, 185, 187	3eqtr2d 2778	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
189	182, 184	addcld 11158	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) ∈ ℂ)
190	189, 51, 52	addsubassd 11519	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
191	20, 1	mulcld 11159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
192	64, 191, 184	subadd23d 11521	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
193	16, 2, 103	subdid 11600	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))))
194	16, 1, 19	mul12d 11349	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))))
195	1, 20	mulcomd 11160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
196	194, 195	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
197	196	oveq2d 7377	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
198	193, 197	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
199	198	oveq1d 7376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)))
200	13, 20, 1	subdird 11601	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) = ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
201	200	oveq2d 7377	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
202	192, 199, 201	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)))
203	202	oveq1d 7376	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
204	188, 190, 203	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
205	72, 142, 204	3eqtr3d 2780	. . . . . . . . 9 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
206	140, 127	eqeltrrd 2838	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
207	202, 189	eqeltrrd 2838	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
208	206, 50, 207, 53	addsubeq4d 11550	. . . . . . . . 9 ⊢ (𝜑 → (((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ↔ ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))))
209	205, 208	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
210	63, 68, 209	3eqtr2d 2778	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
211	59, 60, 210	mvlraddd 11554	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)))
212	35, 2, 42, 211	mvllmuld 11981	. . . . 5 ⊢ (𝜑 → (𝑋↑2) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))))
213	54, 60, 35, 42	divsubdird 11964	. . . . . 6 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
214	46	eqcomi 2746	. . . . . . . . 9 ⊢ -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁
215	214	a1i 11	. . . . . . . 8 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁)
216	55, 215	negcon1ad 11494	. . . . . . 7 ⊢ (𝜑 → -𝑁 = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
217	216	oveq1d 7376	. . . . . 6 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
218	213, 217	eqtr4d 2775	. . . . 5 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
219	34, 1, 35, 42	div23d 11962	. . . . . . 7 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋))
220	3	oveq1i 7371	. . . . . . 7 ⊢ (𝑀 · 𝑋) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋)
221	219, 220	eqtr4di 2790	. . . . . 6 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = (𝑀 · 𝑋))
222	221	oveq2d 7377	. . . . 5 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = (-𝑁 − (𝑀 · 𝑋)))
223	212, 218, 222	3eqtrd 2776	. . . 4 ⊢ (𝜑 → (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋)))
224	216, 55	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → -𝑁 ∈ ℂ)
225	2, 45, 224	addlsub 11560	. . . 4 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁 ↔ (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋))))
226	223, 225	mpbird 257	. . 3 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)
227	2, 45	addcld 11158	. . . 4 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ)
228		addeq0 11567	. . . 4 ⊢ ((((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
229	227, 57, 228	syl2anc 585	. . 3 ⊢ (𝜑 → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
230	226, 229	mpbird 257	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0)
231	58, 230	eqtr3d 2774	1 ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ⊆ wss 3890 ‘cfv 6493 (class class class)co 7361 ℂcc 11030 0cc0 11032 + caddc 11035 · cmul 11037 − cmin 11371 -cneg 11372 / cdiv 11801 2c2 12230 ↑cexp 14017 ∗ccj 15052 abscabs 15190

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-sup 9349 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-n0 12432 df-z 12519 df-uz 12783 df-rp 12937 df-seq 13958 df-exp 14018 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192

This theorem is referenced by: constrrtcc 33898

W3C validator