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 ) → 𝑃𝑆 )