Metamath Proof Explorer


Theorem dquartlem2

Description: Lemma for dquart . (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dquart.b
|- ( ph -> B e. CC )
dquart.c
|- ( ph -> C e. CC )
dquart.x
|- ( ph -> X e. CC )
dquart.s
|- ( ph -> S e. CC )
dquart.m
|- ( ph -> M = ( ( 2 x. S ) ^ 2 ) )
dquart.m0
|- ( ph -> M =/= 0 )
dquart.i
|- ( ph -> I e. CC )
dquart.i2
|- ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )
dquart.d
|- ( ph -> D e. CC )
dquart.3
|- ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) + -u ( C ^ 2 ) ) ) = 0 )
Assertion dquartlem2
|- ( ph -> ( ( ( ( M + B ) / 2 ) ^ 2 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) = D )

Proof

Step Hyp Ref Expression
1 dquart.b
 |-  ( ph -> B e. CC )
2 dquart.c
 |-  ( ph -> C e. CC )
3 dquart.x
 |-  ( ph -> X e. CC )
4 dquart.s
 |-  ( ph -> S e. CC )
5 dquart.m
 |-  ( ph -> M = ( ( 2 x. S ) ^ 2 ) )
6 dquart.m0
 |-  ( ph -> M =/= 0 )
7 dquart.i
 |-  ( ph -> I e. CC )
8 dquart.i2
 |-  ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )
9 dquart.d
 |-  ( ph -> D e. CC )
10 dquart.3
 |-  ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) + -u ( C ^ 2 ) ) ) = 0 )
11 2cn
 |-  2 e. CC
12 mulcl
 |-  ( ( 2 e. CC /\ S e. CC ) -> ( 2 x. S ) e. CC )
13 11 4 12 sylancr
 |-  ( ph -> ( 2 x. S ) e. CC )
14 13 sqcld
 |-  ( ph -> ( ( 2 x. S ) ^ 2 ) e. CC )
15 5 14 eqeltrd
 |-  ( ph -> M e. CC )
16 15 1 addcld
 |-  ( ph -> ( M + B ) e. CC )
17 11 a1i
 |-  ( ph -> 2 e. CC )
18 2ne0
 |-  2 =/= 0
19 18 a1i
 |-  ( ph -> 2 =/= 0 )
20 16 17 19 sqdivd
 |-  ( ph -> ( ( ( M + B ) / 2 ) ^ 2 ) = ( ( ( M + B ) ^ 2 ) / ( 2 ^ 2 ) ) )
21 sq2
 |-  ( 2 ^ 2 ) = 4
22 21 oveq2i
 |-  ( ( ( M + B ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( M + B ) ^ 2 ) / 4 )
23 20 22 eqtrdi
 |-  ( ph -> ( ( ( M + B ) / 2 ) ^ 2 ) = ( ( ( M + B ) ^ 2 ) / 4 ) )
24 23 oveq1d
 |-  ( ph -> ( ( ( ( M + B ) / 2 ) ^ 2 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) = ( ( ( ( M + B ) ^ 2 ) / 4 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) )
25 16 sqcld
 |-  ( ph -> ( ( M + B ) ^ 2 ) e. CC )
26 4cn
 |-  4 e. CC
27 26 a1i
 |-  ( ph -> 4 e. CC )
28 4ne0
 |-  4 =/= 0
29 28 a1i
 |-  ( ph -> 4 =/= 0 )
30 25 27 29 divcld
 |-  ( ph -> ( ( ( M + B ) ^ 2 ) / 4 ) e. CC )
31 2 sqcld
 |-  ( ph -> ( C ^ 2 ) e. CC )
32 31 27 29 divcld
 |-  ( ph -> ( ( C ^ 2 ) / 4 ) e. CC )
33 32 15 6 divcld
 |-  ( ph -> ( ( ( C ^ 2 ) / 4 ) / M ) e. CC )
34 30 33 subcld
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) / 4 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) e. CC )
35 30 33 15 subdird
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) / 4 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) x. M ) = ( ( ( ( ( M + B ) ^ 2 ) / 4 ) x. M ) - ( ( ( ( C ^ 2 ) / 4 ) / M ) x. M ) ) )
36 25 15 27 29 div23d
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) x. M ) / 4 ) = ( ( ( ( M + B ) ^ 2 ) / 4 ) x. M ) )
37 36 eqcomd
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) / 4 ) x. M ) = ( ( ( ( M + B ) ^ 2 ) x. M ) / 4 ) )
38 32 15 6 divcan1d
 |-  ( ph -> ( ( ( ( C ^ 2 ) / 4 ) / M ) x. M ) = ( ( C ^ 2 ) / 4 ) )
