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 0 B 0 A 2 + B 2 = 2 A = 1 B = 1

Proof

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