Metamath Proof Explorer


Theorem 2sqreultlem

Description: Lemma for 2sqreult . (Contributed by AV, 8-Jun-2023) (Proposed by GL, 8-Jun-2023.)

Ref Expression
Assertion 2sqreultlem P P mod 4 = 1 ∃! a 0 ∃! b 0 a < b a 2 + b 2 = P

Proof

Step Hyp Ref Expression
1 2sqreulem1 P P mod 4 = 1 ∃! a 0 ∃! b 0 a b a 2 + b 2 = P
2 oveq1 b = a b 2 = a 2
3 2 oveq2d b = a a 2 + b 2 = a 2 + a 2
4 3 adantr b = a P P mod 4 = 1 a 0 b 0 a 2 + b 2 = a 2 + a 2
5 nn0cn a 0 a
6 5 sqcld a 0 a 2
7 2times a 2 2 a 2 = a 2 + a 2
8 7 eqcomd a 2 a 2 + a 2 = 2 a 2
9 6 8 syl a 0 a 2 + a 2 = 2 a 2
10 9 adantl P P mod 4 = 1 a 0 a 2 + a 2 = 2 a 2
11 10 ad2antrl b = a P P mod 4 = 1 a 0 b 0 a 2 + a 2 = 2 a 2
12 4 11 eqtrd b = a P P mod 4 = 1 a 0 b 0 a 2 + b 2 = 2 a 2
13 12 eqeq1d b = a P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P 2 a 2 = P
14 oveq1 P = 2 a 2 P mod 4 = 2 a 2 mod 4
15 14 eqeq1d P = 2 a 2 P mod 4 = 1 2 a 2 mod 4 = 1
16 eleq1 P = 2 a 2 P 2 a 2
17 15 16 anbi12d P = 2 a 2 P mod 4 = 1 P 2 a 2 mod 4 = 1 2 a 2
18 nn0z a 0 a
19 2nn0 2 0
20 zexpcl a 2 0 a 2
21 18 19 20 sylancl a 0 a 2
22 2mulprm a 2 2 a 2 a 2 = 1
23 21 22 syl a 0 2 a 2 a 2 = 1
24 oveq2 a 2 = 1 2 a 2 = 2 1
25 2t1e2 2 1 = 2
26 24 25 eqtrdi a 2 = 1 2 a 2 = 2
27 26 oveq1d a 2 = 1 2 a 2 mod 4 = 2 mod 4
28 2re 2
29 4nn 4
30 nnrp 4 4 +
31 29 30 ax-mp 4 +
32 0le2 0 2
33 2lt4 2 < 4
34 modid 2 4 + 0 2 2 < 4 2 mod 4 = 2
35 28 31 32 33 34 mp4an 2 mod 4 = 2
36 27 35 eqtrdi a 2 = 1 2 a 2 mod 4 = 2
37 36 eqeq1d a 2 = 1 2 a 2 mod 4 = 1 2 = 1
38 1ne2 1 2
39 eqcom 2 = 1 1 = 2
40 eqneqall 1 = 2 1 2 a b b a
41 40 com12 1 2 1 = 2 a b b a
42 39 41 syl5bi 1 2 2 = 1 a b b a
43 38 42 ax-mp 2 = 1 a b b a
44 37 43 syl6bi a 2 = 1 2 a 2 mod 4 = 1 a b b a
45 23 44 syl6bi a 0 2 a 2 2 a 2 mod 4 = 1 a b b a
46 45 impcomd a 0 2 a 2 mod 4 = 1 2 a 2 a b b a
47 46 com12 2 a 2 mod 4 = 1 2 a 2 a 0 a b b a
48 17 47 syl6bi P = 2 a 2 P mod 4 = 1 P a 0 a b b a
49 48 expd P = 2 a 2 P mod 4 = 1 P a 0 a b b a
50 49 com34 P = 2 a 2 P mod 4 = 1 a 0 P a b b a
51 50 eqcoms 2 a 2 = P P mod 4 = 1 a 0 P a b b a
52 51 com14 P P mod 4 = 1 a 0 2 a 2 = P a b b a
53 52 imp31 P P mod 4 = 1 a 0 2 a 2 = P a b b a
54 53 ad2antrl b = a P P mod 4 = 1 a 0 b 0 2 a 2 = P a b b a
55 13 54 sylbid b = a P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b b a
56 55 expimpd b = a P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b b a
57 2a1 b a P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b b a
58 56 57 pm2.61ine P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b b a
59 58 pm4.71d P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b a b b a
60 nn0re a 0 a
61 60 adantl P P mod 4 = 1 a 0 a
62 nn0re b 0 b
63 ltlen a b a < b a b b a
64 61 62 63 syl2an P P mod 4 = 1 a 0 b 0 a < b a b b a
65 64 bibi2d P P mod 4 = 1 a 0 b 0 a b a < b a b a b b a
66 65 adantr P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b a < b a b a b b a
67 59 66 mpbird P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b a < b
68 67 ex P P mod 4 = 1 a 0 b 0 a 2 + b 2 = P a b a < b
69 68 pm5.32rd P P mod 4 = 1 a 0 b 0 a b a 2 + b 2 = P a < b a 2 + b 2 = P
70 69 reubidva P P mod 4 = 1 a 0 ∃! b 0 a b a 2 + b 2 = P ∃! b 0 a < b a 2 + b 2 = P
71 70 reubidva P P mod 4 = 1 ∃! a 0 ∃! b 0 a b a 2 + b 2 = P ∃! a 0 ∃! b 0 a < b a 2 + b 2 = P
72 1 71 mpbid P P mod 4 = 1 ∃! a 0 ∃! b 0 a < b a 2 + b 2 = P