requad1

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

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

Proof

Step	Hyp	Ref	Expression
1		requad2.a	$⊢ φ \to A \in ℝ$
2		requad2.z	$⊢ φ \to A \neq 0$
3		requad2.b	$⊢ φ \to B \in ℝ$
4		requad2.c	$⊢ φ \to C \in ℝ$
5		requad2.d	$⊢ φ \to D = B^{2} - 4 A C$
6	1	recnd	$⊢ φ \to A \in ℂ$
7	6	ad2antrr	$⊢ ((φ \land 0 \leq D) \land x \in ℝ) \to A \in ℂ$
8	2	ad2antrr	$⊢ ((φ \land 0 \leq D) \land x \in ℝ) \to A \neq 0$
9	3	recnd	$⊢ φ \to B \in ℂ$
10	9	ad2antrr	$⊢ ((φ \land 0 \leq D) \land x \in ℝ) \to B \in ℂ$
11	4	recnd	$⊢ φ \to C \in ℂ$
12	11	ad2antrr	$⊢ ((φ \land 0 \leq D) \land x \in ℝ) \to C \in ℂ$
13		recn	$⊢ x \in ℝ \to x \in ℂ$
14	13	adantl	$⊢ ((φ \land 0 \leq D) \land x \in ℝ) \to x \in ℂ$
15	5	ad2antrr	$⊢ ((φ \land 0 \leq D) \land x \in ℝ) \to D = B^{2} - 4 A C$
16	7 8 10 12 14 15	quad	$⊢ ((φ \land 0 \leq D) \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}))$
17	16	reubidva	$⊢ (φ \land 0 \leq D) \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}))$
18	3	renegcld	$⊢ φ \to - B \in ℝ$
19	18	adantr	$⊢ (φ \land 0 \leq D) \to - B \in ℝ$
20	3	resqcld	$⊢ φ \to B^{2} \in ℝ$
21		4re	$⊢ 4 \in ℝ$
22	21	a1i	$⊢ φ \to 4 \in ℝ$
23	1 4	remulcld	$⊢ φ \to A C \in ℝ$
24	22 23	remulcld	$⊢ φ \to 4 A C \in ℝ$
25	20 24	resubcld	$⊢ φ \to B^{2} - 4 A C \in ℝ$
26	5 25	eqeltrd	$⊢ φ \to D \in ℝ$
27		resqrtcl	$⊢ (D \in ℝ \land 0 \leq D) \to \sqrt{D} \in ℝ$
28	26 27	sylan	$⊢ (φ \land 0 \leq D) \to \sqrt{D} \in ℝ$
29	19 28	readdcld	$⊢ (φ \land 0 \leq D) \to - B + \sqrt{D} \in ℝ$
30		2re	$⊢ 2 \in ℝ$
31	30	a1i	$⊢ φ \to 2 \in ℝ$
32	31 1	remulcld	$⊢ φ \to 2 A \in ℝ$
33	32	adantr	$⊢ (φ \land 0 \leq D) \to 2 A \in ℝ$
34		2cnd	$⊢ φ \to 2 \in ℂ$
35		2ne0	$⊢ 2 \neq 0$
36	35	a1i	$⊢ φ \to 2 \neq 0$
37	34 6 36 2	mulne0d	$⊢ φ \to 2 A \neq 0$
38	37	adantr	$⊢ (φ \land 0 \leq D) \to 2 A \neq 0$
39	29 33 38	redivcld	$⊢ (φ \land 0 \leq D) \to \frac{- B + \sqrt{D}}{2 A} \in ℝ$
40	19 28	resubcld	$⊢ (φ \land 0 \leq D) \to - B - \sqrt{D} \in ℝ$
41	40 33 38	redivcld	$⊢ (φ \land 0 \leq D) \to \frac{- B - \sqrt{D}}{2 A} \in ℝ$
42		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})$
43	39 41 42	syl2anc	$⊢ (φ \land 0 \leq D) \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})$
44	9	negcld	$⊢ φ \to - B \in ℂ$
45	26	recnd	$⊢ φ \to D \in ℂ$
46	45	sqrtcld	$⊢ φ \to \sqrt{D} \in ℂ$
47	32	recnd	$⊢ φ \to 2 A \in ℂ$
48	44 46 47 37	divdird	$⊢ φ \to \frac{- B + \sqrt{D}}{2 A} = (\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A})$
49	48	adantr	$⊢ (φ \land 0 \leq D) \to \frac{- B + \sqrt{D}}{2 A} = (\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A})$
50	44 46 47 37	divsubdird	$⊢ φ \to \frac{- B - \sqrt{D}}{2 A} = (\frac{- B}{2 A}) - (\frac{\sqrt{D}}{2 A})$
51	50	adantr	$⊢ (φ \land 0 \leq D) \to \frac{- B - \sqrt{D}}{2 A} = (\frac{- B}{2 A}) - (\frac{\sqrt{D}}{2 A})$
52	44 47 37	divcld	$⊢ φ \to \frac{- B}{2 A} \in ℂ$
53	52	adantr	$⊢ (φ \land 0 \leq D) \to \frac{- B}{2 A} \in ℂ$
54	46 47 37	divcld	$⊢ φ \to \frac{\sqrt{D}}{2 A} \in ℂ$
55	54	adantr	$⊢ (φ \land 0 \leq D) \to \frac{\sqrt{D}}{2 A} \in ℂ$
56	53 55	negsubd	$⊢ (φ \land 0 \leq D) \to (\frac{- B}{2 A}) + (- \frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) - (\frac{\sqrt{D}}{2 A})$
57	46	adantr	$⊢ (φ \land 0 \leq D) \to \sqrt{D} \in ℂ$
58	47	adantr	$⊢ (φ \land 0 \leq D) \to 2 A \in ℂ$
59	57 58 38	divnegd	$⊢ (φ \land 0 \leq D) \to - \frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A}$
60	59	oveq2d	$⊢ (φ \land 0 \leq D) \to (\frac{- B}{2 A}) + (- \frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A})$
61	51 56 60	3eqtr2d	$⊢ (φ \land 0 \leq D) \to \frac{- B - \sqrt{D}}{2 A} = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A})$
62	49 61	eqeq12d	$⊢ (φ \land 0 \leq D) \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}))$
63	46	negcld	$⊢ φ \to - \sqrt{D} \in ℂ$
64	63 47 37	divcld	$⊢ φ \to \frac{- \sqrt{D}}{2 A} \in ℂ$
65	64	adantr	$⊢ (φ \land 0 \leq D) \to \frac{- \sqrt{D}}{2 A} \in ℂ$
66	53 55 65	addcand	$⊢ (φ \land 0 \leq D) \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})$
67		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})$
68	46 63 47 37 67	syl112anc	$⊢ φ \to (\frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} = - \sqrt{D})$
69	68	adantr	$⊢ (φ \land 0 \leq D) \to (\frac{\sqrt{D}}{2 A} = \frac{- \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} = - \sqrt{D})$
70	57	eqnegd	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} = - \sqrt{D} \leftrightarrow \sqrt{D} = 0)$
71		sqrt00	$⊢ (D \in ℝ \land 0 \leq D) \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
72	26 71	sylan	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
73	70 72	bitrd	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} = - \sqrt{D} \leftrightarrow D = 0)$
74	66 69 73	3bitrd	$⊢ (φ \land 0 \leq D) \to ((\frac{- B}{2 A}) + (\frac{\sqrt{D}}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{D}}{2 A}) \leftrightarrow D = 0)$
75	62 74	bitrd	$⊢ (φ \land 0 \leq D) \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A} \leftrightarrow D = 0)$
76	17 43 75	3bitrd	$⊢ (φ \land 0 \leq D) \to (\exists! x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow D = 0)$
77	76	expcom	$⊢ 0 \leq D \to (φ \to (\exists! x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow D = 0))$
78	1 2 3 4 5	requad01	$⊢ φ \to (\exists x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow 0 \leq D)$
79	78	notbid	$⊢ φ \to (\neg \exists x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow \neg 0 \leq D)$
80	79	biimparc	$⊢ (\neg 0 \leq D \land φ) \to \neg \exists x \in ℝ A x^{2} + B x + C = 0$
81		reurex	$⊢ \exists! x \in ℝ A x^{2} + B x + C = 0 \to \exists x \in ℝ A x^{2} + B x + C = 0$
82	80 81	nsyl	$⊢ (\neg 0 \leq D \land φ) \to \neg \exists! x \in ℝ A x^{2} + B x + C = 0$
83	82	pm2.21d	$⊢ (\neg 0 \leq D \land φ) \to (\exists! x \in ℝ A x^{2} + B x + C = 0 \to D = 0)$
84		0red	$⊢ φ \to 0 \in ℝ$
85	26 84	ltnled	$⊢ φ \to (D < 0 \leftrightarrow \neg 0 \leq D)$
86	85	biimparc	$⊢ (\neg 0 \leq D \land φ) \to D < 0$
87	86	lt0ne0d	$⊢ (\neg 0 \leq D \land φ) \to D \neq 0$
88		eqneqall	$⊢ D = 0 \to (D \neq 0 \to \exists! x \in ℝ A x^{2} + B x + C = 0)$
89	87 88	syl5com	$⊢ (\neg 0 \leq D \land φ) \to (D = 0 \to \exists! x \in ℝ A x^{2} + B x + C = 0)$
90	83 89	impbid	$⊢ (\neg 0 \leq D \land φ) \to (\exists! x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow D = 0)$
91	90	ex	$⊢ \neg 0 \leq D \to (φ \to (\exists! x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow D = 0))$
92	77 91	pm2.61i	$⊢ φ \to (\exists! x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow D = 0)$

Metamath Proof Explorer

Theorem requad1

Proof