Metamath Proof Explorer

Theorem quad2

Description: The quadratic equation, without specifying the particular branch D to the square root. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses quad.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
quad.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
quad.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
quad.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
quad.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
quad2.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
quad2.2 ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion quad2 ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( 𝑋 = ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quad.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 quad.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 quad.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4 quad.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 quad.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6 quad2.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
7 quad2.2 ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
8 2cn ⊢ 2 ∈ ℂ
9 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℂ )
10 8 1 9 sylancr ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
11 10 5 mulcld ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · 𝑋 ) ∈ ℂ )
12 11 3 addcld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ∈ ℂ )
13 12 sqcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) ∈ ℂ )
14 6 sqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
15 13 14 subeq0ad ⊢ ( 𝜑 → ( ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ↔ ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) ) )
16 5 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
17 1 16 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
18 3 5 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ℂ )
19 18 4 addcld ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) + 𝐶 ) ∈ ℂ )
20 17 19 addcld ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ∈ ℂ )
21 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
22 4cn ⊢ 4 ∈ ℂ
23 mulcl ⊢ ( ( 4 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 4 · 𝐴 ) ∈ ℂ )
24 22 1 23 sylancr ⊢ ( 𝜑 → ( 4 · 𝐴 ) ∈ ℂ )
25 22 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
26 4ne0 ⊢ 4 ≠ 0
27 26 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
28 25 1 27 2 mulne0d ⊢ ( 𝜑 → ( 4 · 𝐴 ) ≠ 0 )
29 20 21 24 28 mulcand ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) = ( ( 4 · 𝐴 ) · 0 ) ↔ ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ) )
30 11 sqcld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) ∈ ℂ )
31 11 3 mulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ∈ ℂ )
32 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ∈ ℂ ) → ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ∈ ℂ )
33 8 31 32 sylancr ⊢ ( 𝜑 → ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ∈ ℂ )
34 1 4 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
35 mulcl ⊢ ( ( 4 ∈ ℂ ∧ ( 𝐴 · 𝐶 ) ∈ ℂ ) → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
36 22 34 35 sylancr ⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
37 30 33 36 addassd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) + ( 4 · ( 𝐴 · 𝐶 ) ) ) = ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) + ( 4 · ( 𝐴 · 𝐶 ) ) ) ) )
38 3 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
39 30 33 addcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) ∈ ℂ )
40 38 39 36 pnncand ⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) + ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) ) − ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) = ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) + ( 4 · ( 𝐴 · 𝐶 ) ) ) )
41 10 5 sqmuld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) = ( ( ( 2 · 𝐴 ) ↑ 2 ) · ( 𝑋 ↑ 2 ) ) )
42 sq2 ⊢ ( 2 ↑ 2 ) = 4
43 42 a1i ⊢ ( 𝜑 → ( 2 ↑ 2 ) = 4 )
44 1 sqvald ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
45 43 44 oveq12d ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐴 ) ) )
46 sqmul ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 2 · 𝐴 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
47 8 1 46 sylancr ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
48 25 1 1 mulassd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐴 ) = ( 4 · ( 𝐴 · 𝐴 ) ) )
49 45 47 48 3eqtr4d ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) ↑ 2 ) = ( ( 4 · 𝐴 ) · 𝐴 ) )
50 49 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) ↑ 2 ) · ( 𝑋 ↑ 2 ) ) = ( ( ( 4 · 𝐴 ) · 𝐴 ) · ( 𝑋 ↑ 2 ) ) )
51 24 1 16 mulassd ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · 𝐴 ) · ( 𝑋 ↑ 2 ) ) = ( ( 4 · 𝐴 ) · ( 𝐴 · ( 𝑋 ↑ 2 ) ) ) )
52 41 50 51 3eqtrrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · ( 𝐴 · ( 𝑋 ↑ 2 ) ) ) = ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) )
53 24 18 4 adddid ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = ( ( ( 4 · 𝐴 ) · ( 𝐵 · 𝑋 ) ) + ( ( 4 · 𝐴 ) · 𝐶 ) ) )
54 2t2e4 ⊢ ( 2 · 2 ) = 4
55 54 oveq1i ⊢ ( ( 2 · 2 ) · 𝐴 ) = ( 4 · 𝐴 )
56 8 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
57 56 56 1 mulassd ⊢ ( 𝜑 → ( ( 2 · 2 ) · 𝐴 ) = ( 2 · ( 2 · 𝐴 ) ) )
58 55 57 eqtr3id ⊢ ( 𝜑 → ( 4 · 𝐴 ) = ( 2 · ( 2 · 𝐴 ) ) )
59 58 oveq1d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐵 ) = ( ( 2 · ( 2 · 𝐴 ) ) · 𝐵 ) )
60 56 10 3 mulassd ⊢ ( 𝜑 → ( ( 2 · ( 2 · 𝐴 ) ) · 𝐵 ) = ( 2 · ( ( 2 · 𝐴 ) · 𝐵 ) ) )
61 59 60 eqtrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐵 ) = ( 2 · ( ( 2 · 𝐴 ) · 𝐵 ) ) )
62 61 oveq1d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · 𝐵 ) · 𝑋 ) = ( ( 2 · ( ( 2 · 𝐴 ) · 𝐵 ) ) · 𝑋 ) )
63 10 3 mulcld ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · 𝐵 ) ∈ ℂ )
64 56 63 5 mulassd ⊢ ( 𝜑 → ( ( 2 · ( ( 2 · 𝐴 ) · 𝐵 ) ) · 𝑋 ) = ( 2 · ( ( ( 2 · 𝐴 ) · 𝐵 ) · 𝑋 ) ) )
65 62 64 eqtrd ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · 𝐵 ) · 𝑋 ) = ( 2 · ( ( ( 2 · 𝐴 ) · 𝐵 ) · 𝑋 ) ) )
66 24 3 5 mulassd ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · 𝐵 ) · 𝑋 ) = ( ( 4 · 𝐴 ) · ( 𝐵 · 𝑋 ) ) )
67 10 3 5 mul32d ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝐵 ) · 𝑋 ) = ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) )
68 67 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( ( 2 · 𝐴 ) · 𝐵 ) · 𝑋 ) ) = ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) )
69 65 66 68 3eqtr3d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · ( 𝐵 · 𝑋 ) ) = ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) )
70 25 1 4 mulassd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐶 ) = ( 4 · ( 𝐴 · 𝐶 ) ) )
71 69 70 oveq12d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · ( 𝐵 · 𝑋 ) ) + ( ( 4 · 𝐴 ) · 𝐶 ) ) = ( ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) + ( 4 · ( 𝐴 · 𝐶 ) ) ) )
72 53 71 eqtrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = ( ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) + ( 4 · ( 𝐴 · 𝐶 ) ) ) )
73 52 72 oveq12d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · ( 𝐴 · ( 𝑋 ↑ 2 ) ) ) + ( ( 4 · 𝐴 ) · ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) = ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) + ( 4 · ( 𝐴 · 𝐶 ) ) ) ) )
74 37 40 73 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · ( 𝐴 · ( 𝑋 ↑ 2 ) ) ) + ( ( 4 · 𝐴 ) · ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) = ( ( ( 𝐵 ↑ 2 ) + ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) ) − ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) )
75 24 17 19 adddid ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) = ( ( ( 4 · 𝐴 ) · ( 𝐴 · ( 𝑋 ↑ 2 ) ) ) + ( ( 4 · 𝐴 ) · ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) )
76 binom2 ⊢ ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) = ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
77 11 3 76 syl2anc ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) = ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
78 39 38 77 comraddd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) + ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) ) )
79 78 7 oveq12d ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) + ( ( ( ( 2 · 𝐴 ) · 𝑋 ) ↑ 2 ) + ( 2 · ( ( ( 2 · 𝐴 ) · 𝑋 ) · 𝐵 ) ) ) ) − ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) )
80 74 75 79 3eqtr4d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) = ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) − ( 𝐷 ↑ 2 ) ) )
81 24 mul01d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 0 ) = 0 )
82 80 81 eqeq12d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) ) = ( ( 4 · 𝐴 ) · 0 ) ↔ ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ) )
83 29 82 bitr3d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ) )
84 11 3 subnegd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) )
85 84 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ↑ 2 ) = ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) )
86 85 eqeq1d ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) ↔ ( ( ( ( 2 · 𝐴 ) · 𝑋 ) + 𝐵 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) ) )
87 15 83 86 3bitr4d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) ) )
88 3 negcld ⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
89 11 88 subcld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ∈ ℂ )
90 sqeqor ⊢ ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) ↔ ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = 𝐷 ∨ ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = - 𝐷 ) ) )
91 89 6 90 syl2anc ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) ↔ ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = 𝐷 ∨ ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = - 𝐷 ) ) )
92 11 88 6 subaddd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = 𝐷 ↔ ( - 𝐵 + 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ) )
93 88 6 addcld ⊢ ( 𝜑 → ( - 𝐵 + 𝐷 ) ∈ ℂ )
94 2ne0 ⊢ 2 ≠ 0
95 94 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
96 56 1 95 2 mulne0d ⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
97 93 10 5 96 divmuld ⊢ ( 𝜑 → ( ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) = 𝑋 ↔ ( ( 2 · 𝐴 ) · 𝑋 ) = ( - 𝐵 + 𝐷 ) ) )
98 eqcom ⊢ ( 𝑋 = ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) = 𝑋 )
99 eqcom ⊢ ( ( - 𝐵 + 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ↔ ( ( 2 · 𝐴 ) · 𝑋 ) = ( - 𝐵 + 𝐷 ) )
100 97 98 99 3bitr4g ⊢ ( 𝜑 → ( 𝑋 = ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( - 𝐵 + 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ) )
101 92 100 bitr4d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = 𝐷 ↔ 𝑋 = ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) ) )
102 88 6 negsubd ⊢ ( 𝜑 → ( - 𝐵 + - 𝐷 ) = ( - 𝐵 − 𝐷 ) )
103 102 eqeq1d ⊢ ( 𝜑 → ( ( - 𝐵 + - 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ↔ ( - 𝐵 − 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ) )
104 6 negcld ⊢ ( 𝜑 → - 𝐷 ∈ ℂ )
105 11 88 104 subaddd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = - 𝐷 ↔ ( - 𝐵 + - 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ) )
106 88 6 subcld ⊢ ( 𝜑 → ( - 𝐵 − 𝐷 ) ∈ ℂ )
107 106 10 5 96 divmuld ⊢ ( 𝜑 → ( ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) = 𝑋 ↔ ( ( 2 · 𝐴 ) · 𝑋 ) = ( - 𝐵 − 𝐷 ) ) )
108 eqcom ⊢ ( 𝑋 = ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) = 𝑋 )
109 eqcom ⊢ ( ( - 𝐵 − 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ↔ ( ( 2 · 𝐴 ) · 𝑋 ) = ( - 𝐵 − 𝐷 ) )
110 107 108 109 3bitr4g ⊢ ( 𝜑 → ( 𝑋 = ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) ↔ ( - 𝐵 − 𝐷 ) = ( ( 2 · 𝐴 ) · 𝑋 ) ) )
111 103 105 110 3bitr4d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = - 𝐷 ↔ 𝑋 = ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) ) )
112 101 111 orbi12d ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = 𝐷 ∨ ( ( ( 2 · 𝐴 ) · 𝑋 ) − - 𝐵 ) = - 𝐷 ) ↔ ( 𝑋 = ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) ) ) )
113 87 91 112 3bitrd ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( 𝑋 = ( ( - 𝐵 + 𝐷 ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − 𝐷 ) / ( 2 · 𝐴 ) ) ) ) )