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 ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑎 ∈ ℕ ∃! 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )

Proof

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