requad2

Description: A condition for a quadratic equation with real coefficients to have (exactly) two different real solutions. (Contributed by AV, 28-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	requad2	$⊢ φ \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow 0 < D)$

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	ad3antrrr	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to A \in ℂ$
8	2	ad3antrrr	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to A \neq 0$
9	3	recnd	$⊢ φ \to B \in ℂ$
10	9	ad3antrrr	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to B \in ℂ$
11	4	recnd	$⊢ φ \to C \in ℂ$
12	11	ad3antrrr	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to C \in ℂ$
13		elelpwi	$⊢ (x \in p \land p \in 𝒫 ℝ) \to x \in ℝ$
14	13	expcom	$⊢ p \in 𝒫 ℝ \to (x \in p \to x \in ℝ)$
15	14	adantl	$⊢ ((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \to (x \in p \to x \in ℝ)$
16	15	imp	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to x \in ℝ$
17	16	recnd	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to x \in ℂ$
18	5	ad3antrrr	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to D = B^{2} - 4 A C$
19	7 8 10 12 17 18	quad	$⊢ (((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \land x \in p) \to (A x^{2} + B x + C = 0 \leftrightarrow (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}))$
20	19	ralbidva	$⊢ ((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \to (\forall x \in p A x^{2} + B x + C = 0 \leftrightarrow \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}))$
21	20	anbi2d	$⊢ ((φ \land 0 \leq D) \land p \in 𝒫 ℝ) \to ((\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow (\|p\| = 2 \land \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A})))$
22	21	reubidva	$⊢ (φ \land 0 \leq D) \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A})))$
23		eqid	$⊢ \{q \in 𝒫 ℝ \| \|q\| = 2\} = \{q \in 𝒫 ℝ \| \|q\| = 2\}$
24	23	pairreueq	$⊢ \exists! p \in \{q \in 𝒫 ℝ \| \|q\| = 2\} \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \leftrightarrow \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}))$
25	24	bicomi	$⊢ \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A})) \leftrightarrow \exists! p \in \{q \in 𝒫 ℝ \| \|q\| = 2\} \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A})$
26	25	a1i	$⊢ (φ \land 0 \leq D) \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A})) \leftrightarrow \exists! p \in \{q \in 𝒫 ℝ \| \|q\| = 2\} \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}))$
27	3	renegcld	$⊢ φ \to - B \in ℝ$
28	27	adantr	$⊢ (φ \land 0 \leq D) \to - B \in ℝ$
29	3	resqcld	$⊢ φ \to B^{2} \in ℝ$
30		4re	$⊢ 4 \in ℝ$
31	30	a1i	$⊢ φ \to 4 \in ℝ$
32	1 4	remulcld	$⊢ φ \to A C \in ℝ$
33	31 32	remulcld	$⊢ φ \to 4 A C \in ℝ$
34	29 33	resubcld	$⊢ φ \to B^{2} - 4 A C \in ℝ$
35	5 34	eqeltrd	$⊢ φ \to D \in ℝ$
36	35	adantr	$⊢ (φ \land 0 \leq D) \to D \in ℝ$
37		simpr	$⊢ (φ \land 0 \leq D) \to 0 \leq D$
38	36 37	resqrtcld	$⊢ (φ \land 0 \leq D) \to \sqrt{D} \in ℝ$
39	28 38	readdcld	$⊢ (φ \land 0 \leq D) \to - B + \sqrt{D} \in ℝ$
40		2re	$⊢ 2 \in ℝ$
41	40	a1i	$⊢ φ \to 2 \in ℝ$
42	41 1	remulcld	$⊢ φ \to 2 A \in ℝ$
43	42	adantr	$⊢ (φ \land 0 \leq D) \to 2 A \in ℝ$
44		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
45	44	a1i	$⊢ φ \to (2 \in ℂ \land 2 \neq 0)$
46		mulne0	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (A \in ℂ \land A \neq 0)) \to 2 A \neq 0$
47	45 6 2 46	syl12anc	$⊢ φ \to 2 A \neq 0$
48	47	adantr	$⊢ (φ \land 0 \leq D) \to 2 A \neq 0$
49	39 43 48	redivcld	$⊢ (φ \land 0 \leq D) \to \frac{- B + \sqrt{D}}{2 A} \in ℝ$
50	3	adantr	$⊢ (φ \land 0 \leq D) \to B \in ℝ$
51	50	renegcld	$⊢ (φ \land 0 \leq D) \to - B \in ℝ$
52	51 38	resubcld	$⊢ (φ \land 0 \leq D) \to - B - \sqrt{D} \in ℝ$
53	40	a1i	$⊢ (φ \land 0 \leq D) \to 2 \in ℝ$
54	1	adantr	$⊢ (φ \land 0 \leq D) \to A \in ℝ$
55	53 54	remulcld	$⊢ (φ \land 0 \leq D) \to 2 A \in ℝ$
56	52 55 48	redivcld	$⊢ (φ \land 0 \leq D) \to \frac{- B - \sqrt{D}}{2 A} \in ℝ$
57		fveqeq2	$⊢ q = x \to (\|q\| = 2 \leftrightarrow \|x\| = 2)$
58	57	cbvrabv	$⊢ \{q \in 𝒫 ℝ \| \|q\| = 2\} = \{x \in 𝒫 ℝ \| \|x\| = 2\}$
59	49 56 58	paireqne	$⊢ (φ \land 0 \leq D) \to (\exists! p \in \{q \in 𝒫 ℝ \| \|q\| = 2\} \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \leftrightarrow \frac{- B + \sqrt{D}}{2 A} \neq \frac{- B - \sqrt{D}}{2 A})$
60	9	negcld	$⊢ φ \to - B \in ℂ$
61	35	recnd	$⊢ φ \to D \in ℂ$
62	61	sqrtcld	$⊢ φ \to \sqrt{D} \in ℂ$
63	60 62	addcld	$⊢ φ \to - B + \sqrt{D} \in ℂ$
64	60 62	subcld	$⊢ φ \to - B - \sqrt{D} \in ℂ$
65		2cnd	$⊢ φ \to 2 \in ℂ$
66	65 6	mulcld	$⊢ φ \to 2 A \in ℂ$
67		div11	$⊢ (- B + \sqrt{D} \in ℂ \land - B - \sqrt{D} \in ℂ \land (2 A \in ℂ \land 2 A \neq 0)) \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A} \leftrightarrow - B + \sqrt{D} = - B - \sqrt{D})$
68	63 64 66 47 67	syl112anc	$⊢ φ \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A} \leftrightarrow - B + \sqrt{D} = - B - \sqrt{D})$
69	60 62	negsubd	$⊢ φ \to - B + (- \sqrt{D}) = - B - \sqrt{D}$
70	69	eqcomd	$⊢ φ \to - B - \sqrt{D} = - B + (- \sqrt{D})$
71	70	eqeq2d	$⊢ φ \to (- B + \sqrt{D} = - B - \sqrt{D} \leftrightarrow - B + \sqrt{D} = - B + (- \sqrt{D}))$
72	62	negcld	$⊢ φ \to - \sqrt{D} \in ℂ$
73	60 62 72	addcand	$⊢ φ \to (- B + \sqrt{D} = - B + (- \sqrt{D}) \leftrightarrow \sqrt{D} = - \sqrt{D})$
74	68 71 73	3bitrd	$⊢ φ \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} = - \sqrt{D})$
75	74	necon3bid	$⊢ φ \to (\frac{- B + \sqrt{D}}{2 A} \neq \frac{- B - \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} \neq - \sqrt{D})$
76	75	adantr	$⊢ (φ \land 0 \leq D) \to (\frac{- B + \sqrt{D}}{2 A} \neq \frac{- B - \sqrt{D}}{2 A} \leftrightarrow \sqrt{D} \neq - \sqrt{D})$
77		cnsqrt00	$⊢ D \in ℂ \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
78	61 77	syl	$⊢ φ \to (\sqrt{D} = 0 \leftrightarrow D = 0)$
79	78	necon3bid	$⊢ φ \to (\sqrt{D} \neq 0 \leftrightarrow D \neq 0)$
80	79	adantr	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} \neq 0 \leftrightarrow D \neq 0)$
81	62	eqnegd	$⊢ φ \to (\sqrt{D} = - \sqrt{D} \leftrightarrow \sqrt{D} = 0)$
82	81	adantr	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} = - \sqrt{D} \leftrightarrow \sqrt{D} = 0)$
83	82	necon3bid	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} \neq - \sqrt{D} \leftrightarrow \sqrt{D} \neq 0)$
84		0red	$⊢ (φ \land 0 \leq D) \to 0 \in ℝ$
85	84 36 37	leltned	$⊢ (φ \land 0 \leq D) \to (0 < D \leftrightarrow D \neq 0)$
86	80 83 85	3bitr4d	$⊢ (φ \land 0 \leq D) \to (\sqrt{D} \neq - \sqrt{D} \leftrightarrow 0 < D)$
87	76 86	bitrd	$⊢ (φ \land 0 \leq D) \to (\frac{- B + \sqrt{D}}{2 A} \neq \frac{- B - \sqrt{D}}{2 A} \leftrightarrow 0 < D)$
88	26 59 87	3bitrd	$⊢ (φ \land 0 \leq D) \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p (x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A})) \leftrightarrow 0 < D)$
89	22 88	bitrd	$⊢ (φ \land 0 \leq D) \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow 0 < D)$
90	89	expcom	$⊢ 0 \leq D \to (φ \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow 0 < D))$
91		hash2prb	$⊢ p \in 𝒫 ℝ \to (\|p\| = 2 \leftrightarrow \exists a \in p \exists b \in p (a \neq b \land p = \{a, b\}))$
92	91	adantl	$⊢ (φ \land p \in 𝒫 ℝ) \to (\|p\| = 2 \leftrightarrow \exists a \in p \exists b \in p (a \neq b \land p = \{a, b\}))$
93		raleq	$⊢ p = \{a, b\} \to (\forall x \in p A x^{2} + B x + C = 0 \leftrightarrow \forall x \in \{a, b\} A x^{2} + B x + C = 0)$
94		vex	$⊢ a \in V$
95		vex	$⊢ b \in V$
96		oveq1	$⊢ x = a \to x^{2} = a^{2}$
97	96	oveq2d	$⊢ x = a \to A x^{2} = A a^{2}$
98		oveq2	$⊢ x = a \to B x = B a$
99	98	oveq1d	$⊢ x = a \to B x + C = B a + C$
100	97 99	oveq12d	$⊢ x = a \to A x^{2} + B x + C = A a^{2} + B a + C$
101	100	eqeq1d	$⊢ x = a \to (A x^{2} + B x + C = 0 \leftrightarrow A a^{2} + B a + C = 0)$
102		oveq1	$⊢ x = b \to x^{2} = b^{2}$
103	102	oveq2d	$⊢ x = b \to A x^{2} = A b^{2}$
104		oveq2	$⊢ x = b \to B x = B b$
105	104	oveq1d	$⊢ x = b \to B x + C = B b + C$
106	103 105	oveq12d	$⊢ x = b \to A x^{2} + B x + C = A b^{2} + B b + C$
107	106	eqeq1d	$⊢ x = b \to (A x^{2} + B x + C = 0 \leftrightarrow A b^{2} + B b + C = 0)$
108	94 95 101 107	ralpr	$⊢ \forall x \in \{a, b\} A x^{2} + B x + C = 0 \leftrightarrow (A a^{2} + B a + C = 0 \land A b^{2} + B b + C = 0)$
109	93 108	bitrdi	$⊢ p = \{a, b\} \to (\forall x \in p A x^{2} + B x + C = 0 \leftrightarrow (A a^{2} + B a + C = 0 \land A b^{2} + B b + C = 0))$
110	109	adantl	$⊢ (a \neq b \land p = \{a, b\}) \to (\forall x \in p A x^{2} + B x + C = 0 \leftrightarrow (A a^{2} + B a + C = 0 \land A b^{2} + B b + C = 0))$
111	110	adantl	$⊢ (((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \land (a \neq b \land p = \{a, b\})) \to (\forall x \in p A x^{2} + B x + C = 0 \leftrightarrow (A a^{2} + B a + C = 0 \land A b^{2} + B b + C = 0))$
112		elelpwi	$⊢ (b \in p \land p \in 𝒫 ℝ) \to b \in ℝ$
113	112	ex	$⊢ b \in p \to (p \in 𝒫 ℝ \to b \in ℝ)$
114	113	adantl	$⊢ (a \in p \land b \in p) \to (p \in 𝒫 ℝ \to b \in ℝ)$
115	114	com12	$⊢ p \in 𝒫 ℝ \to ((a \in p \land b \in p) \to b \in ℝ)$
116	115	adantl	$⊢ (φ \land p \in 𝒫 ℝ) \to ((a \in p \land b \in p) \to b \in ℝ)$
117	116	imp	$⊢ ((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \to b \in ℝ$
118		oveq1	$⊢ y = b \to y^{2} = b^{2}$
119	118	oveq2d	$⊢ y = b \to A y^{2} = A b^{2}$
120		oveq2	$⊢ y = b \to B y = B b$
121	120	oveq1d	$⊢ y = b \to B y + C = B b + C$
122	119 121	oveq12d	$⊢ y = b \to A y^{2} + B y + C = A b^{2} + B b + C$
123	122	eqeq1d	$⊢ y = b \to (A y^{2} + B y + C = 0 \leftrightarrow A b^{2} + B b + C = 0)$
124	123	adantl	$⊢ (((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \land y = b) \to (A y^{2} + B y + C = 0 \leftrightarrow A b^{2} + B b + C = 0)$
125	117 124	rspcedv	$⊢ ((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \to (A b^{2} + B b + C = 0 \to \exists y \in ℝ A y^{2} + B y + C = 0)$
126	125	adantr	$⊢ (((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \land (a \neq b \land p = \{a, b\})) \to (A b^{2} + B b + C = 0 \to \exists y \in ℝ A y^{2} + B y + C = 0)$
127	126	adantld	$⊢ (((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \land (a \neq b \land p = \{a, b\})) \to ((A a^{2} + B a + C = 0 \land A b^{2} + B b + C = 0) \to \exists y \in ℝ A y^{2} + B y + C = 0)$
128	111 127	sylbid	$⊢ (((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \land (a \neq b \land p = \{a, b\})) \to (\forall x \in p A x^{2} + B x + C = 0 \to \exists y \in ℝ A y^{2} + B y + C = 0)$
129	128	ex	$⊢ ((φ \land p \in 𝒫 ℝ) \land (a \in p \land b \in p)) \to ((a \neq b \land p = \{a, b\}) \to (\forall x \in p A x^{2} + B x + C = 0 \to \exists y \in ℝ A y^{2} + B y + C = 0))$
130	129	rexlimdvva	$⊢ (φ \land p \in 𝒫 ℝ) \to (\exists a \in p \exists b \in p (a \neq b \land p = \{a, b\}) \to (\forall x \in p A x^{2} + B x + C = 0 \to \exists y \in ℝ A y^{2} + B y + C = 0))$
131	92 130	sylbid	$⊢ (φ \land p \in 𝒫 ℝ) \to (\|p\| = 2 \to (\forall x \in p A x^{2} + B x + C = 0 \to \exists y \in ℝ A y^{2} + B y + C = 0))$
132	131	impd	$⊢ (φ \land p \in 𝒫 ℝ) \to ((\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \to \exists y \in ℝ A y^{2} + B y + C = 0)$
133	132	rexlimdva	$⊢ φ \to (\exists p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \to \exists y \in ℝ A y^{2} + B y + C = 0)$
134	1 2 3 4 5	requad01	$⊢ φ \to (\exists y \in ℝ A y^{2} + B y + C = 0 \leftrightarrow 0 \leq D)$
135	133 134	sylibd	$⊢ φ \to (\exists p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \to 0 \leq D)$
136	135	con3d	$⊢ φ \to (\neg 0 \leq D \to \neg \exists p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0))$
137	136	impcom	$⊢ (\neg 0 \leq D \land φ) \to \neg \exists p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0)$
138		reurex	$⊢ \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \to \exists p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0)$
139	137 138	nsyl	$⊢ (\neg 0 \leq D \land φ) \to \neg \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0)$
140	139	pm2.21d	$⊢ (\neg 0 \leq D \land φ) \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \to 0 < D)$
141		0red	$⊢ φ \to 0 \in ℝ$
142		ltle	$⊢ (0 \in ℝ \land D \in ℝ) \to (0 < D \to 0 \leq D)$
143	141 35 142	syl2anc	$⊢ φ \to (0 < D \to 0 \leq D)$
144		pm2.24	$⊢ 0 \leq D \to (\neg 0 \leq D \to \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0))$
145	143 144	syl6	$⊢ φ \to (0 < D \to (\neg 0 \leq D \to \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0)))$
146	145	com23	$⊢ φ \to (\neg 0 \leq D \to (0 < D \to \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0)))$
147	146	impcom	$⊢ (\neg 0 \leq D \land φ) \to (0 < D \to \exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0))$
148	140 147	impbid	$⊢ (\neg 0 \leq D \land φ) \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow 0 < D)$
149	148	ex	$⊢ \neg 0 \leq D \to (φ \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow 0 < D))$
150	90 149	pm2.61i	$⊢ φ \to (\exists! p \in 𝒫 ℝ (\|p\| = 2 \land \forall x \in p A x^{2} + B x + C = 0) \leftrightarrow 0 < D)$

Metamath Proof Explorer

Theorem requad2

Proof