Metamath Proof Explorer

Theorem 2sqreultblem

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

Ref Expression
Assertion 2sqreultblem ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 2sqreultlem ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2 1 ex ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 → ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
3 2reu2rex ⊢ ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
4 elsni ⊢ ( 𝑃 ∈ { 2 } → 𝑃 = 2 )
5 eqeq2 ⊢ ( 𝑃 = 2 → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ↔ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 ) )
6 5 anbi2d ⊢ ( 𝑃 = 2 → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 ) ) )
7 6 adantl ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑃 = 2 ) → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 ) ) )
8 2sq2 ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 ↔ ( 𝑎 = 1 ∧ 𝑏 = 1 ) ) )
9 breq12 ⊢ ( ( 𝑎 = 1 ∧ 𝑏 = 1 ) → ( 𝑎 < 𝑏 ↔ 1 < 1 ) )
10 1re ⊢ 1 ∈ ℝ
11 10 ltnri ⊢ ¬ 1 < 1
12 11 pm2.21i ⊢ ( 1 < 1 → ( 𝑃 mod 4 ) = 1 )
13 9 12 syl6bi ⊢ ( ( 𝑎 = 1 ∧ 𝑏 = 1 ) → ( 𝑎 < 𝑏 → ( 𝑃 mod 4 ) = 1 ) )
14 8 13 syl6bi ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 → ( 𝑎 < 𝑏 → ( 𝑃 mod 4 ) = 1 ) ) )
15 14 impcomd ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 ) → ( 𝑃 mod 4 ) = 1 ) )
16 15 adantr ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑃 = 2 ) → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 2 ) → ( 𝑃 mod 4 ) = 1 ) )
17 7 16 sylbid ⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑃 = 2 ) → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) )
18 17 ex ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑃 = 2 → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) ) )
19 18 com23 ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 = 2 → ( 𝑃 mod 4 ) = 1 ) ) )
20 19 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 = 2 → ( 𝑃 mod 4 ) = 1 ) )
21 3 4 20 syl2imc ⊢ ( 𝑃 ∈ { 2 } → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) )
22 21 a1d ⊢ ( 𝑃 ∈ { 2 } → ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) ) )
23 eldif ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∈ { 2 } ) )
24 eldifsnneq ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑃 = 2 )
25 nn0ssz ⊢ ℕ0 ⊆ ℤ
26 id ⊢ ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 )
27 26 eqcomd ⊢ ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 → 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
28 27 adantl ⊢ ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
29 28 reximi ⊢ ( ∃ 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
30 29 reximi ⊢ ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
31 ssrexv ⊢ ( ℕ0 ⊆ ℤ → ( ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) )
32 25 31 ax-mp ⊢ ( ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
33 32 reximi ⊢ ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
34 3 30 33 3syl ⊢ ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
35 ssrexv ⊢ ( ℕ0 ⊆ ℤ → ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) )
36 25 34 35 mpsyl ⊢ ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
37 36 adantl ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
38 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
39 38 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → 𝑃 ∈ ℙ )
40 2sqb ⊢ ( 𝑃 ∈ ℙ → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) ) )
41 39 40 syl ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) ) )
42 37 41 mpbid ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) )
43 42 ord ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) → ( ¬ 𝑃 = 2 → ( 𝑃 mod 4 ) = 1 ) )
44 43 ex ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( ¬ 𝑃 = 2 → ( 𝑃 mod 4 ) = 1 ) ) )
45 24 44 mpid ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) )
46 23 45 sylbir ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∈ { 2 } ) → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) )
47 46 expcom ⊢ ( ¬ 𝑃 ∈ { 2 } → ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) ) )
48 22 47 pm2.61i ⊢ ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) → ( 𝑃 mod 4 ) = 1 ) )
49 2 48 impbid ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )