Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	requad2.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	requad2.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	requad2.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	requad2.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion	requad1	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 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	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
8	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ≠ 0 )
9	3	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℂ )
11	4	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
12	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐶 ∈ ℂ )
13		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
14	13	adantl	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
15	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
16	7 8 10 12 14 15	quad	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐷 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
17	16	reubidva	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ∃! 𝑥 ∈ ℝ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )
18	3	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - 𝐵 ∈ ℝ )
20	3	resqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
21		4re	⊢ 4 ∈ ℝ
22	21	a1i	⊢ ( 𝜑 → 4 ∈ ℝ )
23	1 4	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
24	22 23	remulcld	⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ )
25	20 24	resubcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℝ )
26	5 25	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
27		resqrtcl	⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
28	26 27	sylan	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
29	19 28	readdcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 + ( √ ‘ 𝐷 ) ) ∈ ℝ )
30		2re	⊢ 2 ∈ ℝ
31	30	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
32	31 1	remulcld	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
33	32	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℝ )
34		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
35		2ne0	⊢ 2 ≠ 0
36	35	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
37	34 6 36 2	mulne0d	⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
38	37	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ≠ 0 )
39	29 33 38	redivcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
40	19 28	resubcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 − ( √ ‘ 𝐷 ) ) ∈ ℝ )
41	40 33 38	redivcld	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ )
42		euoreqb	⊢ ( ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ∧ ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
43	39 41 42	syl2anc	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑥 ∈ ℝ ( 𝑥 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑥 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ↔ ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) )
44	9	negcld	⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
45	26	recnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
46	45	sqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
47	32	recnd	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
48	44 46 47 37	divdird	⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
49	48	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
50	44 46 47 37	divsubdird	⊢ ( 𝜑 → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
52	44 47 37	divcld	⊢ ( 𝜑 → ( - 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
53	52	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
54	46 47 37	divcld	⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
55	54	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
56	53 55	negsubd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 / ( 2 · 𝐴 ) ) + - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) − ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
57	46	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
58	47	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( 2 · 𝐴 ) ∈ ℂ )
59	57 58 38	divnegd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) )
60	59	oveq2d	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 / ( 2 · 𝐴 ) ) + - ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
61	51 56 60	3eqtr2d	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
62	49 61	eqeq12d	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ) )
63	46	negcld	⊢ ( 𝜑 → - ( √ ‘ 𝐷 ) ∈ ℂ )
64	63 47 37	divcld	⊢ ( 𝜑 → ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
65	64	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ∈ ℂ )
66	53 55 65	addcand	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ↔ ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) )
67		div11	⊢ ( ( ( √ ‘ 𝐷 ) ∈ ℂ ∧ - ( √ ‘ 𝐷 ) ∈ ℂ ∧ ( ( 2 · 𝐴 ) ∈ ℂ ∧ ( 2 · 𝐴 ) ≠ 0 ) ) → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
68	46 63 47 37 67	syl112anc	⊢ ( 𝜑 → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
69	68	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) = ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ) )
70	57	eqnegd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ ( √ ‘ 𝐷 ) = 0 ) )
71		sqrt00	⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
72	26 71	sylan	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = 0 ↔ 𝐷 = 0 ) )
73	70 72	bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( √ ‘ 𝐷 ) = - ( √ ‘ 𝐷 ) ↔ 𝐷 = 0 ) )
74	66 69 73	3bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ 𝐷 ) / ( 2 · 𝐴 ) ) ) ↔ 𝐷 = 0 ) )
75	62 74	bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ↔ 𝐷 = 0 ) )
76	17 43 75	3bitrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝐷 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )
77	76	expcom	⊢ ( 0 ≤ 𝐷 → ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) ) )
78	1 2 3 4 5	requad01	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 0 ≤ 𝐷 ) )
79	78	notbid	⊢ ( 𝜑 → ( ¬ ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ ¬ 0 ≤ 𝐷 ) )
80	79	biimparc	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ¬ ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
81		reurex	⊢ ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
82	80 81	nsyl	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ¬ ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 )
83	82	pm2.21d	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 → 𝐷 = 0 ) )
84		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
85	26 84	ltnled	⊢ ( 𝜑 → ( 𝐷 < 0 ↔ ¬ 0 ≤ 𝐷 ) )
86	85	biimparc	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → 𝐷 < 0 )
87	86	lt0ne0d	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → 𝐷 ≠ 0 )
88		eqneqall	⊢ ( 𝐷 = 0 → ( 𝐷 ≠ 0 → ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
89	87 88	syl5com	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( 𝐷 = 0 → ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ) )
90	83 89	impbid	⊢ ( ( ¬ 0 ≤ 𝐷 ∧ 𝜑 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )
91	90	ex	⊢ ( ¬ 0 ≤ 𝐷 → ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) ) )
92	77 91	pm2.61i	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ ℝ ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( ( 𝐵 · 𝑥 ) + 𝐶 ) ) = 0 ↔ 𝐷 = 0 ) )