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 
|- ( 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 )
quad2.d 
|- ( ph -> D e. CC )
quad2.2 
|- ( ph -> ( D ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
Assertion quad2 
|- ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ( ( -u B + D ) / ( 2 x. A ) ) \/ X = ( ( -u B - 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 quad2.d 
 |-  ( ph -> D e. CC )
7 quad2.2 
 |-  ( ph -> ( D ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
8 2cn 
 |-  2 e. CC
9 mulcl 
 |-  ( ( 2 e. CC /\ A e. CC ) -> ( 2 x. A ) e. CC )
10 8 1 9 sylancr 
 |-  ( ph -> ( 2 x. A ) e. CC )
11 10 5 mulcld 
 |-  ( ph -> ( ( 2 x. A ) x. X ) e. CC )
12 11 3 addcld 
 |-  ( ph -> ( ( ( 2 x. A ) x. X ) + B ) e. CC )
13 12 sqcld 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) e. CC )
14 6 sqcld 
 |-  ( ph -> ( D ^ 2 ) e. CC )
15 13 14 subeq0ad 
 |-  ( ph -> ( ( ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) - ( D ^ 2 ) ) = 0 <-> ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) = ( D ^ 2 ) ) )
16 5 sqcld 
 |-  ( ph -> ( X ^ 2 ) e. CC )
17 1 16 mulcld 
 |-  ( ph -> ( A x. ( X ^ 2 ) ) e. CC )
18 3 5 mulcld 
 |-  ( ph -> ( B x. X ) e. CC )
19 18 4 addcld 
 |-  ( ph -> ( ( B x. X ) + C ) e. CC )
20 17 19 addcld 
 |-  ( ph -> ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) e. CC )
21 0cnd 
 |-  ( ph -> 0 e. CC )
22 4cn 
 |-  4 e. CC
23 mulcl 
 |-  ( ( 4 e. CC /\ A e. CC ) -> ( 4 x. A ) e. CC )
24 22 1 23 sylancr 
 |-  ( ph -> ( 4 x. A ) e. CC )
25 22 a1i 
 |-  ( ph -> 4 e. CC )
26 4ne0 
 |-  4 =/= 0
27 26 a1i 
 |-  ( ph -> 4 =/= 0 )
28 25 1 27 2 mulne0d 
 |-  ( ph -> ( 4 x. A ) =/= 0 )
29 20 21 24 28 mulcand 
 |-  ( ph -> ( ( ( 4 x. A ) x. ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) ) = ( ( 4 x. A ) x. 0 ) <-> ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 ) )
30 11 sqcld 
 |-  ( ph -> ( ( ( 2 x. A ) x. X ) ^ 2 ) e. CC )
31 11 3 mulcld 
 |-  ( ph -> ( ( ( 2 x. A ) x. X ) x. B ) e. CC )
32 mulcl 
 |-  ( ( 2 e. CC /\ ( ( ( 2 x. A ) x. X ) x. B ) e. CC ) -> ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) e. CC )
33 8 31 32 sylancr 
 |-  ( ph -> ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) e. CC )
34 1 4 mulcld 
 |-  ( ph -> ( A x. C ) e. CC )
35 mulcl 
 |-  ( ( 4 e. CC /\ ( A x. C ) e. CC ) -> ( 4 x. ( A x. C ) ) e. CC )
36 22 34 35 sylancr 
 |-  ( ph -> ( 4 x. ( A x. C ) ) e. CC )
37 30 33 36 addassd 
 |-  ( ph -> ( ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) + ( 4 x. ( A x. C ) ) ) = ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) + ( 4 x. ( A x. C ) ) ) ) )
38 3 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
39 30 33 addcld 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) e. CC )
40 38 39 36 pnncand 
 |-  ( ph -> ( ( ( B ^ 2 ) + ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) ) - ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) = ( ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) + ( 4 x. ( A x. C ) ) ) )
41 10 5 sqmuld 
 |-  ( ph -> ( ( ( 2 x. A ) x. X ) ^ 2 ) = ( ( ( 2 x. A ) ^ 2 ) x. ( X ^ 2 ) ) )
42 sq2 
 |-  ( 2 ^ 2 ) = 4
