Metamath Proof Explorer


Theorem 2sqreunnlem1

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

Ref Expression
Assertion 2sqreunnlem1 PPmod4=1∃!a∃!baba2+b2=P

Proof

Step Hyp Ref Expression
1 2sqnn PPmod4=1xyP=x2+y2
2 simpll xyP=x2+y2x
3 2 adantl xyxyP=x2+y2x
4 breq1 a=xabxb
5 oveq1 a=xa2=x2
6 5 oveq1d a=xa2+b2=x2+b2
7 6 eqeq1d a=xa2+b2=Px2+b2=P
8 4 7 anbi12d a=xaba2+b2=Pxbx2+b2=P
9 8 reubidv a=x∃!baba2+b2=P∃!bxbx2+b2=P
10 9 adantl xyxyP=x2+y2a=x∃!baba2+b2=P∃!bxbx2+b2=P
11 simpr xyy
12 11 adantr xyxyy
13 breq2 b=yxbxy
14 oveq1 b=yb2=y2
15 14 oveq2d b=yx2+b2=x2+y2
16 15 eqeq1d b=yx2+b2=x2+y2x2+y2=x2+y2
17 13 16 anbi12d b=yxbx2+b2=x2+y2xyx2+y2=x2+y2
18 equequ1 b=yb=cy=c
19 18 imbi2d b=yxcx2+c2=x2+y2b=cxcx2+c2=x2+y2y=c
20 19 ralbidv b=ycxcx2+c2=x2+y2b=ccxcx2+c2=x2+y2y=c
21 17 20 anbi12d b=yxbx2+b2=x2+y2cxcx2+c2=x2+y2b=cxyx2+y2=x2+y2cxcx2+c2=x2+y2y=c
22 21 adantl xyxyb=yxbx2+b2=x2+y2cxcx2+c2=x2+y2b=cxyx2+y2=x2+y2cxcx2+c2=x2+y2y=c
23 simpr xyxyxy
24 eqidd xyxyx2+y2=x2+y2
25 nnre cc
26 25 resqcld cc2
27 26 adantl xyxycc2
28 nnre yy
29 28 resqcld yy2
30 29 adantl xyy2
31 30 ad2antrr xyxycy2
32 nnre xx
33 32 resqcld xx2
34 33 adantr xyx2
35 34 ad2antrr xyxycx2
36 readdcan c2y2x2x2+c2=x2+y2c2=y2
37 27 31 35 36 syl3anc xyxycx2+c2=x2+y2c2=y2
38 28 ad4antlr xyxycc2=y2y
39 25 ad2antlr xyxycc2=y2c
40 nnnn0 yy0
41 40 nn0ge0d y0y
42 41 ad4antlr xyxycc2=y20y
43 nnnn0 cc0
44 43 nn0ge0d c0c
45 44 ad2antlr xyxycc2=y20c
46 simpr xyxycc2=y2c2=y2
47 46 eqcomd xyxycc2=y2y2=c2
48 38 39 42 45 47 sq11d xyxycc2=y2y=c
49 48 ex xyxycc2=y2y=c
50 37 49 sylbid xyxycx2+c2=x2+y2y=c
51 50 adantld xyxycxcx2+c2=x2+y2y=c
52 51 ralrimiva xyxycxcx2+c2=x2+y2y=c
53 23 24 52 jca31 xyxyxyx2+y2=x2+y2cxcx2+c2=x2+y2y=c
54 12 22 53 rspcedvd xyxybxbx2+b2=x2+y2cxcx2+c2=x2+y2b=c
55 breq2 b=cxbxc
56 oveq1 b=cb2=c2
57 56 oveq2d b=cx2+b2=x2+c2
58 57 eqeq1d b=cx2+b2=x2+y2x2+c2=x2+y2
59 55 58 anbi12d b=cxbx2+b2=x2+y2xcx2+c2=x2+y2
60 59 reu8 ∃!bxbx2+b2=x2+y2bxbx2+b2=x2+y2cxcx2+c2=x2+y2b=c
61 54 60 sylibr xyxy∃!bxbx2+b2=x2+y2
62 61 ex xyxy∃!bxbx2+b2=x2+y2
63 62 adantr xyP=x2+y2xy∃!bxbx2+b2=x2+y2
64 63 impcom xyxyP=x2+y2∃!bxbx2+b2=x2+y2
65 eqeq2 P=x2+y2x2+b2=Px2+b2=x2+y2
66 65 anbi2d P=x2+y2xbx2+b2=Pxbx2+b2=x2+y2
67 66 reubidv P=x2+y2∃!bxbx2+b2=P∃!bxbx2+b2=x2+y2
68 67 adantl xyP=x2+y2∃!bxbx2+b2=P∃!bxbx2+b2=x2+y2
69 68 adantl xyxyP=x2+y2∃!bxbx2+b2=P∃!bxbx2+b2=x2+y2
70 64 69 mpbird xyxyP=x2+y2∃!bxbx2+b2=P
71 3 10 70 rspcedvd xyxyP=x2+y2a∃!baba2+b2=P
72 11 adantr xyP=x2+y2y
73 72 adantl ¬xyxyP=x2+y2y
74 breq1 a=yabyb
75 oveq1 a=ya2=y2
76 75 oveq1d a=ya2+b2=y2+b2
77 76 eqeq1d a=ya2+b2=Py2+b2=P
78 74 77 anbi12d a=yaba2+b2=Pyby2+b2=P
79 78 reubidv a=y∃!baba2+b2=P∃!byby2+b2=P
80 79 adantl ¬xyxyP=x2+y2a=y∃!baba2+b2=P∃!byby2+b2=P
81 simpll xy¬xyx
82 breq2 b=xybyx
83 oveq1 b=xb2=x2
84 83 oveq2d b=xy2+b2=y2+x2
85 84 eqeq1d b=xy2+b2=x2+y2y2+x2=x2+y2
86 82 85 anbi12d b=xyby2+b2=x2+y2yxy2+x2=x2+y2
87 equequ1 b=xb=cx=c
88 87 imbi2d b=xycy2+c2=x2+y2b=cycy2+c2=x2+y2x=c
89 88 ralbidv b=xcycy2+c2=x2+y2b=ccycy2+c2=x2+y2x=c
90 86 89 anbi12d b=xyby2+b2=x2+y2cycy2+c2=x2+y2b=cyxy2+x2=x2+y2cycy2+c2=x2+y2x=c
91 90 adantl xy¬xyb=xyby2+b2=x2+y2cycy2+c2=x2+y2b=cyxy2+x2=x2+y2cycy2+c2=x2+y2x=c
92 ltnle yxy<x¬xy
93 28 32 92 syl2anr xyy<x¬xy
94 28 ad2antlr xyy<xy
95 32 ad2antrr xyy<xx
96 simpr xyy<xy<x
97 94 95 96 ltled xyy<xyx
98 97 ex xyy<xyx
99 93 98 sylbird xy¬xyyx
100 99 imp xy¬xyyx
101 29 recnd yy2
102 101 adantl xyy2
103 33 recnd xx2
104 103 adantr xyx2
105 102 104 addcomd xyy2+x2=x2+y2
106 105 adantr xy¬xyy2+x2=x2+y2
107 34 recnd xyx2
108 107 adantr xycx2
109 30 recnd xyy2
110 109 adantr xycy2
111 108 110 addcomd xycx2+y2=y2+x2
112 111 eqeq2d xycy2+c2=x2+y2y2+c2=y2+x2
113 26 adantl xycc2
114 33 ad2antrr xycx2
115 29 ad2antlr xycy2
116 readdcan c2x2y2y2+c2=y2+x2c2=x2
117 113 114 115 116 syl3anc xycy2+c2=y2+x2c2=x2
118 112 117 bitrd xycy2+c2=x2+y2c2=x2
119 25 ad2antlr xycc2=x2c
120 32 adantr xyx
121 120 ad2antrr xycc2=x2x
122 44 ad2antlr xycc2=x20c
123 nnnn0 xx0
124 123 nn0ge0d x0x
125 124 adantr xy0x
126 125 ad2antrr xycc2=x20x
127 simpr xycc2=x2c2=x2
128 119 121 122 126 127 sq11d xycc2=x2c=x
129 128 eqcomd xycc2=x2x=c
130 129 ex xycc2=x2x=c
131 118 130 sylbid xycy2+c2=x2+y2x=c
132 131 adantld xycycy2+c2=x2+y2x=c
133 132 ralrimiva xycycy2+c2=x2+y2x=c
134 133 adantr xy¬xycycy2+c2=x2+y2x=c
135 100 106 134 jca31 xy¬xyyxy2+x2=x2+y2cycy2+c2=x2+y2x=c
136 81 91 135 rspcedvd xy¬xybyby2+b2=x2+y2cycy2+c2=x2+y2b=c
137 breq2 b=cybyc
138 56 oveq2d b=cy2+b2=y2+c2
139 138 eqeq1d b=cy2+b2=x2+y2y2+c2=x2+y2
140 137 139 anbi12d b=cyby2+b2=x2+y2ycy2+c2=x2+y2
141 140 reu8 ∃!byby2+b2=x2+y2byby2+b2=x2+y2cycy2+c2=x2+y2b=c
142 136 141 sylibr xy¬xy∃!byby2+b2=x2+y2
143 142 ex xy¬xy∃!byby2+b2=x2+y2
144 143 adantr xyP=x2+y2¬xy∃!byby2+b2=x2+y2
145 144 impcom ¬xyxyP=x2+y2∃!byby2+b2=x2+y2
146 eqeq2 P=x2+y2y2+b2=Py2+b2=x2+y2
147 146 anbi2d P=x2+y2yby2+b2=Pyby2+b2=x2+y2
148 147 reubidv P=x2+y2∃!byby2+b2=P∃!byby2+b2=x2+y2
149 148 adantl xyP=x2+y2∃!byby2+b2=P∃!byby2+b2=x2+y2
150 149 adantl ¬xyxyP=x2+y2∃!byby2+b2=P∃!byby2+b2=x2+y2
151 145 150 mpbird ¬xyxyP=x2+y2∃!byby2+b2=P
152 73 80 151 rspcedvd ¬xyxyP=x2+y2a∃!baba2+b2=P
153 71 152 pm2.61ian xyP=x2+y2a∃!baba2+b2=P
154 153 ex xyP=x2+y2a∃!baba2+b2=P
155 154 adantl PPmod4=1xyP=x2+y2a∃!baba2+b2=P
156 155 rexlimdvva PPmod4=1xyP=x2+y2a∃!baba2+b2=P
157 1 156 mpd PPmod4=1a∃!baba2+b2=P
158 reurex ∃!baba2+b2=Pbaba2+b2=P
159 158 a1i PPmod4=1a∃!baba2+b2=Pbaba2+b2=P
160 159 ralrimiva PPmod4=1a∃!baba2+b2=Pbaba2+b2=P
161 2sqmo P*a0b0aba2+b2=P
162 nnssnn0 0
163 nfcv _a
164 nfcv _a0
165 163 164 ssrmof 0*a0b0aba2+b2=P*ab0aba2+b2=P
166 162 165 ax-mp *a0b0aba2+b2=P*ab0aba2+b2=P
167 ssrexv 0baba2+b2=Pb0aba2+b2=P
168 162 167 ax-mp baba2+b2=Pb0aba2+b2=P
169 168 rmoimi *ab0aba2+b2=P*ababa2+b2=P
170 161 166 169 3syl P*ababa2+b2=P
171 170 adantr PPmod4=1*ababa2+b2=P
172 rmoim a∃!baba2+b2=Pbaba2+b2=P*ababa2+b2=P*a∃!baba2+b2=P
173 160 171 172 sylc PPmod4=1*a∃!baba2+b2=P
174 reu5 ∃!a∃!baba2+b2=Pa∃!baba2+b2=P*a∃!baba2+b2=P
175 157 173 174 sylanbrc PPmod4=1∃!a∃!baba2+b2=P