requad01 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > requad01		Structured version Visualization version GIF version

Theorem requad01 48924

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

**Hypotheses**
Ref	Expression
requad2.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
requad2.z	⊢ (𝜑 → 𝐴 ≠ 0)
requad2.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
requad2.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
requad2.d	⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))

**Assertion**
Ref	Expression
requad01	⊢ (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐶 𝑥,𝐷 𝜑,𝑥

**Proof of Theorem requad01**
Step	Hyp	Ref	Expression
1		requad2.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2	1	recnd 11364	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	2	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ)
4		requad2.z	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 0)
5	4	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ≠ 0)
6		requad2.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
7	6	recnd 11364	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
8	7	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ)
9		requad2.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℝ)
10	9	recnd 11364	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
11	10	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐶 ∈ ℂ)
12		recn 11317	. . . . . 6 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
13	12	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
14		requad2.d	. . . . . 6 ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
15	14	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
16	3, 5, 8, 11, 13, 15	quad 27198	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
17		eleq1 2852	. . . . . . . . . 10 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ ↔ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
18	17	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ ↔ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
19		2re 12444	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
20	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℝ)
21	20, 1	remulcld 11366	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝐴) ∈ ℝ)
22	21	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ)
23	7	negcld 11683	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -𝐵 ∈ ℂ)
24	6	resqcld 14295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵↑2) ∈ ℝ)
25		4re 12454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 4 ∈ ℝ
26	25	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 4 ∈ ℝ)
27	1, 9	remulcld 11366	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℝ)
28	26, 27	remulcld 11366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℝ)
29	24, 28	resubcld 11771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℝ)
30	14, 29	eqeltrd 2864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ ℝ)
31	30	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℂ)
32	31	sqrtcld 15636	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝐷) ∈ ℂ)
33	23, 32	addcld 11355	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -𝐵 + (√‘𝐷)) ∈ ℂ)
34	33	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ( -𝐵 + (√‘𝐷)) ∈ ℂ)
35	6	renegcld 11770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝐵 ∈ ℝ)
36	35	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → -𝐵 ∈ ℝ)
37	32	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℂ)
38	31	negnegd 11687	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → - -𝐷 = 𝐷)
39	38	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → - -𝐷 = 𝐷)
40	39	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → 𝐷 = - -𝐷)
41	40	fveq2d 6912	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) = (√‘ - -𝐷))
42	30	renegcld 11770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → -𝐷 ∈ ℝ)
43	42	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → -𝐷 ∈ ℝ)
44		0red 11338	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 ∈ ℝ)
45	30, 44	ltnled 11484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐷 < 0 ↔ ¬ 0 ≤ 𝐷))
46		ltle 11425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐷 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐷 < 0 → 𝐷 ≤ 0))
47	30, 44, 46	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐷 < 0 → 𝐷 ≤ 0))
48	45, 47	sylbird 263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (¬ 0 ≤ 𝐷 → 𝐷 ≤ 0))
49	48	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → 𝐷 ≤ 0)
50	30	le0neg1d 11914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐷 ≤ 0 ↔ 0 ≤ -𝐷))
51	50	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (𝐷 ≤ 0 ↔ 0 ≤ -𝐷))
52	49, 51	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → 0 ≤ -𝐷)
53	43, 52	sqrtnegd 15618	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘ - -𝐷) = (i · (√‘ -𝐷)))
54	41, 53	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) = (i · (√‘ -𝐷)))
55		ax-icn 11286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ i ∈ ℂ
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → i ∈ ℂ)
57	31	negcld 11683	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → -𝐷 ∈ ℂ)
58	57	sqrtcld 15636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (√‘ -𝐷) ∈ ℂ)
59	58	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘ -𝐷) ∈ ℂ)
60	56, 59	mulcomd 11357	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (i · (√‘ -𝐷)) = ((√‘ -𝐷) · i))
61	43, 52	resqrtcld 15614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘ -𝐷) ∈ ℝ)
62		inelr 12337	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ i ∈ ℝ
63		eldif 4052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (i ∈ (ℂ ∖ ℝ) ↔ (i ∈ ℂ ∧ ¬ i ∈ ℝ))
64	55, 62, 63	mpbir2an 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ i ∈ (ℂ ∖ ℝ)
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → i ∈ (ℂ ∖ ℝ))
66	30	lt0neg1d 11912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐷 < 0 ↔ 0 < -𝐷))
67		ltne 11434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℝ ∧ 0 < -𝐷) → -𝐷 ≠ 0)
68	44, 67	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 0 < -𝐷) → -𝐷 ≠ 0)
69	42	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 0 < -𝐷) → -𝐷 ∈ ℝ)
70		ltle 11425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((0 ∈ ℝ ∧ -𝐷 ∈ ℝ) → (0 < -𝐷 → 0 ≤ -𝐷))
71	44, 42, 70	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (0 < -𝐷 → 0 ≤ -𝐷))
72	71	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 0 < -𝐷) → 0 ≤ -𝐷)
73		sqrt00 15459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (( -𝐷 ∈ ℝ ∧ 0 ≤ -𝐷) → ((√‘ -𝐷) = 0 ↔ -𝐷 = 0))
74	69, 72, 73	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 0 < -𝐷) → ((√‘ -𝐷) = 0 ↔ -𝐷 = 0))
75	74	bicomd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 0 < -𝐷) → ( -𝐷 = 0 ↔ (√‘ -𝐷) = 0))
76	75	necon3bid 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 0 < -𝐷) → ( -𝐷 ≠ 0 ↔ (√‘ -𝐷) ≠ 0))
77	68, 76	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 0 < -𝐷) → (√‘ -𝐷) ≠ 0)
78	77	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 < -𝐷 → (√‘ -𝐷) ≠ 0))
79	66, 78	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐷 < 0 → (√‘ -𝐷) ≠ 0))
80	45, 79	sylbird 263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (¬ 0 ≤ 𝐷 → (√‘ -𝐷) ≠ 0))
81	80	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘ -𝐷) ≠ 0)
82	61, 65, 81	recnmulnred 48580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ((√‘ -𝐷) · i) ∉ ℝ)
83		df-nel 3066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((√‘ -𝐷) · i) ∉ ℝ ↔ ¬ ((√‘ -𝐷) · i) ∈ ℝ)
84	82, 83	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ ((√‘ -𝐷) · i) ∈ ℝ)
85	60, 84	eqneltrd 2884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (i · (√‘ -𝐷)) ∈ ℝ)
86	54, 85	eqneltrd 2884	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (√‘𝐷) ∈ ℝ)
87	37, 86	eldifd 4053	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (√‘𝐷) ∈ (ℂ ∖ ℝ))
88	36, 87	readdcnnred 48578	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ( -𝐵 + (√‘𝐷)) ∉ ℝ)
89		df-nel 3066	. . . . . . . . . . . . . . . 16 ⊢ (( -𝐵 + (√‘𝐷)) ∉ ℝ ↔ ¬ ( -𝐵 + (√‘𝐷)) ∈ ℝ)
90	88, 89	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ ( -𝐵 + (√‘𝐷)) ∈ ℝ)
91	34, 90	eldifd 4053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ( -𝐵 + (√‘𝐷)) ∈ (ℂ ∖ ℝ))
92		2cnd 12448	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
93		2ne0 12476	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
94	93	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ≠ 0)
95	92, 2, 94, 4	mulne0d 11995	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
96	95	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0)
97	22, 91, 96	cndivrenred 48581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ)
98		df-nel 3066	. . . . . . . . . . . . 13 ⊢ ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ ↔ ¬ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
99	97, 98	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
100	99	ex 418	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 0 ≤ 𝐷 → ¬ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
101	100	con4d 116	. . . . . . . . . 10 ⊢ (𝜑 → ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
102	101	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) → ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
103	18, 102	sylbid 243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ → 0 ≤ 𝐷))
104	103	ex 418	. . . . . . 7 ⊢ (𝜑 → (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ → 0 ≤ 𝐷)))
105		eleq1 2852	. . . . . . . . . 10 ⊢ (𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ ↔ (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
106	105	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ ↔ (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
107	23, 32	subcld 11696	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -𝐵 − (√‘𝐷)) ∈ ℂ)
108	107	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ( -𝐵 − (√‘𝐷)) ∈ ℂ)
109	36, 87	resubcnnred 48579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ( -𝐵 − (√‘𝐷)) ∉ ℝ)
110		df-nel 3066	. . . . . . . . . . . . . . . 16 ⊢ (( -𝐵 − (√‘𝐷)) ∉ ℝ ↔ ¬ ( -𝐵 − (√‘𝐷)) ∈ ℝ)
111	109, 110	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ ( -𝐵 − (√‘𝐷)) ∈ ℝ)
112	108, 111	eldifd 4053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ( -𝐵 − (√‘𝐷)) ∈ (ℂ ∖ ℝ))
113	22, 112, 96	cndivrenred 48581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ)
114		df-nel 3066	. . . . . . . . . . . . 13 ⊢ ((( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∉ ℝ ↔ ¬ (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
115	113, 114	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐷) → ¬ (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
116	115	ex 418	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 0 ≤ 𝐷 → ¬ (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ))
117	116	con4d 116	. . . . . . . . . 10 ⊢ (𝜑 → ((( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
118	117	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))) → ((( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ → 0 ≤ 𝐷))
119	106, 118	sylbid 243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ → 0 ≤ 𝐷))
120	119	ex 418	. . . . . . 7 ⊢ (𝜑 → (𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)) → (𝑥 ∈ ℝ → 0 ≤ 𝐷)))
121	104, 120	jaod 873	. . . . . 6 ⊢ (𝜑 → ((𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))) → (𝑥 ∈ ℝ → 0 ≤ 𝐷)))
122	121	com23 87	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ → ((𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))) → 0 ≤ 𝐷)))
123	122	imp 412	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))) → 0 ≤ 𝐷))
124	16, 123	sylbid 243	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → 0 ≤ 𝐷))
125	124	rexlimdva 3167	. 2 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → 0 ≤ 𝐷))
126	35	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → -𝐵 ∈ ℝ)
127	30	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐷 ∈ ℝ)
128		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 0 ≤ 𝐷)
129	127, 128	resqrtcld 15614	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℝ)
130	126, 129	readdcld 11365	. . . . 5 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ( -𝐵 + (√‘𝐷)) ∈ ℝ)
131	19	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 2 ∈ ℝ)
132	1	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ∈ ℝ)
133	131, 132	remulcld 11366	. . . . 5 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ)
134	95	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0)
135	130, 133, 134	redivcld 12172	. . . 4 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ)
136		oveq1 7450	. . . . . . . 8 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝑥↑2) = ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2))
137	136	oveq2d 7459	. . . . . . 7 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝐴 · (𝑥↑2)) = (𝐴 · ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)))
138		oveq2 7451	. . . . . . . 8 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (𝐵 · 𝑥) = (𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))))
139	138	oveq1d 7458	. . . . . . 7 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → ((𝐵 · 𝑥) + 𝐶) = ((𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶))
140	137, 139	oveq12d 7461	. . . . . 6 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = ((𝐴 · ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)))
141	140	eqeq1d 2765	. . . . 5 ⊢ (𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ((𝐴 · ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0))
142	141	adantl 487	. . . 4 ⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ((𝐴 · ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0))
143		eqidd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)))
144	143	orcd 887	. . . . 5 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴))))
145	2	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ∈ ℂ)
146	4	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐴 ≠ 0)
147	7	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐵 ∈ ℂ)
148	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐶 ∈ ℂ)
149	92, 2	mulcld 11356	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
150	33, 149, 95	divcld 12120	. . . . . . 7 ⊢ (𝜑 → (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℂ)
151	150	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℂ)
152	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
153	145, 146, 147, 148, 151, 152	quad 27198	. . . . 5 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((𝐴 · ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0 ↔ ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) = (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ (( -𝐵 + (√‘𝐷)) / (2 · 𝐴)) = (( -𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
154	144, 153	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((𝐴 · ((( -𝐵 + (√‘𝐷)) / (2 · 𝐴))↑2)) + ((𝐵 · (( -𝐵 + (√‘𝐷)) / (2 · 𝐴))) + 𝐶)) = 0)
155	135, 142, 154	rspcedvd 3582	. . 3 ⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)
156	155	ex 418	. 2 ⊢ (𝜑 → (0 ≤ 𝐷 → ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0))
157	125, 156	impbid 215	1 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∉ wnel 3065 ∃wrex 3090 ∖ cdif 4048 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ℂcc 11225 ℝcr 11226 0cc0 11227 ici 11229 + caddc 11230 · cmul 11232 < clt 11370 ≤ cle 11371 − cmin 11568 -cneg 11569 / cdiv 12000 2c2 12424 4c4 12426 ↑cexp 14231 √csqrt 15429

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-er 8745 df-en 9002 df-dom 9003 df-sdom 9004 df-sup 9461 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-n0 12634 df-z 12721 df-uz 12993 df-rp 13148 df-seq 14172 df-exp 14232 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432

This theorem is used by: requad1 48925 requad2 48926

W3C validator