Metamath Proof Explorer

Theorem 2sqlem11

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

Ref Expression
Hypotheses 2sq.1 ⊢ S = ran ⁡ w ∈ ℤ i ⟼ w 2
2sqlem7.2 ⊢ Y = z | ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ z = x 2 + y 2
Assertion 2sqlem11 ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P ∈ S

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ S = ran ⁡ w ∈ ℤ i ⟼ w 2
2 2sqlem7.2 ⊢ Y = z | ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ z = x 2 + y 2
3 simpr ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P mod 4 = 1
4 simpl ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P ∈ ℙ
5 1ne2 ⊢ 1 ≠ 2
6 5 necomi ⊢ 2 ≠ 1
7 oveq1 ⊢ P = 2 → P 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 ⊢ P = 2 → P mod 4 = 2
17 16 neeq1d ⊢ P = 2 → P mod 4 ≠ 1 ↔ 2 ≠ 1
18 6 17 mpbiri ⊢ P = 2 → P mod 4 ≠ 1
19 18 necon2i ⊢ P mod 4 = 1 → P ≠ 2
20 3 19 syl ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P ≠ 2
21 eldifsn ⊢ P ∈ ℙ ∖ 2 ↔ P ∈ ℙ ∧ P ≠ 2
22 4 20 21 sylanbrc ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P ∈ ℙ ∖ 2
23 m1lgs ⊢ P ∈ ℙ ∖ 2 → -1 / L P = 1 ↔ P mod 4 = 1
24 22 23 syl ⊢ P ∈ ℙ ∧ P mod 4 = 1 → -1 / L P = 1 ↔ P mod 4 = 1
25 3 24 mpbird ⊢ P ∈ ℙ ∧ P mod 4 = 1 → -1 / L P = 1
26 neg1z ⊢ − 1 ∈ ℤ
27 lgsqr ⊢ − 1 ∈ ℤ ∧ P ∈ ℙ ∖ 2 → -1 / L P = 1 ↔ ¬ P ∥ -1 ∧ ∃ n ∈ ℤ P ∥ n 2 − -1
28 26 22 27 sylancr ⊢ P ∈ ℙ ∧ P mod 4 = 1 → -1 / L P = 1 ↔ ¬ P ∥ -1 ∧ ∃ n ∈ ℤ P ∥ n 2 − -1
29 25 28 mpbid ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ¬ P ∥ -1 ∧ ∃ n ∈ ℤ P ∥ n 2 − -1
30 29 simprd ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃ n ∈ ℤ P ∥ n 2 − -1
31 simprl ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n ∈ ℤ
32 1zzd ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → 1 ∈ ℤ
33 gcd1 ⊢ n ∈ ℤ → n gcd 1 = 1
34 33 ad2antrl ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n gcd 1 = 1
35 eqidd ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n 2 + 1 = n 2 + 1
36 oveq1 ⊢ x = n → x gcd y = n gcd y
37 36 eqeq1d ⊢ x = n → x gcd y = 1 ↔ n gcd y = 1
38 oveq1 ⊢ x = n → x 2 = n 2
39 38 oveq1d ⊢ x = n → x 2 + y 2 = n 2 + y 2
40 39 eqeq2d ⊢ x = n → n 2 + 1 = x 2 + y 2 ↔ n 2 + 1 = n 2 + y 2
41 37 40 anbi12d ⊢ x = n → x gcd y = 1 ∧ n 2 + 1 = x 2 + y 2 ↔ n gcd y = 1 ∧ n 2 + 1 = n 2 + y 2
42 oveq2 ⊢ y = 1 → n gcd y = n gcd 1
43 42 eqeq1d ⊢ y = 1 → n gcd y = 1 ↔ n gcd 1 = 1
44 oveq1 ⊢ y = 1 → y 2 = 1 2
45 sq1 ⊢ 1 2 = 1
46 44 45 eqtrdi ⊢ y = 1 → y 2 = 1
47 46 oveq2d ⊢ y = 1 → n 2 + y 2 = n 2 + 1
48 47 eqeq2d ⊢ y = 1 → n 2 + 1 = n 2 + y 2 ↔ n 2 + 1 = n 2 + 1
49 43 48 anbi12d ⊢ y = 1 → n gcd y = 1 ∧ n 2 + 1 = n 2 + y 2 ↔ n gcd 1 = 1 ∧ n 2 + 1 = n 2 + 1
50 41 49 rspc2ev ⊢ n ∈ ℤ ∧ 1 ∈ ℤ ∧ n gcd 1 = 1 ∧ n 2 + 1 = n 2 + 1 → ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ n 2 + 1 = x 2 + y 2
51 31 32 34 35 50 syl112anc ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ n 2 + 1 = x 2 + y 2
52 ovex ⊢ n 2 + 1 ∈ V
53 eqeq1 ⊢ z = n 2 + 1 → z = x 2 + y 2 ↔ n 2 + 1 = x 2 + y 2
54 53 anbi2d ⊢ z = n 2 + 1 → x gcd y = 1 ∧ z = x 2 + y 2 ↔ x gcd y = 1 ∧ n 2 + 1 = x 2 + y 2
55 54 2rexbidv ⊢ z = n 2 + 1 → ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ z = x 2 + y 2 ↔ ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ n 2 + 1 = x 2 + y 2
56 52 55 2 elab2 ⊢ n 2 + 1 ∈ Y ↔ ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ n 2 + 1 = x 2 + y 2
57 51 56 sylibr ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n 2 + 1 ∈ Y
58 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
59 58 ad2antrr ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → P ∈ ℕ
60 simprr ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → P ∥ n 2 − -1
61 31 zcnd ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n ∈ ℂ
62 61 sqcld ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n 2 ∈ ℂ
63 ax-1cn ⊢ 1 ∈ ℂ
64 subneg ⊢ n 2 ∈ ℂ ∧ 1 ∈ ℂ → n 2 − -1 = n 2 + 1
65 62 63 64 sylancl ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → n 2 − -1 = n 2 + 1
66 60 65 breqtrd ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → P ∥ n 2 + 1
67 1 2 2sqlem10 ⊢ n 2 + 1 ∈ Y ∧ P ∈ ℕ ∧ P ∥ n 2 + 1 → P ∈ S
68 57 59 66 67 syl3anc ⊢ P ∈ ℙ ∧ P mod 4 = 1 ∧ n ∈ ℤ ∧ P ∥ n 2 − -1 → P ∈ S
69 30 68 rexlimddv ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P ∈ S