quad1

Description: A condition for a quadratic equation with complex coefficients to have (exactly) one complex solution. (Contributed by AV, 23-Jan-2023)

	Ref	Expression
Hypotheses	quad1.a	$⊢ φ \to A \in ℂ$
	quad1.z	$⊢ φ \to A \neq 0$
	quad1.b	$⊢ φ \to B \in ℂ$
	quad1.c	$⊢ φ \to C \in ℂ$
	quad1.d	$⊢ φ \to D = B^{2} - 4 A C$
Assertion	quad1	$⊢ φ \to (\exists! x \in ℂ A x^{2} + B x + C = 0 \leftrightarrow D = 0)$

Proof

Step	Hyp	Ref	Expression
1		quad1.a	$⊢ φ \to A \in ℂ$
2		quad1.z	$⊢ φ \to A \neq 0$
3		quad1.b	$⊢ φ \to B \in ℂ$
4		quad1.c	$⊢ φ \to C \in ℂ$
5		quad1.d	$⊢ φ \to D = B^{2} - 4 A C$
6	1	adantr	$⊢ (φ \land x \in ℂ) \to A \in ℂ$
7	2	adantr	$⊢ (φ \land x \in ℂ) \to A \neq 0$
8	3	adantr	$⊢ (φ \land x \in ℂ) \to B \in ℂ$
9	4	adantr	$⊢ (φ \land x \in ℂ) \to C \in ℂ$
10		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
11	5	adantr	$⊢ (φ \land x \in ℂ) \to D = B^{2} - 4 A C$
12	6 7 8 9 10 11	quad	$⊢ (φ \land x \in ℂ) \to (A x^{2} + B x + C = 0 \leftrightarrow (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}))$
13	12	reubidva	$⊢ φ \to (\exists! x \in ℂ A x^{2} + B x + C = 0 \leftrightarrow \exists! x \in ℂ (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}))$
14	3	negcld	$⊢ φ \to - B \in ℂ$
15	3	sqcld	$⊢ φ \to B^{2} \in ℂ$
16		4cn	$⊢ 4 \in ℂ$
17	16	a1i	$⊢ φ \to 4 \in ℂ$
18	1 4	mulcld	$⊢ φ \to A C \in ℂ$
19	17 18	mulcld	$⊢ φ \to 4 A C \in ℂ$
20	15 19	subcld	$⊢ φ \to B^{2} - 4 A C \in ℂ$
21	5 20	eqeltrd	$⊢ φ \to D \in ℂ$
22	21	sqrtcld	$⊢ φ \to \sqrt{D} \in ℂ$
23	14 22	addcld	$⊢ φ \to - B + \sqrt{D} \in ℂ$
24		2cnd	$⊢ φ \to 2 \in ℂ$
25	24 1	mulcld	$⊢ φ \to 2 A \in ℂ$
26		2ne0	$⊢ 2 \neq 0$
27	26	a1i	$⊢ φ \to 2 \neq 0$
28	24 1 27 2	mulne0d	$⊢ φ \to 2 A \neq 0$
29	23 25 28	divcld	$⊢ φ \to \frac{- B + \sqrt{D}}{2 A} \in ℂ$
30	14 22	subcld	$⊢ φ \to - B - \sqrt{D} \in ℂ$
31	30 25 28	divcld	$⊢ φ \to \frac{- B - \sqrt{D}}{2 A} \in ℂ$
32		euoreqb	$⊢ (\frac{- B + \sqrt{D}}{2 A} \in ℂ \land \frac{- B - \sqrt{D}}{2 A} \in ℂ) \to (\exists! x \in ℂ (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \leftrightarrow \frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A})$
33	29 31 32	syl2anc	$⊢ φ \to (\exists! x \in ℂ (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \leftrightarrow \frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A})$
34	14 22 25 28	divdird	$⊢ φ \to \frac{- B + \sqrt{D}}{2 A} = (\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A})$
35	14 22 25 28	divsubdird	$⊢ φ \to \frac{- B - \sqrt{D}}{2 A} = (\frac{- B}{2 A}) - (\frac{\sqrt{D}}{2 A})$
36	14 25 28	divcld	$⊢ φ \to \frac{- B}{2 A} \in ℂ$
37	22 25 28	divcld	$⊢ φ \to \frac{\sqrt{D}}{2 A} \in ℂ$
38	36 37	negsubd	$⊢ φ \to (\frac{- B}{2 A}) + (- \frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) - (\frac{\sqrt{D}}{2 A})$
39	22 25 28	divnegd	$⊢ φ \to - \frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A}$
40	39	oveq2d	$⊢ φ \to (\frac{- B}{2 A}) + (- \frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A})$
41	35 38 40	3eqtr2d	$⊢ φ \to \frac{- B - \sqrt{D}}{2 A} = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A})$
42	34 41	eqeq12d	$⊢ φ \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A} \leftrightarrow (\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A}))$
43	22	negcld	$⊢ φ \to - \sqrt{D} \in ℂ$
44	43 25 28	divcld	$⊢ φ \to \frac{- \sqrt{D}}{2 A} \in ℂ$
45	36 37 44	addcand	$⊢ φ \to ((\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A}) \leftrightarrow \frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A})$
46		div11	$⊢ (\sqrt{D} \in ℂ \land - \sqrt{D} \in ℂ \land (2 A \in ℂ \land 2 A \neq 0)) \to (\frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} = - \sqrt{D})$
47	22 43 25 28 46	syl112anc	$⊢ φ \to (\frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} = - \sqrt{D})$
48	22	eqnegd	$⊢ φ \to (\sqrt{D} = - \sqrt{D} \leftrightarrow \sqrt{D} = 0)$
49		cnsqrt00	$⊢ D \in ℂ \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
50	21 49	syl	$⊢ φ \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
51	48 50	bitrd	$⊢ φ \to (\sqrt{D} = - \sqrt{D} \leftrightarrow D = 0)$
52	45 47 51	3bitrd	$⊢ φ \to ((\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A}) \leftrightarrow D = 0)$
53	42 52	bitrd	$⊢ φ \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A} \leftrightarrow D = 0)$
54	13 33 53	3bitrd	$⊢ φ \to (\exists! x \in ℂ A x^{2} + B x + C = 0 \leftrightarrow D = 0)$

Metamath Proof Explorer

Theorem quad1

Proof