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 34247

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 14211	. . 3 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
3		constrrtcc.m	. . . . 5 ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
4		constrrtcc.5	. . . . . . . . 9 ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
5		constrrtcc.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		constrrtcc.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ 𝑆)
7	5, 6	sseldd 3932	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
8		constrrtcc.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
9	5, 8	sseldd 3932	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
10	7, 9	subcld 11596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ)
11	10	cjcld 15286	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
12	10, 11	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) ∈ ℂ)
13	4, 12	eqeltrid 2864	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℂ)
14		constrrtcc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑆)
15	5, 14	sseldd 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
16	15	cjcld 15286	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
17		constrrtcc.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	5, 17	sseldd 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
19	15, 18	addcld 11255	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
20	16, 19	mulcld 11256	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
21	13, 20	subcld 11596	. . . . . . 7 ⊢ (𝜑 → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) ∈ ℂ)
22		constrrtcc.4	. . . . . . . . 9 ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
23		constrrtcc.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
24	5, 23	sseldd 3932	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
25		constrrtcc.c	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
26	5, 25	sseldd 3932	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
27	24, 26	subcld 11596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
28	27	cjcld 15286	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
29	27, 28	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) ∈ ℂ)
30	22, 29	eqeltrid 2864	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
31	18	cjcld 15286	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
32	31, 19	mulcld 11256	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
33	30, 32	subcld 11596	. . . . . . 7 ⊢ (𝜑 → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) ∈ ℂ)
34	21, 33	subcld 11596	. . . . . 6 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) ∈ ℂ)
35	16, 31	subcld 11596	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ∈ ℂ)
36	15, 18	cjsubd 33216	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
37	15, 18	subcld 11596	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
38		constrrtcc.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
39	38	necomd 3010	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐴)
40	15, 18, 39	subne0d 11606	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0)
41	37, 40	cjne0d 15293	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0)
42	36, 41	eqnetrrd 3023	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ≠ 0)
43	34, 35, 42	divcld 12018	. . . . 5 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
44	3, 43	eqeltrid 2864	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℂ)
45	44, 1	mulcld 11256	. . 3 ⊢ (𝜑 → (𝑀 · 𝑋) ∈ ℂ)
46		constrrtcc.n	. . . 4 ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
47	15, 18	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
48	31, 47	mulcld 11256	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
49	30, 15	mulcld 11256	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · 𝐷) ∈ ℂ)
50	48, 49	subcld 11596	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) ∈ ℂ)
51	16, 47	mulcld 11256	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
52	13, 18	mulcld 11256	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · 𝐴) ∈ ℂ)
53	51, 52	subcld 11596	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) ∈ ℂ)
54	50, 53	subcld 11596	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ∈ ℂ)
55	54, 35, 42	divcld 12018	. . . . 5 ⊢ (𝜑 → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
56	55	negcld 11583	. . . 4 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
57	46, 56	eqeltrid 2864	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℂ)
58	2, 45, 57	addassd 11258	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)))
59	35, 2	mulcld 11256	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) ∈ ℂ)
60	34, 1	mulcld 11256	. . . . . . 7 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) ∈ ℂ)
61	16, 31, 2	subdird 11698	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))))
62	21, 33, 1	subdird 11698	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
63	61, 62	oveq12d 7432	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
64	16, 2	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋↑2)) ∈ ℂ)
65	21, 1	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
66	31, 2	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋↑2)) ∈ ℂ)
67	33, 1	mulcld 11256	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
68	64, 65, 66, 67	addsub4d 11643	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
69	1, 18	subcld 11596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ)
70	1, 15	subcld 11596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ)
71	69, 70	mulcomd 11257	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = ((𝑋 − 𝐷) · (𝑋 − 𝐴)))
72	71	oveq2d 7430	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
73	69	cjcld 15286	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) ∈ ℂ)
74		constrrtcc.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
75		constrrtcclem.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
76	24, 26, 75	subne0d 11606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
77	27, 76	absne0d 15540	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ≠ 0)
78	74, 77	eqnetrd 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) ≠ 0)
79	69	abs00ad 15380	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) = 0 ↔ (𝑋 − 𝐴) = 0))
80	79	necon3bid 2999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) ≠ 0 ↔ (𝑋 − 𝐴) ≠ 0))
81	78, 80	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐴) ≠ 0)
82	74	oveq1d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((abs‘(𝐵 − 𝐶))↑2))
83	69	absvalsqd 15535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))))
84	27	absvalsqd 15535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
85	82, 83, 84	3eqtr3d 2803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
86	85, 22	eqtr4di 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = 𝑃)
87	69, 73, 81, 86	mvllmuld 12074	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = (𝑃 / (𝑋 − 𝐴)))
88	87, 73	eqeltrrd 2861	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 / (𝑋 − 𝐴)) ∈ ℂ)
89	31, 88	addcld 11255	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) ∈ ℂ)
90	89, 69, 70	mulassd 11259	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
91	30, 69, 81	divcan1d 12019	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴)) = 𝑃)
92	91	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) + ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴))) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
93	31, 69, 88, 92	joinlmuladdmuld 11263	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
94	93	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)))
95	31, 69	mulcld 11256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 − 𝐴)) ∈ ℂ)
96	95, 30, 70	adddird 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))))
97	31, 69, 70	mulassd 11259	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
98	1, 18, 1, 15	mulsubd 11700	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
99	1	sqvald 14210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑋↑2) = (𝑋 · 𝑋))
100	99	oveq1d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋↑2) + (𝐷 · 𝐴)) = ((𝑋 · 𝑋) + (𝐷 · 𝐴)))
101	1, 15, 18	adddid 11260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) = ((𝑋 · 𝐷) + (𝑋 · 𝐴)))
102	100, 101	oveq12d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
103	1, 19	mulcld 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) ∈ ℂ)
104	2, 47, 103	addsubd 11617	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
105	98, 102, 104	3eqtr2d 2801	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
106	105	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
107	2, 103	subcld 11596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) ∈ ℂ)
108	31, 107, 47	adddid 11260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
109	97, 106, 108	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
110	30, 1, 15	subdid 11697	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 · (𝑋 − 𝐷)) = ((𝑃 · 𝑋) − (𝑃 · 𝐷)))
111	109, 110	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
112	94, 96, 111	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
113	1, 18	cjsubd 33216	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = ((∗‘𝑋) − (∗‘𝐴)))
114	113, 87	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)))
115	1	cjcld 15286	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝑋) ∈ ℂ)
116	115, 31, 88	subaddd 11614	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)) ↔ ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋)))
117	114, 116	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋))
118	117	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
119	90, 112, 118	3eqtr3rd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
120	31, 107	mulcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
121	120, 48	addcld 11255	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) ∈ ℂ)
122	30, 1	mulcld 11256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · 𝑋) ∈ ℂ)
123	121, 122, 49	addsubassd 11616	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
124	120, 48, 122	add32d 11465	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))))
125	124	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
126	119, 123, 125	3eqtr2d 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
127	120, 122	addcld 11255	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) ∈ ℂ)
128	127, 48, 49	addsubassd 11616	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
129	32, 1	mulcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
130	66, 129, 122	subadd23d 11618	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
131	31, 2, 103	subdid 11697	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))))
132	31, 1, 19	mul12d 11446	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))))
133	1, 32	mulcomd 11257	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
134	132, 133	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
135	134	oveq2d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
136	131, 135	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
137	136	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)))
138	30, 32, 1	subdird 11698	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) = ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
139	138	oveq2d 7430	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
140	130, 137, 139	3eqtr4d 2805	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
141	140	oveq1d 7429	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
142	126, 128, 141	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
143	70	cjcld 15286	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) ∈ ℂ)
144		constrrtcc.3	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
145		constrrtcclem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ≠ 𝐹)
146	7, 9, 145	subne0d 11606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 − 𝐹) ≠ 0)
147	10, 146	absne0d 15540	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐸 − 𝐹)) ≠ 0)
148	144, 147	eqnetrd 3022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) ≠ 0)
149	70	abs00ad 15380	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) = 0 ↔ (𝑋 − 𝐷) = 0))
150	149	necon3bid 2999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) ≠ 0 ↔ (𝑋 − 𝐷) ≠ 0))
151	148, 150	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐷) ≠ 0)
152	144	oveq1d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((abs‘(𝐸 − 𝐹))↑2))
153	70	absvalsqd 15535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))))
154	10	absvalsqd 15535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
155	152, 153, 154	3eqtr3d 2803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
156	155, 4	eqtr4di 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = 𝑄)
157	70, 143, 151, 156	mvllmuld 12074	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = (𝑄 / (𝑋 − 𝐷)))
158	157, 143	eqeltrrd 2861	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 / (𝑋 − 𝐷)) ∈ ℂ)
159	16, 158	addcld 11255	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) ∈ ℂ)
160	159, 70, 69	mulassd 11259	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
161	13, 70, 151	divcan1d 12019	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷)) = 𝑄)
162	161	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) + ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷))) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
163	16, 70, 158, 162	joinlmuladdmuld 11263	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
164	163	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)))
165	16, 70	mulcld 11256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 − 𝐷)) ∈ ℂ)
166	165, 13, 69	adddird 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))))
167	16, 70, 69	mulassd 11259	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
168	71	oveq2d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
169	167, 168	eqtr4d 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
170	105	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
171	16, 107, 47	adddid 11260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
172	169, 170, 171	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
173	13, 1, 18	subdid 11697	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 · (𝑋 − 𝐴)) = ((𝑄 · 𝑋) − (𝑄 · 𝐴)))
174	172, 173	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
175	164, 166, 174	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
176	1, 15	cjsubd 33216	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = ((∗‘𝑋) − (∗‘𝐷)))
177	176, 157	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)))
178	115, 16, 158	subaddd 11614	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)) ↔ ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋)))
179	177, 178	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋))
180	179	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
181	160, 175, 180	3eqtr3rd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
182	16, 107	mulcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
183	182, 51	addcld 11255	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) ∈ ℂ)
184	13, 1	mulcld 11256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
185	183, 184, 52	addsubassd 11616	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
186	182, 51, 184	add32d 11465	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))))
187	186	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
188	181, 185, 187	3eqtr2d 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
189	182, 184	addcld 11255	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) ∈ ℂ)
190	189, 51, 52	addsubassd 11616	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
191	20, 1	mulcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
192	64, 191, 184	subadd23d 11618	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
193	16, 2, 103	subdid 11697	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))))
194	16, 1, 19	mul12d 11446	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))))
195	1, 20	mulcomd 11257	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
196	194, 195	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
197	196	oveq2d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
198	193, 197	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
199	198	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)))
200	13, 20, 1	subdird 11698	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) = ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
201	200	oveq2d 7430	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
202	192, 199, 201	3eqtr4d 2805	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)))
203	202	oveq1d 7429	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
204	188, 190, 203	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
205	72, 142, 204	3eqtr3d 2803	. . . . . . . . 9 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
206	140, 127	eqeltrrd 2861	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
207	202, 189	eqeltrrd 2861	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
208	206, 50, 207, 53	addsubeq4d 11647	. . . . . . . . 9 ⊢ (𝜑 → (((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ↔ ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))))
209	205, 208	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
210	63, 68, 209	3eqtr2d 2801	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
211	59, 60, 210	mvlraddd 11651	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)))
212	35, 2, 42, 211	mvllmuld 12074	. . . . 5 ⊢ (𝜑 → (𝑋↑2) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))))
213	54, 60, 35, 42	divsubdird 12057	. . . . . 6 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
214	46	eqcomi 2769	. . . . . . . . 9 ⊢ -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁
215	214	a1i 11	. . . . . . . 8 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁)
216	55, 215	negcon1ad 11591	. . . . . . 7 ⊢ (𝜑 → -𝑁 = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
217	216	oveq1d 7429	. . . . . 6 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
218	213, 217	eqtr4d 2798	. . . . 5 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
219	34, 1, 35, 42	div23d 12055	. . . . . . 7 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋))
220	3	oveq1i 7424	. . . . . . 7 ⊢ (𝑀 · 𝑋) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋)
221	219, 220	eqtr4di 2813	. . . . . 6 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = (𝑀 · 𝑋))
222	221	oveq2d 7430	. . . . 5 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = (-𝑁 − (𝑀 · 𝑋)))
223	212, 218, 222	3eqtrd 2799	. . . 4 ⊢ (𝜑 → (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋)))
224	216, 55	eqeltrd 2860	. . . . 5 ⊢ (𝜑 → -𝑁 ∈ ℂ)
225	2, 45, 224	addlsub 11657	. . . 4 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁 ↔ (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋))))
226	223, 225	mpbird 260	. . 3 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)
227	2, 45	addcld 11255	. . . 4 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ)
228		addeq0 11664	. . . 4 ⊢ ((((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
229	227, 57, 228	syl2anc 596	. . 3 ⊢ (𝜑 → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
230	226, 229	mpbird 260	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0)
231	58, 230	eqtr3d 2797	1 ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ⊆ wss 3899 ‘cfv 6533 (class class class)co 7414 ℂcc 11125 0cc0 11127 + caddc 11130 · cmul 11132 − cmin 11468 -cneg 11469 / cdiv 11898 2c2 12322 ↑cexp 14128 ∗ccj 15186 abscabs 15324

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-sup 9415 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-rp 13046 df-seq 14069 df-exp 14129 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326

This theorem is used by: constrrtcc 34248

W3C validator