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 · 𝐴 ) ) ) ) )