Metamath Proof Explorer

Theorem itsclc0yqsollem1

Description: Lemma 1 for itsclc0yqsol . (Contributed by AV, 6-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q ⊢Q=A2+B2
itscnhlc0yqe.t ⊢T=−2⁢B⁢C
itscnhlc0yqe.u ⊢U=C2−A2⁢R2
itsclc0yqsollem1.d ⊢D=R2⁢Q−C2
Assertion itsclc0yqsollem1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→T2−4⁢Q⁢U=4⁢A2⁢D

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q ⊢Q=A2+B2
2 itscnhlc0yqe.t ⊢T=−2⁢B⁢C
3 itscnhlc0yqe.u ⊢U=C2−A2⁢R2
4 itsclc0yqsollem1.d ⊢D=R2⁢Q−C2
5 2 oveq1i ⊢T2=−2⁢B⁢C2
6 2cnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→2∈ℂ
7 simpl2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B∈ℂ
8 simpl3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→C∈ℂ
9 7 8 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B⁢C∈ℂ
10 6 9 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→2⁢B⁢C∈ℂ
11 sqneg ⊢2⁢B⁢C∈ℂ→−2⁢B⁢C2=2⁢B⁢C2
12 10 11 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→−2⁢B⁢C2=2⁢B⁢C2
13 6 9 sqmuld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→2⁢B⁢C2=22⁢B⁢C2
14 sq2 ⊢22=4
15 14 a1i ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→22=4
16 7 8 sqmuld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B⁢C2=B2⁢C2
17 15 16 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→22⁢B⁢C2=4⁢B2⁢C2
18 12 13 17 3eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→−2⁢B⁢C2=4⁢B2⁢C2
19 5 18 eqtrid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→T2=4⁢B2⁢C2
20 1 3 oveq12i ⊢Q⁢U=A2+B2⁢C2−A2⁢R2
21 simpl1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A∈ℂ
22 21 sqcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2∈ℂ
23 7 sqcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2∈ℂ
24 22 23 addcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2∈ℂ
25 8 sqcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→C2∈ℂ
26 simpr ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R∈ℂ
27 26 sqcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2∈ℂ
28 22 27 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢R2∈ℂ
29 24 25 28 subdid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢C2−A2⁢R2=A2+B2⁢C2−A2+B2⁢A2⁢R2
30 22 23 25 adddird ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢C2=A2⁢C2+B2⁢C2
31 22 23 28 adddird ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢A2⁢R2=A2⁢A2⁢R2+B2⁢A2⁢R2
32 30 31 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢C2−A2+B2⁢A2⁢R2=A2⁢C2+B2⁢C2-A2⁢A2⁢R2+B2⁢A2⁢R2
33 23 25 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2∈ℂ
34 22 25 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢C2∈ℂ
35 22 28 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2∈ℂ
36 23 27 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢R2∈ℂ
37 22 36 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢B2⁢R2∈ℂ
38 35 37 addcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+A2⁢B2⁢R2∈ℂ
39 34 33 addcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢C2+B2⁢C2=B2⁢C2+A2⁢C2
40 23 22 27 mul12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢A2⁢R2=A2⁢B2⁢R2
41 40 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+B2⁢A2⁢R2=A2⁢A2⁢R2+A2⁢B2⁢R2
42 39 41 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢C2+B2⁢C2-A2⁢A2⁢R2+B2⁢A2⁢R2=B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
43 33 34 38 42 assraddsubd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢C2+B2⁢C2-A2⁢A2⁢R2+B2⁢A2⁢R2=B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
44 29 32 43 3eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢C2−A2⁢R2=B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
45 20 44 eqtrid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→Q⁢U=B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
46 45 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→4⁢Q⁢U=4⁢B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
47 19 46 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→T2−4⁢Q⁢U=4⁢B2⁢C2−4⁢B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
48 4cn ⊢4∈ℂ
49 48 a1i ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→4∈ℂ
50 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ
51 50 sqcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A2∈ℂ
52 51 adantr ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2∈ℂ
53 1 24 eqeltrid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→Q∈ℂ
54 27 53 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2⁢Q∈ℂ
55 54 25 subcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2⁢Q−C2∈ℂ
56 4 55 eqeltrid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→D∈ℂ
57 49 52 56 mulassd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→4⁢A2⁢D=4⁢A2⁢D
58 34 38 subcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢C2−A2⁢A2⁢R2+A2⁢B2⁢R2∈ℂ
59 33 33 58 subsub4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2-B2⁢C2-A2⁢C2−A2⁢A2⁢R2+A2⁢B2⁢R2=B2⁢C2−B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
60 33 subidd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2−B2⁢C2=0
61 60 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2-B2⁢C2-A2⁢C2−A2⁢A2⁢R2+A2⁢B2⁢R2=0−A2⁢C2−A2⁢A2⁢R2+A2⁢B2⁢R2
62 0cnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→0∈ℂ
63 62 34 38 subsub2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→0−A2⁢C2−A2⁢A2⁢R2+A2⁢B2⁢R2=0+A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2
64 38 34 subcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2∈ℂ
65 64 addlidd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→0+A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2=A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2
66 61 63 65 3eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2-B2⁢C2-A2⁢C2−A2⁢A2⁢R2+A2⁢B2⁢R2=A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2
67 59 66 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2−B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2=A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2
68 22 28 36 adddid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+B2⁢R2=A2⁢A2⁢R2+A2⁢B2⁢R2
69 22 23 27 adddird ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢R2=A2⁢R2+B2⁢R2
70 69 eqcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢R2+B2⁢R2=A2+B2⁢R2
71 70 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+B2⁢R2=A2⁢A2+B2⁢R2
72 68 71 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+A2⁢B2⁢R2=A2⁢A2+B2⁢R2
73 72 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2=A2⁢A2+B2⁢R2−A2⁢C2
74 24 27 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢R2∈ℂ
75 22 74 25 subdid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2+B2⁢R2−C2=A2⁢A2+B2⁢R2−A2⁢C2
76 73 75 eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2⁢R2+A2⁢B2⁢R2-A2⁢C2=A2⁢A2+B2⁢R2−C2
77 1 a1i ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→Q=A2+B2
78 77 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2⁢Q=R2⁢A2+B2
79 27 24 mulcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2⁢A2+B2=A2+B2⁢R2
80 78 79 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2⁢Q=A2+B2⁢R2
81 80 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→R2⁢Q−C2=A2+B2⁢R2−C2
82 4 81 eqtrid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→D=A2+B2⁢R2−C2
83 82 eqcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2+B2⁢R2−C2=D
84 83 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→A2⁢A2+B2⁢R2−C2=A2⁢D
85 67 76 84 3eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2−B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2=A2⁢D
86 85 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→4⁢B2⁢C2−B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2=4⁢A2⁢D
87 33 58 addcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2∈ℂ
88 49 33 87 subdid ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→4⁢B2⁢C2−B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2=4⁢B2⁢C2−4⁢B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2
89 57 86 88 3eqtr2rd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→4⁢B2⁢C2−4⁢B2⁢C2+A2⁢C2-A2⁢A2⁢R2+A2⁢B2⁢R2=4⁢A2⁢D
90 47 89 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧R∈ℂ→T2−4⁢Q⁢U=4⁢A2⁢D