Metamath Proof Explorer


Theorem 2sqb

Description: The converse to 2sq . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion 2sqb P x y P = x 2 + y 2 P = 2 P mod 4 = 1

Proof

Step Hyp Ref Expression
1 df-ne P 2 ¬ P = 2
2 prmz P P
3 2 ad3antrrr P P 2 x y P = x 2 + y 2 P
4 simplrr P P 2 x y P = x 2 + y 2 y
5 bezout P y a b P gcd y = P a + y b
6 3 4 5 syl2anc P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b
7 simplll P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b P P 2
8 simpllr P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b x y
9 simplr P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b P = x 2 + y 2
10 simprll P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b a
11 simprlr P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b b
12 simprr P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b P gcd y = P a + y b
13 7 8 9 10 11 12 2sqblem P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b P mod 4 = 1
14 13 expr P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b P mod 4 = 1
15 14 rexlimdvva P P 2 x y P = x 2 + y 2 a b P gcd y = P a + y b P mod 4 = 1
16 6 15 mpd P P 2 x y P = x 2 + y 2 P mod 4 = 1
17 16 ex P P 2 x y P = x 2 + y 2 P mod 4 = 1
18 17 rexlimdvva P P 2 x y P = x 2 + y 2 P mod 4 = 1
19 18 impancom P x y P = x 2 + y 2 P 2 P mod 4 = 1
20 1 19 syl5bir P x y P = x 2 + y 2 ¬ P = 2 P mod 4 = 1
21 20 orrd P x y P = x 2 + y 2 P = 2 P mod 4 = 1
22 1z 1
23 oveq1 x = 1 x 2 = 1 2
24 sq1 1 2 = 1
25 23 24 eqtrdi x = 1 x 2 = 1
26 25 oveq1d x = 1 x 2 + y 2 = 1 + y 2
27 26 eqeq2d x = 1 P = x 2 + y 2 P = 1 + y 2
28 oveq1 y = 1 y 2 = 1 2
29 28 24 eqtrdi y = 1 y 2 = 1
30 29 oveq2d y = 1 1 + y 2 = 1 + 1
31 1p1e2 1 + 1 = 2
32 30 31 eqtrdi y = 1 1 + y 2 = 2
33 32 eqeq2d y = 1 P = 1 + y 2 P = 2
34 27 33 rspc2ev 1 1 P = 2 x y P = x 2 + y 2
35 22 22 34 mp3an12 P = 2 x y P = x 2 + y 2
36 35 adantl P P = 2 x y P = x 2 + y 2
37 2sq P P mod 4 = 1 x y P = x 2 + y 2
38 36 37 jaodan P P = 2 P mod 4 = 1 x y P = x 2 + y 2
39 21 38 impbida P x y P = x 2 + y 2 P = 2 P mod 4 = 1