Metamath Proof Explorer

Theorem 2sq2

Description: 2 is the sum of squares of two nonnegative integers iff the two integers are 1 . (Contributed by AV, 19-Jun-2023)

Ref Expression
Assertion 2sq2 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 <-> ( A = 1 /\ B = 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0sqcl 
 |-  ( A e. NN0 -> ( A ^ 2 ) e. NN0 )
2 nn0sqcl 
 |-  ( B e. NN0 -> ( B ^ 2 ) e. NN0 )
3 2 nn0red 
 |-  ( B e. NN0 -> ( B ^ 2 ) e. RR )
4 1 3 anim12ci 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( B ^ 2 ) e. RR /\ ( A ^ 2 ) e. NN0 ) )
5 4 adantr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) e. RR /\ ( A ^ 2 ) e. NN0 ) )
6 nn0addge2 
 |-  ( ( ( B ^ 2 ) e. RR /\ ( A ^ 2 ) e. NN0 ) -> ( B ^ 2 ) <_ ( ( A ^ 2 ) + ( B ^ 2 ) ) )
7 5 6 syl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( B ^ 2 ) <_ ( ( A ^ 2 ) + ( B ^ 2 ) ) )
8 breq2 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 -> ( ( B ^ 2 ) <_ ( ( A ^ 2 ) + ( B ^ 2 ) ) <-> ( B ^ 2 ) <_ 2 ) )
9 8 adantl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) <_ ( ( A ^ 2 ) + ( B ^ 2 ) ) <-> ( B ^ 2 ) <_ 2 ) )
10 2 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( B ^ 2 ) e. NN0 )
11 nn0le2is012 
 |-  ( ( ( B ^ 2 ) e. NN0 /\ ( B ^ 2 ) <_ 2 ) -> ( ( B ^ 2 ) = 0 \/ ( B ^ 2 ) = 1 \/ ( B ^ 2 ) = 2 ) )
12 11 ex 
 |-  ( ( B ^ 2 ) e. NN0 -> ( ( B ^ 2 ) <_ 2 -> ( ( B ^ 2 ) = 0 \/ ( B ^ 2 ) = 1 \/ ( B ^ 2 ) = 2 ) ) )
13 10 12 syl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) <_ 2 -> ( ( B ^ 2 ) = 0 \/ ( B ^ 2 ) = 1 \/ ( B ^ 2 ) = 2 ) ) )
14 oveq2 
 |-  ( ( B ^ 2 ) = 0 -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + 0 ) )
15 14 eqeq1d 
 |-  ( ( B ^ 2 ) = 0 -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 <-> ( ( A ^ 2 ) + 0 ) = 2 ) )
16 15 adantl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( B ^ 2 ) = 0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 <-> ( ( A ^ 2 ) + 0 ) = 2 ) )
17 1 nn0cnd 
 |-  ( A e. NN0 -> ( A ^ 2 ) e. CC )
18 17 addridd 
 |-  ( A e. NN0 -> ( ( A ^ 2 ) + 0 ) = ( A ^ 2 ) )
19 18 adantr 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A ^ 2 ) + 0 ) = ( A ^ 2 ) )
20 19 eqeq1d 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( ( A ^ 2 ) + 0 ) = 2 <-> ( A ^ 2 ) = 2 ) )
21 1 nn0red 
 |-  ( A e. NN0 -> ( A ^ 2 ) e. RR )
22 nn0re 
 |-  ( A e. NN0 -> A e. RR )
23 22 sqge0d 
 |-  ( A e. NN0 -> 0 <_ ( A ^ 2 ) )
24 2nn0 
 |-  2 e. NN0
25 24 a1i 
 |-  ( A e. NN0 -> 2 e. NN0 )
26 25 nn0red 
 |-  ( A e. NN0 -> 2 e. RR )
27 0le2 
 |-  0 <_ 2
28 27 a1i 
 |-  ( A e. NN0 -> 0 <_ 2 )
29 sqrt11 
 |-  ( ( ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) /\ ( 2 e. RR /\ 0 <_ 2 ) ) -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 2 ) <-> ( A ^ 2 ) = 2 ) )
30 21 23 26 28 29 syl22anc 
 |-  ( A e. NN0 -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 2 ) <-> ( A ^ 2 ) = 2 ) )
