Skip to content

Commit 9af9a7e

Browse files
jkingdonjkingdon
committed
Remove isummo from iset.mm
No longer used and replaced by summodc .
1 parent 16bc0ae commit 9af9a7e

File tree

2 files changed

+12
-81
lines changed

2 files changed

+12
-81
lines changed

‎iset-discouraged‎

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -176,13 +176,11 @@
176176
"iseqcl" is used by "iseqp1".
177177
"iseqcoll" is used by "isummolem2a".
178178
"iseqeq1" is used by "iseqid".
179-
"iseqeq1" is used by "isummo".
180179
"iseqeq1" is used by "isummolem2".
181180
"iseqeq1" is used by "seqeq1".
182181
"iseqeq1" is used by "zisum".
183182
"iseqeq2" is used by "seqeq2".
184183
"iseqeq3" is used by "cbvsum".
185-
"iseqeq3" is used by "isummo".
186184
"iseqeq3" is used by "seqeq3".
187185
"iseqeq3" is used by "sumeq1".
188186
"iseqeq3" is used by "sumeq2".
@@ -232,12 +230,9 @@
232230
"iseradd" is used by "ser3add".
233231
"iserf" is used by "fisumcvg".
234232
"iserf" is used by "ser0f".
235-
"isummolem2" is used by "isummo".
236233
"isummolem2a" is used by "isummolem2".
237234
"isummolem2a" is used by "zisum".
238-
"isummolem3" is used by "isummo".
239235
"isummolem3" is used by "isummolem2a".
240-
"isumrb" is used by "isummo".
241236
"isumrb" is used by "zisum".
242237
"mo3h" is used by "mo2dc".
243238
"mo3h" is used by "mo3".
@@ -397,9 +392,9 @@ New usage of "iseqcaopr2" is discouraged (1 uses).
397392
New usage of "iseqcaopr3" is discouraged (1 uses).
398393
New usage of "iseqcl" is discouraged (3 uses).
399394
New usage of "iseqcoll" is discouraged (1 uses).
400-
New usage of "iseqeq1" is discouraged (5 uses).
395+
New usage of "iseqeq1" is discouraged (4 uses).
401396
New usage of "iseqeq2" is discouraged (1 uses).
402-
New usage of "iseqeq3" is discouraged (6 uses).
397+
New usage of "iseqeq3" is discouraged (5 uses).
403398
New usage of "iseqex" is discouraged (4 uses).
404399
New usage of "iseqfcl" is discouraged (4 uses).
405400
New usage of "iseqfclt" is discouraged (2 uses).
@@ -418,11 +413,10 @@ New usage of "iseqvalt" is discouraged (3 uses).
418413
New usage of "iser0" is discouraged (1 uses).
419414
New usage of "iseradd" is discouraged (1 uses).
420415
New usage of "iserf" is discouraged (2 uses).
421-
New usage of "isummo" is discouraged (0 uses).
422-
New usage of "isummolem2" is discouraged (1 uses).
416+
New usage of "isummolem2" is discouraged (0 uses).
423417
New usage of "isummolem2a" is discouraged (2 uses).
424-
New usage of "isummolem3" is discouraged (2 uses).
425-
New usage of "isumrb" is discouraged (2 uses).
418+
New usage of "isummolem3" is discouraged (1 uses).
419+
New usage of "isumrb" is discouraged (1 uses).
426420
New usage of "mathbox" is discouraged (0 uses).
427421
New usage of "mo3h" is discouraged (7 uses).
428422
New usage of "nfiseq" is discouraged (3 uses).

‎iset.mm‎

