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 φA
quad.z φA0
quad.b φB
quad.c φC
quad.x φX
quad2.d φD
quad2.2 φD2=B24AC
Assertion quad2 φAX2+BX+C=0X=-B+D2AX=-B-D2A

Proof

Step Hyp Ref Expression
1 quad.a φA
2 quad.z φA0
3 quad.b φB
4 quad.c φC
5 quad.x φX
6 quad2.d φD
7 quad2.2 φD2=B24AC
8 2cn 2
9 mulcl 2A2A
10 8 1 9 sylancr φ2A
11 10 5 mulcld φ2AX
12 11 3 addcld φ2AX+B
13 12 sqcld φ2AX+B2
14 6 sqcld φD2
15 13 14 subeq0ad φ2AX+B2D2=02AX+B2=D2
16 5 sqcld φX2
17 1 16 mulcld φAX2
18 3 5 mulcld φBX
19 18 4 addcld φBX+C
20 17 19 addcld φAX2+BX+C
21 0cnd φ0
22 4cn 4
23 mulcl 4A4A
24 22 1 23 sylancr φ4A
25 22 a1i φ4
26 4ne0 40
27 26 a1i φ40
28 25 1 27 2 mulne0d φ4A0
29 20 21 24 28 mulcand φ4AAX2+BX+C=4A0AX2+BX+C=0
30 11 sqcld φ2AX2
31 11 3 mulcld φ2AXB
32 mulcl 22AXB22AXB
33 8 31 32 sylancr φ22AXB
34 1 4 mulcld φAC
35 mulcl 4AC4AC
36 22 34 35 sylancr φ4AC
37 30 33 36 addassd φ2AX2+22AXB+4AC=2AX2+22AXB+4AC
38 3 sqcld φB2
39 30 33 addcld φ2AX2+22AXB
40 38 39 36 pnncand φB2+2AX2+22AXB-B24AC=2AX2+22AXB+4AC
41 10 5 sqmuld φ2AX2=2A2X2
42 sq2 22=4
43 42 a1i φ22=4
44 1 sqvald φA2=AA
45 43 44 oveq12d φ22A2=4AA
46 sqmul 2A2A2=22A2
47 8 1 46 sylancr φ2A2=22A2
48 25 1 1 mulassd φ4AA=4AA
49 45 47 48 3eqtr4d φ2A2=4AA
50 49 oveq1d φ2A2X2=4AAX2
51 24 1 16 mulassd φ4AAX2=4AAX2
52 41 50 51 3eqtrrd φ4AAX2=2AX2
53 24 18 4 adddid φ4ABX+C=4ABX+4AC
54 2t2e4 22=4
55 54 oveq1i 22A=4A
56 8 a1i φ2
57 56 56 1 mulassd φ22A=22A
58 55 57 eqtr3id φ4A=22A
59 58 oveq1d φ4AB=22AB
60 56 10 3 mulassd φ22AB=22AB
61 59 60 eqtrd φ4AB=22AB
62 61 oveq1d φ4ABX=22ABX
63 10 3 mulcld φ2AB
64 56 63 5 mulassd φ22ABX=22ABX
65 62 64 eqtrd φ4ABX=22ABX
66 24 3 5 mulassd φ4ABX=4ABX
67 10 3 5 mul32d φ2ABX=2AXB
68 67 oveq2d φ22ABX=22AXB
69 65 66 68 3eqtr3d φ4ABX=22AXB
70 25 1 4 mulassd φ4AC=4AC
71 69 70 oveq12d φ4ABX+4AC=22AXB+4AC
72 53 71 eqtrd φ4ABX+C=22AXB+4AC
73 52 72 oveq12d φ4AAX2+4ABX+C=2AX2+22AXB+4AC
74 37 40 73 3eqtr4rd φ4AAX2+4ABX+C=B2+2AX2+22AXB-B24AC
75 24 17 19 adddid φ4AAX2+BX+C=4AAX2+4ABX+C
76 binom2 2AXB2AX+B2=2AX2+22AXB+B2
77 11 3 76 syl2anc φ2AX+B2=2AX2+22AXB+B2
78 39 38 77 comraddd φ2AX+B2=B2+2AX2+22AXB
79 78 7 oveq12d φ2AX+B2D2=B2+2AX2+22AXB-B24AC
80 74 75 79 3eqtr4d φ4AAX2+BX+C=2AX+B2D2
81 24 mul01d φ4A0=0
82 80 81 eqeq12d φ4AAX2+BX+C=4A02AX+B2D2=0
83 29 82 bitr3d φAX2+BX+C=02AX+B2D2=0
84 11 3 subnegd φ2AXB=2AX+B
85 84 oveq1d φ2AXB2=2AX+B2
86 85 eqeq1d φ2AXB2=D22AX+B2=D2
87 15 83 86 3bitr4d φAX2+BX+C=02AXB2=D2
88 3 negcld φB
89 11 88 subcld φ2AXB
90 sqeqor 2AXBD2AXB2=D22AXB=D2AXB=D
91 89 6 90 syl2anc φ2AXB2=D22AXB=D2AXB=D
92 11 88 6 subaddd φ2AXB=D-B+D=2AX
93 88 6 addcld φ-B+D
94 2ne0 20
95 94 a1i φ20
96 56 1 95 2 mulne0d φ2A0
97 93 10 5 96 divmuld φ-B+D2A=X2AX=-B+D
98 eqcom X=-B+D2A-B+D2A=X
99 eqcom -B+D=2AX2AX=-B+D
100 97 98 99 3bitr4g φX=-B+D2A-B+D=2AX
101 92 100 bitr4d φ2AXB=DX=-B+D2A
102 88 6 negsubd φ-B+D=-B-D
103 102 eqeq1d φ-B+D=2AX-B-D=2AX
104 6 negcld φD
105 11 88 104 subaddd φ2AXB=D-B+D=2AX
106 88 6 subcld φ-B-D
107 106 10 5 96 divmuld φ-B-D2A=X2AX=-B-D
108 eqcom X=-B-D2A-B-D2A=X
109 eqcom -B-D=2AX2AX=-B-D
110 107 108 109 3bitr4g φX=-B-D2A-B-D=2AX
111 103 105 110 3bitr4d φ2AXB=DX=-B-D2A
112 101 111 orbi12d φ2AXB=D2AXB=DX=-B+D2AX=-B-D2A
113 87 91 112 3bitrd φAX2+BX+C=0X=-B+D2AX=-B-D2A