31 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
32 22 31 sqrtsqd 
 |-  ( A e. NN0 -> ( sqrt ` ( A ^ 2 ) ) = A )
33 32 eqeq1d 
 |-  ( A e. NN0 -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 2 ) <-> A = ( sqrt ` 2 ) ) )
34 sqrt2irr 
 |-  ( sqrt ` 2 ) e/ QQ
35 df-nel 
 |-  ( ( sqrt ` 2 ) e/ QQ <-> -. ( sqrt ` 2 ) e. QQ )
36 id 
 |-  ( ( sqrt ` 2 ) = A -> ( sqrt ` 2 ) = A )
37 36 eqcoms 
 |-  ( A = ( sqrt ` 2 ) -> ( sqrt ` 2 ) = A )
38 37 eleq1d 
 |-  ( A = ( sqrt ` 2 ) -> ( ( sqrt ` 2 ) e. QQ <-> A e. QQ ) )
39 38 notbid 
 |-  ( A = ( sqrt ` 2 ) -> ( -. ( sqrt ` 2 ) e. QQ <-> -. A e. QQ ) )
40 39 adantl 
 |-  ( ( A e. NN0 /\ A = ( sqrt ` 2 ) ) -> ( -. ( sqrt ` 2 ) e. QQ <-> -. A e. QQ ) )
41 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
42 zq 
 |-  ( A e. ZZ -> A e. QQ )
43 41 42 syl 
 |-  ( A e. NN0 -> A e. QQ )
44 43 pm2.24d 
 |-  ( A e. NN0 -> ( -. A e. QQ -> ( A = 1 /\ B = 1 ) ) )
45 44 adantr 
 |-  ( ( A e. NN0 /\ A = ( sqrt ` 2 ) ) -> ( -. A e. QQ -> ( A = 1 /\ B = 1 ) ) )
46 40 45 sylbid 
 |-  ( ( A e. NN0 /\ A = ( sqrt ` 2 ) ) -> ( -. ( sqrt ` 2 ) e. QQ -> ( A = 1 /\ B = 1 ) ) )
47 46 com12 
 |-  ( -. ( sqrt ` 2 ) e. QQ -> ( ( A e. NN0 /\ A = ( sqrt ` 2 ) ) -> ( A = 1 /\ B = 1 ) ) )
48 47 expd 
 |-  ( -. ( sqrt ` 2 ) e. QQ -> ( A e. NN0 -> ( A = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) ) )
49 35 48 sylbi 
 |-  ( ( sqrt ` 2 ) e/ QQ -> ( A e. NN0 -> ( A = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) ) )
50 34 49 ax-mp 
 |-  ( A e. NN0 -> ( A = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) )
51 33 50 sylbid 
 |-  ( A e. NN0 -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) )
52 30 51 sylbird 
 |-  ( A e. NN0 -> ( ( A ^ 2 ) = 2 -> ( A = 1 /\ B = 1 ) ) )
53 52 adantr 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A ^ 2 ) = 2 -> ( A = 1 /\ B = 1 ) ) )
54 20 53 sylbid 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( ( A ^ 2 ) + 0 ) = 2 -> ( A = 1 /\ B = 1 ) ) )
55 54 adantr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( B ^ 2 ) = 0 ) -> ( ( ( A ^ 2 ) + 0 ) = 2 -> ( A = 1 /\ B = 1 ) ) )
56 16 55 sylbid 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( B ^ 2 ) = 0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 -> ( A = 1 /\ B = 1 ) ) )
57 56 impancom 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) = 0 -> ( A = 1 /\ B = 1 ) ) )
58 oveq2 
 |-  ( ( B ^ 2 ) = 1 -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + 1 ) )
59 58 eqeq1d 
 |-  ( ( B ^ 2 ) = 1 -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 <-> ( ( A ^ 2 ) + 1 ) = 2 ) )
60 2cnd 
 |-  ( A e. NN0 -> 2 e. CC )
61 1cnd 
 |-  ( A e. NN0 -> 1 e. CC )
62 60 61 17 3jca 
 |-  ( A e. NN0 -> ( 2 e. CC /\ 1 e. CC /\ ( A ^ 2 ) e. CC ) )
