Theorem quad

Description: The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	quad.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	quad.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	quad.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	quad.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	quad.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	quad.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
Assertion	quad	⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 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		quad.d	⊢ ( 𝜑 → 𝐷 = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
7	3	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
8		4cn	⊢ 4 ∈ ℂ
9	1 4	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
10		mulcl	⊢ ( ( 4 ∈ ℂ ∧ ( 𝐴 · 𝐶 ) ∈ ℂ ) → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
11	8 9 10	sylancr	⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
12	7 11	subcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ )
13	6 12	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
14	13	sqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℂ )
15	13	sqsqrtd	⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
16	15 6	eqtrd	⊢ ( 𝜑 → ( ( √ ‘ 𝐷 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
17	1 2 3 4 5 14 16	quad2	⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( 𝑋 = ( ( - 𝐵 + ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − ( √ ‘ 𝐷 ) ) / ( 2 · 𝐴 ) ) ) ) )