This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sqlem4a

Description: Lemma for 4sqlem4 . (Contributed by Mario Carneiro, 14-Jul-2014)

Ref

Expression

Hypothesis

4sq.1

|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }

Assertion

|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. S )

Proof

Step	Hyp	Ref	Expression
1		4sq.1	\|- S = { n \| E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2		gzcn	\|- ( A e. Z[i] -> A e. CC )
3	2	absvalsq2d	\|- ( A e. Z[i] -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
4		gzcn	\|- ( B e. Z[i] -> B e. CC )
5	4	absvalsq2d	\|- ( B e. Z[i] -> ( ( abs ` B ) ^ 2 ) = ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) )
6	3 5	oveqan12d	\|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) + ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) ) )
7		elgz	\|- ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
8	7	simp2bi	\|- ( A e. Z[i] -> ( Re ` A ) e. ZZ )
9	7	simp3bi	\|- ( A e. Z[i] -> ( Im ` A ) e. ZZ )
10	8 9	jca	\|- ( A e. Z[i] -> ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
11		elgz	\|- ( B e. Z[i] <-> ( B e. CC /\ ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) )
12	11	simp2bi	\|- ( B e. Z[i] -> ( Re ` B ) e. ZZ )
13	11	simp3bi	\|- ( B e. Z[i] -> ( Im ` B ) e. ZZ )
14	12 13	jca	\|- ( B e. Z[i] -> ( ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) )
15	1	4sqlem3	\|- ( ( ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) /\ ( ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) + ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) ) e. S )
16	10 14 15	syl2an	\|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) + ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) ) e. S )
17	6 16	eqeltrd	\|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. S )