Remove isummolem2 from iset.mm

No longer used and replaced by summodclem2 .

Author: jkingdon

iset-discouraged

@@ -176,7 +176,6 @@
 "iseqcl" is used by "iseqp1".
 "iseqcoll" is used by "isummolem2a".
 "iseqeq1" is used by "iseqid".
-"iseqeq1" is used by "isummolem2".
 "iseqeq1" is used by "seqeq1".
 "iseqeq1" is used by "zisum".
 "iseqeq2" is used by "seqeq2".
@@ -230,7 +229,6 @@
 "iseradd" is used by "ser3add".
 "iserf" is used by "fisumcvg".
 "iserf" is used by "ser0f".
-"isummolem2a" is used by "isummolem2".
 "isummolem2a" is used by "zisum".
 "isummolem3" is used by "isummolem2a".
 "isumrb" is used by "zisum".
@@ -392,7 +390,7 @@ New usage of "iseqcaopr2" is discouraged (1 uses).
 New usage of "iseqcaopr3" is discouraged (1 uses).
 New usage of "iseqcl" is discouraged (3 uses).
 New usage of "iseqcoll" is discouraged (1 uses).
-New usage of "iseqeq1" is discouraged (4 uses).
+New usage of "iseqeq1" is discouraged (3 uses).
 New usage of "iseqeq2" is discouraged (1 uses).
 New usage of "iseqeq3" is discouraged (5 uses).
 New usage of "iseqex" is discouraged (4 uses).
@@ -413,8 +411,7 @@ New usage of "iseqvalt" is discouraged (3 uses).
 New usage of "iser0" is discouraged (1 uses).
 New usage of "iseradd" is discouraged (1 uses).
 New usage of "iserf" is discouraged (2 uses).
-New usage of "isummolem2" is discouraged (0 uses).
-New usage of "isummolem2a" is discouraged (2 uses).
+New usage of "isummolem2a" is discouraged (1 uses).
 New usage of "isummolem3" is discouraged (1 uses).
 New usage of "isumrb" is discouraged (1 uses).
 New usage of "mathbox" is discouraged (0 uses).

iset.mm

@@ -115375,40 +115375,6 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
         UWPUWRUVQUWKHRUWRUVPUWJUVIUVMUVOUWIUVNUKUVAUVBYTUWRUWFUWOHTUWRUWEUWNEUW
         RUWDUWMUWAUVOUWIUWCUVCYRXOYTUVDUVEUVF $.
     $}
-
-    ${
-      $d A a f g j k m n $.  $d B n $.  $d F a f g k m n $.  $d G a g $.
-      $d a f g k m n ph $.  $d a f g k m n x $.  $d a f m y $.
-      isummolem2.g $e |- G = ( n e. NN |-> if ( n <_ ( # ` A ) ,
-        [_ ( f ` n ) / k ]_ B , 0 ) ) $.
-      $( Lemma for ~ summodc .  (Contributed by Mario Carneiro, 3-Apr-2014.)
-         (Revised by Jim Kingdon, 8-Sep-2022.)  Use ~ summodclem2 instead.
-         (New usage is discouraged.) $)
-      isummolem2 $p |- ( ( ph /\
-         E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m ) DECID j e. A
-         /\ seq m ( + , F , CC ) ~~> x ) ) ->
-         ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\
-           y = ( seq 1 ( + , G , CC ) ` m ) ) -> x = y ) ) $=
-        ( cv wcel wbr cz wa va vg cuz cfv wss wdc wral caddc cseq4 cli w3a wrex
-        cc c1 cfz co wf1o wceq wex cn wi fveq2 sseq2d raleqdv iseqeq1 3anbi123d
-        weq breq1d cbvrexv simplr3 chash clt wiso cfn simplr1 uzssz syl6ss 1zzd
-        cen simprl nnzd fzfigd simprr f1oeng syl2anc ensymd zfz1iso cle csb cc0
-        enfii cif cmpt simplll sylan eleq1w dcbid simpr2 ad2antrr simpr rspcdva
-        eqid simprll simpllr simprlr isummolem2a expr exlimdv mpd climuni eqeq2
-        anassrs syl5ibrcom expimpd rexlimdva r19.29an sylan2b ) DIPZUCUDZUEZGPD
-        QZUFZGXSUGZUHUMKXRUIZBPZUJRZUKZISULADUAPZUCUDZUEZYBGYIUGZUHUMKYHUIZYEUJ
-        RZUKZUASULUNXRUOUPZDFPZUQZCPZXRUHUMLUNUIUDZURZTZFUSZIUTULBCVGZVAZYGYNIU
-        ASIUAVGZXTYJYCYKYFYMUUEXSYIDXRYHUCVBZVCUUEYBGXSYIUUFVDUUEYDYLYEUJUHUMKX
-        RYHVEVHVFVIAYNUUDUASAYHSQZTZYNTZUUBUUCIUTUUIXRUTQZTZUUAUUCFUUKYQYTUUCUU
-        KYQTUUCYTYEYSURZUUIUUJYQUULUUIUUJYQTZTZYMYLYSUJRZUULYJYKYMUUHUUMVJUUNUN
-        DVKUDUOUPDVLVLUBPZVMZUBUSZUUOUUNDSUEDVNQZUURUUNDYISYJYKYMUUHUUMVOYHVPVQ
-        UUNYOVNQZDYOVSRUUSUUNUNXRUUNVRUUNXRUUIUUJYQVTWAWBZUUNYODUUNUUTYQYODVSRU
-        VAUUIUUJYQWCYODVNYPWDWEWFDYOWKWEDUBWGWEUUNUUQUUOUBUUIUUMUUQUUOUUIUUMUUQ
-        TZTZDEFHJKLJUTJPZXRWHRHUVDUUPUDEWIWJWLWMZUUPYHXRMUVCAHPZDQZEUMQAUUGYNUV
-        BWNNWOUVCUVFYIQZTYBUVGUFGYIUVFGHVGYAUVGGHDWPWQUUIYKUVBUVHUUHYJYKYMWRWSU
-        VCUVHWTXAOUVEXBUUIUUJYQUUQXCAUUGYNUVBXDYJYKYMUUHUVBVOUUIUUJYQUUQXEUUIUU
-        MUUQWCXFXGXHXIYEYSYLXJWEXLYRYSYEXKXMXNXHXOXPXQ $.
-    $}
   $}
 
   ${