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 e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )

Proof

Step Hyp Ref Expression
1 2sqreulem1
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN0 E! b e. NN0 ( 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 e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( a ^ 2 ) + ( a ^ 2 ) ) )
5 nn0cn
 |-  ( a e. NN0 -> a e. CC )
6 5 sqcld
 |-  ( a e. NN0 -> ( a ^ 2 ) e. CC )
7 2times
 |-  ( ( a ^ 2 ) e. CC -> ( 2 x. ( a ^ 2 ) ) = ( ( a ^ 2 ) + ( a ^ 2 ) ) )
8 7 eqcomd
 |-  ( ( a ^ 2 ) e. CC -> ( ( a ^ 2 ) + ( a ^ 2 ) ) = ( 2 x. ( a ^ 2 ) ) )
9 6 8 syl
 |-  ( a e. NN0 -> ( ( a ^ 2 ) + ( a ^ 2 ) ) = ( 2 x. ( a ^ 2 ) ) )
10 9 adantl
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) -> ( ( a ^ 2 ) + ( a ^ 2 ) ) = ( 2 x. ( a ^ 2 ) ) )
11 10 ad2antrl
 |-  ( ( b = a /\ ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) ) -> ( ( a ^ 2 ) + ( a ^ 2 ) ) = ( 2 x. ( a ^ 2 ) ) )
12 4 11 eqtrd
 |-  ( ( b = a /\ ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( 2 x. ( a ^ 2 ) ) )
13 12 eqeq1d
 |-  ( ( b = a /\ ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( 2 x. ( a ^ 2 ) ) = P ) )
14 oveq1
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( P mod 4 ) = ( ( 2 x. ( a ^ 2 ) ) mod 4 ) )
15 14 eqeq1d
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( ( P mod 4 ) = 1 <-> ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = 1 ) )
16 eleq1
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( P e. Prime <-> ( 2 x. ( a ^ 2 ) ) e. Prime ) )
17 15 16 anbi12d
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( ( ( P mod 4 ) = 1 /\ P e. Prime ) <-> ( ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = 1 /\ ( 2 x. ( a ^ 2 ) ) e. Prime ) ) )
18 nn0z
 |-  ( a e. NN0 -> a e. ZZ )
19 2nn0
 |-  2 e. NN0
20 zexpcl
 |-  ( ( a e. ZZ /\ 2 e. NN0 ) -> ( a ^ 2 ) e. ZZ )
21 18 19 20 sylancl
 |-  ( a e. NN0 -> ( a ^ 2 ) e. ZZ )
22 2mulprm
 |-  ( ( a ^ 2 ) e. ZZ -> ( ( 2 x. ( a ^ 2 ) ) e. Prime <-> ( a ^ 2 ) = 1 ) )
23 21 22 syl
 |-  ( a e. NN0 -> ( ( 2 x. ( a ^ 2 ) ) e. Prime <-> ( a ^ 2 ) = 1 ) )
24 oveq2
 |-  ( ( a ^ 2 ) = 1 -> ( 2 x. ( a ^ 2 ) ) = ( 2 x. 1 ) )
25 2t1e2
 |-  ( 2 x. 1 ) = 2
26 24 25 eqtrdi
 |-  ( ( a ^ 2 ) = 1 -> ( 2 x. ( a ^ 2 ) ) = 2 )
27 26 oveq1d
 |-  ( ( a ^ 2 ) = 1 -> ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = ( 2 mod 4 ) )
28 2re
 |-  2 e. RR
29 4nn
 |-  4 e. NN
30 nnrp
 |-  ( 4 e. NN -> 4 e. RR+ )
31 29 30 ax-mp
 |-  4 e. RR+
32 0le2
 |-  0 <_ 2
33 2lt4
 |-  2 < 4
34 modid
 |-  ( ( ( 2 e. RR /\ 4 e. RR+ ) /\ ( 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 x. ( a ^ 2 ) ) mod 4 ) = 2 )