43 42 a1i 
 |-  ( ph -> ( 2 ^ 2 ) = 4 )
44 1 sqvald 
 |-  ( ph -> ( A ^ 2 ) = ( A x. A ) )
45 43 44 oveq12d 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( A ^ 2 ) ) = ( 4 x. ( A x. A ) ) )
46 sqmul 
 |-  ( ( 2 e. CC /\ A e. CC ) -> ( ( 2 x. A ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( A ^ 2 ) ) )
47 8 1 46 sylancr 
 |-  ( ph -> ( ( 2 x. A ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( A ^ 2 ) ) )
48 25 1 1 mulassd 
 |-  ( ph -> ( ( 4 x. A ) x. A ) = ( 4 x. ( A x. A ) ) )
49 45 47 48 3eqtr4d 
 |-  ( ph -> ( ( 2 x. A ) ^ 2 ) = ( ( 4 x. A ) x. A ) )
50 49 oveq1d 
 |-  ( ph -> ( ( ( 2 x. A ) ^ 2 ) x. ( X ^ 2 ) ) = ( ( ( 4 x. A ) x. A ) x. ( X ^ 2 ) ) )
51 24 1 16 mulassd 
 |-  ( ph -> ( ( ( 4 x. A ) x. A ) x. ( X ^ 2 ) ) = ( ( 4 x. A ) x. ( A x. ( X ^ 2 ) ) ) )
52 41 50 51 3eqtrrd 
 |-  ( ph -> ( ( 4 x. A ) x. ( A x. ( X ^ 2 ) ) ) = ( ( ( 2 x. A ) x. X ) ^ 2 ) )
53 24 18 4 adddid 
 |-  ( ph -> ( ( 4 x. A ) x. ( ( B x. X ) + C ) ) = ( ( ( 4 x. A ) x. ( B x. X ) ) + ( ( 4 x. A ) x. C ) ) )
54 2t2e4 
 |-  ( 2 x. 2 ) = 4
55 54 oveq1i 
 |-  ( ( 2 x. 2 ) x. A ) = ( 4 x. A )
56 8 a1i 
 |-  ( ph -> 2 e. CC )
57 56 56 1 mulassd 
 |-  ( ph -> ( ( 2 x. 2 ) x. A ) = ( 2 x. ( 2 x. A ) ) )
58 55 57 eqtr3id 
 |-  ( ph -> ( 4 x. A ) = ( 2 x. ( 2 x. A ) ) )
59 58 oveq1d 
 |-  ( ph -> ( ( 4 x. A ) x. B ) = ( ( 2 x. ( 2 x. A ) ) x. B ) )
60 56 10 3 mulassd 
 |-  ( ph -> ( ( 2 x. ( 2 x. A ) ) x. B ) = ( 2 x. ( ( 2 x. A ) x. B ) ) )
61 59 60 eqtrd 
 |-  ( ph -> ( ( 4 x. A ) x. B ) = ( 2 x. ( ( 2 x. A ) x. B ) ) )
62 61 oveq1d 
 |-  ( ph -> ( ( ( 4 x. A ) x. B ) x. X ) = ( ( 2 x. ( ( 2 x. A ) x. B ) ) x. X ) )
63 10 3 mulcld 
 |-  ( ph -> ( ( 2 x. A ) x. B ) e. CC )
64 56 63 5 mulassd 
 |-  ( ph -> ( ( 2 x. ( ( 2 x. A ) x. B ) ) x. X ) = ( 2 x. ( ( ( 2 x. A ) x. B ) x. X ) ) )
65 62 64 eqtrd 
 |-  ( ph -> ( ( ( 4 x. A ) x. B ) x. X ) = ( 2 x. ( ( ( 2 x. A ) x. B ) x. X ) ) )
66 24 3 5 mulassd 
 |-  ( ph -> ( ( ( 4 x. A ) x. B ) x. X ) = ( ( 4 x. A ) x. ( B x. X ) ) )
67 10 3 5 mul32d 
 |-  ( ph -> ( ( ( 2 x. A ) x. B ) x. X ) = ( ( ( 2 x. A ) x. X ) x. B ) )
68 67 oveq2d 
 |-  ( ph -> ( 2 x. ( ( ( 2 x. A ) x. B ) x. X ) ) = ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) )
69 65 66 68 3eqtr3d 
 |-  ( ph -> ( ( 4 x. A ) x. ( B x. X ) ) = ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) )