Lines changed: 7 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -115008,7 +115008,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115008115008
isummolem3.5 $e |- ( ph -> ( M e. NN /\ N e. NN ) ) $.
115009115009
isummolem3.6 $e |- ( ph -> f : ( 1 ... M ) -1-1-onto-> A ) $.
115010115010
isummolem3.7 $e |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A ) $.
115011-
$( Lemma for ~ isummo . (Contributed by Jim Kingdon, 15-Aug-2022.) $)
115011+
$( Lemma for ~ summodc . (Contributed by Jim Kingdon, 15-Aug-2022.) $)
115012115012
isummolemnm $p |- ( ph -> N = M ) $=
115013115013
( c1 cfz co chash wcel wf1o cfv cv ccnv ccom 1zzd cn simprd nnzd fzfigd
115014115014
f1ocnv syl f1oco syl2anc fihasheqf1od wceq nnnn0 hashfz1 simpld 3eqtr3d
@@ -115024,7 +115024,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115024115024
[_ ( f ` n ) / k ]_ B , 0 ) ) $.
115025115025
isummolem3.4 $e |- H = ( n e. NN |-> if ( n <_ N ,
115026115026
[_ ( K ` n ) / k ]_ B , 0 ) ) $.
115027-
$( Lemma for ~ isummo . (Contributed by Mario Carneiro, 29-Mar-2014.)
115027+
$( Lemma for ~ summodc . (Contributed by Mario Carneiro, 29-Mar-2014.)
115028115028
(Revised by Jim Kingdon, 9-Apr-2023.) $)
115029115029
summodclem3 $p |- ( ph ->
115030115030
( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` N ) ) $=
@@ -115074,7 +115074,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115074115074
JUYHVUKUYMWBUYHVUNVUKVUOUYKUFKWJVHWKZVUCUUAVUIXEXFVUPYTUUBUUCAKLUUEUVHY
115075115075
MUUD $.
115076115076

115077-
$( Lemma for ~ isummo . (Contributed by Mario Carneiro, 29-Mar-2014.)
115077+
$( Lemma for ~ summodc . (Contributed by Mario Carneiro, 29-Mar-2014.)
115078115078
Use ~ summodclem3 instead. (New usage is discouraged.) $)
115079115079
isummolem3 $p |- ( ph ->
115080115080
( seq 1 ( + , G , CC ) ` M ) = ( seq 1 ( + , H , CC ) ` N ) ) $=
@@ -115140,7 +115140,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115140115140
summolem2.7 $e |- ( ph -> A C_ ( ZZ>= ` M ) ) $.
115141115141
summolem2.8 $e |- ( ph -> f : ( 1 ... N ) -1-1-onto-> A ) $.
115142115142
summolem2.9 $e |- ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) $.
115143-
$( Lemma for ~ isummo . (Contributed by Mario Carneiro, 3-Apr-2014.)
115143+
$( Lemma for ~ summodc . (Contributed by Mario Carneiro, 3-Apr-2014.)
115144115144
(Revised by Jim Kingdon, 9-Apr-2023.) $)
115145115145
summodclem2a $p |- ( ph -> seq M ( + , F )
115146115146
~~> ( seq 1 ( + , G ) ` N ) ) $=
@@ -115209,7 +115209,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115209115209
QBUXTUMZUAAUXLUXQURVYQVYRUSAUXQUXLUYDUWSUXLUXQBUXTUWTVNVOUYFPQUXAAUXPLU
115210115210
XIUYCUXBUXDUXE $.
115211115211

115212-
$( Lemma for ~ isummo . (Contributed by Mario Carneiro, 3-Apr-2014.)
115212+
$( Lemma for ~ summodc . (Contributed by Mario Carneiro, 3-Apr-2014.)
115213115213
(Revised by Jim Kingdon, 3-Sep-2022.) Use ~ summodclem2a instead.
115214115214
(New usage is discouraged.) $)
115215115215
isummolem2a $p |- ( ph -> seq M ( + , F , CC )
@@ -115285,7 +115285,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115285115285
$d a f g k m n ph $. $d a f g k m n x $. $d a f m y $.
115286115286
summodclem2.g $e |- G = ( n e. NN |-> if ( n <_ ( # ` A ) ,
115287115287
[_ ( f ` n ) / k ]_ B , 0 ) ) $.
115288-
$( Lemma for ~ isummo . (Contributed by Mario Carneiro, 3-Apr-2014.)
115288+
$( Lemma for ~ summodc . (Contributed by Mario Carneiro, 3-Apr-2014.)
115289115289
(Revised by Jim Kingdon, 4-May-2023.) $)
115290115290
summodclem2 $p |- ( ( ph /\
115291115291
E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m ) DECID j e. A
@@ -115381,7 +115381,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115381115381
$d a f g k m n ph $. $d a f g k m n x $. $d a f m y $.
115382115382
isummolem2.g $e |- G = ( n e. NN |-> if ( n <_ ( # ` A ) ,
115383115383
[_ ( f ` n ) / k ]_ B , 0 ) ) $.
115384-
$( Lemma for ~ isummo . (Contributed by Mario Carneiro, 3-Apr-2014.)
115384+
$( Lemma for ~ summodc . (Contributed by Mario Carneiro, 3-Apr-2014.)
115385115385
(Revised by Jim Kingdon, 8-Sep-2022.) Use ~ summodclem2 instead.
115386115386
(New usage is discouraged.) $)
115387115387
isummolem2 $p |- ( ( ph /\
@@ -115409,69 +115409,6 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115409115409
VCUVHWTXAOUVEXBUUIUUJYQUUQXCAUUGYNUVBXDYJYKYMUUHUVBVOUUIUUJYQUUQXEUUIUU
115410115410
MUUQWCXFXGXHXIYEYSYLXJWEXLYRYSYEXKXMXNXHXOXPXQ $.
115411115411
$}
115412-
115413-
$d A a f g j k m n $. $d A f g j k m n x y $. $d B a f j m n $.
115414-
$d F f j k m n x y $. $d G g n x y $. $d a f g j k m n ph $.
115415-
$d ph x y $.
115416-
isummo.3 $e |- G = ( n e. NN
115417-
|-> if ( n <_ ( # ` A ) , [_ ( f ` n ) / k ]_ B , 0 ) ) $.
115418-
$( A sum has at most one limit. (Contributed by Mario Carneiro,
115419-
3-Apr-2014.) (Revised by Jim Kingdon, 10-Sep-2022.) Use ~ summodc
115420-
instead. (New usage is discouraged.) $)
115421-
isummo $p |- ( ph -> E* x
115422-
( E. m e. ZZ ( A C_ ( ZZ>= ` m )
115423-
/\ A. j e. ( ZZ>= ` m ) DECID j e. A
115424-
/\ seq m ( + , F , CC ) ~~> x ) \/
115425-
E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\
115426-
x = ( seq 1 ( + , G , CC ) ` m ) ) ) ) $=
115427-
( cfv wcel cz wceq wa cn vy vg va cv cuz wss wdc wral caddc cseq4 cli wbr
115428-
cc w3a wrex c1 cfz co wf1o wex wo weq wi wal fveq2 sseq2d raleqdv iseqeq1
115429-
wmo breq1d 3anbi123d cbvrexv reeanv simprl3 sylan simplrl simplrr simprl1
115430-
simpll simprr1 eleq1w dcbid simprl2 adantr rspcdva simprr2 isumrb simprr3
115431-
simpr mpbid climuni syl2anc exp31 rexlimdvv syl5bir expdimp syl5bi equcom
115432-
isummolem2 jaod syl6ib impancom chash cle csb cc0 cif wb oveq2 f1oeq2 syl
115433-
cmpt eqeq2d anbi12d exbidv f1oeq1 breq1 csbeq1d ifbieq1d cbvmptv mpteq2dv
115434-
fveq1 ifeq1d syl5eq iseqeq3 fveq1d cbvexv syl6bb nnzd fzfigd fihasheqf1od
115435-
eeanv an4 cn0 nnnn0d hashfz1 eqtr3d anbi2d expimpd rexbidv ifbid eqeltrrd
115436-
1zzd simprr breq2d simprl fveq2d jca oveq2d eqtri isummolem3 eqtrd eqeq12
115437-
syl5ibrcom sylbid exlimdvv rexlimdvva jaodan alrimivv breq2 3anbi3d eqeq1
115438-
orbi12d mo4 sylibr ) ACHUDZUEOZUFZFUDZCPZUGZFUVGUHZUIUMJUVFUJZBUDZUKULZUN
115439-
ZHQUOZUPUVFUQURZCEUDZUSZUVNUVFUIUMKUPUJZOZRZSZEUTZHTUOZVAZUVHUVLUVMUAUDZU
115440-
KULZUNZHQUOZUVTUWHUWBRZSZEUTZHTUOZVAZSBUAVBZVCZUAVDBVDUWGBVIAUWRBUAAUWGUW
115441-
PUWQAUVQUWPUWQVCUWFAUVQSZUWKUWQUWOUWKCIUDZUEOZUFZUVKFUXAUHZUIUMJUWTUJZUWH
115442-
UKULZUNZIQUOZUWSUWQUWJUXFHIQHIVBZUVHUXBUVLUXCUWIUXEUXHUVGUXACUVFUWTUEVEZV
115443-
FUXHUVKFUVGUXAUXIVGUXHUVMUXDUWHUKUIUMJUVFUWTVHVJVKVLAUVQUXGUWQUVQUXGSUVPU
115444-
XFSZIQUOHQUOAUWQUVPUXFHIQQVMAUXJUWQHIQQAUVFQPZUWTQPZSZUXJUWQAUXMSZUXJSZUX
115445-
DUVNUKULZUXEUWQUXOUVOUXPUVHUVLUVOUXFUXNVNUXOCDUVNGJUVFUWTLUXOAGUDZCPZDUMP
115446-
ZAUXMUXJVSMVOAUXKUXLUXJVPAUXKUXLUXJVQUVHUVLUVOUXFUXNVRUXBUXCUXEUVPUXNVTUX
115447-
OUXQUVGPZSUVKUXRUGZFUVGUXQFGVBUVJUXRFGCWAWBZUXOUVLUXTUVHUVLUVOUXFUXNWCWDU
115448-
XOUXTWIWEUXOUXQUXAPZSUVKUYAFUXAUXQUYBUXOUXCUYCUXBUXCUXEUVPUXNWFWDUXOUYCWI
115449-
WEWGWJUXBUXCUXEUVPUXNWHUVNUWHUXDWKWLWMWNWOWPWQABUACDEFGHIJKLMNWSWTAUWFSZU
115450-
WKUWQUWOAUWKUWFUWQAUWKSUWFUABVBUWQAUABCDEFGHIJKLMNWSUABWRXAXBUWOUPUWTUQUR
115451-
ZCUBUDZUSZUWHUWTUIUMUCTUCUDZCXCOZXDULZGUYHUYFOZDXEZXFXGZXLZUPUJZOZRZSZUBU
115452-
TZITUOZUYDUWQUWNUYSHITUXHUWNUYECUVSUSZUWHUWTUWAOZRZSZEUTUYSUXHUWMVUDEUXHU
115453-
VTVUAUWLVUCUXHUVRUYERUVTVUAXHUVFUWTUPUQXIUVRUYECUVSXJXKUXHUWBVUBUWHUVFUWT
115454-
UWAVEXMXNXOVUDUYREUBEUBVBZVUAUYGVUCUYQUYECUVSUYFXPVUEVUBUYPUWHVUEUWTUWAUY
115455-
OVUEKUYNRUWAUYORVUEKITUWTUYIXDULZGUWTUVSOZDXEZXFXGZXLZUYNNVUEVUJUCTUYJGUY
115456-
HUVSOZDXEZXFXGZXLUYNIUCTVUIVUMIUCVBZVUFUYJVUHVULXFUWTUYHUYIXDXQVUNGVUGVUK
115457-
DUWTUYHUVSVEXRXSXTVUEUCTVUMUYMVUEUYJVULUYLXFVUEGVUKUYKDUYHUVSUYFYBXRYCYAY
115458-
DYDUIUMKUYNUPYEXKYFXMXNYGYHVLAUWFUYTUWQUWFUYTSUWEUYSSZITUOHTUOAUWQUWEUYSH
115459-
ITTVMAVUOUWQHITTVUOUWDUYRSZUBUTEUTAUVFTPZUWTTPZSZSZUWQUWDUYREUBYLVUTVUPUW
115460-
QEUBVUPUVTUYGSZUWCUYQSZSVUTUWQUVTUWCUYGUYQYMVUTVVAVVBUWQVUTVVASZVVBUWCUWH
115461-
UWTUIUMUCTUYHUWTXDULZUYLXFXGZXLZUPUJZOZRZSZUWQVVCUYQVVIUWCVVCUYPVVHUWHVVC
115462-
UWTUYOVVGVVCUYNVVFRUYOVVGRVVCUCTUYMVVEVVCUYJVVDUYLXFVVCUYIUWTUYHXDVVCUYEX
115463-
COZUYIUWTVVCUYECUYFVVCUPUWTVVCUUCZVVCUWTAVUQVURVVAVQZYIYJVUTUVTUYGUUDZYKV
115464-
VCUWTYNPVVKUWTRVVCUWTVVMYOUWTYPXKYQUUEUUAYAUIUMUYNVVFUPYEXKYFXMYRVVCUWQVV
115465-
JUWBVVHRVVCUWBUYIUWAOVVHVVCUVFUYIUWAVVCUVRXCOZUVFUYIVVCUVFYNPVVOUVFRVVCUV
115466-
FAVUQVURVVAVPZYOUVFYPXKVVCUVRCUVSVVCUPUVFVVLVVCUVFVVPYIYJVUTUVTUYGUUFZYKY
115467-
QZUUGVVCCDEGFJKVVFUYFUYIUWTLVVCAUXRUXSAVUSVVAVSMVOVVCUYITPVURVVCUVFUYITVV
115468-
RVVPUUBVVMUUHVVCUVTUPUYIUQURZCUVSUSZVVQVVCUVRVVSRUVTVVTXHVVCUVFUYIUPUQVVR
115469-
UUIUVRVVSCUVSXJXKWJVVNKVUJFTUVIUYIXDULZGUVIUVSOZDXEZXFXGZXLNIFTVUIVWDIFVB
115470-
ZVUFVWAVUHVWCXFUWTUVIUYIXDXQVWEGVUGVWBDUWTUVIUVSVEXRXSXTUUJUCFTVVEUVIUWTX
115471-
DULZGUVIUYFOZDXEZXFXGUCFVBZVVDVWFUYLVWHXFUYHUVIUWTXDXQVWIGUYKVWGDUYHUVIUY
115472-
FVEXRXSXTUUKUULUVNUWBUWHVVHUUMUUNUUOYSWQUUPWOUUQWOWPWQWTUURYSUUSUWGUWPBUA
115473-
UWQUVQUWKUWFUWOUWQUVPUWJHQUWQUVOUWIUVHUVLUVNUWHUVMUKUUTUVAYTUWQUWEUWNHTUW
115474-
QUWDUWMEUWQUWCUWLUVTUVNUWHUWBUVBYRXOYTUVCUVDUVE $.
115475115412
$}
115476115413

115477115414
${

0 commit comments

Comments
 (0)