Metamath Proof Explorer

Theorem 2sqreunnlem1

Description: Lemma 1 for 2sqreunn . (Contributed by AV, 11-Jun-2023)

Ref Expression
Assertion 2sqreunnlem1 
|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )

Proof

Step Hyp Ref Expression
1 2sqnn 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
2 simpll 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x e. NN )
3 2 adantl 
 |-  ( ( x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> x e. NN )
4 breq1 
 |-  ( a = x -> ( a <_ b <-> x <_ b ) )
5 oveq1 
 |-  ( a = x -> ( a ^ 2 ) = ( x ^ 2 ) )
6 5 oveq1d 
 |-  ( a = x -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( b ^ 2 ) ) )
7 6 eqeq1d 
 |-  ( a = x -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) )
8 4 7 anbi12d 
 |-  ( a = x -> ( ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
9 8 reubidv 
 |-  ( a = x -> ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
10 9 adantl 
 |-  ( ( ( x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) /\ a = x ) -> ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
11 simpr 
 |-  ( ( x e. NN /\ y e. NN ) -> y e. NN )
12 11 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> y e. NN )
13 breq2 
 |-  ( b = y -> ( x <_ b <-> x <_ y ) )
14 oveq1 
 |-  ( b = y -> ( b ^ 2 ) = ( y ^ 2 ) )
15 14 oveq2d 
 |-  ( b = y -> ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
16 15 eqeq1d 
 |-  ( b = y -> ( ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
17 13 16 anbi12d 
 |-  ( b = y -> ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( x <_ y /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
18 equequ1 
 |-  ( b = y -> ( b = c <-> y = c ) )
19 18 imbi2d 
 |-  ( b = y -> ( ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) <-> ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) ) )
20 19 ralbidv 
 |-  ( b = y -> ( A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) <-> A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) ) )
21 17 20 anbi12d 
 |-  ( b = y -> ( ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) <-> ( ( x <_ y /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) ) ) )
22 21 adantl 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ b = y ) -> ( ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) <-> ( ( x <_ y /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) ) ) )
23 simpr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> x <_ y )
24 eqidd 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
25 nnre 
 |-  ( c e. NN -> c e. RR )
26 25 resqcld 
 |-  ( c e. NN -> ( c ^ 2 ) e. RR )
27 26 adantl 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( c ^ 2 ) e. RR )
28 nnre 
 |-  ( y e. NN -> y e. RR )
29 28 resqcld 
 |-  ( y e. NN -> ( y ^ 2 ) e. RR )
30 29 adantl 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y ^ 2 ) e. RR )
31 30 ad2antrr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( y ^ 2 ) e. RR )
32 nnre 
 |-  ( x e. NN -> x e. RR )
33 32 resqcld 
 |-  ( x e. NN -> ( x ^ 2 ) e. RR )
34 33 adantr 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x ^ 2 ) e. RR )
35 34 ad2antrr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( x ^ 2 ) e. RR )
36 readdcan 
 |-  ( ( ( c ^ 2 ) e. RR /\ ( y ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( c ^ 2 ) = ( y ^ 2 ) ) )
37 27 31 35 36 syl3anc 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( c ^ 2 ) = ( y ^ 2 ) ) )
38 28 ad4antlr 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> y e. RR )
39 25 ad2antlr 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> c e. RR )
40 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
41 40 nn0ge0d 
 |-  ( y e. NN -> 0 <_ y )
42 41 ad4antlr 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> 0 <_ y )
43 nnnn0 
 |-  ( c e. NN -> c e. NN0 )
44 43 nn0ge0d 
 |-  ( c e. NN -> 0 <_ c )
45 44 ad2antlr 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> 0 <_ c )
46 simpr 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> ( c ^ 2 ) = ( y ^ 2 ) )
47 46 eqcomd 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> ( y ^ 2 ) = ( c ^ 2 ) )
48 38 39 42 45 47 sq11d 
 |-  ( ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) /\ ( c ^ 2 ) = ( y ^ 2 ) ) -> y = c )
49 48 ex 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( ( c ^ 2 ) = ( y ^ 2 ) -> y = c ) )
50 37 49 sylbid 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> y = c ) )
51 50 adantld 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) /\ c e. NN ) -> ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) )
52 51 ralrimiva 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) )
53 23 24 52 jca31 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> ( ( x <_ y /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y = c ) ) )
54 12 22 53 rspcedvd 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> E. b e. NN ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) )
55 breq2 
 |-  ( b = c -> ( x <_ b <-> x <_ c ) )
56 oveq1 
 |-  ( b = c -> ( b ^ 2 ) = ( c ^ 2 ) )