70 25 1 4 mulassd 
 |-  ( ph -> ( ( 4 x. A ) x. C ) = ( 4 x. ( A x. C ) ) )
71 69 70 oveq12d 
 |-  ( ph -> ( ( ( 4 x. A ) x. ( B x. X ) ) + ( ( 4 x. A ) x. C ) ) = ( ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) + ( 4 x. ( A x. C ) ) ) )
72 53 71 eqtrd 
 |-  ( ph -> ( ( 4 x. A ) x. ( ( B x. X ) + C ) ) = ( ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) + ( 4 x. ( A x. C ) ) ) )
73 52 72 oveq12d 
 |-  ( ph -> ( ( ( 4 x. A ) x. ( A x. ( X ^ 2 ) ) ) + ( ( 4 x. A ) x. ( ( B x. X ) + C ) ) ) = ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) + ( 4 x. ( A x. C ) ) ) ) )
74 37 40 73 3eqtr4rd 
 |-  ( ph -> ( ( ( 4 x. A ) x. ( A x. ( X ^ 2 ) ) ) + ( ( 4 x. A ) x. ( ( B x. X ) + C ) ) ) = ( ( ( B ^ 2 ) + ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) ) - ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) )
75 24 17 19 adddid 
 |-  ( ph -> ( ( 4 x. A ) x. ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) ) = ( ( ( 4 x. A ) x. ( A x. ( X ^ 2 ) ) ) + ( ( 4 x. A ) x. ( ( B x. X ) + C ) ) ) )
76 binom2 
 |-  ( ( ( ( 2 x. A ) x. X ) e. CC /\ B e. CC ) -> ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) = ( ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) + ( B ^ 2 ) ) )
77 11 3 76 syl2anc 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) = ( ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) + ( B ^ 2 ) ) )
78 39 38 77 comraddd 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) = ( ( B ^ 2 ) + ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) ) )
79 78 7 oveq12d 
 |-  ( ph -> ( ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) - ( D ^ 2 ) ) = ( ( ( B ^ 2 ) + ( ( ( ( 2 x. A ) x. X ) ^ 2 ) + ( 2 x. ( ( ( 2 x. A ) x. X ) x. B ) ) ) ) - ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) )
80 74 75 79 3eqtr4d 
 |-  ( ph -> ( ( 4 x. A ) x. ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) ) = ( ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) - ( D ^ 2 ) ) )
81 24 mul01d 
 |-  ( ph -> ( ( 4 x. A ) x. 0 ) = 0 )
82 80 81 eqeq12d 
 |-  ( ph -> ( ( ( 4 x. A ) x. ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) ) = ( ( 4 x. A ) x. 0 ) <-> ( ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) - ( D ^ 2 ) ) = 0 ) )
83 29 82 bitr3d 
 |-  ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) - ( D ^ 2 ) ) = 0 ) )
84 11 3 subnegd 
 |-  ( ph -> ( ( ( 2 x. A ) x. X ) - -u B ) = ( ( ( 2 x. A ) x. X ) + B ) )
85 84 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) - -u B ) ^ 2 ) = ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) )
86 85 eqeq1d 
 |-  ( ph -> ( ( ( ( ( 2 x. A ) x. X ) - -u B ) ^ 2 ) = ( D ^ 2 ) <-> ( ( ( ( 2 x. A ) x. X ) + B ) ^ 2 ) = ( D ^ 2 ) ) )
87 15 83 86 3bitr4d 
 |-  ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( ( ( ( 2 x. A ) x. X ) - -u B ) ^ 2 ) = ( D ^ 2 ) ) )
88 3 negcld 
 |-  ( ph -> -u B e. CC )
89 11 88 subcld 
 |-  ( ph -> ( ( ( 2 x. A ) x. X ) - -u B ) e. CC )
90 sqeqor 
 |-  ( ( ( ( ( 2 x. A ) x. X ) - -u B ) e. CC /\ D e. CC ) -> ( ( ( ( ( 2 x. A ) x. X ) - -u B ) ^ 2 ) = ( D ^ 2 ) <-> ( ( ( ( 2 x. A ) x. X ) - -u B ) = D \/ ( ( ( 2 x. A ) x. X ) - -u B ) = -u D ) ) )