39 37 38 oveq12d
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) / 4 ) x. M ) - ( ( ( ( C ^ 2 ) / 4 ) / M ) x. M ) ) = ( ( ( ( ( M + B ) ^ 2 ) x. M ) / 4 ) - ( ( C ^ 2 ) / 4 ) ) )
40 binom2
 |-  ( ( M e. CC /\ B e. CC ) -> ( ( M + B ) ^ 2 ) = ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) + ( B ^ 2 ) ) )
41 15 1 40 syl2anc
 |-  ( ph -> ( ( M + B ) ^ 2 ) = ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) + ( B ^ 2 ) ) )
42 41 oveq1d
 |-  ( ph -> ( ( ( M + B ) ^ 2 ) x. M ) = ( ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) + ( B ^ 2 ) ) x. M ) )
43 15 sqcld
 |-  ( ph -> ( M ^ 2 ) e. CC )
44 15 1 mulcld
 |-  ( ph -> ( M x. B ) e. CC )
45 mulcl
 |-  ( ( 2 e. CC /\ ( M x. B ) e. CC ) -> ( 2 x. ( M x. B ) ) e. CC )
46 11 44 45 sylancr
 |-  ( ph -> ( 2 x. ( M x. B ) ) e. CC )
47 43 46 addcld
 |-  ( ph -> ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) e. CC )
48 1 sqcld
 |-  ( ph -> ( B ^ 2 ) e. CC )
49 47 48 15 adddird
 |-  ( ph -> ( ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) + ( B ^ 2 ) ) x. M ) = ( ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) x. M ) + ( ( B ^ 2 ) x. M ) ) )
50 43 46 15 adddird
 |-  ( ph -> ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) x. M ) = ( ( ( M ^ 2 ) x. M ) + ( ( 2 x. ( M x. B ) ) x. M ) ) )
51 df-3
 |-  3 = ( 2 + 1 )
52 51 oveq2i
 |-  ( M ^ 3 ) = ( M ^ ( 2 + 1 ) )
53 2nn0
 |-  2 e. NN0
54 expp1
 |-  ( ( M e. CC /\ 2 e. NN0 ) -> ( M ^ ( 2 + 1 ) ) = ( ( M ^ 2 ) x. M ) )
55 15 53 54 sylancl
 |-  ( ph -> ( M ^ ( 2 + 1 ) ) = ( ( M ^ 2 ) x. M ) )
56 52 55 eqtr2id
 |-  ( ph -> ( ( M ^ 2 ) x. M ) = ( M ^ 3 ) )
57 mulcl
 |-  ( ( 2 e. CC /\ B e. CC ) -> ( 2 x. B ) e. CC )
58 11 1 57 sylancr
 |-  ( ph -> ( 2 x. B ) e. CC )
59 58 15 15 mulassd
 |-  ( ph -> ( ( ( 2 x. B ) x. M ) x. M ) = ( ( 2 x. B ) x. ( M x. M ) ) )
60 17 15 1 mulassd
 |-  ( ph -> ( ( 2 x. M ) x. B ) = ( 2 x. ( M x. B ) ) )
61 17 15 1 mul32d
 |-  ( ph -> ( ( 2 x. M ) x. B ) = ( ( 2 x. B ) x. M ) )
62 60 61 eqtr3d
 |-  ( ph -> ( 2 x. ( M x. B ) ) = ( ( 2 x. B ) x. M ) )
63 62 oveq1d
 |-  ( ph -> ( ( 2 x. ( M x. B ) ) x. M ) = ( ( ( 2 x. B ) x. M ) x. M ) )
64 15 sqvald
 |-  ( ph -> ( M ^ 2 ) = ( M x. M ) )
65 64 oveq2d
 |-  ( ph -> ( ( 2 x. B ) x. ( M ^ 2 ) ) = ( ( 2 x. B ) x. ( M x. M ) ) )
66 59 63 65 3eqtr4d
 |-  ( ph -> ( ( 2 x. ( M x. B ) ) x. M ) = ( ( 2 x. B ) x. ( M ^ 2 ) ) )
67 56 66 oveq12d
 |-  ( ph -> ( ( ( M ^ 2 ) x. M ) + ( ( 2 x. ( M x. B ) ) x. M ) ) = ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) )
68 50 67 eqtrd
 |-  ( ph -> ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) x. M ) = ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) )
69 68 oveq1d
 |-  ( ph -> ( ( ( ( M ^ 2 ) + ( 2 x. ( M x. B ) ) ) x. M ) + ( ( B ^ 2 ) x. M ) ) = ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( B ^ 2 ) x. M ) ) )
70 42 49 69 3eqtrd
 |-  ( ph -> ( ( ( M + B ) ^ 2 ) x. M ) = ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( B ^ 2 ) x. M ) ) )
71 70 oveq1d
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) = ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( B ^ 2 ) x. M ) ) - ( ( 4 x. D ) x. M ) ) )
72 3nn0
 |-  3 e. NN0
