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∈ℙ→Pmod4=1↔∃!a∈ℕ∃!b∈ℕa<b∧a2+b2=P

Proof

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