4sqlem2

Description: Lemma for 4sq . Change bound variables 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	4sqlem2	$⊢ A \in S \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2}$

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	1	eleq2i	$⊢ A \in S \leftrightarrow A \in \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
3		id	$⊢ A = a^{2} + b^{2} + c^{2} + d^{2} \to A = a^{2} + b^{2} + c^{2} + d^{2}$
4		ovex	$⊢ a^{2} + b^{2} + c^{2} + d^{2} \in V$
5	3 4	eqeltrdi	$⊢ A = a^{2} + b^{2} + c^{2} + d^{2} \to A \in V$
6	5	a1i	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \to (A = a^{2} + b^{2} + c^{2} + d^{2} \to A \in V)$
7	6	rexlimdvva	$⊢ (a \in ℤ \land b \in ℤ) \to (\exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2} \to A \in V)$
8	7	rexlimivv	$⊢ \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2} \to A \in V$
9		oveq1	$⊢ x = a \to x^{2} = a^{2}$
10	9	oveq1d	$⊢ x = a \to x^{2} + y^{2} = a^{2} + y^{2}$
11	10	oveq1d	$⊢ x = a \to x^{2} + y^{2} + z^{2} + w^{2} = a^{2} + y^{2} + z^{2} + w^{2}$
12	11	eqeq2d	$⊢ x = a \to (n = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow n = a^{2} + y^{2} + z^{2} + w^{2})$
13	12	2rexbidv	$⊢ x = a \to (\exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow \exists z \in ℤ \exists w \in ℤ n = a^{2} + y^{2} + z^{2} + w^{2})$
14		oveq1	$⊢ y = b \to y^{2} = b^{2}$
15	14	oveq2d	$⊢ y = b \to a^{2} + y^{2} = a^{2} + b^{2}$
16	15	oveq1d	$⊢ y = b \to a^{2} + y^{2} + z^{2} + w^{2} = a^{2} + b^{2} + z^{2} + w^{2}$
17	16	eqeq2d	$⊢ y = b \to (n = a^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow n = a^{2} + b^{2} + z^{2} + w^{2})$
18	17	2rexbidv	$⊢ y = b \to (\exists z \in ℤ \exists w \in ℤ n = a^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow \exists z \in ℤ \exists w \in ℤ n = a^{2} + b^{2} + z^{2} + w^{2})$
19	13 18	cbvrex2vw	$⊢ \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists z \in ℤ \exists w \in ℤ n = a^{2} + b^{2} + z^{2} + w^{2}$
20		oveq1	$⊢ z = c \to z^{2} = c^{2}$
21	20	oveq1d	$⊢ z = c \to z^{2} + w^{2} = c^{2} + w^{2}$
22	21	oveq2d	$⊢ z = c \to a^{2} + b^{2} + z^{2} + w^{2} = a^{2} + b^{2} + c^{2} + w^{2}$
23	22	eqeq2d	$⊢ z = c \to (n = a^{2} + b^{2} + z^{2} + w^{2} \leftrightarrow n = a^{2} + b^{2} + c^{2} + w^{2})$
24		oveq1	$⊢ w = d \to w^{2} = d^{2}$
25	24	oveq2d	$⊢ w = d \to c^{2} + w^{2} = c^{2} + d^{2}$
26	25	oveq2d	$⊢ w = d \to a^{2} + b^{2} + c^{2} + w^{2} = a^{2} + b^{2} + c^{2} + d^{2}$
27	26	eqeq2d	$⊢ w = d \to (n = a^{2} + b^{2} + c^{2} + w^{2} \leftrightarrow n = a^{2} + b^{2} + c^{2} + d^{2})$
28	23 27	cbvrex2vw	$⊢ \exists z \in ℤ \exists w \in ℤ n = a^{2} + b^{2} + z^{2} + w^{2} \leftrightarrow \exists c \in ℤ \exists d \in ℤ n = a^{2} + b^{2} + c^{2} + d^{2}$
29		eqeq1	$⊢ n = A \to (n = a^{2} + b^{2} + c^{2} + d^{2} \leftrightarrow A = a^{2} + b^{2} + c^{2} + d^{2})$
30	29	2rexbidv	$⊢ n = A \to (\exists c \in ℤ \exists d \in ℤ n = a^{2} + b^{2} + c^{2} + d^{2} \leftrightarrow \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2})$
31	28 30	syl5bb	$⊢ n = A \to (\exists z \in ℤ \exists w \in ℤ n = a^{2} + b^{2} + z^{2} + w^{2} \leftrightarrow \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2})$
32	31	2rexbidv	$⊢ n = A \to (\exists a \in ℤ \exists b \in ℤ \exists z \in ℤ \exists w \in ℤ n = a^{2} + b^{2} + z^{2} + w^{2} \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2})$
33	19 32	syl5bb	$⊢ n = A \to (\exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2})$
34	8 33	elab3	$⊢ A \in \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\} \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2}$
35	2 34	bitri	$⊢ A \in S \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2}$

Metamath Proof Explorer

Theorem 4sqlem2

Proof