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 33725

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 14194	. . 3 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
3		constrrtcc.m	. . . . 5 ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))
4		constrrtcc.5	. . . . . . . . 9 ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))
5		constrrtcc.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		constrrtcc.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ 𝑆)
7	5, 6	sseldd 4009	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
8		constrrtcc.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
9	5, 8	sseldd 4009	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ ℂ)
10	7, 9	subcld 11647	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 − 𝐹) ∈ ℂ)
11	10	cjcld 15245	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐸 − 𝐹)) ∈ ℂ)
12	10, 11	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) ∈ ℂ)
13	4, 12	eqeltrid 2848	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℂ)
14		constrrtcc.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑆)
15	5, 14	sseldd 4009	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
16	15	cjcld 15245	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
17		constrrtcc.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	5, 17	sseldd 4009	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
19	15, 18	addcld 11309	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℂ)
20	16, 19	mulcld 11310	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 + 𝐴)) ∈ ℂ)
21	13, 20	subcld 11647	. . . . . . 7 ⊢ (𝜑 → (𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) ∈ ℂ)
22		constrrtcc.4	. . . . . . . . 9 ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))
23		constrrtcc.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
24	5, 23	sseldd 4009	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
25		constrrtcc.c	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
26	5, 25	sseldd 4009	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
27	24, 26	subcld 11647	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
28	27	cjcld 15245	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 − 𝐶)) ∈ ℂ)
29	27, 28	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) ∈ ℂ)
30	22, 29	eqeltrid 2848	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
31	18	cjcld 15245	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
32	31, 19	mulcld 11310	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 + 𝐴)) ∈ ℂ)
33	30, 32	subcld 11647	. . . . . . 7 ⊢ (𝜑 → (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) ∈ ℂ)
34	21, 33	subcld 11647	. . . . . 6 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) ∈ ℂ)
35	16, 31	subcld 11647	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ∈ ℂ)
36	15, 18	cjsubd 32755	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) = ((∗‘𝐷) − (∗‘𝐴)))
37	15, 18	subcld 11647	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
38		constrrtcc.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
39	38	necomd 3002	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐴)
40	15, 18, 39	subne0d 11656	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐴) ≠ 0)
41	37, 40	cjne0d 15252	. . . . . . 7 ⊢ (𝜑 → (∗‘(𝐷 − 𝐴)) ≠ 0)
42	36, 41	eqnetrrd 3015	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐴)) ≠ 0)
43	34, 35, 42	divcld 12070	. . . . 5 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
44	3, 43	eqeltrid 2848	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℂ)
45	44, 1	mulcld 11310	. . 3 ⊢ (𝜑 → (𝑀 · 𝑋) ∈ ℂ)
46		constrrtcc.n	. . . 4 ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))
47	15, 18	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · 𝐴) ∈ ℂ)
48	31, 47	mulcld 11310	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · (𝐷 · 𝐴)) ∈ ℂ)
49	30, 15	mulcld 11310	. . . . . . . 8 ⊢ (𝜑 → (𝑃 · 𝐷) ∈ ℂ)
50	48, 49	subcld 11647	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) ∈ ℂ)
51	16, 47	mulcld 11310	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐷) · (𝐷 · 𝐴)) ∈ ℂ)
52	13, 18	mulcld 11310	. . . . . . . 8 ⊢ (𝜑 → (𝑄 · 𝐴) ∈ ℂ)
53	51, 52	subcld 11647	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)) ∈ ℂ)
54	50, 53	subcld 11647	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ∈ ℂ)
55	54, 35, 42	divcld 12070	. . . . 5 ⊢ (𝜑 → (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
56	55	negcld 11634	. . . 4 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ∈ ℂ)
57	46, 56	eqeltrid 2848	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℂ)
58	2, 45, 57	addassd 11312	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)))
59	35, 2	mulcld 11310	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) ∈ ℂ)
60	34, 1	mulcld 11310	. . . . . . 7 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) ∈ ℂ)
61	16, 31, 2	subdird 11747	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))))
62	21, 33, 1	subdird 11747	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
63	61, 62	oveq12d 7466	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
64	16, 2	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋↑2)) ∈ ℂ)
65	21, 1	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
66	31, 2	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋↑2)) ∈ ℂ)
67	33, 1	mulcld 11310	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) ∈ ℂ)
68	64, 65, 66, 67	addsub4d 11694	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋↑2))) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) − ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))))
69	1, 18	subcld 11647	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℂ)
70	1, 15	subcld 11647	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 − 𝐷) ∈ ℂ)
71	69, 70	mulcomd 11311	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = ((𝑋 − 𝐷) · (𝑋 − 𝐴)))
72	71	oveq2d 7464	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
73	69	cjcld 15245	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) ∈ ℂ)
74		constrrtcc.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))
75		constrrtcclem.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
76	24, 26, 75	subne0d 11656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐶) ≠ 0)
77	27, 76	absne0d 15496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ≠ 0)
78	74, 77	eqnetrd 3014	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) ≠ 0)
79	69	abs00ad 15339	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) = 0 ↔ (𝑋 − 𝐴) = 0))
80	79	necon3bid 2991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴)) ≠ 0 ↔ (𝑋 − 𝐴) ≠ 0))
81	78, 80	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐴) ≠ 0)
82	74	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((abs‘(𝐵 − 𝐶))↑2))
83	69	absvalsqd 15491	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐴))↑2) = ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))))
84	27	absvalsqd 15491	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐵 − 𝐶))↑2) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
85	82, 83, 84	3eqtr3d 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))))
86	85, 22	eqtr4di 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (∗‘(𝑋 − 𝐴))) = 𝑃)
87	69, 73, 81, 86	mvllmuld 12126	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = (𝑃 / (𝑋 − 𝐴)))
88	87, 73	eqeltrrd 2845	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 / (𝑋 − 𝐴)) ∈ ℂ)
89	31, 88	addcld 11309	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) ∈ ℂ)
90	89, 69, 70	mulassd 11313	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
91	30, 69, 81	divcan1d 12071	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴)) = 𝑃)
92	91	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) + ((𝑃 / (𝑋 − 𝐴)) · (𝑋 − 𝐴))) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
93	31, 69, 88, 92	joinlmuladdmuld 11317	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) = (((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃))
94	93	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)))
95	31, 69	mulcld 11310	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 − 𝐴)) ∈ ℂ)
96	95, 30, 70	adddird 11315	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) + 𝑃) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))))
97	31, 69, 70	mulassd 11313	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
98	1, 18, 1, 15	mulsubd 11749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
99	1	sqvald 14193	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑋↑2) = (𝑋 · 𝑋))
100	99	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑋↑2) + (𝐷 · 𝐴)) = ((𝑋 · 𝑋) + (𝐷 · 𝐴)))
101	1, 15, 18	adddid 11314	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) = ((𝑋 · 𝐷) + (𝑋 · 𝐴)))
102	100, 101	oveq12d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋 · 𝑋) + (𝐷 · 𝐴)) − ((𝑋 · 𝐷) + (𝑋 · 𝐴))))
103	1, 19	mulcld 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 · (𝐷 + 𝐴)) ∈ ℂ)
104	2, 47, 103	addsubd 11668	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑋↑2) + (𝐷 · 𝐴)) − (𝑋 · (𝐷 + 𝐴))) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
105	98, 102, 104	3eqtr2d 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐴) · (𝑋 − 𝐷)) = (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴)))
106	105	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
107	2, 103	subcld 11647	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) ∈ ℂ)
108	31, 107, 47	adddid 11314	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
109	97, 106, 108	3eqtrd 2784	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))))
110	30, 1, 15	subdid 11746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 · (𝑋 − 𝐷)) = ((𝑃 · 𝑋) − (𝑃 · 𝐷)))
111	109, 110	oveq12d 7466	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) + (𝑃 · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
112	94, 96, 111	3eqtrd 2784	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · (𝑋 − 𝐴)) · (𝑋 − 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
113	1, 18	cjsubd 32755	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐴)) = ((∗‘𝑋) − (∗‘𝐴)))
114	113, 87	eqtr3d 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)))
115	1	cjcld 15245	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘𝑋) ∈ ℂ)
116	115, 31, 88	subaddd 11665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐴)) = (𝑃 / (𝑋 − 𝐴)) ↔ ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋)))
117	114, 116	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) = (∗‘𝑋))
118	117	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) + (𝑃 / (𝑋 − 𝐴))) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
119	90, 112, 118	3eqtr3rd 2789	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
120	31, 107	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
121	120, 48	addcld 11309	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) ∈ ℂ)
122	30, 1	mulcld 11310	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 · 𝑋) ∈ ℂ)
123	121, 122, 49	addsubassd 11667	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + ((𝑃 · 𝑋) − (𝑃 · 𝐷))))
124	120, 48, 122	add32d 11517	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))))
125	124	oveq1d 7463	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐴) · (𝐷 · 𝐴))) + (𝑃 · 𝑋)) − (𝑃 · 𝐷)) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
126	119, 123, 125	3eqtr2d 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)))
127	120, 122	addcld 11309	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) ∈ ℂ)
128	127, 48, 49	addsubassd 11667	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + ((∗‘𝐴) · (𝐷 · 𝐴))) − (𝑃 · 𝐷)) = ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
129	32, 1	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
130	66, 129, 122	subadd23d 11669	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
131	31, 2, 103	subdid 11746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))))
132	31, 1, 19	mul12d 11499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))))
133	1, 32	mulcomd 11311	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐴) · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
134	132, 133	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))
135	134	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) − ((∗‘𝐴) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
136	131, 135	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
137	136	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = ((((∗‘𝐴) · (𝑋↑2)) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)) + (𝑃 · 𝑋)))
138	30, 32, 1	subdird 11747	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋) = ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋)))
139	138	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 · 𝑋) − (((∗‘𝐴) · (𝐷 + 𝐴)) · 𝑋))))
140	130, 137, 139	3eqtr4d 2790	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) = (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)))
141	140	oveq1d 7463	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐴) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑃 · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
142	126, 128, 141	3eqtrd 2784	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))))
143	70	cjcld 15245	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) ∈ ℂ)
144		constrrtcc.3	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))
145		constrrtcclem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ≠ 𝐹)
146	7, 9, 145	subne0d 11656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 − 𝐹) ≠ 0)
147	10, 146	absne0d 15496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘(𝐸 − 𝐹)) ≠ 0)
148	144, 147	eqnetrd 3014	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) ≠ 0)
149	70	abs00ad 15339	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) = 0 ↔ (𝑋 − 𝐷) = 0))
150	149	necon3bid 2991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷)) ≠ 0 ↔ (𝑋 − 𝐷) ≠ 0))
151	148, 150	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 − 𝐷) ≠ 0)
152	144	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((abs‘(𝐸 − 𝐹))↑2))
153	70	absvalsqd 15491	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝑋 − 𝐷))↑2) = ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))))
154	10	absvalsqd 15491	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘(𝐸 − 𝐹))↑2) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
155	152, 153, 154	3eqtr3d 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))))
156	155, 4	eqtr4di 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 − 𝐷) · (∗‘(𝑋 − 𝐷))) = 𝑄)
157	70, 143, 151, 156	mvllmuld 12126	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = (𝑄 / (𝑋 − 𝐷)))
158	157, 143	eqeltrrd 2845	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 / (𝑋 − 𝐷)) ∈ ℂ)
159	16, 158	addcld 11309	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) ∈ ℂ)
160	159, 70, 69	mulassd 11313	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
161	13, 70, 151	divcan1d 12071	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷)) = 𝑄)
162	161	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) + ((𝑄 / (𝑋 − 𝐷)) · (𝑋 − 𝐷))) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
163	16, 70, 158, 162	joinlmuladdmuld 11317	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) = (((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄))
164	163	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)))
165	16, 70	mulcld 11310	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 − 𝐷)) ∈ ℂ)
166	165, 13, 69	adddird 11315	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) + 𝑄) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))))
167	16, 70, 69	mulassd 11313	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
168	71	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
169	167, 168	eqtr4d 2783	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))))
170	105	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋 − 𝐴) · (𝑋 − 𝐷))) = ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))))
171	16, 107, 47	adddid 11314	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (((𝑋↑2) − (𝑋 · (𝐷 + 𝐴))) + (𝐷 · 𝐴))) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
172	169, 170, 171	3eqtrd 2784	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))))
173	13, 1, 18	subdid 11746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 · (𝑋 − 𝐴)) = ((𝑄 · 𝑋) − (𝑄 · 𝐴)))
174	172, 173	oveq12d 7466	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) + (𝑄 · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
175	164, 166, 174	3eqtrd 2784	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · (𝑋 − 𝐷)) · (𝑋 − 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
176	1, 15	cjsubd 32755	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∗‘(𝑋 − 𝐷)) = ((∗‘𝑋) − (∗‘𝐷)))
177	176, 157	eqtr3d 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)))
178	115, 16, 158	subaddd 11665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝑋) − (∗‘𝐷)) = (𝑄 / (𝑋 − 𝐷)) ↔ ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋)))
179	177, 178	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) = (∗‘𝑋))
180	179	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) + (𝑄 / (𝑋 − 𝐷))) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))))
181	160, 175, 180	3eqtr3rd 2789	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
182	16, 107	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) ∈ ℂ)
183	182, 51	addcld 11309	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) ∈ ℂ)
184	13, 1	mulcld 11310	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄 · 𝑋) ∈ ℂ)
185	183, 184, 52	addsubassd 11667	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + ((𝑄 · 𝑋) − (𝑄 · 𝐴))))
186	182, 51, 184	add32d 11517	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))))
187	186	oveq1d 7463	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + ((∗‘𝐷) · (𝐷 · 𝐴))) + (𝑄 · 𝑋)) − (𝑄 · 𝐴)) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
188	181, 185, 187	3eqtr2d 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)))
189	182, 184	addcld 11309	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) ∈ ℂ)
190	189, 51, 52	addsubassd 11667	. . . . . . . . . . 11 ⊢ (𝜑 → (((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + ((∗‘𝐷) · (𝐷 · 𝐴))) − (𝑄 · 𝐴)) = ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
191	20, 1	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋) ∈ ℂ)
192	64, 191, 184	subadd23d 11669	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
193	16, 2, 103	subdid 11746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))))
194	16, 1, 19	mul12d 11499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))))
195	1, 20	mulcomd 11311	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 · ((∗‘𝐷) · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
196	194, 195	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴))) = (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))
197	196	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) − ((∗‘𝐷) · (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
198	193, 197	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) = (((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
199	198	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = ((((∗‘𝐷) · (𝑋↑2)) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)) + (𝑄 · 𝑋)))
200	13, 20, 1	subdird 11747	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋) = ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋)))
201	200	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 · 𝑋) − (((∗‘𝐷) · (𝐷 + 𝐴)) · 𝑋))))
202	192, 199, 201	3eqtr4d 2790	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) = (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)))
203	202	oveq1d 7463	. . . . . . . . . . 11 ⊢ (𝜑 → ((((∗‘𝐷) · ((𝑋↑2) − (𝑋 · (𝐷 + 𝐴)))) + (𝑄 · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
204	188, 190, 203	3eqtrd 2784	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝑋) · ((𝑋 − 𝐷) · (𝑋 − 𝐴))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
205	72, 142, 204	3eqtr3d 2788	. . . . . . . . 9 ⊢ (𝜑 → ((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
206	140, 127	eqeltrrd 2845	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
207	202, 189	eqeltrrd 2845	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) ∈ ℂ)
208	206, 50, 207, 53	addsubeq4d 11698	. . . . . . . . 9 ⊢ (𝜑 → (((((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷))) = ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) + (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) ↔ ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴)))))
209	205, 208	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐷) · (𝑋↑2)) + ((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) · 𝑋)) − (((∗‘𝐴) · (𝑋↑2)) + ((𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴))) · 𝑋))) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
210	63, 68, 209	3eqtr2d 2786	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) + (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) = ((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))))
211	59, 60, 210	mvlraddd 11700	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐷) − (∗‘𝐴)) · (𝑋↑2)) = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)))
212	35, 2, 42, 211	mvllmuld 12126	. . . . 5 ⊢ (𝜑 → (𝑋↑2) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))))
213	54, 60, 35, 42	divsubdird 12109	. . . . . 6 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
214	46	eqcomi 2749	. . . . . . . . 9 ⊢ -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁
215	214	a1i 11	. . . . . . . 8 ⊢ (𝜑 → -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) = 𝑁)
216	55, 215	negcon1ad 11642	. . . . . . 7 ⊢ (𝜑 → -𝑁 = (((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))))
217	216	oveq1d 7463	. . . . . 6 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
218	213, 217	eqtr4d 2783	. . . . 5 ⊢ (𝜑 → ((((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) − (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋)) / ((∗‘𝐷) − (∗‘𝐴))) = (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))))
219	34, 1, 35, 42	div23d 12107	. . . . . . 7 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋))
220	3	oveq1i 7458	. . . . . . 7 ⊢ (𝑀 · 𝑋) = ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) · 𝑋)
221	219, 220	eqtr4di 2798	. . . . . 6 ⊢ (𝜑 → ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴))) = (𝑀 · 𝑋))
222	221	oveq2d 7464	. . . . 5 ⊢ (𝜑 → (-𝑁 − ((((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) · 𝑋) / ((∗‘𝐷) − (∗‘𝐴)))) = (-𝑁 − (𝑀 · 𝑋)))
223	212, 218, 222	3eqtrd 2784	. . . 4 ⊢ (𝜑 → (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋)))
224	216, 55	eqeltrd 2844	. . . . 5 ⊢ (𝜑 → -𝑁 ∈ ℂ)
225	2, 45, 224	addlsub 11706	. . . 4 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁 ↔ (𝑋↑2) = (-𝑁 − (𝑀 · 𝑋))))
226	223, 225	mpbird 257	. . 3 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁)
227	2, 45	addcld 11309	. . . 4 ⊢ (𝜑 → ((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ)
228		addeq0 11713	. . . 4 ⊢ ((((𝑋↑2) + (𝑀 · 𝑋)) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
229	227, 57, 228	syl2anc 583	. . 3 ⊢ (𝜑 → ((((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0 ↔ ((𝑋↑2) + (𝑀 · 𝑋)) = -𝑁))
230	226, 229	mpbird 257	. 2 ⊢ (𝜑 → (((𝑋↑2) + (𝑀 · 𝑋)) + 𝑁) = 0)
231	58, 230	eqtr3d 2782	1 ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ⊆ wss 3976 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 0cc0 11184 + caddc 11187 · cmul 11189 − cmin 11520 -cneg 11521 / cdiv 11947 2c2 12348 ↑cexp 14112 ∗ccj 15145 abscabs 15283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-sup 9511 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-z 12640 df-uz 12904 df-rp 13058 df-seq 14053 df-exp 14113 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285

This theorem is referenced by: constrrtcc 33726

W3C validator