37 36 eqeq1d
 |-  ( ( a ^ 2 ) = 1 -> ( ( ( 2 x. ( 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 x. ( a ^ 2 ) ) mod 4 ) = 1 -> ( a <_ b -> b =/= a ) ) )
45 23 44 syl6bi
 |-  ( a e. NN0 -> ( ( 2 x. ( a ^ 2 ) ) e. Prime -> ( ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = 1 -> ( a <_ b -> b =/= a ) ) ) )
46 45 impcomd
 |-  ( a e. NN0 -> ( ( ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = 1 /\ ( 2 x. ( a ^ 2 ) ) e. Prime ) -> ( a <_ b -> b =/= a ) ) )
47 46 com12
 |-  ( ( ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = 1 /\ ( 2 x. ( a ^ 2 ) ) e. Prime ) -> ( a e. NN0 -> ( a <_ b -> b =/= a ) ) )
48 17 47 syl6bi
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( ( ( P mod 4 ) = 1 /\ P e. Prime ) -> ( a e. NN0 -> ( a <_ b -> b =/= a ) ) ) )
49 48 expd
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( ( P mod 4 ) = 1 -> ( P e. Prime -> ( a e. NN0 -> ( a <_ b -> b =/= a ) ) ) ) )
50 49 com34
 |-  ( P = ( 2 x. ( a ^ 2 ) ) -> ( ( P mod 4 ) = 1 -> ( a e. NN0 -> ( P e. Prime -> ( a <_ b -> b =/= a ) ) ) ) )
51 50 eqcoms
 |-  ( ( 2 x. ( a ^ 2 ) ) = P -> ( ( P mod 4 ) = 1 -> ( a e. NN0 -> ( P e. Prime -> ( a <_ b -> b =/= a ) ) ) ) )
52 51 com14
 |-  ( P e. Prime -> ( ( P mod 4 ) = 1 -> ( a e. NN0 -> ( ( 2 x. ( a ^ 2 ) ) = P -> ( a <_ b -> b =/= a ) ) ) ) )
53 52 imp31
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) -> ( ( 2 x. ( a ^ 2 ) ) = P -> ( a <_ b -> b =/= a ) ) )
54 53 ad2antrl
 |-  ( ( b = a /\ ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) ) -> ( ( 2 x. ( a ^ 2 ) ) = P -> ( a <_ b -> b =/= a ) ) )
55 13 54 sylbid
 |-  ( ( b = a /\ ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> ( a <_ b -> b =/= a ) ) )
56 55 expimpd
 |-  ( b = a -> ( ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( a <_ b -> b =/= a ) ) )
57 2a1
 |-  ( b =/= a -> ( ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( a <_ b -> b =/= a ) ) )
58 56 57 pm2.61ine
 |-  ( ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( a <_ b -> b =/= a ) )
59 58 pm4.71d
 |-  ( ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( a <_ b <-> ( a <_ b /\ b =/= a ) ) )
60 nn0re
 |-  ( a e. NN0 -> a e. RR )
61 60 adantl
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) -> a e. RR )
62 nn0re
 |-  ( b e. NN0 -> b e. RR )
63 ltlen
 |-  ( ( a e. RR /\ b e. RR ) -> ( a < b <-> ( a <_ b /\ b =/= a ) ) )
64 61 62 63 syl2an
 |-  ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) -> ( a < b <-> ( a <_ b /\ b =/= a ) ) )
65 64 bibi2d
 |-  ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) -> ( ( a <_ b <-> a < b ) <-> ( a <_ b <-> ( a <_ b /\ b =/= a ) ) ) )
66 65 adantr
 |-  ( ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( ( a <_ b <-> a < b ) <-> ( a <_ b <-> ( a <_ b /\ b =/= a ) ) ) )
67 59 66 mpbird
 |-  ( ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( a <_ b <-> a < b ) )
68 67 ex
 |-  ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> ( a <_ b <-> a < b ) ) )
69 68 pm5.32rd
 |-  ( ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) /\ b e. NN0 ) -> ( ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
70 69 reubidva
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN0 ) -> ( E! b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
71 70 reubidva
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E! a e. NN0 E! b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
72 1 71 mpbid
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )