Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	requad2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	requad2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	requad2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	requad2.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion	requad01	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 0 ≤ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		requad2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		requad2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		requad2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		requad2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5		requad2.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
6	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ≠ 0 )
9	3	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℂ )
11	4	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐶 ∈ ℂ )
13		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
16	7 8 10 12 14 15	quad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
17		eleq1	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
19		2re	⊢ 2 ∈ ℝ
20	19	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
21	20 1	remulcld	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
22	21	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
23	9	negcld	⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
24	3	resqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
25		4re	⊢ 4 ∈ ℝ
26	25	a1i	⊢ ( 𝜑 → 4 ∈ ℝ )
27	1 4	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
28	26 27	remulcld	⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ )
29	24 28	resubcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℝ )
30	5 29	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
31	30	recnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
32	31	sqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
33	23 32	addcld	⊢ ( 𝜑 → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ )
34	33	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℂ )
35	3	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
36	35	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
37	32	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
38	31	negnegd	⊢ ( 𝜑 → - - 𝐷 = 𝐷 )
39	38	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → - - 𝐷 = 𝐷 )
40	39	eqcomd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → 𝐷 = - - 𝐷 )
41	40	fveq2d	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) = ( √ ‘ - - 𝐷 ) )
42	30	renegcld	⊢ ( 𝜑 → - 𝐷 ∈ ℝ )
43	42	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → - 𝐷 ∈ ℝ )
44		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
45	30 44	ltnled	⊢ ( 𝜑 → ( 𝐷 < 0 ↔ ¬ 0 ≤ 𝐷 ) )
46		ltle	⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐷 < 0 → 𝐷 ≤ 0 ) )
47	30 44 46	syl2anc	⊢ ( 𝜑 → ( 𝐷 < 0 → 𝐷 ≤ 0 ) )
48	45 47	sylbird	⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → 𝐷 ≤ 0 ) )
49	48	imp	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → 𝐷 ≤ 0 )
50	30	le0neg1d	⊢ ( 𝜑 → ( 𝐷 ≤ 0 ↔ 0 ≤ - 𝐷 ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( 𝐷 ≤ 0 ↔ 0 ≤ - 𝐷 ) )
52	49 51	mpbid	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → 0 ≤ - 𝐷 )
53	43 52	sqrtnegd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - - 𝐷 ) = ( i · ( √ ‘ - 𝐷 ) ) )
54	41 53	eqtrd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) = ( i · ( √ ‘ - 𝐷 ) ) )
55		ax-icn	⊢ i ∈ ℂ
56	55	a1i	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → i ∈ ℂ )
57	31	negcld	⊢ ( 𝜑 → - 𝐷 ∈ ℂ )
58	57	sqrtcld	⊢ ( 𝜑 → ( √ ‘ - 𝐷 ) ∈ ℂ )
59	58	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - 𝐷 ) ∈ ℂ )
60	56 59	mulcomd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( i · ( √ ‘ - 𝐷 ) ) = ( ( √ ‘ - 𝐷 ) · i ) )
61	43 52	resqrtcld	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - 𝐷 ) ∈ ℝ )
62		inelr	⊢ ¬ i ∈ ℝ
63		eldif	⊢ ( i ∈ ( ℂ ∖ ℝ ) ↔ ( i ∈ ℂ ∧ ¬ i ∈ ℝ ) )
64	55 62 63	mpbir2an	⊢ i ∈ ( ℂ ∖ ℝ )
65	64	a1i	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → i ∈ ( ℂ ∖ ℝ ) )
66	30	lt0neg1d	⊢ ( 𝜑 → ( 𝐷 < 0 ↔ 0 < - 𝐷 ) )
67		ltne	⊢ ( ( 0 ∈ ℝ ∧ 0 < - 𝐷 ) → - 𝐷 ≠ 0 )
68	44 67	sylan	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → - 𝐷 ≠ 0 )
69	42	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → - 𝐷 ∈ ℝ )
70		ltle	⊢ ( ( 0 ∈ ℝ ∧ - 𝐷 ∈ ℝ ) → ( 0 < - 𝐷 → 0 ≤ - 𝐷 ) )
71	44 42 70	syl2anc	⊢ ( 𝜑 → ( 0 < - 𝐷 → 0 ≤ - 𝐷 ) )
72	71	imp	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → 0 ≤ - 𝐷 )
73		sqrt00	⊢ ( ( - 𝐷 ∈ ℝ ∧ 0 ≤ - 𝐷 ) → ( ( √ ‘ - 𝐷 ) = 0 ↔ - 𝐷 = 0 ) )
74	69 72 73	syl2anc	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( ( √ ‘ - 𝐷 ) = 0 ↔ - 𝐷 = 0 ) )
75	74	bicomd	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( - 𝐷 = 0 ↔ ( √ ‘ - 𝐷 ) = 0 ) )
76	75	necon3bid	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( - 𝐷 ≠ 0 ↔ ( √ ‘ - 𝐷 ) ≠ 0 ) )
77	68 76	mpbid	⊢ ( ( 𝜑 ∧ 0 < - 𝐷 ) → ( √ ‘ - 𝐷 ) ≠ 0 )
78	77	ex	⊢ ( 𝜑 → ( 0 < - 𝐷 → ( √ ‘ - 𝐷 ) ≠ 0 ) )
79	66 78	sylbid	⊢ ( 𝜑 → ( 𝐷 < 0 → ( √ ‘ - 𝐷 ) ≠ 0 ) )
80	45 79	sylbird	⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ( √ ‘ - 𝐷 ) ≠ 0 ) )
81	80	imp	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ - 𝐷 ) ≠ 0 )
82	61 65 81	recnmulnred	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( ( √ ‘ - 𝐷 ) · i ) ∉ ℝ )
83		df-nel	⊢ ( ( ( √ ‘ - 𝐷 ) · i ) ∉ ℝ ↔ ¬ ( ( √ ‘ - 𝐷 ) · i ) ∈ ℝ )
84	82 83	sylib	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( ( √ ‘ - 𝐷 ) · i ) ∈ ℝ )
85	60 84	eqneltrd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( i · ( √ ‘ - 𝐷 ) ) ∈ ℝ )
86	54 85	eqneltrd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( √ ‘ 𝐷 ) ∈ ℝ )
87	37 86	eldifd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ( ℂ ∖ ℝ ) )
88	36 87	readdcnnred	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∉ ℝ )
89		df-nel	⊢ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∉ ℝ ↔ ¬ ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
90	88 89	sylib	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
91	34 90	eldifd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ( ℂ ∖ ℝ ) )
92		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
93		2ne0	⊢ 2 ≠ 0
94	93	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
95	92 6 94 2	mulne0d	⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
96	95	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
97	22 91 96	cndivrenred	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ )
98		df-nel	⊢ ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ ↔ ¬ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
99	97 98	sylib	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
100	99	ex	⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ¬ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
101	100	con4d	⊢ ( 𝜑 → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
102	101	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
103	18 102	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) )
104	103	ex	⊢ ( 𝜑 → ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) ) )
105		eleq1	⊢ ( 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
106	105	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ ↔ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
107	23 32	subcld	⊢ ( 𝜑 → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ )
108	107	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℂ )
109	36 87	resubcnnred	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∉ ℝ )
110		df-nel	⊢ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∉ ℝ ↔ ¬ ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
111	109 110	sylib	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
112	108 111	eldifd	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ( ℂ ∖ ℝ ) )
113	22 112 96	cndivrenred	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ )
114		df-nel	⊢ ( ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∉ ℝ ↔ ¬ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
115	113 114	sylib	⊢ ( ( 𝜑 ∧ ¬ 0 ≤ 𝐷 ) → ¬ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
116	115	ex	⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐷 → ¬ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) )
117	116	con4d	⊢ ( 𝜑 → ( ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
118	117	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ → 0 ≤ 𝐷 ) )
119	106 118	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) )
120	119	ex	⊢ ( 𝜑 → ( 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) ) )
121	104 120	jaod	⊢ ( 𝜑 → ( ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( 𝑥 ∈ ℝ → 0 ≤ 𝐷 ) ) )
122	121	com23	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ → ( ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → 0 ≤ 𝐷 ) ) )
123	122	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → 0 ≤ 𝐷 ) )
124	16 123	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → 0 ≤ 𝐷 ) )
125	124	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → 0 ≤ 𝐷 ) )
126	35	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
127	30	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐷 ∈ ℝ )
128		simpr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 0 ≤ 𝐷 )
129	127 128	resqrtcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
130	126 129	readdcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
131	19	a1i	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 2 ∈ ℝ )
132	1	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ∈ ℝ )
133	131 132	remulcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
134	95	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
135	130 133 134	redivcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
136		oveq1	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝑥 ↑ 2 ) = ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) )
137	136	oveq2d	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) )
138		oveq2	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
139	138	oveq1d	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( ( 𝐵 · 𝑥 ) + 𝐶 ) = ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) )
140	137 139	oveq12d	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) )
141	140	eqeq1d	⊢ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 ) )
142	141	adantl	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 ) )
143		eqidd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) )
144	143	orcd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
145	6	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ∈ ℂ )
146	2	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐴 ≠ 0 )
147	9	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐵 ∈ ℂ )
148	11	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐶 ∈ ℂ )
149	92 6	mulcld	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
150	33 149 95	divcld	⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
151	150	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
152	5	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
153	145 146 147 148 151 152	quad	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 ↔ ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
154	144 153	mpbird	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( 𝐴 · ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↑ 2 ) ) + ( ( 𝐵 · ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) + 𝐶 ) ) = 0 )
155	135 142 154	rspcedvd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
156	155	ex	⊢ ( 𝜑 → ( 0 ≤ 𝐷 → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
157	125 156	impbid	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 0 ≤ 𝐷 ) )