Proof of Theorem quad1
| Step | Hyp | Ref
| Expression |
| 1 | | quad1.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) |
| 3 | | quad1.z |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ 0) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ≠ 0) |
| 5 | | quad1.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 6 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
| 7 | | quad1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 8 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐶 ∈ ℂ) |
| 9 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
| 10 | | quad1.d |
. . . . 5
⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) |
| 12 | 2, 4, 6, 8, 9, 11 | quad 26883 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) |
| 13 | 12 | reubidva 3396 |
. 2
⊢ (𝜑 → (∃!𝑥 ∈ ℂ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ∃!𝑥 ∈ ℂ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) |
| 14 | 5 | negcld 11607 |
. . . . 5
⊢ (𝜑 → -𝐵 ∈ ℂ) |
| 15 | 5 | sqcld 14184 |
. . . . . . . 8
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
| 16 | | 4cn 12351 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
| 17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℂ) |
| 18 | 1, 7 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
| 19 | 17, 18 | mulcld 11281 |
. . . . . . . 8
⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ) |
| 20 | 15, 19 | subcld 11620 |
. . . . . . 7
⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ) |
| 21 | 10, 20 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℂ) |
| 22 | 21 | sqrtcld 15476 |
. . . . 5
⊢ (𝜑 → (√‘𝐷) ∈
ℂ) |
| 23 | 14, 22 | addcld 11280 |
. . . 4
⊢ (𝜑 → (-𝐵 + (√‘𝐷)) ∈ ℂ) |
| 24 | | 2cnd 12344 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℂ) |
| 25 | 24, 1 | mulcld 11281 |
. . . 4
⊢ (𝜑 → (2 · 𝐴) ∈
ℂ) |
| 26 | | 2ne0 12370 |
. . . . . 6
⊢ 2 ≠
0 |
| 27 | 26 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ≠ 0) |
| 28 | 24, 1, 27, 3 | mulne0d 11915 |
. . . 4
⊢ (𝜑 → (2 · 𝐴) ≠ 0) |
| 29 | 23, 25, 28 | divcld 12043 |
. . 3
⊢ (𝜑 → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℂ) |
| 30 | 14, 22 | subcld 11620 |
. . . 4
⊢ (𝜑 → (-𝐵 − (√‘𝐷)) ∈ ℂ) |
| 31 | 30, 25, 28 | divcld 12043 |
. . 3
⊢ (𝜑 → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℂ) |
| 32 | | euoreqb 47121 |
. . 3
⊢
((((-𝐵 +
(√‘𝐷)) / (2
· 𝐴)) ∈ ℂ
∧ ((-𝐵 −
(√‘𝐷)) / (2
· 𝐴)) ∈
ℂ) → (∃!𝑥
∈ ℂ (𝑥 =
((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) |
| 33 | 29, 31, 32 | syl2anc 584 |
. 2
⊢ (𝜑 → (∃!𝑥 ∈ ℂ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) |
| 34 | 14, 22, 25, 28 | divdird 12081 |
. . . 4
⊢ (𝜑 → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴)))) |
| 35 | 14, 22, 25, 28 | divsubdird 12082 |
. . . . 5
⊢ (𝜑 → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) |
| 36 | 14, 25, 28 | divcld 12043 |
. . . . . 6
⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ) |
| 37 | 22, 25, 28 | divcld 12043 |
. . . . . 6
⊢ (𝜑 → ((√‘𝐷) / (2 · 𝐴)) ∈
ℂ) |
| 38 | 36, 37 | negsubd 11626 |
. . . . 5
⊢ (𝜑 → ((-𝐵 / (2 · 𝐴)) + -((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) |
| 39 | 22, 25, 28 | divnegd 12056 |
. . . . . 6
⊢ (𝜑 → -((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴))) |
| 40 | 39 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((-𝐵 / (2 · 𝐴)) + -((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴)))) |
| 41 | 35, 38, 40 | 3eqtr2d 2783 |
. . . 4
⊢ (𝜑 → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴)))) |
| 42 | 34, 41 | eqeq12d 2753 |
. . 3
⊢ (𝜑 → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))))) |
| 43 | 22 | negcld 11607 |
. . . . . 6
⊢ (𝜑 → -(√‘𝐷) ∈
ℂ) |
| 44 | 43, 25, 28 | divcld 12043 |
. . . . 5
⊢ (𝜑 → (-(√‘𝐷) / (2 · 𝐴)) ∈
ℂ) |
| 45 | 36, 37, 44 | addcand 11464 |
. . . 4
⊢ (𝜑 → (((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))) ↔ ((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)))) |
| 46 | | div11 11950 |
. . . . 5
⊢
(((√‘𝐷)
∈ ℂ ∧ -(√‘𝐷) ∈ ℂ ∧ ((2 · 𝐴) ∈ ℂ ∧ (2
· 𝐴) ≠ 0)) →
(((√‘𝐷) / (2
· 𝐴)) =
(-(√‘𝐷) / (2
· 𝐴)) ↔
(√‘𝐷) =
-(√‘𝐷))) |
| 47 | 22, 43, 25, 28, 46 | syl112anc 1376 |
. . . 4
⊢ (𝜑 → (((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)) ↔ (√‘𝐷) = -(√‘𝐷))) |
| 48 | 22 | eqnegd 11988 |
. . . . 5
⊢ (𝜑 → ((√‘𝐷) = -(√‘𝐷) ↔ (√‘𝐷) = 0)) |
| 49 | | cnsqrt00 15431 |
. . . . . 6
⊢ (𝐷 ∈ ℂ →
((√‘𝐷) = 0
↔ 𝐷 =
0)) |
| 50 | 21, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → ((√‘𝐷) = 0 ↔ 𝐷 = 0)) |
| 51 | 48, 50 | bitrd 279 |
. . . 4
⊢ (𝜑 → ((√‘𝐷) = -(√‘𝐷) ↔ 𝐷 = 0)) |
| 52 | 45, 47, 51 | 3bitrd 305 |
. . 3
⊢ (𝜑 → (((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))) ↔ 𝐷 = 0)) |
| 53 | 42, 52 | bitrd 279 |
. 2
⊢ (𝜑 → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ 𝐷 = 0)) |
| 54 | 13, 33, 53 | 3bitrd 305 |
1
⊢ (𝜑 → (∃!𝑥 ∈ ℂ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) |