Metamath Proof Explorer


Theorem dquartlem2

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

Ref Expression
Hypotheses dquart.b φ B
dquart.c φ C
dquart.x φ X
dquart.s φ S
dquart.m φ M = 2 S 2
dquart.m0 φ M 0
dquart.i φ I
dquart.i2 φ I 2 = S 2 - B 2 + C 4 S
dquart.d φ D
dquart.3 φ M 3 + 2 B M 2 + B 2 4 D M + C 2 = 0
Assertion dquartlem2 φ M + B 2 2 C 2 4 M = D

Proof

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