57 56 oveq2d 
 |-  ( b = c -> ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( c ^ 2 ) ) )
58 57 eqeq1d 
 |-  ( b = c -> ( ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
59 55 58 anbi12d 
 |-  ( b = c -> ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
60 59 reu8 
 |-  ( E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. b e. NN ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( x <_ c /\ ( ( x ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) )
61 54 60 sylibr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ x <_ y ) -> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
62 61 ex 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x <_ y -> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
63 62 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( x <_ y -> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
64 63 impcom 
 |-  ( ( x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
65 eqeq2 
 |-  ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( ( ( x ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
66 65 anbi2d 
 |-  ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
67 66 reubidv 
 |-  ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
68 67 adantl 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
69 68 adantl 
 |-  ( ( x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> ( E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
70 64 69 mpbird 
 |-  ( ( x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> E! b e. NN ( x <_ b /\ ( ( x ^ 2 ) + ( b ^ 2 ) ) = P ) )
71 3 10 70 rspcedvd 
 |-  ( ( x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
72 11 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y e. NN )
73 72 adantl 
 |-  ( ( -. x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> y e. NN )
74 breq1 
 |-  ( a = y -> ( a <_ b <-> y <_ b ) )
75 oveq1 
 |-  ( a = y -> ( a ^ 2 ) = ( y ^ 2 ) )
76 75 oveq1d 
 |-  ( a = y -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( y ^ 2 ) + ( b ^ 2 ) ) )
77 76 eqeq1d 
 |-  ( a = y -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) )
78 74 77 anbi12d 
 |-  ( a = y -> ( ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
79 78 reubidv 
 |-  ( a = y -> ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
80 79 adantl 
 |-  ( ( ( -. x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) /\ a = y ) -> ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
81 simpll 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> x e. NN )
82 breq2 
 |-  ( b = x -> ( y <_ b <-> y <_ x ) )
83 oveq1 
 |-  ( b = x -> ( b ^ 2 ) = ( x ^ 2 ) )
84 83 oveq2d 
 |-  ( b = x -> ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( y ^ 2 ) + ( x ^ 2 ) ) )
85 84 eqeq1d 
 |-  ( b = x -> ( ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
86 82 85 anbi12d 
 |-  ( b = x -> ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( y <_ x /\ ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
87 equequ1 
 |-  ( b = x -> ( b = c <-> x = c ) )
88 87 imbi2d 
 |-  ( b = x -> ( ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) <-> ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) ) )
89 88 ralbidv 
 |-  ( b = x -> ( A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) <-> A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) ) )
90 86 89 anbi12d 
 |-  ( b = x -> ( ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) <-> ( ( y <_ x /\ ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) ) ) )
91 90 adantl 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) /\ b = x ) -> ( ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) <-> ( ( y <_ x /\ ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) ) ) )
92 ltnle 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y < x <-> -. x <_ y ) )
93 28 32 92 syl2anr 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y < x <-> -. x <_ y ) )
94 28 ad2antlr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ y < x ) -> y e. RR )
95 32 ad2antrr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ y < x ) -> x e. RR )
96 simpr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ y < x ) -> y < x )
97 94 95 96 ltled 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ y < x ) -> y <_ x )
98 97 ex 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y < x -> y <_ x ) )
99 93 98 sylbird 
 |-  ( ( x e. NN /\ y e. NN ) -> ( -. x <_ y -> y <_ x ) )
100 99 imp 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> y <_ x )
101 29 recnd 
 |-  ( y e. NN -> ( y ^ 2 ) e. CC )
102 101 adantl 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y ^ 2 ) e. CC )
103 33 recnd 
 |-  ( x e. NN -> ( x ^ 2 ) e. CC )
104 103 adantr 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x ^ 2 ) e. CC )
105 102 104 addcomd 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
106 105 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
107 34 recnd 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x ^ 2 ) e. CC )
108 107 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( x ^ 2 ) e. CC )
109 30 recnd 
 |-  ( ( x e. NN /\ y e. NN ) -> ( y ^ 2 ) e. CC )
110 109 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( y ^ 2 ) e. CC )
111 108 110 addcomd 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( y ^ 2 ) + ( x ^ 2 ) ) )
112 111 eqeq2d 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( y ^ 2 ) + ( x ^ 2 ) ) ) )
113 26 adantl 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( c ^ 2 ) e. RR )
114 33 ad2antrr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( x ^ 2 ) e. RR )
115 29 ad2antlr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( y ^ 2 ) e. RR )
116 readdcan 
 |-  ( ( ( c ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR /\ ( y ^ 2 ) e. RR ) -> ( ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( y ^ 2 ) + ( x ^ 2 ) ) <-> ( c ^ 2 ) = ( x ^ 2 ) ) )