63 62 adantr 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( 2 e. CC /\ 1 e. CC /\ ( A ^ 2 ) e. CC ) )
64 subadd2 
 |-  ( ( 2 e. CC /\ 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( ( 2 - 1 ) = ( A ^ 2 ) <-> ( ( A ^ 2 ) + 1 ) = 2 ) )
65 63 64 syl 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( 2 - 1 ) = ( A ^ 2 ) <-> ( ( A ^ 2 ) + 1 ) = 2 ) )
66 65 bicomd 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( ( A ^ 2 ) + 1 ) = 2 <-> ( 2 - 1 ) = ( A ^ 2 ) ) )
67 59 66 sylan9bbr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( B ^ 2 ) = 1 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 <-> ( 2 - 1 ) = ( A ^ 2 ) ) )
68 nn0sqeq1 
 |-  ( ( B e. NN0 /\ ( B ^ 2 ) = 1 ) -> B = 1 )
69 68 ex 
 |-  ( B e. NN0 -> ( ( B ^ 2 ) = 1 -> B = 1 ) )
70 69 adantl 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( B ^ 2 ) = 1 -> B = 1 ) )
71 2m1e1 
 |-  ( 2 - 1 ) = 1
72 71 a1i 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( 2 - 1 ) = 1 )
73 72 eqeq1d 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( 2 - 1 ) = ( A ^ 2 ) <-> 1 = ( A ^ 2 ) ) )
74 eqcom 
 |-  ( 1 = ( A ^ 2 ) <-> ( A ^ 2 ) = 1 )
75 73 74 bitrdi 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( 2 - 1 ) = ( A ^ 2 ) <-> ( A ^ 2 ) = 1 ) )
76 nn0sqeq1 
 |-  ( ( A e. NN0 /\ ( A ^ 2 ) = 1 ) -> A = 1 )
77 76 ex 
 |-  ( A e. NN0 -> ( ( A ^ 2 ) = 1 -> A = 1 ) )
78 77 adantr 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A ^ 2 ) = 1 -> A = 1 ) )
79 id 
 |-  ( ( A = 1 /\ B = 1 ) -> ( A = 1 /\ B = 1 ) )
80 79 ex 
 |-  ( A = 1 -> ( B = 1 -> ( A = 1 /\ B = 1 ) ) )
81 78 80 syl6 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A ^ 2 ) = 1 -> ( B = 1 -> ( A = 1 /\ B = 1 ) ) ) )
82 75 81 sylbid 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( 2 - 1 ) = ( A ^ 2 ) -> ( B = 1 -> ( A = 1 /\ B = 1 ) ) ) )
83 82 com23 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( B = 1 -> ( ( 2 - 1 ) = ( A ^ 2 ) -> ( A = 1 /\ B = 1 ) ) ) )
84 70 83 syld 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( B ^ 2 ) = 1 -> ( ( 2 - 1 ) = ( A ^ 2 ) -> ( A = 1 /\ B = 1 ) ) ) )
85 84 imp 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( B ^ 2 ) = 1 ) -> ( ( 2 - 1 ) = ( A ^ 2 ) -> ( A = 1 /\ B = 1 ) ) )
86 67 85 sylbid 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( B ^ 2 ) = 1 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 -> ( A = 1 /\ B = 1 ) ) )
87 86 impancom 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) = 1 -> ( A = 1 /\ B = 1 ) ) )
88 nn0re 
 |-  ( B e. NN0 -> B e. RR )
89 nn0ge0 
 |-  ( B e. NN0 -> 0 <_ B )
90 88 89 sqrtsqd 
 |-  ( B e. NN0 -> ( sqrt ` ( B ^ 2 ) ) = B )
91 90 eqcomd 
 |-  ( B e. NN0 -> B = ( sqrt ` ( B ^ 2 ) ) )
92 91 eqeq1d 
 |-  ( B e. NN0 -> ( B = ( sqrt ` 2 ) <-> ( sqrt ` ( B ^ 2 ) ) = ( sqrt ` 2 ) ) )
93 88 sqge0d 
 |-  ( B e. NN0 -> 0 <_ ( B ^ 2 ) )
94 2re 
 |-  2 e. RR
95 94 a1i 
 |-  ( B e. NN0 -> 2 e. RR )
96 27 a1i 
 |-  ( B e. NN0 -> 0 <_ 2 )
97 sqrt11 
 |-  ( ( ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) /\ ( 2 e. RR /\ 0 <_ 2 ) ) -> ( ( sqrt ` ( B ^ 2 ) ) = ( sqrt ` 2 ) <-> ( B ^ 2 ) = 2 ) )
98 3 93 95 96 97 syl22anc 
 |-  ( B e. NN0 -> ( ( sqrt ` ( B ^ 2 ) ) = ( sqrt ` 2 ) <-> ( B ^ 2 ) = 2 ) )
99 92 98 bitrd 
 |-  ( B e. NN0 -> ( B = ( sqrt ` 2 ) <-> ( B ^ 2 ) = 2 ) )