73 expcl
 |-  ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
74 15 72 73 sylancl
 |-  ( ph -> ( M ^ 3 ) e. CC )
75 58 43 mulcld
 |-  ( ph -> ( ( 2 x. B ) x. ( M ^ 2 ) ) e. CC )
76 74 75 addcld
 |-  ( ph -> ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) e. CC )
77 48 15 mulcld
 |-  ( ph -> ( ( B ^ 2 ) x. M ) e. CC )
78 mulcl
 |-  ( ( 4 e. CC /\ D e. CC ) -> ( 4 x. D ) e. CC )
79 26 9 78 sylancr
 |-  ( ph -> ( 4 x. D ) e. CC )
80 79 15 mulcld
 |-  ( ph -> ( ( 4 x. D ) x. M ) e. CC )
81 76 77 80 addsubassd
 |-  ( ph -> ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( B ^ 2 ) x. M ) ) - ( ( 4 x. D ) x. M ) ) = ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) ) )
82 48 79 15 subdird
 |-  ( ph -> ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) = ( ( ( B ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) )
83 82 oveq2d
 |-  ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) = ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) ) )
84 81 83 eqtr4d
 |-  ( ph -> ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( B ^ 2 ) x. M ) ) - ( ( 4 x. D ) x. M ) ) = ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) )
85 48 79 subcld
 |-  ( ph -> ( ( B ^ 2 ) - ( 4 x. D ) ) e. CC )
86 85 15 mulcld
 |-  ( ph -> ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) e. CC )
87 76 86 addcld
 |-  ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) e. CC )
88 31 negcld
 |-  ( ph -> -u ( C ^ 2 ) e. CC )
89 76 86 88 addassd
 |-  ( ph -> ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) + -u ( C ^ 2 ) ) = ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) + -u ( C ^ 2 ) ) ) )
90 87 31 negsubd
 |-  ( ph -> ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) + -u ( C ^ 2 ) ) = ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) - ( C ^ 2 ) ) )
91 89 90 10 3eqtr3d
 |-  ( ph -> ( ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) - ( C ^ 2 ) ) = 0 )
92 87 31 91 subeq0d
 |-  ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) ) = ( C ^ 2 ) )
93 71 84 92 3eqtrd
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) = ( C ^ 2 ) )
94 25 15 mulcld
 |-  ( ph -> ( ( ( M + B ) ^ 2 ) x. M ) e. CC )
95 subsub23
 |-  ( ( ( ( ( M + B ) ^ 2 ) x. M ) e. CC /\ ( ( 4 x. D ) x. M ) e. CC /\ ( C ^ 2 ) e. CC ) -> ( ( ( ( ( M + B ) ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) = ( C ^ 2 ) <-> ( ( ( ( M + B ) ^ 2 ) x. M ) - ( C ^ 2 ) ) = ( ( 4 x. D ) x. M ) ) )
96 94 80 31 95 syl3anc
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) x. M ) - ( ( 4 x. D ) x. M ) ) = ( C ^ 2 ) <-> ( ( ( ( M + B ) ^ 2 ) x. M ) - ( C ^ 2 ) ) = ( ( 4 x. D ) x. M ) ) )
97 93 96 mpbid
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) x. M ) - ( C ^ 2 ) ) = ( ( 4 x. D ) x. M ) )
98 27 9 15 mulassd
 |-  ( ph -> ( ( 4 x. D ) x. M ) = ( 4 x. ( D x. M ) ) )
99 97 98 eqtrd
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) x. M ) - ( C ^ 2 ) ) = ( 4 x. ( D x. M ) ) )
100 99 oveq1d
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) x. M ) - ( C ^ 2 ) ) / 4 ) = ( ( 4 x. ( D x. M ) ) / 4 ) )
101 94 31 27 29 divsubdird
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) x. M ) - ( C ^ 2 ) ) / 4 ) = ( ( ( ( ( M + B ) ^ 2 ) x. M ) / 4 ) - ( ( C ^ 2 ) / 4 ) ) )
102 9 15 mulcld
 |-  ( ph -> ( D x. M ) e. CC )
103 102 27 29 divcan3d
 |-  ( ph -> ( ( 4 x. ( D x. M ) ) / 4 ) = ( D x. M ) )
104 100 101 103 3eqtr3d
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) x. M ) / 4 ) - ( ( C ^ 2 ) / 4 ) ) = ( D x. M ) )
105 35 39 104 3eqtrd
 |-  ( ph -> ( ( ( ( ( M + B ) ^ 2 ) / 4 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) x. M ) = ( D x. M ) )
106 34 9 15 6 105 mulcan2ad
 |-  ( ph -> ( ( ( ( M + B ) ^ 2 ) / 4 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) = D )
107 24 106 eqtrd
 |-  ( ph -> ( ( ( ( M + B ) / 2 ) ^ 2 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) = D )