Metamath Proof Explorer

Theorem 2sqlem11

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
Assertion 2sqlem11 ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → 𝑃 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
3 simpr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( 𝑃 mod 4 ) = 1 )
4 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → 𝑃 ∈ ℙ )
5 1ne2 ⊢ 1 ≠ 2
6 5 necomi ⊢ 2 ≠ 1
7 oveq1 ⊢ ( 𝑃 = 2 → ( 𝑃 mod 4 ) = ( 2 mod 4 ) )
8 2re ⊢ 2 ∈ ℝ
9 4re ⊢ 4 ∈ ℝ
10 4pos ⊢ 0 < 4
11 9 10 elrpii ⊢ 4 ∈ ℝ+
12 0le2 ⊢ 0 ≤ 2
13 2lt4 ⊢ 2 < 4
14 modid ⊢ ( ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ+ ) ∧ ( 0 ≤ 2 ∧ 2 < 4 ) ) → ( 2 mod 4 ) = 2 )
15 8 11 12 13 14 mp4an ⊢ ( 2 mod 4 ) = 2
16 7 15 eqtrdi ⊢ ( 𝑃 = 2 → ( 𝑃 mod 4 ) = 2 )
17 16 neeq1d ⊢ ( 𝑃 = 2 → ( ( 𝑃 mod 4 ) ≠ 1 ↔ 2 ≠ 1 ) )
18 6 17 mpbiri ⊢ ( 𝑃 = 2 → ( 𝑃 mod 4 ) ≠ 1 )
19 18 necon2i ⊢ ( ( 𝑃 mod 4 ) = 1 → 𝑃 ≠ 2 )
20 3 19 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → 𝑃 ≠ 2 )
21 eldifsn ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
22 4 20 21 sylanbrc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
23 m1lgs ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = 1 ) )
24 22 23 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = 1 ) )
25 3 24 mpbird ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( - 1 /L 𝑃 ) = 1 )
26 neg1z ⊢ - 1 ∈ ℤ
27 lgsqr ⊢ ( ( - 1 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃 ∥ - 1 ∧ ∃ 𝑛 ∈ ℤ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) )
28 26 22 27 sylancr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃 ∥ - 1 ∧ ∃ 𝑛 ∈ ℤ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) )
29 25 28 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ¬ 𝑃 ∥ - 1 ∧ ∃ 𝑛 ∈ ℤ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) )
30 29 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑛 ∈ ℤ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) )
31 simprl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 𝑛 ∈ ℤ )
32 1zzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 1 ∈ ℤ )
33 gcd1 ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 gcd 1 ) = 1 )
34 33 ad2antrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → ( 𝑛 gcd 1 ) = 1 )
35 eqidd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + 1 ) )
36 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 gcd 𝑦 ) = ( 𝑛 gcd 𝑦 ) )
37 36 eqeq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 gcd 𝑦 ) = 1 ↔ ( 𝑛 gcd 𝑦 ) = 1 ) )
38 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ↑ 2 ) = ( 𝑛 ↑ 2 ) )
39 38 oveq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑛 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
40 39 eqeq2d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
41 37 40 anbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑛 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
42 oveq2 ⊢ ( 𝑦 = 1 → ( 𝑛 gcd 𝑦 ) = ( 𝑛 gcd 1 ) )
43 42 eqeq1d ⊢ ( 𝑦 = 1 → ( ( 𝑛 gcd 𝑦 ) = 1 ↔ ( 𝑛 gcd 1 ) = 1 ) )
44 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 ↑ 2 ) = ( 1 ↑ 2 ) )
45 sq1 ⊢ ( 1 ↑ 2 ) = 1
46 44 45 eqtrdi ⊢ ( 𝑦 = 1 → ( 𝑦 ↑ 2 ) = 1 )
47 46 oveq2d ⊢ ( 𝑦 = 1 → ( ( 𝑛 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑛 ↑ 2 ) + 1 ) )
48 47 eqeq2d ⊢ ( 𝑦 = 1 → ( ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + 1 ) ) )
49 43 48 anbi12d ⊢ ( 𝑦 = 1 → ( ( ( 𝑛 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑛 gcd 1 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + 1 ) ) ) )
50 41 49 rspc2ev ⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ∧ ( ( 𝑛 gcd 1 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑛 ↑ 2 ) + 1 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
51 31 32 34 35 50 syl112anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
52 ovex ⊢ ( ( 𝑛 ↑ 2 ) + 1 ) ∈ V
53 eqeq1 ⊢ ( 𝑧 = ( ( 𝑛 ↑ 2 ) + 1 ) → ( 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
54 53 anbi2d ⊢ ( 𝑧 = ( ( 𝑛 ↑ 2 ) + 1 ) → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
55 54 2rexbidv ⊢ ( 𝑧 = ( ( 𝑛 ↑ 2 ) + 1 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
56 52 55 2 elab2 ⊢ ( ( ( 𝑛 ↑ 2 ) + 1 ) ∈ 𝑌 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝑛 ↑ 2 ) + 1 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
57 51 56 sylibr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → ( ( 𝑛 ↑ 2 ) + 1 ) ∈ 𝑌 )
58 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
59 58 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 𝑃 ∈ ℕ )
60 simprr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) )
61 31 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 𝑛 ∈ ℂ )
62 61 sqcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
63 ax-1cn ⊢ 1 ∈ ℂ
64 subneg ⊢ ( ( ( 𝑛 ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 ↑ 2 ) − - 1 ) = ( ( 𝑛 ↑ 2 ) + 1 ) )
65 62 63 64 sylancl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → ( ( 𝑛 ↑ 2 ) − - 1 ) = ( ( 𝑛 ↑ 2 ) + 1 ) )
66 60 65 breqtrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 𝑃 ∥ ( ( 𝑛 ↑ 2 ) + 1 ) )
67 1 2 2sqlem10 ⊢ ( ( ( ( 𝑛 ↑ 2 ) + 1 ) ∈ 𝑌 ∧ 𝑃 ∈ ℕ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) + 1 ) ) → 𝑃 ∈ 𝑆 )
68 57 59 66 67 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑛 ↑ 2 ) − - 1 ) ) ) → 𝑃 ∈ 𝑆 )
69 30 68 rexlimddv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → 𝑃 ∈ 𝑆 )