100 id 
 |-  ( ( sqrt ` 2 ) = B -> ( sqrt ` 2 ) = B )
101 100 eqcoms 
 |-  ( B = ( sqrt ` 2 ) -> ( sqrt ` 2 ) = B )
102 101 eleq1d 
 |-  ( B = ( sqrt ` 2 ) -> ( ( sqrt ` 2 ) e. QQ <-> B e. QQ ) )
103 102 adantl 
 |-  ( ( B e. NN0 /\ B = ( sqrt ` 2 ) ) -> ( ( sqrt ` 2 ) e. QQ <-> B e. QQ ) )
104 103 notbid 
 |-  ( ( B e. NN0 /\ B = ( sqrt ` 2 ) ) -> ( -. ( sqrt ` 2 ) e. QQ <-> -. B e. QQ ) )
105 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
106 zq 
 |-  ( B e. ZZ -> B e. QQ )
107 105 106 syl 
 |-  ( B e. NN0 -> B e. QQ )
108 107 pm2.24d 
 |-  ( B e. NN0 -> ( -. B e. QQ -> ( A = 1 /\ B = 1 ) ) )
109 108 adantr 
 |-  ( ( B e. NN0 /\ B = ( sqrt ` 2 ) ) -> ( -. B e. QQ -> ( A = 1 /\ B = 1 ) ) )
110 104 109 sylbid 
 |-  ( ( B e. NN0 /\ B = ( sqrt ` 2 ) ) -> ( -. ( sqrt ` 2 ) e. QQ -> ( A = 1 /\ B = 1 ) ) )
111 110 com12 
 |-  ( -. ( sqrt ` 2 ) e. QQ -> ( ( B e. NN0 /\ B = ( sqrt ` 2 ) ) -> ( A = 1 /\ B = 1 ) ) )
112 111 expd 
 |-  ( -. ( sqrt ` 2 ) e. QQ -> ( B e. NN0 -> ( B = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) ) )
113 35 112 sylbi 
 |-  ( ( sqrt ` 2 ) e/ QQ -> ( B e. NN0 -> ( B = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) ) )
114 34 113 ax-mp 
 |-  ( B e. NN0 -> ( B = ( sqrt ` 2 ) -> ( A = 1 /\ B = 1 ) ) )
115 99 114 sylbird 
 |-  ( B e. NN0 -> ( ( B ^ 2 ) = 2 -> ( A = 1 /\ B = 1 ) ) )
116 115 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) = 2 -> ( A = 1 /\ B = 1 ) ) )
117 57 87 116 3jaod 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( ( B ^ 2 ) = 0 \/ ( B ^ 2 ) = 1 \/ ( B ^ 2 ) = 2 ) -> ( A = 1 /\ B = 1 ) ) )
118 13 117 syld 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) <_ 2 -> ( A = 1 /\ B = 1 ) ) )
119 9 118 sylbid 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( ( B ^ 2 ) <_ ( ( A ^ 2 ) + ( B ^ 2 ) ) -> ( A = 1 /\ B = 1 ) ) )
120 7 119 mpd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) -> ( A = 1 /\ B = 1 ) )
121 120 ex 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 -> ( A = 1 /\ B = 1 ) ) )
122 oveq1 
 |-  ( A = 1 -> ( A ^ 2 ) = ( 1 ^ 2 ) )
123 sq1 
 |-  ( 1 ^ 2 ) = 1
124 122 123 eqtrdi 
 |-  ( A = 1 -> ( A ^ 2 ) = 1 )
125 oveq1 
 |-  ( B = 1 -> ( B ^ 2 ) = ( 1 ^ 2 ) )
126 125 123 eqtrdi 
 |-  ( B = 1 -> ( B ^ 2 ) = 1 )
127 124 126 oveqan12d 
 |-  ( ( A = 1 /\ B = 1 ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( 1 + 1 ) )
128 1p1e2 
 |-  ( 1 + 1 ) = 2
129 127 128 eqtrdi 
 |-  ( ( A = 1 /\ B = 1 ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 )
130 121 129 impbid1 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 <-> ( A = 1 /\ B = 1 ) ) )