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 )