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 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
Assertion 4sqlem3 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 eqid ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
3 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ↑ 2 ) = ( 𝐶 ↑ 2 ) )
4 3 oveq1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) )
5 4 oveq2d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
6 5 eqeq2d ⊢ ( 𝑐 = 𝐶 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ↔ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) )
7 oveq1 ⊢ ( 𝑑 = 𝐷 → ( 𝑑 ↑ 2 ) = ( 𝐷 ↑ 2 ) )
8 7 oveq2d ⊢ ( 𝑑 = 𝐷 → ( ( 𝐶 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
9 8 oveq2d ⊢ ( 𝑑 = 𝐷 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
10 9 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ↔ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
11 6 10 rspc2ev ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) → ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
12 2 11 mp3an3 ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
13 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
14 13 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
15 14 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
16 15 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ↔ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) )
17 16 2rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ↔ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) )
18 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
19 18 oveq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
20 19 oveq1d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
21 20 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ↔ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) )
22 21 2rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ↔ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) )
23 17 22 rspc2ev ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
24 23 3expa ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
25 1 4sqlem2 ⊢ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ 𝑆 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )
26 24 25 sylibr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ 𝑆 )
27 12 26 sylan2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ 𝑆 )