117 113 114 115 116 syl3anc 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( y ^ 2 ) + ( x ^ 2 ) ) <-> ( c ^ 2 ) = ( x ^ 2 ) ) )
118 112 117 bitrd 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( c ^ 2 ) = ( x ^ 2 ) ) )
119 25 ad2antlr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> c e. RR )
120 32 adantr 
 |-  ( ( x e. NN /\ y e. NN ) -> x e. RR )
121 120 ad2antrr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> x e. RR )
122 44 ad2antlr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> 0 <_ c )
123 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
124 123 nn0ge0d 
 |-  ( x e. NN -> 0 <_ x )
125 124 adantr 
 |-  ( ( x e. NN /\ y e. NN ) -> 0 <_ x )
126 125 ad2antrr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> 0 <_ x )
127 simpr 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> ( c ^ 2 ) = ( x ^ 2 ) )
128 119 121 122 126 127 sq11d 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> c = x )
129 128 eqcomd 
 |-  ( ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) /\ ( c ^ 2 ) = ( x ^ 2 ) ) -> x = c )
130 129 ex 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( c ^ 2 ) = ( x ^ 2 ) -> x = c ) )
131 118 130 sylbid 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> x = c ) )
132 131 adantld 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ c e. NN ) -> ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) )
133 132 ralrimiva 
 |-  ( ( x e. NN /\ y e. NN ) -> A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) )
134 133 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) )
135 100 106 134 jca31 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> ( ( y <_ x /\ ( ( y ^ 2 ) + ( x ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> x = c ) ) )
136 81 91 135 rspcedvd 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> E. b e. NN ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) )
137 breq2 
 |-  ( b = c -> ( y <_ b <-> y <_ c ) )
138 56 oveq2d 
 |-  ( b = c -> ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( y ^ 2 ) + ( c ^ 2 ) ) )
139 138 eqeq1d 
 |-  ( b = c -> ( ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
140 137 139 anbi12d 
 |-  ( b = c -> ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
141 140 reu8 
 |-  ( E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. b e. NN ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ A. c e. NN ( ( y <_ c /\ ( ( y ^ 2 ) + ( c ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> b = c ) ) )
142 136 141 sylibr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ -. x <_ y ) -> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
143 142 ex 
 |-  ( ( x e. NN /\ y e. NN ) -> ( -. x <_ y -> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
144 143 adantr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( -. x <_ y -> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
145 144 impcom 
 |-  ( ( -. x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
146 eqeq2 
 |-  ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( ( ( y ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
147 146 anbi2d 
 |-  ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
148 147 reubidv 
 |-  ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
149 148 adantl 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
150 149 adantl 
 |-  ( ( -. x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> ( E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
151 145 150 mpbird 
 |-  ( ( -. x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> E! b e. NN ( y <_ b /\ ( ( y ^ 2 ) + ( b ^ 2 ) ) = P ) )
152 73 80 151 rspcedvd 
 |-  ( ( -. x <_ y /\ ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
153 71 152 pm2.61ian 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
154 153 ex 
 |-  ( ( x e. NN /\ y e. NN ) -> ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
155 154 adantl 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( x e. NN /\ y e. NN ) ) -> ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
156 155 rexlimdvva 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
157 1 156 mpd 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
158 reurex 
 |-  ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
159 158 a1i 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ a e. NN ) -> ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
160 159 ralrimiva 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> A. a e. NN ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
161 2sqmo 
 |-  ( P e. Prime -> E* a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
162 nnssnn0 
 |-  NN C_ NN0
163 nfcv 
 |-  F/_ a NN
164 nfcv 
 |-  F/_ a NN0
165 163 164 ssrmof 
 |-  ( NN C_ NN0 -> ( E* a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E* a e. NN E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
166 162 165 ax-mp 
 |-  ( E* a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E* a e. NN E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
167 ssrexv 
 |-  ( NN C_ NN0 -> ( E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
168 162 167 ax-mp 
 |-  ( E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
169 168 rmoimi 
 |-  ( E* a e. NN E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E* a e. NN E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
170 161 166 169 3syl 
 |-  ( P e. Prime -> E* a e. NN E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
171 170 adantr 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E* a e. NN E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
172 rmoim 
 |-  ( A. a e. NN ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> ( E* a e. NN E. b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E* a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
173 160 171 172 sylc 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E* a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
174 reu5 
 |-  ( E! a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( E. a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E* a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
175 157 173 174 sylanbrc 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )