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 ) ) |