Metamath Proof Explorer


Theorem 2itscplem3

Description: Lemma D for 2itscp . (Contributed by AV, 4-Mar-2023)

Ref Expression
Hypotheses 2itscp.a φ A
2itscp.b φ B
2itscp.x φ X
2itscp.y φ Y
2itscp.d D = X A
2itscp.e E = B Y
2itscp.c C = D B + E A
2itscp.r φ R
2itscplem3.q Q = E 2 + D 2
2itscplem3.s S = R 2 Q C 2
Assertion 2itscplem3 φ S = E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B

Proof

Step Hyp Ref Expression
1 2itscp.a φ A
2 2itscp.b φ B
3 2itscp.x φ X
4 2itscp.y φ Y
5 2itscp.d D = X A
6 2itscp.e E = B Y
7 2itscp.c C = D B + E A
8 2itscp.r φ R
9 2itscplem3.q Q = E 2 + D 2
10 2itscplem3.s S = R 2 Q C 2
11 10 a1i φ S = R 2 Q C 2
12 9 a1i φ Q = E 2 + D 2
13 12 oveq2d φ R 2 Q = R 2 E 2 + D 2
14 8 recnd φ R
15 14 sqcld φ R 2
16 2 recnd φ B
17 4 recnd φ Y
18 16 17 subcld φ B Y
19 6 18 eqeltrid φ E
20 19 sqcld φ E 2
21 3 recnd φ X
22 1 recnd φ A
23 21 22 subcld φ X A
24 5 23 eqeltrid φ D
25 24 sqcld φ D 2
26 20 25 addcld φ E 2 + D 2
27 15 26 mulcomd φ R 2 E 2 + D 2 = E 2 + D 2 R 2
28 20 25 15 adddird φ E 2 + D 2 R 2 = E 2 R 2 + D 2 R 2
29 13 27 28 3eqtrd φ R 2 Q = E 2 R 2 + D 2 R 2
30 1 2 3 4 5 6 7 2itscplem2 φ C 2 = D 2 B 2 + 2 D A E B + E 2 A 2
31 29 30 oveq12d φ R 2 Q C 2 = E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B + E 2 A 2
32 20 15 mulcld φ E 2 R 2
33 25 15 mulcld φ D 2 R 2
34 32 33 addcld φ E 2 R 2 + D 2 R 2
35 16 sqcld φ B 2
36 25 35 mulcld φ D 2 B 2
37 2cnd φ 2
38 24 22 mulcld φ D A
39 19 16 mulcld φ E B
40 38 39 mulcld φ D A E B
41 37 40 mulcld φ 2 D A E B
42 34 36 41 subsub4d φ E 2 R 2 + D 2 R 2 - D 2 B 2 - 2 D A E B = E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B
43 42 eqcomd φ E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B = E 2 R 2 + D 2 R 2 - D 2 B 2 - 2 D A E B
44 43 oveq1d φ E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B - E 2 A 2 = E 2 R 2 + D 2 R 2 - D 2 B 2 - 2 D A E B - E 2 A 2
45 34 36 subcld φ E 2 R 2 + D 2 R 2 - D 2 B 2
46 22 sqcld φ A 2
47 20 46 mulcld φ E 2 A 2
48 45 41 47 sub32d φ E 2 R 2 + D 2 R 2 - D 2 B 2 - 2 D A E B - E 2 A 2 = E 2 R 2 + D 2 R 2 - D 2 B 2 - E 2 A 2 - 2 D A E B
49 44 48 eqtrd φ E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B - E 2 A 2 = E 2 R 2 + D 2 R 2 - D 2 B 2 - E 2 A 2 - 2 D A E B
50 36 41 addcld φ D 2 B 2 + 2 D A E B
51 34 50 47 subsub4d φ E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B - E 2 A 2 = E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B + E 2 A 2
52 32 33 36 addsubassd φ E 2 R 2 + D 2 R 2 - D 2 B 2 = E 2 R 2 + D 2 R 2 - D 2 B 2
53 25 15 35 subdid φ D 2 R 2 B 2 = D 2 R 2 D 2 B 2
54 53 eqcomd φ D 2 R 2 D 2 B 2 = D 2 R 2 B 2
55 54 oveq2d φ E 2 R 2 + D 2 R 2 - D 2 B 2 = E 2 R 2 + D 2 R 2 B 2
56 52 55 eqtrd φ E 2 R 2 + D 2 R 2 - D 2 B 2 = E 2 R 2 + D 2 R 2 B 2
57 56 oveq1d φ E 2 R 2 + D 2 R 2 - D 2 B 2 - E 2 A 2 = E 2 R 2 + D 2 R 2 B 2 - E 2 A 2
58 15 35 subcld φ R 2 B 2
59 25 58 mulcld φ D 2 R 2 B 2
60 32 59 47 addsubd φ E 2 R 2 + D 2 R 2 B 2 - E 2 A 2 = E 2 R 2 - E 2 A 2 + D 2 R 2 B 2
61 20 15 46 subdid φ E 2 R 2 A 2 = E 2 R 2 E 2 A 2
62 61 eqcomd φ E 2 R 2 E 2 A 2 = E 2 R 2 A 2
63 62 oveq1d φ E 2 R 2 - E 2 A 2 + D 2 R 2 B 2 = E 2 R 2 A 2 + D 2 R 2 B 2
64 57 60 63 3eqtrd φ E 2 R 2 + D 2 R 2 - D 2 B 2 - E 2 A 2 = E 2 R 2 A 2 + D 2 R 2 B 2
65 64 oveq1d φ E 2 R 2 + D 2 R 2 - D 2 B 2 - E 2 A 2 - 2 D A E B = E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B
66 49 51 65 3eqtr3d φ E 2 R 2 + D 2 R 2 - D 2 B 2 + 2 D A E B + E 2 A 2 = E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B
67 11 31 66 3eqtrd φ S = E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B