Metamath Proof Explorer

Theorem 2sqlem5

Description: Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2sqlem5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2sqlem5.3 ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) ∈ 𝑆 )
2sqlem5.4 ⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )
Assertion 2sqlem5 ( 𝜑 → 𝑁 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 2sqlem5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
4 2sqlem5.3 ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) ∈ 𝑆 )
5 2sqlem5.4 ⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )
6 1 2sqlem2 ⊢ ( 𝑃 ∈ 𝑆 ↔ ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) )
7 5 6 sylib ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) )
8 1 2sqlem2 ⊢ ( ( 𝑁 · 𝑃 ) ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
9 4 8 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
10 reeanv ⊢ ( ∃ 𝑝 ∈ ℤ ∃ 𝑥 ∈ ℤ ( ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
11 reeanv ⊢ ( ∃ 𝑞 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
12 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑁 ∈ ℕ )
13 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑃 ∈ ℙ )
14 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑥 ∈ ℤ )
15 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑦 ∈ ℤ )
16 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑝 ∈ ℤ )
17 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑞 ∈ ℤ )
18 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
19 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) )
20 1 12 13 14 15 16 17 18 19 2sqlem4 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) → 𝑁 ∈ 𝑆 )
21 20 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) ∧ ( 𝑞 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑁 ∈ 𝑆 ) )
22 21 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( ∃ 𝑞 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑁 ∈ 𝑆 ) )
23 11 22 syl5bir ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( ( ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑁 ∈ 𝑆 ) )
24 23 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℤ ∃ 𝑥 ∈ ℤ ( ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑁 ∈ 𝑆 ) )
25 10 24 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℤ 𝑃 = ( ( 𝑝 ↑ 2 ) + ( 𝑞 ↑ 2 ) ) ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 · 𝑃 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑁 ∈ 𝑆 ) )
26 7 9 25 mp2and ⊢ ( 𝜑 → 𝑁 ∈ 𝑆 )