Skip to content

Commit

Permalink
rewrap
Browse files Browse the repository at this point in the history
  • Loading branch information
@sctfn
sctfn committed Jan 21, 2025
1 parent adaed15 commit e5f4f10
Showing 1 changed file with 45 additions and 46 deletions.
91 changes: 45 additions & 46 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -536394,12 +536394,12 @@ Real and complex numbers (cont.)
(Contributed by Scott Fenton, 20-Jan-2025.) $)
imaeqalov $p |- ( ( F Fn A /\ ( B X. C ) C_ A ) ->
( A. x e. ( F " ( B X. C ) ) ph <-> A. y e. B A. z e. C ps ) ) $=
( wral cv wrex wi wal ralcom4 r19.23v ralbii bitri bitr3i wfn cxp wss cima
wa co wceq wcel df-ral ovelimab imbi1d albidv bitrid albii ceqsalv bitrdi
ovex ) IFUAGHUBZFUCUEZACIURUDZKZCLZDLZELZIUFZUGZEHMZDGMZANZCOZBEHKZDGKZVAV
BUTUHZANZCOUSVJACUTUIUSVNVICUSVMVHADEFGHVBIUJUKULUMVJVFANZEHKZCOZDGKZVLVRV
PDGKZCOVJVPDCGPVSVICVSVGANZDGKVIVPVTDGVFAEHQRVGADGQSUNSVQVKDGVQVOCOZEHKVKV
OECHPWABEHABCVEVCVDIUQJUORTRTUP $.
( wral cv wrex wi wal ralcom4 r19.23v ralbii bitri bitr3i wfn cxp wa cima
wss co wceq wcel df-ral ovelimab imbi1d albidv bitrid ovex ceqsalv bitrdi
albii ) IFUAGHUBZFUEUCZACIURUDZKZCLZDLZELZIUFZUGZEHMZDGMZANZCOZBEHKZDGKZV
AVBUTUHZANZCOUSVJACUTUIUSVNVICUSVMVHADEFGHVBIUJUKULUMVJVFANZEHKZCOZDGKZVL
VRVPDGKZCOVJVPDCGPVSVICVSVGANZDGKVIVPVTDGVFAEHQRVGADGQSUQSVQVKDGVQVOCOZEH
KVKVOECHPWABEHABCVEVCVDIUNJUORTRTUP $.
$}

${
Expand Down Expand Up @@ -539671,10 +539671,10 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
$( Function statement for natural addition. (Contributed by Scott Fenton,
20-Jan-2025.) $)
naddf $p |- +no : ( On X. On ) --> On $=
( vx vy vz con0 cxp cnadd wf wfn cv cfv wcel wral naddfn co naddcl rgen2
cop wceq fveq2 df-ov eqtr4di eleq1d ralxp mpbir ffnfv mpbir2an ) DDEZDFG
FUGHAIZFJZDKZAUGLZMUKBIZCIZFNZDKZCDLBDLUOBCDDULUMOPUJUOABCDDUHULUMQZRZUI
UNDUQUIUPFJUNUHUPFSULUMFTUAUBUCUDAUGDFUEUF $.
( vx vy vz con0 cxp cnadd wf wfn cv cfv wcel wral naddfn naddcl rgen2 cop
co wceq fveq2 df-ov eqtr4di eleq1d ralxp mpbir ffnfv mpbir2an ) DDEZDFGFU
GHAIZFJZDKZAUGLZMUKBIZCIZFQZDKZCDLBDLUOBCDDULUMNOUJUOABCDDUHULUMPZRZUIUND
UQUIUPFJUNUHUPFSULUMFTUAUBUCUDAUGDFUEUF $.
$}

${
Expand Down Expand Up @@ -539882,36 +539882,36 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
( A. a e. A ( ( a +no B ) +no C ) e. x /\
A. b e. B ( ( A +no b ) +no C ) e. x /\
A. c e. C ( ( A +no B ) +no c ) e. x ) } ) $=
( vp con0 wcel cnadd co cxp cima cv wss wral wceq wb sylancr w3a csn cun
crab naddcl 3adant3 simp3 naddov3 intmin eqcomd 3ad2ant3 naddunif df-3an
cint wa unss ancom xpundir imaeq2i imaundi sseq1i 3bitr4i anbi1i 3bitrri
eqtri wfun cdm wfn naddfn fnfun ax-mp crn imassrn naddf frn sstri simpl3
snssd xpss12 fndmi sseqtrrdi funimassov oveq2 eleq1d ralsng ralbidv onss
wf syl 3ad2ant1 adantr simpl2 oveq1 imaeqalov oveq1d bitrd 3bitrd simpl1
syl2anc 3ad2ant2 ralsn bitrdi 3anbi123d bitrid rabbidva inteqd eqtrd
ovex ) BIJZCIJZDIJZUAZBCKLZDKLKKBUBZCMZNZKBCUBZMZNZUCZDUBZMZNZKXMUBZDMZN
ZUCAOZPZAIUDZUNEOZCKLZDKLZYGJZEBQZBFOZKLZDKLZYGJZFCQZXMGOZKLZYGJZGDQZUAZ
AIUDZUNXLEGAXMDXTDXIXJXMIJZXKBCUEUFZXIXJXKUGXIXJXMXTYJPEIUDUNRXKEBCUHUFX
KXIDDYTPGIUDUNZRXJXKUUHDGDIUIUJUKULXLYIUUEXLYHUUDAIYHKXSYAMZNZYGPZKXPYAM
ZNZYGPZYFYGPZUAZXLYGIJZUOZUUDUUPUUKUUNUOZUUOUOYCYGPZUUOUOYHUUKUUNUUOUMUU
SUUTUUOUUNUUKUOUUMUUJUCZYGPUUSUUTUUMUUJYGUPUUKUUNUQYCUVAYGYCKUULUUIUCZNU
VAYBUVBKXPXSYAURUSKUULUUIUTVEVAVBVCYCYFYGUPVDUURUUKYNUUNYSUUOUUCUURUUKHO
ZYTKLZYGJZGYAQZHXSQZUVCDKLZYGJZHXSQZYNUURKVFZUUIKVGZPUUKUVGSKIIMZVHZUVKV
IUVMKVJVKZUURUUIUVMUVLUURXSIPYAIPZUUIUVMPXSKVLZIKXRVMUVMIKWHUVQIPVNUVMIK
VOVKZVPUURDIXIXJXKUUQVQZVRZXSIYAIVSTUVMKVIVTZWAHGXSYAYGKWBTUURUVFUVIHXSU
URXKUVFUVISUVSUVEUVIGDIYTDRUVDUVHYGYTDUVCKWCWDWEWIZWFUURUVJYJYOKLZDKLZYG
JZFXQQZEBQZYNUURUVNXRUVMPZUVJUWGSVIUURBIPZXQIPUWHXLUWIUUQXIXJUWIXKBWGWJW
KUURCIXIXJXKUUQWLZVRBIXQIVSWSUVIUWEHEFUVMBXQKUVCUWCRUVHUWDYGUVCUWCDKWMWD
ZWNTUURUWFYMEBUURXJUWFYMSUWJUWEYMFCIYOCRZUWDYLYGUWLUWCYKDKYOCYJKWCWOWDWE
WIWFWPWQUURUUNUVFHXPQZUVIHXPQZYSUURUVKUULUVLPUUNUWMSUVOUURUULUVMUVLUURXP
IPUVPUULUVMPXPUVQIKXOVMUVRVPUVTXPIYAIVSTUWAWAHGXPYAYGKWBTUURUVFUVIHXPUWB
WFUURUWNUWEFCQZEXNQZYSUURUVNXOUVMPZUWNUWPSVIUURXNIPCIPZUWQUURBIXIXJXKUUQ
WRZVRXLUWRUUQXJXIUWRXKCWGWTWKXNICIVSWSUVIUWEHEFUVMXNCKUWKWNTUURXIUWPYSSU
WSUWOYSEBIYJBRZUWEYRFCUWTUWDYQYGUWTUWCYPDKYJBYOKWMWOWDWFWEWIWPWQUURUUOYJ
YTKLZYGJZGDQZEYDQZUUCUURUVKYEUVLPUUOUXDSUVOUURYEUVMUVLUURYDIPDIPZYEUVMPU
URXMIXLUUFUUQUUGWKVRXLUXEUUQXKXIUXEXJDWGUKWKYDIDIVSWSUWAWAEGYDDYGKWBTUXC
UUCEXMBCKXHYJXMRZUXBUUBGDUXFUXAUUAYGYJXMYTKWMWDWFXAXBXCXDXEXFXG $.
( vp con0 wcel cnadd co cxp cima cv wss wral wceq wb sylancr w3a csn crab
cun cint naddcl 3adant3 naddov3 intmin eqcomd 3ad2ant3 naddunif wa df-3an
simp3 unss ancom xpundir imaeq2i imaundi eqtri sseq1i 3bitr4i anbi1i wfun
3bitrri cdm wfn naddfn fnfun ax-mp crn imassrn wf naddf frn simpl3 xpss12
sstri snssd fndmi sseqtrrdi funimassov eleq1d ralsng syl ralbidv 3ad2ant1
oveq2 adantr simpl2 syl2anc oveq1 imaeqalov oveq1d 3bitrd simpl1 3ad2ant2
onss bitrd ovex ralsn bitrdi 3anbi123d bitrid rabbidva inteqd eqtrd ) BIJ
ZCIJZDIJZUAZBCKLZDKLKKBUBZCMZNZKBCUBZMZNZUDZDUBZMZNZKXMUBZDMZNZUDAOZPZAIU
CZUEEOZCKLZDKLZYGJZEBQZBFOZKLZDKLZYGJZFCQZXMGOZKLZYGJZGDQZUAZAIUCZUEXLEGA
XMDXTDXIXJXMIJZXKBCUFUGZXIXJXKUOXIXJXMXTYJPEIUCUERXKEBCUHUGXKXIDDYTPGIUCU
EZRXJXKUUHDGDIUIUJUKULXLYIUUEXLYHUUDAIYHKXSYAMZNZYGPZKXPYAMZNZYGPZYFYGPZU
AZXLYGIJZUMZUUDUUPUUKUUNUMZUUOUMYCYGPZUUOUMYHUUKUUNUUOUNUUSUUTUUOUUNUUKUM
UUMUUJUDZYGPUUSUUTUUMUUJYGUPUUKUUNUQYCUVAYGYCKUULUUIUDZNUVAYBUVBKXPXSYAUR
USKUULUUIUTVAVBVCVDYCYFYGUPVFUURUUKYNUUNYSUUOUUCUURUUKHOZYTKLZYGJZGYAQZHX
SQZUVCDKLZYGJZHXSQZYNUURKVEZUUIKVGZPUUKUVGSKIIMZVHZUVKVIUVMKVJVKZUURUUIUV
MUVLUURXSIPYAIPZUUIUVMPXSKVLZIKXRVMUVMIKVNUVQIPVOUVMIKVPVKZVSUURDIXIXJXKU
UQVQZVTZXSIYAIVRTUVMKVIWAZWBHGXSYAYGKWCTUURUVFUVIHXSUURXKUVFUVISUVSUVEUVI
GDIYTDRUVDUVHYGYTDUVCKWIWDWEWFZWGUURUVJYJYOKLZDKLZYGJZFXQQZEBQZYNUURUVNXR
UVMPZUVJUWGSVIUURBIPZXQIPUWHXLUWIUUQXIXJUWIXKBWSWHWJUURCIXIXJXKUUQWKZVTBI
XQIVRWLUVIUWEHEFUVMBXQKUVCUWCRUVHUWDYGUVCUWCDKWMWDZWNTUURUWFYMEBUURXJUWFY
MSUWJUWEYMFCIYOCRZUWDYLYGUWLUWCYKDKYOCYJKWIWOWDWEWFWGWTWPUURUUNUVFHXPQZUV
IHXPQZYSUURUVKUULUVLPUUNUWMSUVOUURUULUVMUVLUURXPIPUVPUULUVMPXPUVQIKXOVMUV
RVSUVTXPIYAIVRTUWAWBHGXPYAYGKWCTUURUVFUVIHXPUWBWGUURUWNUWEFCQZEXNQZYSUURU
VNXOUVMPZUWNUWPSVIUURXNIPCIPZUWQUURBIXIXJXKUUQWQZVTXLUWRUUQXJXIUWRXKCWSWR
WJXNICIVRWLUVIUWEHEFUVMXNCKUWKWNTUURXIUWPYSSUWSUWOYSEBIYJBRZUWEYRFCUWTUWD
YQYGUWTUWCYPDKYJBYOKWMWOWDWGWEWFWTWPUURUUOYJYTKLZYGJZGDQZEYDQZUUCUURUVKYE
UVLPUUOUXDSUVOUURYEUVMUVLUURYDIPDIPZYEUVMPUURXMIXLUUFUUQUUGWJVTXLUXEUUQXK
XIUXEXJDWSUKWJYDIDIVRWLUWAWBEGYDDYGKWCTUXCUUCEXMBCKXAYJXMRZUXBUUBGDUXFUXA
UUAYGYJXMYTKWMWDWGXBXCXDXEXFXGXH $.

$( Lemma for ~ naddass . Expand out the expression for natural addition of
three arguments. (Contributed by Scott Fenton, 20-Jan-2025.) $)
naddasslem2 $p |- ( ( A e. On /\ B e. On /\ C e. On ) ->
Expand Down Expand Up @@ -539952,11 +539952,10 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
$}

${
$d A a b c x y z w $. $d B a b c x y z w $.
$d C a b c x y z w $.
$d A a b c x y z w $. $d B a b c x y z w $. $d C a b c x y z w $.

$( Natural ordinal addition is associative. (Contributed by Scott
Fenton, 20-Jan-2025.) $)
$( Natural ordinal addition is associative. (Contributed by Scott Fenton,
20-Jan-2025.) $)
naddass $p |- ( ( A e. On /\ B e. On /\ C e. On ) ->
( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) $=
( vx vy vz vw cv cnadd co wceq oveq1 oveq1d eqeq12d oveq2 oveq2d con0 w3a
Expand All @@ -539980,8 +539979,8 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
GVEVFVHDEFURUSYBVKUUIKYIGVEVFVHDEFUTUSVAVBVD $.
$}

$( Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Scott Fenton, 20-Jan-2025.) $)
$( Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by Scott Fenton, 20-Jan-2025.) $)
nadd32 $p |- ( ( A e. On /\ B e. On /\ C e. On ) ->
( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) $=
( con0 wcel w3a cnadd co wceq naddcom 3adant1 oveq2d naddass 3com23 3eqtr4d
Expand Down

0 comments on commit e5f4f10

Please sign in to comment.