Metamath Proof Explorer


Theorem 4sqlem3

Description: Lemma for 4sq . Sufficient condition to be in S . (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Hypothesis 4sq.1 S=n|xyzwn=x2+y2+z2+w2
Assertion 4sqlem3 ABCDA2+B2+C2+D2S

Proof

Step Hyp Ref Expression
1 4sq.1 S=n|xyzwn=x2+y2+z2+w2
2 eqid A2+B2+C2+D2=A2+B2+C2+D2
3 oveq1 c=Cc2=C2
4 3 oveq1d c=Cc2+d2=C2+d2
5 4 oveq2d c=CA2+B2+c2+d2=A2+B2+C2+d2
6 5 eqeq2d c=CA2+B2+C2+D2=A2+B2+c2+d2A2+B2+C2+D2=A2+B2+C2+d2
7 oveq1 d=Dd2=D2
8 7 oveq2d d=DC2+d2=C2+D2
9 8 oveq2d d=DA2+B2+C2+d2=A2+B2+C2+D2
10 9 eqeq2d d=DA2+B2+C2+D2=A2+B2+C2+d2A2+B2+C2+D2=A2+B2+C2+D2
11 6 10 rspc2ev CDA2+B2+C2+D2=A2+B2+C2+D2cdA2+B2+C2+D2=A2+B2+c2+d2
12 2 11 mp3an3 CDcdA2+B2+C2+D2=A2+B2+c2+d2
13 oveq1 a=Aa2=A2
14 13 oveq1d a=Aa2+b2=A2+b2
15 14 oveq1d a=Aa2+b2+c2+d2=A2+b2+c2+d2
16 15 eqeq2d a=AA2+B2+C2+D2=a2+b2+c2+d2A2+B2+C2+D2=A2+b2+c2+d2
17 16 2rexbidv a=AcdA2+B2+C2+D2=a2+b2+c2+d2cdA2+B2+C2+D2=A2+b2+c2+d2
18 oveq1 b=Bb2=B2
19 18 oveq2d b=BA2+b2=A2+B2
20 19 oveq1d b=BA2+b2+c2+d2=A2+B2+c2+d2
21 20 eqeq2d b=BA2+B2+C2+D2=A2+b2+c2+d2A2+B2+C2+D2=A2+B2+c2+d2
22 21 2rexbidv b=BcdA2+B2+C2+D2=A2+b2+c2+d2cdA2+B2+C2+D2=A2+B2+c2+d2
23 17 22 rspc2ev ABcdA2+B2+C2+D2=A2+B2+c2+d2abcdA2+B2+C2+D2=a2+b2+c2+d2
24 23 3expa ABcdA2+B2+C2+D2=A2+B2+c2+d2abcdA2+B2+C2+D2=a2+b2+c2+d2
25 1 4sqlem2 A2+B2+C2+D2SabcdA2+B2+C2+D2=a2+b2+c2+d2
26 24 25 sylibr ABcdA2+B2+C2+D2=A2+B2+c2+d2A2+B2+C2+D2S
27 12 26 sylan2 ABCDA2+B2+C2+D2S