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 33773

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 14167	. . 3 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
3		constrrtcc.m	. . . . 5 ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
4		constrrtcc.5	. . . . . . . . 9 ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
5		constrrtcc.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		constrrtcc.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ 𝑆)
7	5, 6	sseldd 3964	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
8		constrrtcc.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
9	5, 8	sseldd 3964	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
10	7, 9	subcld 11599	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ)
11	10	cjcld 15220	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
12	10, 11	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) ∈ ℂ)
13	4, 12	eqeltrid 2839	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℂ)
14		constrrtcc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑆)
15	5, 14	sseldd 3964	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
16	15	cjcld 15220	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
17		constrrtcc.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	5, 17	sseldd 3964	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
19	15, 18	addcld 11259	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
20	16, 19	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
21	13, 20	subcld 11599	. . . . . . 7 ⊢ (𝜑 → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) ∈ ℂ)
22		constrrtcc.4	. . . . . . . . 9 ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
23		constrrtcc.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
24	5, 23	sseldd 3964	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
25		constrrtcc.c	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
26	5, 25	sseldd 3964	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
27	24, 26	subcld 11599	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
28	27	cjcld 15220	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
29	27, 28	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) ∈ ℂ)
30	22, 29	eqeltrid 2839	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
31	18	cjcld 15220	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
32	31, 19	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
33	30, 32	subcld 11599	. . . . . . 7 ⊢ (𝜑 → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) ∈ ℂ)
34	21, 33	subcld 11599	. . . . . 6 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) ∈ ℂ)
35	16, 31	subcld 11599	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ∈ ℂ)
36	15, 18	cjsubd 32725	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
37	15, 18	subcld 11599	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
38		constrrtcc.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
39	38	necomd 2988	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐴)
40	15, 18, 39	subne0d 11608	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0)
41	37, 40	cjne0d 15227	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0)
42	36, 41	eqnetrrd 3001	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ≠ 0)
43	34, 35, 42	divcld 12022	. . . . 5 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
44	3, 43	eqeltrid 2839	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℂ)
45	44, 1	mulcld 11260	. . 3 ⊢ (𝜑 → (𝑀 · 𝑋) ∈ ℂ)
46		constrrtcc.n	. . . 4 ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
47	15, 18	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
48	31, 47	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
49	30, 15	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · 𝐷) ∈ ℂ)
50	48, 49	subcld 11599	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) ∈ ℂ)
51	16, 47	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
52	13, 18	mulcld 11260	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · 𝐴) ∈ ℂ)
53	51, 52	subcld 11599	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) ∈ ℂ)
54	50, 53	subcld 11599	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ∈ ℂ)
55	54, 35, 42	divcld 12022	. . . . 5 ⊢ (𝜑 → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
56	55	negcld 11586	. . . 4 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
57	46, 56	eqeltrid 2839	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℂ)
58	2, 45, 57	addassd 11262	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)))
59	35, 2	mulcld 11260	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) ∈ ℂ)
60	34, 1	mulcld 11260	. . . . . . 7 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) ∈ ℂ)
61	16, 31, 2	subdird 11699	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))))
62	21, 33, 1	subdird 11699	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
63	61, 62	oveq12d 7428	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
64	16, 2	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋↑2)) ∈ ℂ)
65	21, 1	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
66	31, 2	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋↑2)) ∈ ℂ)
67	33, 1	mulcld 11260	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
68	64, 65, 66, 67	addsub4d 11646	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
69	1, 18	subcld 11599	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ)
70	1, 15	subcld 11599	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ)
71	69, 70	mulcomd 11261	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = ((𝑋 − 𝐷) · (𝑋 − 𝐴)))
72	71	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
73	69	cjcld 15220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) ∈ ℂ)
74		constrrtcc.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
75		constrrtcclem.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
76	24, 26, 75	subne0d 11608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
77	27, 76	absne0d 15471	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ≠ 0)
78	74, 77	eqnetrd 3000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) ≠ 0)
79	69	abs00ad 15314	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) = 0 ↔ (𝑋 − 𝐴) = 0))
80	79	necon3bid 2977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) ≠ 0 ↔ (𝑋 − 𝐴) ≠ 0))
81	78, 80	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐴) ≠ 0)
82	74	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((abs‘(𝐵 − 𝐶))↑2))
83	69	absvalsqd 15466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))))
84	27	absvalsqd 15466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
85	82, 83, 84	3eqtr3d 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
86	85, 22	eqtr4di 2789	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = 𝑃)
87	69, 73, 81, 86	mvllmuld 12078	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = (𝑃 / (𝑋 − 𝐴)))
88	87, 73	eqeltrrd 2836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 / (𝑋 − 𝐴)) ∈ ℂ)
89	31, 88	addcld 11259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) ∈ ℂ)
90	89, 69, 70	mulassd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
91	30, 69, 81	divcan1d 12023	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴)) = 𝑃)
92	91	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) + ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴))) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
93	31, 69, 88, 92	joinlmuladdmuld 11267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
94	93	oveq1d 7425	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)))
95	31, 69	mulcld 11260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 − 𝐴)) ∈ ℂ)
96	95, 30, 70	adddird 11265	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))))
97	31, 69, 70	mulassd 11263	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
98	1, 18, 1, 15	mulsubd 11701	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
99	1	sqvald 14166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑋↑2) = (𝑋 · 𝑋))
100	99	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋↑2) + (𝐷 · 𝐴)) = ((𝑋 · 𝑋) + (𝐷 · 𝐴)))
101	1, 15, 18	adddid 11264	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) = ((𝑋 · 𝐷) + (𝑋 · 𝐴)))
102	100, 101	oveq12d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
103	1, 19	mulcld 11260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) ∈ ℂ)
104	2, 47, 103	addsubd 11620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
105	98, 102, 104	3eqtr2d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
106	105	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
107	2, 103	subcld 11599	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) ∈ ℂ)
108	31, 107, 47	adddid 11264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
109	97, 106, 108	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
110	30, 1, 15	subdid 11698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 · (𝑋 − 𝐷)) = ((𝑃 · 𝑋) − (𝑃 · 𝐷)))
111	109, 110	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
112	94, 96, 111	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
113	1, 18	cjsubd 32725	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = ((∗‘𝑋) − (∗‘𝐴)))
114	113, 87	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)))
115	1	cjcld 15220	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝑋) ∈ ℂ)
116	115, 31, 88	subaddd 11617	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)) ↔ ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋)))
117	114, 116	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋))
118	117	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
119	90, 112, 118	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
120	31, 107	mulcld 11260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
121	120, 48	addcld 11259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) ∈ ℂ)
122	30, 1	mulcld 11260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · 𝑋) ∈ ℂ)
123	121, 122, 49	addsubassd 11619	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
124	120, 48, 122	add32d 11468	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))))
125	124	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
126	119, 123, 125	3eqtr2d 2777	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
127	120, 122	addcld 11259	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) ∈ ℂ)
128	127, 48, 49	addsubassd 11619	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
129	32, 1	mulcld 11260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
130	66, 129, 122	subadd23d 11621	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
131	31, 2, 103	subdid 11698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))))
132	31, 1, 19	mul12d 11449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))))
133	1, 32	mulcomd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
134	132, 133	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
135	134	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
136	131, 135	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
137	136	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)))
138	30, 32, 1	subdird 11699	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) = ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
139	138	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
140	130, 137, 139	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
141	140	oveq1d 7425	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
142	126, 128, 141	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
143	70	cjcld 15220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) ∈ ℂ)
144		constrrtcc.3	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
145		constrrtcclem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ≠ 𝐹)
146	7, 9, 145	subne0d 11608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 − 𝐹) ≠ 0)
147	10, 146	absne0d 15471	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐸 − 𝐹)) ≠ 0)
148	144, 147	eqnetrd 3000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) ≠ 0)
149	70	abs00ad 15314	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) = 0 ↔ (𝑋 − 𝐷) = 0))
150	149	necon3bid 2977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) ≠ 0 ↔ (𝑋 − 𝐷) ≠ 0))
151	148, 150	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐷) ≠ 0)
152	144	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((abs‘(𝐸 − 𝐹))↑2))
153	70	absvalsqd 15466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))))
154	10	absvalsqd 15466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
155	152, 153, 154	3eqtr3d 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
156	155, 4	eqtr4di 2789	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = 𝑄)
157	70, 143, 151, 156	mvllmuld 12078	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = (𝑄 / (𝑋 − 𝐷)))
158	157, 143	eqeltrrd 2836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 / (𝑋 − 𝐷)) ∈ ℂ)
159	16, 158	addcld 11259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) ∈ ℂ)
160	159, 70, 69	mulassd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
161	13, 70, 151	divcan1d 12023	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷)) = 𝑄)
162	161	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) + ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷))) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
163	16, 70, 158, 162	joinlmuladdmuld 11267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
164	163	oveq1d 7425	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)))
165	16, 70	mulcld 11260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 − 𝐷)) ∈ ℂ)
166	165, 13, 69	adddird 11265	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))))
167	16, 70, 69	mulassd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
168	71	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
169	167, 168	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
170	105	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
171	16, 107, 47	adddid 11264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
172	169, 170, 171	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
173	13, 1, 18	subdid 11698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 · (𝑋 − 𝐴)) = ((𝑄 · 𝑋) − (𝑄 · 𝐴)))
174	172, 173	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
175	164, 166, 174	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
176	1, 15	cjsubd 32725	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = ((∗‘𝑋) − (∗‘𝐷)))
177	176, 157	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)))
178	115, 16, 158	subaddd 11617	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)) ↔ ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋)))
179	177, 178	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋))
180	179	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
181	160, 175, 180	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
182	16, 107	mulcld 11260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
183	182, 51	addcld 11259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) ∈ ℂ)
184	13, 1	mulcld 11260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
185	183, 184, 52	addsubassd 11619	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
186	182, 51, 184	add32d 11468	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))))
187	186	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
188	181, 185, 187	3eqtr2d 2777	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
189	182, 184	addcld 11259	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) ∈ ℂ)
190	189, 51, 52	addsubassd 11619	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
191	20, 1	mulcld 11260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
192	64, 191, 184	subadd23d 11621	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
193	16, 2, 103	subdid 11698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))))
194	16, 1, 19	mul12d 11449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))))
195	1, 20	mulcomd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
196	194, 195	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
197	196	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
198	193, 197	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
199	198	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)))
200	13, 20, 1	subdird 11699	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) = ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
201	200	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
202	192, 199, 201	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)))
203	202	oveq1d 7425	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
204	188, 190, 203	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
205	72, 142, 204	3eqtr3d 2779	. . . . . . . . 9 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
206	140, 127	eqeltrrd 2836	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
207	202, 189	eqeltrrd 2836	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
208	206, 50, 207, 53	addsubeq4d 11650	. . . . . . . . 9 ⊢ (𝜑 → (((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ↔ ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))))
209	205, 208	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
210	63, 68, 209	3eqtr2d 2777	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
211	59, 60, 210	mvlraddd 11652	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)))
212	35, 2, 42, 211	mvllmuld 12078	. . . . 5 ⊢ (𝜑 → (𝑋↑2) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))))
213	54, 60, 35, 42	divsubdird 12061	. . . . . 6 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
214	46	eqcomi 2745	. . . . . . . . 9 ⊢ -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁
215	214	a1i 11	. . . . . . . 8 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁)
216	55, 215	negcon1ad 11594	. . . . . . 7 ⊢ (𝜑 → -𝑁 = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
217	216	oveq1d 7425	. . . . . 6 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
218	213, 217	eqtr4d 2774	. . . . 5 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
219	34, 1, 35, 42	div23d 12059	. . . . . . 7 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋))
220	3	oveq1i 7420	. . . . . . 7 ⊢ (𝑀 · 𝑋) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋)
221	219, 220	eqtr4di 2789	. . . . . 6 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = (𝑀 · 𝑋))
222	221	oveq2d 7426	. . . . 5 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = (-𝑁 − (𝑀 · 𝑋)))
223	212, 218, 222	3eqtrd 2775	. . . 4 ⊢ (𝜑 → (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋)))
224	216, 55	eqeltrd 2835	. . . . 5 ⊢ (𝜑 → -𝑁 ∈ ℂ)
225	2, 45, 224	addlsub 11658	. . . 4 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁 ↔ (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋))))
226	223, 225	mpbird 257	. . 3 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)
227	2, 45	addcld 11259	. . . 4 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ)
228		addeq0 11665	. . . 4 ⊢ ((((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
229	227, 57, 228	syl2anc 584	. . 3 ⊢ (𝜑 → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
230	226, 229	mpbird 257	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0)
231	58, 230	eqtr3d 2773	1 ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ⊆ wss 3931 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 0cc0 11134 + caddc 11137 · cmul 11139 − cmin 11471 -cneg 11472 / cdiv 11899 2c2 12300 ↑cexp 14084 ∗ccj 15120 abscabs 15258

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-sup 9459 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-n0 12507 df-z 12594 df-uz 12858 df-rp 13014 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260

This theorem is referenced by: constrrtcc 33774

W3C validator