Metamath Proof Explorer

Theorem 2sqreunnltblem

Description: Lemma for 2sqreunnltb . (Contributed by AV, 11-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023)

Ref Expression
Assertion 2sqreunnltblem ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P

Proof

Step Hyp Ref Expression
1 2sqreunnltlem ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P
2 1 ex ⊢ P ∈ ℙ → P mod 4 = 1 → ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P
3 2reu2rex ⊢ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P
4 eqeq2 ⊢ P = 2 → a 2 + b 2 = P ↔ a 2 + b 2 = 2
5 4 adantr ⊢ P = 2 ∧ a ∈ ℕ ∧ b ∈ ℕ → a 2 + b 2 = P ↔ a 2 + b 2 = 2
6 nnnn0 ⊢ a ∈ ℕ → a ∈ ℕ 0
7 nnnn0 ⊢ b ∈ ℕ → b ∈ ℕ 0
8 2sq2 ⊢ a ∈ ℕ 0 ∧ b ∈ ℕ 0 → a 2 + b 2 = 2 ↔ a = 1 ∧ b = 1
9 6 7 8 syl2an ⊢ a ∈ ℕ ∧ b ∈ ℕ → a 2 + b 2 = 2 ↔ a = 1 ∧ b = 1
10 breq12 ⊢ a = 1 ∧ b = 1 → a < b ↔ 1 < 1
11 1re ⊢ 1 ∈ ℝ
12 11 ltnri ⊢ ¬ 1 < 1
13 12 pm2.21i ⊢ 1 < 1 → P mod 4 = 1
14 10 13 syl6bi ⊢ a = 1 ∧ b = 1 → a < b → P mod 4 = 1
15 9 14 syl6bi ⊢ a ∈ ℕ ∧ b ∈ ℕ → a 2 + b 2 = 2 → a < b → P mod 4 = 1
16 15 adantl ⊢ P = 2 ∧ a ∈ ℕ ∧ b ∈ ℕ → a 2 + b 2 = 2 → a < b → P mod 4 = 1
17 5 16 sylbid ⊢ P = 2 ∧ a ∈ ℕ ∧ b ∈ ℕ → a 2 + b 2 = P → a < b → P mod 4 = 1
18 17 impcomd ⊢ P = 2 ∧ a ∈ ℕ ∧ b ∈ ℕ → a < b ∧ a 2 + b 2 = P → P mod 4 = 1
19 18 rexlimdvva ⊢ P = 2 → ∃ a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P → P mod 4 = 1
20 3 19 syl5 ⊢ P = 2 → ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → P mod 4 = 1
21 20 a1d ⊢ P = 2 → P ∈ ℙ → ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → P mod 4 = 1
22 nnssz ⊢ ℕ ⊆ ℤ
23 id ⊢ a 2 + b 2 = P → a 2 + b 2 = P
24 23 eqcomd ⊢ a 2 + b 2 = P → P = a 2 + b 2
25 24 adantl ⊢ a < b ∧ a 2 + b 2 = P → P = a 2 + b 2
26 25 reximi ⊢ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ b ∈ ℕ P = a 2 + b 2
27 26 reximi ⊢ ∃ a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ a ∈ ℕ ∃ b ∈ ℕ P = a 2 + b 2
28 ssrexv ⊢ ℕ ⊆ ℤ → ∃ b ∈ ℕ P = a 2 + b 2 → ∃ b ∈ ℤ P = a 2 + b 2
29 22 28 ax-mp ⊢ ∃ b ∈ ℕ P = a 2 + b 2 → ∃ b ∈ ℤ P = a 2 + b 2
30 29 reximi ⊢ ∃ a ∈ ℕ ∃ b ∈ ℕ P = a 2 + b 2 → ∃ a ∈ ℕ ∃ b ∈ ℤ P = a 2 + b 2
31 3 27 30 3syl ⊢ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ a ∈ ℕ ∃ b ∈ ℤ P = a 2 + b 2
32 ssrexv ⊢ ℕ ⊆ ℤ → ∃ a ∈ ℕ ∃ b ∈ ℤ P = a 2 + b 2 → ∃ a ∈ ℤ ∃ b ∈ ℤ P = a 2 + b 2
33 22 31 32 mpsyl ⊢ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ a ∈ ℤ ∃ b ∈ ℤ P = a 2 + b 2
34 33 adantl ⊢ P ∈ ℙ ∧ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ a ∈ ℤ ∃ b ∈ ℤ P = a 2 + b 2
35 2sqb ⊢ P ∈ ℙ → ∃ a ∈ ℤ ∃ b ∈ ℤ P = a 2 + b 2 ↔ P = 2 ∨ P mod 4 = 1
36 35 adantr ⊢ P ∈ ℙ ∧ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → ∃ a ∈ ℤ ∃ b ∈ ℤ P = a 2 + b 2 ↔ P = 2 ∨ P mod 4 = 1
37 34 36 mpbid ⊢ P ∈ ℙ ∧ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → P = 2 ∨ P mod 4 = 1
38 37 ord ⊢ P ∈ ℙ ∧ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → ¬ P = 2 → P mod 4 = 1
39 38 expcom ⊢ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → P ∈ ℙ → ¬ P = 2 → P mod 4 = 1
40 39 com13 ⊢ ¬ P = 2 → P ∈ ℙ → ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → P mod 4 = 1
41 21 40 pm2.61i ⊢ P ∈ ℙ → ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P → P mod 4 = 1
42 2 41 impbid ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ ∃! b ∈ ℕ a < b ∧ a 2 + b 2 = P