Metamath Proof Explorer

Theorem 2sqreulem1

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

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