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 \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
	Assertion	4sqlem3	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A^{2} + B^{2} + C^{2} + D^{2} \in S$

Proof

Step	Hyp	Ref	Expression
1		4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
2		eqid	$⊢ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + C^{2} + D^{2}$
3		oveq1	$⊢ c = C \to c^{2} = C^{2}$
4	3	oveq1d	$⊢ c = C \to c^{2} + d^{2} = C^{2} + d^{2}$
5	4	oveq2d	$⊢ c = C \to A^{2} + B^{2} + c^{2} + d^{2} = A^{2} + B^{2} + C^{2} + d^{2}$
6	5	eqeq2d	$⊢ c = C \to (A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2} \leftrightarrow A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + C^{2} + d^{2})$
7		oveq1	$⊢ d = D \to d^{2} = D^{2}$
8	7	oveq2d	$⊢ d = D \to C^{2} + d^{2} = C^{2} + D^{2}$
9	8	oveq2d	$⊢ d = D \to A^{2} + B^{2} + C^{2} + d^{2} = A^{2} + B^{2} + C^{2} + D^{2}$
10	9	eqeq2d	$⊢ d = D \to (A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + C^{2} + d^{2} \leftrightarrow A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + C^{2} + D^{2})$
11	6 10	rspc2ev	$⊢ (C \in ℤ \land D \in ℤ \land A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + C^{2} + D^{2}) \to \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2}$
12	2 11	mp3an3	$⊢ (C \in ℤ \land D \in ℤ) \to \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2}$
13		oveq1	$⊢ a = A \to a^{2} = A^{2}$
14	13	oveq1d	$⊢ a = A \to a^{2} + b^{2} = A^{2} + b^{2}$
15	14	oveq1d	$⊢ a = A \to a^{2} + b^{2} + c^{2} + d^{2} = A^{2} + b^{2} + c^{2} + d^{2}$
16	15	eqeq2d	$⊢ a = A \to (A^{2} + B^{2} + C^{2} + D^{2} = a^{2} + b^{2} + c^{2} + d^{2} \leftrightarrow A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + b^{2} + c^{2} + d^{2})$
17	16	2rexbidv	$⊢ a = A \to (\exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = a^{2} + b^{2} + c^{2} + d^{2} \leftrightarrow \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + b^{2} + c^{2} + d^{2})$
18		oveq1	$⊢ b = B \to b^{2} = B^{2}$
19	18	oveq2d	$⊢ b = B \to A^{2} + b^{2} = A^{2} + B^{2}$
20	19	oveq1d	$⊢ b = B \to A^{2} + b^{2} + c^{2} + d^{2} = A^{2} + B^{2} + c^{2} + d^{2}$
21	20	eqeq2d	$⊢ b = B \to (A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + b^{2} + c^{2} + d^{2} \leftrightarrow A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2})$
22	21	2rexbidv	$⊢ b = B \to (\exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + b^{2} + c^{2} + d^{2} \leftrightarrow \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2})$
23	17 22	rspc2ev	$⊢ (A \in ℤ \land B \in ℤ \land \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2}) \to \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = a^{2} + b^{2} + c^{2} + d^{2}$
24	23	3expa	$⊢ ((A \in ℤ \land B \in ℤ) \land \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2}) \to \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = a^{2} + b^{2} + c^{2} + d^{2}$
25	1	4sqlem2	$⊢ A^{2} + B^{2} + C^{2} + D^{2} \in S \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = a^{2} + b^{2} + c^{2} + d^{2}$
26	24 25	sylibr	$⊢ ((A \in ℤ \land B \in ℤ) \land \exists c \in ℤ \exists d \in ℤ A^{2} + B^{2} + C^{2} + D^{2} = A^{2} + B^{2} + c^{2} + d^{2}) \to A^{2} + B^{2} + C^{2} + D^{2} \in S$
27	12 26	sylan2	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A^{2} + B^{2} + C^{2} + D^{2} \in S$

Metamath Proof Explorer

Theorem 4sqlem3

Proof