requad01

Description: A condition for a quadratic equation with real coefficients to have (at least) one real solution. (Contributed by AV, 23-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	requad01	$⊢ φ \to (\exists x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow 0 \leq 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	adantr	$⊢ (φ \land x \in ℝ) \to A \in ℂ$
8	2	adantr	$⊢ (φ \land x \in ℝ) \to A \neq 0$
9	3	recnd	$⊢ φ \to B \in ℂ$
10	9	adantr	$⊢ (φ \land x \in ℝ) \to B \in ℂ$
11	4	recnd	$⊢ φ \to C \in ℂ$
12	11	adantr	$⊢ (φ \land x \in ℝ) \to C \in ℂ$
13		recn	$⊢ x \in ℝ \to x \in ℂ$
14	13	adantl	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
15	5	adantr	$⊢ (φ \land x \in ℝ) \to D = B^{2} - 4 A C$
16	7 8 10 12 14 15	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}))$
17		eleq1	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to (x \in ℝ \leftrightarrow \frac{- B + \sqrt{D}}{2 A} \in ℝ)$
18	17	adantl	$⊢ (φ \land x = \frac{- B + \sqrt{D}}{2 A}) \to (x \in ℝ \leftrightarrow \frac{- B + \sqrt{D}}{2 A} \in ℝ)$
19		2re	$⊢ 2 \in ℝ$
20	19	a1i	$⊢ φ \to 2 \in ℝ$
21	20 1	remulcld	$⊢ φ \to 2 A \in ℝ$
22	21	adantr	$⊢ (φ \land \neg 0 \leq D) \to 2 A \in ℝ$
23	9	negcld	$⊢ φ \to - B \in ℂ$
24	3	resqcld	$⊢ φ \to B^{2} \in ℝ$
25		4re	$⊢ 4 \in ℝ$
26	25	a1i	$⊢ φ \to 4 \in ℝ$
27	1 4	remulcld	$⊢ φ \to A C \in ℝ$
28	26 27	remulcld	$⊢ φ \to 4 A C \in ℝ$
29	24 28	resubcld	$⊢ φ \to B^{2} - 4 A C \in ℝ$
30	5 29	eqeltrd	$⊢ φ \to D \in ℝ$
31	30	recnd	$⊢ φ \to D \in ℂ$
32	31	sqrtcld	$⊢ φ \to \sqrt{D} \in ℂ$
33	23 32	addcld	$⊢ φ \to - B + \sqrt{D} \in ℂ$
34	33	adantr	$⊢ (φ \land \neg 0 \leq D) \to - B + \sqrt{D} \in ℂ$
35	3	renegcld	$⊢ φ \to - B \in ℝ$
36	35	adantr	$⊢ (φ \land \neg 0 \leq D) \to - B \in ℝ$
37	32	adantr	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{D} \in ℂ$
38	31	negnegd	$⊢ φ \to - (- D) = D$
39	38	adantr	$⊢ (φ \land \neg 0 \leq D) \to - (- D) = D$
40	39	eqcomd	$⊢ (φ \land \neg 0 \leq D) \to D = - (- D)$
41	40	fveq2d	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{D} = \sqrt{- (- D)}$
42	30	renegcld	$⊢ φ \to - D \in ℝ$
43	42	adantr	$⊢ (φ \land \neg 0 \leq D) \to - D \in ℝ$
44		0red	$⊢ φ \to 0 \in ℝ$
45	30 44	ltnled	$⊢ φ \to (D < 0 \leftrightarrow \neg 0 \leq D)$
46		ltle	$⊢ (D \in ℝ \land 0 \in ℝ) \to (D < 0 \to D \leq 0)$
47	30 44 46	syl2anc	$⊢ φ \to (D < 0 \to D \leq 0)$
48	45 47	sylbird	$⊢ φ \to (\neg 0 \leq D \to D \leq 0)$
49	48	imp	$⊢ (φ \land \neg 0 \leq D) \to D \leq 0$
50	30	le0neg1d	$⊢ φ \to (D \leq 0 \leftrightarrow 0 \leq - D)$
51	50	adantr	$⊢ (φ \land \neg 0 \leq D) \to (D \leq 0 \leftrightarrow 0 \leq - D)$
52	49 51	mpbid	$⊢ (φ \land \neg 0 \leq D) \to 0 \leq - D$
53	43 52	sqrtnegd	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{- (- D)} = i \sqrt{- D}$
54	41 53	eqtrd	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{D} = i \sqrt{- D}$
55		ax-icn	$⊢ i \in ℂ$
56	55	a1i	$⊢ (φ \land \neg 0 \leq D) \to i \in ℂ$
57	31	negcld	$⊢ φ \to - D \in ℂ$
58	57	sqrtcld	$⊢ φ \to \sqrt{- D} \in ℂ$
59	58	adantr	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{- D} \in ℂ$
60	56 59	mulcomd	$⊢ (φ \land \neg 0 \leq D) \to i \sqrt{- D} = \sqrt{- D} i$
61	43 52	resqrtcld	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{- D} \in ℝ$
62		inelr	$⊢ \neg i \in ℝ$
63		eldif	$⊢ i \in (ℂ ∖ ℝ) \leftrightarrow (i \in ℂ \land \neg i \in ℝ)$
64	55 62 63	mpbir2an	$⊢ i \in (ℂ ∖ ℝ)$
65	64	a1i	$⊢ (φ \land \neg 0 \leq D) \to i \in (ℂ ∖ ℝ)$
66	30	lt0neg1d	$⊢ φ \to (D < 0 \leftrightarrow 0 < - D)$
67		ltne	$⊢ (0 \in ℝ \land 0 < - D) \to - D \neq 0$
68	44 67	sylan	$⊢ (φ \land 0 < - D) \to - D \neq 0$
69	42	adantr	$⊢ (φ \land 0 < - D) \to - D \in ℝ$
70		ltle	$⊢ (0 \in ℝ \land - D \in ℝ) \to (0 < - D \to 0 \leq - D)$
71	44 42 70	syl2anc	$⊢ φ \to (0 < - D \to 0 \leq - D)$
72	71	imp	$⊢ (φ \land 0 < - D) \to 0 \leq - D$
73		sqrt00	$⊢ (- D \in ℝ \land 0 \leq - D) \to (\sqrt{- D} = 0 \leftrightarrow - D = 0)$
74	69 72 73	syl2anc	$⊢ (φ \land 0 < - D) \to (\sqrt{- D} = 0 \leftrightarrow - D = 0)$
75	74	bicomd	$⊢ (φ \land 0 < - D) \to (- D = 0 \leftrightarrow \sqrt{- D} = 0)$
76	75	necon3bid	$⊢ (φ \land 0 < - D) \to (- D \neq 0 \leftrightarrow \sqrt{- D} \neq 0)$
77	68 76	mpbid	$⊢ (φ \land 0 < - D) \to \sqrt{- D} \neq 0$
78	77	ex	$⊢ φ \to (0 < - D \to \sqrt{- D} \neq 0)$
79	66 78	sylbid	$⊢ φ \to (D < 0 \to \sqrt{- D} \neq 0)$
80	45 79	sylbird	$⊢ φ \to (\neg 0 \leq D \to \sqrt{- D} \neq 0)$
81	80	imp	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{- D} \neq 0$
82	61 65 81	recnmulnred	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{- D} i \notin ℝ$
83		df-nel	$⊢ \sqrt{- D} i \notin ℝ \leftrightarrow \neg \sqrt{- D} i \in ℝ$
84	82 83	sylib	$⊢ (φ \land \neg 0 \leq D) \to \neg \sqrt{- D} i \in ℝ$
85	60 84	eqneltrd	$⊢ (φ \land \neg 0 \leq D) \to \neg i \sqrt{- D} \in ℝ$
86	54 85	eqneltrd	$⊢ (φ \land \neg 0 \leq D) \to \neg \sqrt{D} \in ℝ$
87	37 86	eldifd	$⊢ (φ \land \neg 0 \leq D) \to \sqrt{D} \in (ℂ ∖ ℝ)$
88	36 87	readdcnnred	$⊢ (φ \land \neg 0 \leq D) \to (- B + \sqrt{D}) \notin ℝ$
89		df-nel	$⊢ (- B + \sqrt{D}) \notin ℝ \leftrightarrow \neg - B + \sqrt{D} \in ℝ$
90	88 89	sylib	$⊢ (φ \land \neg 0 \leq D) \to \neg - B + \sqrt{D} \in ℝ$
91	34 90	eldifd	$⊢ (φ \land \neg 0 \leq D) \to - B + \sqrt{D} \in (ℂ ∖ ℝ)$
92		2cnd	$⊢ φ \to 2 \in ℂ$
93		2ne0	$⊢ 2 \neq 0$
94	93	a1i	$⊢ φ \to 2 \neq 0$
95	92 6 94 2	mulne0d	$⊢ φ \to 2 A \neq 0$
96	95	adantr	$⊢ (φ \land \neg 0 \leq D) \to 2 A \neq 0$
97	22 91 96	cndivrenred	$⊢ (φ \land \neg 0 \leq D) \to (\frac{- B + \sqrt{D}}{2 A}) \notin ℝ$
98		df-nel	$⊢ (\frac{- B + \sqrt{D}}{2 A}) \notin ℝ \leftrightarrow \neg \frac{- B + \sqrt{D}}{2 A} \in ℝ$
99	97 98	sylib	$⊢ (φ \land \neg 0 \leq D) \to \neg \frac{- B + \sqrt{D}}{2 A} \in ℝ$
100	99	ex	$⊢ φ \to (\neg 0 \leq D \to \neg \frac{- B + \sqrt{D}}{2 A} \in ℝ)$
101	100	con4d	$⊢ φ \to (\frac{- B + \sqrt{D}}{2 A} \in ℝ \to 0 \leq D)$
102	101	adantr	$⊢ (φ \land x = \frac{- B + \sqrt{D}}{2 A}) \to (\frac{- B + \sqrt{D}}{2 A} \in ℝ \to 0 \leq D)$
103	18 102	sylbid	$⊢ (φ \land x = \frac{- B + \sqrt{D}}{2 A}) \to (x \in ℝ \to 0 \leq D)$
104	103	ex	$⊢ φ \to (x = \frac{- B + \sqrt{D}}{2 A} \to (x \in ℝ \to 0 \leq D))$
105		eleq1	$⊢ x = \frac{- B - \sqrt{D}}{2 A} \to (x \in ℝ \leftrightarrow \frac{- B - \sqrt{D}}{2 A} \in ℝ)$
106	105	adantl	$⊢ (φ \land x = \frac{- B - \sqrt{D}}{2 A}) \to (x \in ℝ \leftrightarrow \frac{- B - \sqrt{D}}{2 A} \in ℝ)$
107	23 32	subcld	$⊢ φ \to - B - \sqrt{D} \in ℂ$
108	107	adantr	$⊢ (φ \land \neg 0 \leq D) \to - B - \sqrt{D} \in ℂ$
109	36 87	resubcnnred	$⊢ (φ \land \neg 0 \leq D) \to (- B - \sqrt{D}) \notin ℝ$
110		df-nel	$⊢ (- B - \sqrt{D}) \notin ℝ \leftrightarrow \neg - B - \sqrt{D} \in ℝ$
111	109 110	sylib	$⊢ (φ \land \neg 0 \leq D) \to \neg - B - \sqrt{D} \in ℝ$
112	108 111	eldifd	$⊢ (φ \land \neg 0 \leq D) \to - B - \sqrt{D} \in (ℂ ∖ ℝ)$
113	22 112 96	cndivrenred	$⊢ (φ \land \neg 0 \leq D) \to (\frac{- B - \sqrt{D}}{2 A}) \notin ℝ$
114		df-nel	$⊢ (\frac{- B - \sqrt{D}}{2 A}) \notin ℝ \leftrightarrow \neg \frac{- B - \sqrt{D}}{2 A} \in ℝ$
115	113 114	sylib	$⊢ (φ \land \neg 0 \leq D) \to \neg \frac{- B - \sqrt{D}}{2 A} \in ℝ$
116	115	ex	$⊢ φ \to (\neg 0 \leq D \to \neg \frac{- B - \sqrt{D}}{2 A} \in ℝ)$
117	116	con4d	$⊢ φ \to (\frac{- B - \sqrt{D}}{2 A} \in ℝ \to 0 \leq D)$
118	117	adantr	$⊢ (φ \land x = \frac{- B - \sqrt{D}}{2 A}) \to (\frac{- B - \sqrt{D}}{2 A} \in ℝ \to 0 \leq D)$
119	106 118	sylbid	$⊢ (φ \land x = \frac{- B - \sqrt{D}}{2 A}) \to (x \in ℝ \to 0 \leq D)$
120	119	ex	$⊢ φ \to (x = \frac{- B - \sqrt{D}}{2 A} \to (x \in ℝ \to 0 \leq D))$
121	104 120	jaod	$⊢ φ \to ((x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \to (x \in ℝ \to 0 \leq D))$
122	121	com23	$⊢ φ \to (x \in ℝ \to ((x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \to 0 \leq D))$
123	122	imp	$⊢ (φ \land x \in ℝ) \to ((x = \frac{- B + \sqrt{D}}{2 A} \lor x = \frac{- B - \sqrt{D}}{2 A}) \to 0 \leq D)$
124	16 123	sylbid	$⊢ (φ \land x \in ℝ) \to (A x^{2} + B x + C = 0 \to 0 \leq D)$
125	124	rexlimdva	$⊢ φ \to (\exists x \in ℝ A x^{2} + B x + C = 0 \to 0 \leq D)$
126	35	adantr	$⊢ (φ \land 0 \leq D) \to - B \in ℝ$
127	30	adantr	$⊢ (φ \land 0 \leq D) \to D \in ℝ$
128		simpr	$⊢ (φ \land 0 \leq D) \to 0 \leq D$
129	127 128	resqrtcld	$⊢ (φ \land 0 \leq D) \to \sqrt{D} \in ℝ$
130	126 129	readdcld	$⊢ (φ \land 0 \leq D) \to - B + \sqrt{D} \in ℝ$
131	19	a1i	$⊢ (φ \land 0 \leq D) \to 2 \in ℝ$
132	1	adantr	$⊢ (φ \land 0 \leq D) \to A \in ℝ$
133	131 132	remulcld	$⊢ (φ \land 0 \leq D) \to 2 A \in ℝ$
134	95	adantr	$⊢ (φ \land 0 \leq D) \to 2 A \neq 0$
135	130 133 134	redivcld	$⊢ (φ \land 0 \leq D) \to \frac{- B + \sqrt{D}}{2 A} \in ℝ$
136		oveq1	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to x^{2} = {(\frac{- B + \sqrt{D}}{2 A})}^{2}$
137	136	oveq2d	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to A x^{2} = A {(\frac{- B + \sqrt{D}}{2 A})}^{2}$
138		oveq2	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to B x = B (\frac{- B + \sqrt{D}}{2 A})$
139	138	oveq1d	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to B x + C = B (\frac{- B + \sqrt{D}}{2 A}) + C$
140	137 139	oveq12d	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to A x^{2} + B x + C = A {(\frac{- B + \sqrt{D}}{2 A})}^{2} + B (\frac{- B + \sqrt{D}}{2 A}) + C$
141	140	eqeq1d	$⊢ x = \frac{- B + \sqrt{D}}{2 A} \to (A x^{2} + B x + C = 0 \leftrightarrow A {(\frac{- B + \sqrt{D}}{2 A})}^{2} + B (\frac{- B + \sqrt{D}}{2 A}) + C = 0)$
142	141	adantl	$⊢ ((φ \land 0 \leq D) \land x = \frac{- B + \sqrt{D}}{2 A}) \to (A x^{2} + B x + C = 0 \leftrightarrow A {(\frac{- B + \sqrt{D}}{2 A})}^{2} + B (\frac{- B + \sqrt{D}}{2 A}) + C = 0)$
143		eqidd	$⊢ (φ \land 0 \leq D) \to \frac{- B + \sqrt{D}}{2 A} = \frac{- B + \sqrt{D}}{2 A}$
144	143	orcd	$⊢ (φ \land 0 \leq D) \to (\frac{- B + \sqrt{D}}{2 A} = \frac{- B + \sqrt{D}}{2 A} \lor \frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A})$
145	6	adantr	$⊢ (φ \land 0 \leq D) \to A \in ℂ$
146	2	adantr	$⊢ (φ \land 0 \leq D) \to A \neq 0$
147	9	adantr	$⊢ (φ \land 0 \leq D) \to B \in ℂ$
148	11	adantr	$⊢ (φ \land 0 \leq D) \to C \in ℂ$
149	92 6	mulcld	$⊢ φ \to 2 A \in ℂ$
150	33 149 95	divcld	$⊢ φ \to \frac{- B + \sqrt{D}}{2 A} \in ℂ$
151	150	adantr	$⊢ (φ \land 0 \leq D) \to \frac{- B + \sqrt{D}}{2 A} \in ℂ$
152	5	adantr	$⊢ (φ \land 0 \leq D) \to D = B^{2} - 4 A C$
153	145 146 147 148 151 152	quad	$⊢ (φ \land 0 \leq D) \to (A {(\frac{- B + \sqrt{D}}{2 A})}^{2} + B (\frac{- B + \sqrt{D}}{2 A}) + C = 0 \leftrightarrow (\frac{- B + \sqrt{D}}{2 A} = \frac{- B + \sqrt{D}}{2 A} \lor \frac{- B + \sqrt{D}}{2 A} = \frac{- B - \sqrt{D}}{2 A}))$
154	144 153	mpbird	$⊢ (φ \land 0 \leq D) \to A {(\frac{- B + \sqrt{D}}{2 A})}^{2} + B (\frac{- B + \sqrt{D}}{2 A}) + C = 0$
155	135 142 154	rspcedvd	$⊢ (φ \land 0 \leq D) \to \exists x \in ℝ A x^{2} + B x + C = 0$
156	155	ex	$⊢ φ \to (0 \leq D \to \exists x \in ℝ A x^{2} + B x + C = 0)$
157	125 156	impbid	$⊢ φ \to (\exists x \in ℝ A x^{2} + B x + C = 0 \leftrightarrow 0 \leq D)$

Metamath Proof Explorer

Theorem requad01

Proof