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 P P mod 4 = 1 ∃! a 0 ∃! b 0 a < b a 2 + b 2 = P

Proof

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