Metamath Proof Explorer

Theorem quad

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

Ref Expression
Hypotheses quad.a 
|- ( ph -> A e. CC )
quad.z 
|- ( ph -> A =/= 0 )
quad.b 
|- ( ph -> B e. CC )
quad.c 
|- ( ph -> C e. CC )
quad.x 
|- ( ph -> X e. CC )
quad.d 
|- ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
Assertion quad 
|- ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quad.a 
 |-  ( ph -> A e. CC )
2 quad.z 
 |-  ( ph -> A =/= 0 )
3 quad.b 
 |-  ( ph -> B e. CC )
4 quad.c 
 |-  ( ph -> C e. CC )
5 quad.x 
 |-  ( ph -> X e. CC )
6 quad.d 
 |-  ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
7 3 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
8 4cn 
 |-  4 e. CC
9 1 4 mulcld 
 |-  ( ph -> ( A x. C ) e. CC )
10 mulcl 
 |-  ( ( 4 e. CC /\ ( A x. C ) e. CC ) -> ( 4 x. ( A x. C ) ) e. CC )
11 8 9 10 sylancr 
 |-  ( ph -> ( 4 x. ( A x. C ) ) e. CC )
12 7 11 subcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. CC )
13 6 12 eqeltrd 
 |-  ( ph -> D e. CC )
14 13 sqrtcld 
 |-  ( ph -> ( sqrt ` D ) e. CC )
15 13 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` D ) ^ 2 ) = D )
16 15 6 eqtrd 
 |-  ( ph -> ( ( sqrt ` D ) ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
17 1 2 3 4 5 14 16 quad2 
 |-  ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) ) )