On Sun, 5 Jan 2020 16:52:07 -0800 (PST), Norman Megill <[email protected]> wrote: > OK. you (or David or whoever wants) can add the "t".
Okay. I did a quick look to see how many labels would probably change, by running this: metamath 'read set.mm' 'set scroll continuous' 'set width 9999' 'show statement *sqr*' quit | grep ' sqr ' > ,sqr It looks like it's less than 100. I think we can first change all the labels (e.g., "df-sqr" becomes "df-sqrt"), as listed below. We can then separately change the actual expressions so "sqr" becomes "sqrt". Doing this in separate steps should reduce the risk of errors in it. --- David A. Wheeler ========================================= 40921 csqr $a class sqr $. 40925 df-sqr $a |- sqr = ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) $. 40927 sqrval $p |- ( A e. CC -> ( sqr ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) ) $= ... $. 40933 sqr0 $p |- ( sqr ` 0 ) = 0 $= ... $. 40967 resqrcl $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR ) $= ... $. 40968 resqrthlem $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqr ` A ) ) /\ ( _i x. ( sqr ` A ) ) e/ RR+ ) ) $= ... $. 40970 resqrth $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $. 40971 remsqsqr $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A ) $= ... $. 40972 sqrge0 $p |- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqr ` A ) ) $= ... $. 40973 sqrgt0 $p |- ( ( A e. RR /\ 0 < A ) -> 0 < ( sqr ` A ) ) $= ... $. 40974 sqrmul $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ) $= ... $. 40975 sqrle $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) ) $= ... $. 40976 sqrlt $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) ) $= ... $. 40977 sqr11 $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) ) $= ... $. 40978 sqr00 $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) = 0 <-> A = 0 ) ) $= ... $. 40979 rpsqrcl $p |- ( A e. RR+ -> ( sqr ` A ) e. RR+ ) $= ... $. 40980 sqrdiv $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) ) $= ... $. 40981 sqrneglem $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( _i x. ( sqr ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqr ` A ) ) ) /\ ( _i x. ( _i x. ( sqr ` A ) ) ) e/ RR+ ) ) $= ... $. 40984 sqrneg $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) ) $= ... $. 40986 sqrsq2 $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) ) $= ... $. 40987 sqrsq $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A ^ 2 ) ) = A ) $= ... $. 40988 sqrmsq $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A x. A ) ) = A ) $= ... $. 40989 sqr1 $p |- ( sqr ` 1 ) = 1 $= ... $. 40990 sqr4 $p |- ( sqr ` 4 ) = 2 $= ... $. 40991 sqr9 $p |- ( sqr ` 9 ) = 3 $= ... $. 40992 sqr2gt1lt2 $p |- ( 1 < ( sqr ` 2 ) /\ ( sqr ` 2 ) < 2 ) $= ... $. 40993 sqrm1 $p |- _i = ( sqr ` -u 1 ) $= ... $. 41151 sqreulem.1 $e |- B = ( ( sqr ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) $. 41160 sqrcl $p |- ( A e. CC -> ( sqr ` A ) e. CC ) $= ... $. 41161 sqrthlem $p |- ( A e. CC -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqr ` A ) ) /\ ( _i x. ( sqr ` A ) ) e/ RR+ ) ) $= ... $. 41162 sqrf $p |- sqr : CC --> CC $= ... $. 41164 sqrth $p |- ( A e. CC -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $. 41165 sqrrege0 $p |- ( A e. CC -> 0 <_ ( Re ` ( sqr ` A ) ) ) $= ... $. 41166 eqsqror $p |- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = B <-> ( A = ( sqr ` B ) \/ A = -u ( sqr ` B ) ) ) ) $= ... $. 41176 eqsqrd $p |- ( ph -> A = ( sqr ` B ) ) $= ... $. 41179 eqsqr2d $p |- ( ph -> A = ( sqr ` B ) ) $= ... $. 41184 sqrthi $p |- ( 0 <_ A -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A ) $= ... $. 41185 sqrcli $p |- ( 0 <_ A -> ( sqr ` A ) e. RR ) $= ... $. 41186 sqrgt0i $p |- ( 0 < A -> 0 < ( sqr ` A ) ) $= ... $. 41187 sqrmsqi $p |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A ) $= ... $. 41188 sqrsqi $p |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A ) $= ... $. 41189 sqsqri $p |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $. 41190 sqrge0i $p |- ( 0 <_ A -> 0 <_ ( sqr ` A ) ) $= ... $. 41198 sqrpclii $p |- ( sqr ` A ) e. RR $= ... $. 41199 sqrgt0ii $p |- 0 < ( sqr ` A ) $= ... $. 41202 sqr11i $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) ) $= ... $. 41203 sqrmuli $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ) $= ... $. 41207 sqrmulii $p |- ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) $= ... $. 41209 sqrmsq2i $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = B <-> A = ( B x. B ) ) ) $= ... $. 41210 sqrlei $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) ) $= ... $. 41211 sqrlti $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) ) $= ... $. 41241 rpsqrcld $p |- ( ph -> ( sqr ` A ) e. RR+ ) $= ... $. 41242 sqrgt0d $p |- ( ph -> 0 < ( sqr ` A ) ) $= ... $. 41254 resqrcld $p |- ( ph -> ( sqr ` A ) e. RR ) $= ... $. 41255 sqrmsqd $p |- ( ph -> ( sqr ` ( A x. A ) ) = A ) $= ... $. 41256 sqrsqd $p |- ( ph -> ( sqr ` ( A ^ 2 ) ) = A ) $= ... $. 41257 sqrge0d $p |- ( ph -> 0 <_ ( sqr ` A ) ) $= ... $. 41258 sqrnegd $p |- ( ph -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) ) $= ... $. 41262 sqrdivd $p |- ( ph -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) ) $= ... $. 41266 sqrmuld $p |- ( ph -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ) $= ... $. 41267 sqrsq2d $p |- ( ph -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) ) $= ... $. 41268 sqrled $p |- ( ph -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) ) $= ... $. 41269 sqrltd $p |- ( ph -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) ) $= ... $. 41270 sqr11d.5 $e |- ( ph -> ( sqr ` A ) = ( sqr ` B ) ) $. 41290 sqrcld $p |- ( ph -> ( sqr ` A ) e. CC ) $= ... $. 41291 sqrrege0d $p |- ( ph -> 0 <_ ( Re ` ( sqr ` A ) ) ) $= ... $. 41292 sqsqrd $p |- ( ph -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $. 41293 msqsqrd $p |- ( ph -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A ) $= ... $. 41295 sqr00d.2 $e |- ( ph -> ( sqr ` A ) = 0 ) $. 44497 sqr2irrlem.3 $e |- ( ph -> ( sqr ` 2 ) = ( A / B ) ) $. 44502 sqr2irr $p |- ( sqr ` 2 ) e/ QQ $= ... $. 44504 sqr2re $p |- ( sqr ` 2 ) e. RR $= ... $. 45491 zsqrelqelz $p |- ( ( A e. ZZ /\ ( sqr ` A ) e. QQ ) -> ( sqr ` A ) e. ZZ ) $= ... $. 84684 cphsqrcl $p |- ( ( W e. CPreHil /\ ( A e. K /\ A e. RR /\ 0 <_ A ) ) -> ( sqr ` A ) e. K ) $= ... $. 84686 cphsqrcl2 $p |- ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) -> ( sqr ` A ) e. K ) $= ... $. 84687 cphsqrcl3 $p |- ( ( W e. CPreHil /\ _i e. K /\ A e. K ) -> ( sqr ` A ) e. K ) $= ... $. 91919 cxpsqrlem $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqr ` A ) ) -> ( _i x. ( sqr ` A ) ) e. RR ) $= ... $. 91920 cxpsqr $p |- ( A e. CC -> ( A ^c ( 1 / 2 ) ) = ( sqr ` A ) ) $= ... $. 91921 logsqr $p |- ( A e. RR+ -> ( log ` ( sqr ` A ) ) = ( ( log ` A ) / 2 ) ) $= ... $. 92016 dvsqr $p |- ( RR _D ( x e. RR+ |-> ( sqr ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqr ` x ) ) ) ) $= ... $. 92054 resqrcn $p |- ( sqr |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR ) $= ... $. 92056 sqrcn $p |- ( sqr |` D ) e. ( D -cn-> CC ) $= ... $. 92100 loglesqr $p |- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( A + 1 ) ) <_ ( sqr ` A ) ) $= ... $. 92831 sqrlim $p |- ( n e. RR+ |-> ( 1 / ( sqr ` n ) ) ) ~~>r 0 $= ... $. 92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $. 92870 divsqrsumlem $p |- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqr ` A ) ) ) ) $= ... $. 92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $. 92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $. 92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $. 92874 divsqrsum2 $p |- ( ( ph /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqr ` A ) ) ) $= ... $. 92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $. 92875 divsqrsumo1 $p |- ( ph -> ( y e. RR+ |-> ( ( ( F ` y ) - L ) x. ( sqr ` y ) ) ) e. O(1) ) $= ... $. 120881 dvcnsqr $p |- ( CC _D ( x e. D |-> ( sqr ` x ) ) ) = ( x e. D |-> ( 1 / ( 2 x. ( sqr ` x ) ) ) ) $= ... $. 124714 rmspecsqrnq $p |- ( A e. ( ZZ>= ` 2 ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) ) $= ... $. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1iofYF-0006Co-3i%40rmmprod07.runbox.
