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 biimtrid 
 |-  ( 1 =/= 2 -> ( 2 = 1 -> ( a <_ b -> b =/= a ) ) )
43 38 42 ax-mp 
 |-  ( 2 = 1 -> ( a <_ b -> b =/= a ) )
44 37 43 biimtrdi 
 |-  ( ( a ^ 2 ) = 1 -> ( ( ( 2 x. ( a ^ 2 ) ) mod 4 ) = 1 -> ( a <_ b -> b =/= a ) ) )
45 23 44 biimtrdi 
 |-  ( 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 biimtrdi 
 |-  ( 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 ) )