91 89 6 90 syl2anc 
 |-  ( ph -> ( ( ( ( ( 2 x. A ) x. X ) - -u B ) ^ 2 ) = ( D ^ 2 ) <-> ( ( ( ( 2 x. A ) x. X ) - -u B ) = D \/ ( ( ( 2 x. A ) x. X ) - -u B ) = -u D ) ) )
92 11 88 6 subaddd 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) - -u B ) = D <-> ( -u B + D ) = ( ( 2 x. A ) x. X ) ) )
93 88 6 addcld 
 |-  ( ph -> ( -u B + D ) e. CC )
94 2ne0 
 |-  2 =/= 0
95 94 a1i 
 |-  ( ph -> 2 =/= 0 )
96 56 1 95 2 mulne0d 
 |-  ( ph -> ( 2 x. A ) =/= 0 )
97 93 10 5 96 divmuld 
 |-  ( ph -> ( ( ( -u B + D ) / ( 2 x. A ) ) = X <-> ( ( 2 x. A ) x. X ) = ( -u B + D ) ) )
98 eqcom 
 |-  ( X = ( ( -u B + D ) / ( 2 x. A ) ) <-> ( ( -u B + D ) / ( 2 x. A ) ) = X )
99 eqcom 
 |-  ( ( -u B + D ) = ( ( 2 x. A ) x. X ) <-> ( ( 2 x. A ) x. X ) = ( -u B + D ) )
100 97 98 99 3bitr4g 
 |-  ( ph -> ( X = ( ( -u B + D ) / ( 2 x. A ) ) <-> ( -u B + D ) = ( ( 2 x. A ) x. X ) ) )
101 92 100 bitr4d 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) - -u B ) = D <-> X = ( ( -u B + D ) / ( 2 x. A ) ) ) )
102 88 6 negsubd 
 |-  ( ph -> ( -u B + -u D ) = ( -u B - D ) )
103 102 eqeq1d 
 |-  ( ph -> ( ( -u B + -u D ) = ( ( 2 x. A ) x. X ) <-> ( -u B - D ) = ( ( 2 x. A ) x. X ) ) )
104 6 negcld 
 |-  ( ph -> -u D e. CC )
105 11 88 104 subaddd 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) - -u B ) = -u D <-> ( -u B + -u D ) = ( ( 2 x. A ) x. X ) ) )
106 88 6 subcld 
 |-  ( ph -> ( -u B - D ) e. CC )
107 106 10 5 96 divmuld 
 |-  ( ph -> ( ( ( -u B - D ) / ( 2 x. A ) ) = X <-> ( ( 2 x. A ) x. X ) = ( -u B - D ) ) )
108 eqcom 
 |-  ( X = ( ( -u B - D ) / ( 2 x. A ) ) <-> ( ( -u B - D ) / ( 2 x. A ) ) = X )
109 eqcom 
 |-  ( ( -u B - D ) = ( ( 2 x. A ) x. X ) <-> ( ( 2 x. A ) x. X ) = ( -u B - D ) )
110 107 108 109 3bitr4g 
 |-  ( ph -> ( X = ( ( -u B - D ) / ( 2 x. A ) ) <-> ( -u B - D ) = ( ( 2 x. A ) x. X ) ) )
111 103 105 110 3bitr4d 
 |-  ( ph -> ( ( ( ( 2 x. A ) x. X ) - -u B ) = -u D <-> X = ( ( -u B - D ) / ( 2 x. A ) ) ) )
112 101 111 orbi12d 
 |-  ( ph -> ( ( ( ( ( 2 x. A ) x. X ) - -u B ) = D \/ ( ( ( 2 x. A ) x. X ) - -u B ) = -u D ) <-> ( X = ( ( -u B + D ) / ( 2 x. A ) ) \/ X = ( ( -u B - D ) / ( 2 x. A ) ) ) ) )
113 87 91 112 3bitrd 
 |-  ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ( ( -u B + D ) / ( 2 x. A ) ) \/ X = ( ( -u B - D ) / ( 2 x. A ) ) ) ) )