From cf79a465105d38bfe0da532b3954eb990b303bbd Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Wed, 28 Feb 2024 14:26:56 +0100 Subject: [PATCH] minimize ax-13 usage 25 --- set.mm | 993 +++++++++++++++++++++++++++++---------------------------- 1 file changed, 497 insertions(+), 496 deletions(-) diff --git a/set.mm b/set.mm index 9035b4b00c..c1d46e9545 100644 --- a/set.mm +++ b/set.mm @@ -595049,13 +595049,13 @@ then f(s) ` <_ ` f_s(t) ` \/ ` v. TODO: FIX COMMENT. (Contributed by cdleme31sn1 $p |- ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C ) $= ( csb wcel co wbr wa cif wceq eqid cdleme31sn adantr cv wn wi wral iftrue - crio csbeq2i syl6eq wnfc nfcv nfv nfcsb1v nfeq2 nfral nfriota a1i csbeq1a - nfim eqeq2d imbi2d ralbidv riotabidv csbiegf sylan9eqr syl6eqr eqtrd ) IC - UAZIGHLUBZMUCZUDZPINTZVRPIKTZPIFTZUEZEVPVTWCUFVRCWCFGHIKLMNPRWCUGUHUIVSWC - BUJZOMUCUKWDVQMUCUKUDZAUJZPIJTZUFZULZBCUMZADUOZEVRVPWCPIWEWFJUFZULZBCUMZA - DUOZTZWKVRWCWAWPVRWAWBUNPIKWOQUPUQPIWOWKCPWKURVPWJPADWIPBCPCUSWEWHPWEPUTP - WFWGPIJVAVBVGVCPDUSVDVEPUJIUFZWNWJADWQWMWIBCWQWLWHWEWQJWGWFPIJVFVHVIVJVKV - LVMSVNVO $. + crio csbeq2i syl6eq wnfc nfcv nfv nfcsb1v nfim nfralw nfriota a1i csbeq1a + nfeq2 eqeq2d imbi2d ralbidv riotabidv csbiegf sylan9eqr syl6eqr eqtrd ) I + CUAZIGHLUBZMUCZUDZPINTZVRPIKTZPIFTZUEZEVPVTWCUFVRCWCFGHIKLMNPRWCUGUHUIVSW + CBUJZOMUCUKWDVQMUCUKUDZAUJZPIJTZUFZULZBCUMZADUOZEVRVPWCPIWEWFJUFZULZBCUMZ + ADUOZTZWKVRWCWAWPVRWAWBUNPIKWOQUPUQPIWOWKCPWKURVPWJPADWIPBCPCUSWEWHPWEPUT + PWFWGPIJVAVGVBVCPDUSVDVEPUJIUFZWNWJADWQWMWIBCWQWLWHWEWQJWGWFPIJVFVHVIVJVK + VLVMSVNVO $. $} ${ @@ -595145,7 +595145,7 @@ then f(s) ` <_ ` f_s(t) ` \/ ` v. TODO: FIX COMMENT. (Contributed by 1-Apr-2013.) $) cdleme31snd $p |- ( S e. A -> [_ S / v ]_ [_ N / t ]_ D = E ) $= - ( csb wcel csbnestg cdleme31sc csbeq1d cvv wceq ovexi ax-mp syl6eq eqtrd + ( csb wcel csbnestgw cdleme31sc csbeq1d cvv wceq ovexi ax-mp syl6eq eqtrd co ) GCUAZAGBLDTTBAGLTZDTZIABGLDCUBULUNBMDTZIULBUMMDCLFEGNJKOMAQSUCUDMUEU AUOIUFMGNJUKEFGJUKOKUKJUKKSUGUEDEFMHJKOIBPRUCUHUIUJ $. $} @@ -597138,20 +597138,20 @@ then f(s) ` <_ ` f_s(t) ` \/ ` v. TODO: FIX COMMENT. (Contributed by cdleme40v $p |- ( R e. A -> [_ R / s ]_ N = [_ R / u ]_ V ) $= ( csb wceq wcel cv co wbr cif breq1 wn wa wral crio oveq1 oveq1d oveq2d wi syl5eq eqeq2d imbi2d ralbidv riotabidv eqeq1 anbi12d oveq12d 3eqtr4g - notbid oveq2 syl6eqr imbi12d cbvralv syl6bb cbvriotav ifbieq12d cbvcsbv - syl6eq a1i ) UHKUBVFDKUDVFVGKFVHUHDKUBUDUHVIZDVIZVGZXBIJRVJZTVKZQHVLXCX - ETVKZUCUGVLUBUDXDXFXGQHUCUGXBXCXETVMXDEVIZUETVKZVNZXHXETVKZVNZVOZAVIZOV - GZWAZEFVPZAGVQZCVIZUETVKZVNZXSXETVKZVNZVOZBVIZUFVGZWAZCFVPZBGVQZQUCXDXR - XMXNXENXCXHRVJZUEUAVJZRVJZUAVJZVGZWAZEFVPZAGVQYIXDXQYPAGXDXPYOEFXDXOYNX - MXDOYMXNXDOXENXBXHRVJZUEUAVJZRVJZUAVJYMUQXDYSYLXEUAXDYRYKNRXDYQYJUEUAXB - XCXHRVRVSVTVTWBWCWDWEWFYPYHABGXNYEVGZYPXMYEYMVGZWAZEFVPYHYTYOUUBEFYTYNU - UAXMXNYEYMWGWDWEUUBYGECFXHXSVGZXMYDUUAYFUUCXJYAXLYCUUCXIXTXHXSUETVMWKUU - CXKYBXHXSXETVMWKWHUUCYMUFYEUUCYMXELXCXSRVJZUEUAVJZRVJZUAVJUFUUCYLUUFXEU - AUUCNLYKUUERUUCXHMRVJZJIXHRVJZUEUAVJZRVJZUAVJXSMRVJZJIXSRVJZUEUAVJZRVJZ - UAVJNLUUCUUGUUKUUJUUNUAXHXSMRVRUUCUUIUUMJRUUCUUHUULUEUAXHXSIRWLVSVTWIUP - VBWJUUCYJUUDUEUAXHXSXCRWLVSWIVTVCWMWCWNWOWPWQWTURVDWJXDXBMRVJZJIXBRVJZU - EUAVJZRVJZUAVJXCMRVJZJIXCRVJZUEUAVJZRVJZUAVJHUGXDUUOUUSUURUVBUAXBXCMRVR - XDUUQUVAJRXDUUPUUTUEUAXBXCIRWLVSVTWIUTVAWJWRUSVEWJWSXA $. + notbid oveq2 syl6eqr imbi12d syl6bb cbvriotavw syl6eq ifbieq12d cbvcsbv + cbvralvw a1i ) UHKUBVFDKUDVFVGKFVHUHDKUBUDUHVIZDVIZVGZXBIJRVJZTVKZQHVLX + CXETVKZUCUGVLUBUDXDXFXGQHUCUGXBXCXETVMXDEVIZUETVKZVNZXHXETVKZVNZVOZAVIZ + OVGZWAZEFVPZAGVQZCVIZUETVKZVNZXSXETVKZVNZVOZBVIZUFVGZWAZCFVPZBGVQZQUCXD + XRXMXNXENXCXHRVJZUEUAVJZRVJZUAVJZVGZWAZEFVPZAGVQYIXDXQYPAGXDXPYOEFXDXOY + NXMXDOYMXNXDOXENXBXHRVJZUEUAVJZRVJZUAVJYMUQXDYSYLXEUAXDYRYKNRXDYQYJUEUA + XBXCXHRVRVSVTVTWBWCWDWEWFYPYHABGXNYEVGZYPXMYEYMVGZWAZEFVPYHYTYOUUBEFYTY + NUUAXMXNYEYMWGWDWEUUBYGECFXHXSVGZXMYDUUAYFUUCXJYAXLYCUUCXIXTXHXSUETVMWK + UUCXKYBXHXSXETVMWKWHUUCYMUFYEUUCYMXELXCXSRVJZUEUAVJZRVJZUAVJUFUUCYLUUFX + EUAUUCNLYKUUERUUCXHMRVJZJIXHRVJZUEUAVJZRVJZUAVJXSMRVJZJIXSRVJZUEUAVJZRV + JZUAVJNLUUCUUGUUKUUJUUNUAXHXSMRVRUUCUUIUUMJRUUCUUHUULUEUAXHXSIRWLVSVTWI + UPVBWJUUCYJUUDUEUAXHXSXCRWLVSWIVTVCWMWCWNWTWOWPWQURVDWJXDXBMRVJZJIXBRVJ + ZUEUAVJZRVJZUAVJXCMRVJZJIXCRVJZUEUAVJZRVJZUAVJHUGXDUUOUUSUURUVBUAXBXCMR + VRXDUUQUVAJRXDUUPUUTUEUAXBXCIRWLVSVTWIUTVAWJWRUSVEWJWSXA $. $} $d v D $. $d v y z E $. $d v I $. $d u v N $. $d s S $. $d s u U $. @@ -598148,16 +598148,16 @@ then f(s) ` <_ ` f_s(t) ` \/ ` v. TODO: FIX COMMENT. (Contributed by ( chlt wcel wa wbr wn w3a wne co cfv cdlemeg47b csbeq1d wceq simp1 simp2l csb simp11 simp13 simp12 cdleme46fvaw cdleme46f2g2 cdleme46frvlpq simp11l simp2r syl31anc simp12l simp13l hlatjcom syl3anc breq2d mtbird cdlemefr45 - syl syl121anc simp2rl csbnestg 3eqtr4d ) SVDVEZUEQVEZVFZJGVEZJUETVGVHZVFZ - KGVEZKUETVGVHZVFZVIZJKVJZLGVEZLUETVGVHZVFZVFZLJKRVKZTVGVHZVIZFLPVLZIVRZFD - LUBVRZIVRZXROVLZDLFUBIVRVRZXQFXRXTIDEGHJKLPQRSTUAUBUCUDUEUGUHUIUJUKULUMUN - UOUTVAVBVCVMVNXQXIXJXRGVEXRUETVGVHVFZXRXOTVGZVHYBXSVOXIXNXPVPXIXJXMXPVQXQ - XBXHXEXMYDXBXEXHXNXPVSXBXEXHXNXPVTXBXEXHXNXPWAXIXJXMXPWFUGUHUIDGHUBKJLUDU - CPQRSTUAUEEUJUKULUMUNUOUTVAVBVCWBWGXQYEXRKJRVKZTVGZXQXBXHXEVIKJVJXMVFLYFT - VGVHVIYGVHGJKLQRSTUEULUNWCUGUHUIDGHUBKJLUDUCPQRSTUAUEEUJUKULUMUNUOUTVAVBV - CWDWOXQXOYFXRTXQWTXCXFXOYFVOWTXAXEXHXNXPWEXCXDXBXHXNXPWHXFXGXBXEXNXPWIGRS - JKULUNWJWKWLWMABCFGHIJKXRMNOQRSTUAUEUFUJUKULUMUNUOUPUQUSWNWPXQXKYCYAVOXKX - LXJXIXPWQDFLUBIGWRWOWS $. + syl syl121anc simp2rl csbnestgw 3eqtr4d ) SVDVEZUEQVEZVFZJGVEZJUETVGVHZVF + ZKGVEZKUETVGVHZVFZVIZJKVJZLGVEZLUETVGVHZVFZVFZLJKRVKZTVGVHZVIZFLPVLZIVRZF + DLUBVRZIVRZXROVLZDLFUBIVRVRZXQFXRXTIDEGHJKLPQRSTUAUBUCUDUEUGUHUIUJUKULUMU + NUOUTVAVBVCVMVNXQXIXJXRGVEXRUETVGVHVFZXRXOTVGZVHYBXSVOXIXNXPVPXIXJXMXPVQX + QXBXHXEXMYDXBXEXHXNXPVSXBXEXHXNXPVTXBXEXHXNXPWAXIXJXMXPWFUGUHUIDGHUBKJLUD + UCPQRSTUAUEEUJUKULUMUNUOUTVAVBVCWBWGXQYEXRKJRVKZTVGZXQXBXHXEVIKJVJXMVFLYF + TVGVHVIYGVHGJKLQRSTUEULUNWCUGUHUIDGHUBKJLUDUCPQRSTUAUEEUJUKULUMUNUOUTVAVB + VCWDWOXQXOYFXRTXQWTXCXFXOYFVOWTXAXEXHXNXPWEXCXDXBXHXNXPWHXFXGXBXEXNXPWIGR + SJKULUNWJWKWLWMABCFGHIJKXRMNOQRSTUAUEUFUJUKULUMUNUOUPUQUSWNWPXQXKYCYAVOXK + XLXJXIXPWQDFLUBIGWRWOWS $. $( Value of g_s(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT. (Contributed by @@ -606338,15 +606338,15 @@ one of its values (at a non-identity translation) is the identity ( chlt wcel wa cid cres wne w3a wbr wn cfv wceq cv wi wral crio eqcomi wb simpl1 simpl2 simpl3 simpr1 simpr2 simpr3 syl132anc eqeltrrid cltrn fvexi wreu cdlemk35 riotaclbBAD sylibr nfriota1 nfcxfr nfcv nfv nffv nfeq1 nfim - nfral nfra1 nfriota nfeq2 eqeq1d imbi2d ralbid riota2f syl2anc mpbiri rsp - fveq1 syl impd 3impia ) KUKULOIULUMZGFULGUNCUOZUPUMZHFULHXEUPUMZUQZNFULZD - BULDOLURUSUMZGEUTZNEUTVAZUQZSVBZFULZXNXEUPXNEUTZXKUPXPHEUTUPUQZUMDPUTZQVA - ZXHXMUMZXOXQXSXTXQXSVCZSFVDZXOYAVCXTYBXQDAVBZUTZQVAZVCZSFVDZAFVEZPVAZPYHU - JVFXTPFULZYGAFVRZYBYIVGXTXDXFXGXIXJXLYJXDXFXGXMVHXDXFXGXMVIXDXFXGXMVJXHXI - XJXLVKXHXIXJXLVLXHXIXJXLVMABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJVSVNZXT - YHFULYKXTYHPFUJYLVOYGAFFOKVPUTUFVQVTWAYGYBAFPAPYHUJYGAFWBWCZYAASFAFWDXQXS - AXQAWEAXRQADPYMADWDWFWGWHWIYCPVAZYFYASFSYCPSPYHUJYGSAFYFSFWJSFWDWKWCWLYNY - EXSXQYNYDXRQDYCPWTWMWNWOWPWQWRYASFWSXAXBXC $. + nfralw nfra1 nfriota nfeq2 fveq1 eqeq1d imbi2d ralbid riota2f syl2anc rsp + mpbiri syl impd 3impia ) KUKULOIULUMZGFULGUNCUOZUPUMZHFULHXEUPUMZUQZNFULZ + DBULDOLURUSUMZGEUTZNEUTVAZUQZSVBZFULZXNXEUPXNEUTZXKUPXPHEUTUPUQZUMDPUTZQV + AZXHXMUMZXOXQXSXTXQXSVCZSFVDZXOYAVCXTYBXQDAVBZUTZQVAZVCZSFVDZAFVEZPVAZPYH + UJVFXTPFULZYGAFVRZYBYIVGXTXDXFXGXIXJXLYJXDXFXGXMVHXDXFXGXMVIXDXFXGXMVJXHX + IXJXLVKXHXIXJXLVLXHXIXJXLVMABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJVSVNZX + TYHFULYKXTYHPFUJYLVOYGAFFOKVPUTUFVQVTWAYGYBAFPAPYHUJYGAFWBWCZYAASFAFWDXQX + SAXQAWEAXRQADPYMADWDWFWGWHWIYCPVAZYFYASFSYCPSPYHUJYGSAFYFSFWJSFWDWKWCWLYN + YEXSXQYNYDXRQDYCPWMWNWOWPWQWRWTYASFWSXAXBXC $. $( Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) $) @@ -606842,14 +606842,14 @@ one of its values (at a non-identity translation) is the identity /\ ( ( P e. A /\ -. P .<_ W ) /\ G = ( _I |` B ) ) ) -> [_ G / g ]_ X = ( _I |` B ) ) $= ( chlt wcel wa cfv wceq w3a wbr wn cid cvv csb cltrn fvexi cv wne nfv wnf - cres nfcv wi wral nfra1 nfriota nfcxfr nfcsb nfeq1 a1i cdlemkid4 wb eqeq1 - crio adantl eqidd cdlemkid5 wrex cdlemftr2 3ad2ant1 riotasv3d mpan2 ) LUL - UMPJUMUNZHFUMOFUMHEUOZOEUOUPUQZDBUMDPMURUSUNIUTCVIZUPUNZUQZFVAUMGIQVBZWNU - PZFPLVCUOUGVDWPTVEZWNVFZWSEUOZWLVFZXAIEUOZVFUQZWNWNUPZWRATFFWNWQVAWPTVGWR - TVHWPTWQWNTGIQTIVJTQWTXBXAGVEEUOVFUQDAVEUORUPVKZTFVLZAFWBUKXGTAFXFTFVMTFV - JVNVOVPVQVRABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKVSWNWQUPXEWRVTWPWNWQ - WNWAWCWSFUMXDUNZXEVKWPXHWNWDVRABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKW - EWKWMXDTFWFWOCEFTJLPWLXCUAUFUGUHWGWHWIWJ $. + cres nfcv wi wral crio nfra1 nfriota nfcxfr nfcsbw nfeq1 a1i cdlemkid4 wb + eqeq1 adantl eqidd cdlemkid5 wrex cdlemftr2 3ad2ant1 riotasv3d mpan2 ) LU + LUMPJUMUNZHFUMOFUMHEUOZOEUOUPUQZDBUMDPMURUSUNIUTCVIZUPUNZUQZFVAUMGIQVBZWN + UPZFPLVCUOUGVDWPTVEZWNVFZWSEUOZWLVFZXAIEUOZVFUQZWNWNUPZWRATFFWNWQVAWPTVGW + RTVHWPTWQWNTGIQTIVJTQWTXBXAGVEEUOVFUQDAVEUORUPVKZTFVLZAFVMUKXGTAFXFTFVNTF + VJVOVPVQVRVSABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKVTWNWQUPXEWRWAWPWNW + QWNWBWCWSFUMXDUNZXEVKWPXHWNWDVSABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUK + WEWKWMXDTFWFWOCEFTJLPWLXCUAUFUGUHWGWHWIWJ $. $( Substitution version of ~ cdlemk35 . (Contributed by NM, 22-Jul-2013.) $) @@ -606968,13 +606968,13 @@ one of its values (at a non-identity translation) is the identity /\ ( P e. A /\ -. P .<_ W ) ) -> ( [_ F / g ]_ X ` P ) = ( N ` P ) ) $= ( chlt wcel wa cfv wceq cid cres wne w3a wbr wn wrex csb simp1l cdlemftr1 - cv syl nfv nfcv wi wral crio nfra1 nfriota nfcxfr nfcsb nffv nfeq1 simpl1 - simpl2 simpl3 simpr cdlemk19xlem syl121anc exp32 rexlimd mpd ) KUKULOIULU - MZHEUNZNEUNUOZUMZHFULHUPCUQZURNFULUSZDBULDOLUTVAUMZUSZSVFZWLURZWPEUNZWIUR - ZUMZSFVBZDGHPVCZUNZDNUNZUOZWOWHXAWHWJWMWNVDCEFSIKOWITUEUFUGVEVGWOWTXESFWO - SVHSXCXDSDXBSGHPSHVISPWQWSWRGVFEUNURUSDAVFUNQUOVJZSFVKZAFVLUJXGSAFXFSFVMS - FVIVNVOVPSDVIVQVRWOWPFULZWTXEWOXHWTUMZUMWKWMWNXIXEWKWMWNXIVSWKWMWNXIVTWKW - MWNXIWAWOXIWBABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJWCWDWEWFWG $. + cv syl nfv nfcv wral crio nfra1 nfriota nfcxfr nfcsbw nfeq1 simpl1 simpl2 + wi nffv simpl3 simpr cdlemk19xlem syl121anc exp32 rexlimd mpd ) KUKULOIUL + UMZHEUNZNEUNUOZUMZHFULHUPCUQZURNFULUSZDBULDOLUTVAUMZUSZSVFZWLURZWPEUNZWIU + RZUMZSFVBZDGHPVCZUNZDNUNZUOZWOWHXAWHWJWMWNVDCEFSIKOWITUEUFUGVEVGWOWTXESFW + OSVHSXCXDSDXBSGHPSHVISPWQWSWRGVFEUNURUSDAVFUNQUOVSZSFVJZAFVKUJXGSAFXFSFVL + SFVIVMVNVOSDVIVTVPWOWPFULZWTXEWOXHWTUMZUMWKWMWNXIXEWKWMWNXIVQWKWMWNXIVRWK + WMWNXIWAWOXIWBABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJWCWDWEWFWG $. $d g ./\ $. $d g .\/ $. $d g Z $. $( Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. @@ -607030,18 +607030,18 @@ one of its values (at a non-identity translation) is the identity -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) ) $= ( chlt wcel wa cid cres wne w3a wbr wn cfv wceq cv wrex ccnv ccom simp11l - csb co simp11r cdlemftr3 syl2anc nfv nfcv wi wral crio nfra1 nfcxfr nfcsb - nfriota nffv nfov nfbr simp11 simp12 simp2 simp3l simp3r1 simp3r2 simp13l - 3jca simp13r simp3r3 cdlemk11tc syl113anc 3exp rexlimd mpd ) MUMUNZQJUNZU - OHFUNHUPCUQZURUOZIFUNIXCURUOZUSZPFUNDBUNDQNUTVAUOHEVBZPEVBVCUSZKFUNZKXCUR - ZUOZUSZUAVDZXCURZXMEVBZXGURZXOIEVBZURZXOKEVBZURZUSZUOZUAFVEZDGIRVIZVBZDGK - RVIZVBZKIVFVGEVBZLVJZNUTZXLXAXBYCXAXBXDXEXHXKVHXAXBXDXEXHXKVKCEFUAJMQXGXQ - XSUBUGUHUIVLVMXLYBYJUAFXLUAVNUAYEYINUADYDUAGIRUAIVOUARXNXPXOGVDEVBURUSDAV - DVBSVCVPZUAFVQZAFVRULYLUAAFYKUAFVSUAFVOWBVTZWAUADVOZWCUANVOUAYGYHLUADYFUA - GKRUAKVOYMWAYNWCUALVOUAYHVOWDWEXLXMFUNZYBYJXLYOYBUSZXFXHYOXNXPXRUSXIXJXTU - SYJXFXHXKYOYBWFXFXHXKYOYBWGXLYOYBWHYPXNXPXRXLYOXNYAWIXPXRXTXNXLYOWJXPXRXT - XNXLYOWKWMYPXIXJXTXIXJXFXHYOYBWLXIXJXFXHYOYBWNXPXRXTXNXLYOWOWMABCDEFGHIJK - LMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKULWPWQWRWSWT $. + csb co simp11r cdlemftr3 syl2anc nfv nfcv wral crio nfriota nfcxfr nfcsbw + wi nfra1 nffv nfov nfbr simp11 simp12 simp3l simp3r1 simp3r2 3jca simp13l + simp2 simp13r simp3r3 cdlemk11tc syl113anc 3exp rexlimd mpd ) MUMUNZQJUNZ + UOHFUNHUPCUQZURUOZIFUNIXCURUOZUSZPFUNDBUNDQNUTVAUOHEVBZPEVBVCUSZKFUNZKXCU + RZUOZUSZUAVDZXCURZXMEVBZXGURZXOIEVBZURZXOKEVBZURZUSZUOZUAFVEZDGIRVIZVBZDG + KRVIZVBZKIVFVGEVBZLVJZNUTZXLXAXBYCXAXBXDXEXHXKVHXAXBXDXEXHXKVKCEFUAJMQXGX + QXSUBUGUHUIVLVMXLYBYJUAFXLUAVNUAYEYINUADYDUAGIRUAIVOUARXNXPXOGVDEVBURUSDA + VDVBSVCWAZUAFVPZAFVQULYLUAAFYKUAFWBUAFVOVRVSZVTUADVOZWCUANVOUAYGYHLUADYFU + AGKRUAKVOYMVTYNWCUALVOUAYHVOWDWEXLXMFUNZYBYJXLYOYBUSZXFXHYOXNXPXRUSXIXJXT + USYJXFXHXKYOYBWFXFXHXKYOYBWGXLYOYBWMYPXNXPXRXLYOXNYAWHXPXRXTXNXLYOWIXPXRX + TXNXLYOWJWKYPXIXJXTXIXJXFXHYOYBWLXIXJXFXHYOYBWNXPXRXTXNXLYOWOWKABCDEFGHIJ + KLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKULWPWQWRWSWT $. $( Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119. ` G ` , ` I ` stand for g, h. ` X ` represents tau. They do not explicitly @@ -612092,35 +612092,35 @@ all translations (for a fiducial co-atom ` W ` ). (Contributed by NM, eqeltrd 3jca simpr3 simpr2 jca impbida dvhbase rexeqdv tendoidcl ad2antrr ccom dvhopvsca syl13anc eqeq2d opth syl6bb tendo1mulr equcom anbi2d bitrd adantlr ancom rexbidva 3anbi3d fveq1 ceqsrexv pm5.32i anbi2i 3anass eqeq1 - 3bitr4i syl6rbb rexbidv eleq2i opabid bitr2i eqrelrdv2 syl21anc wi eleq2d - rabxp syl2anc syl12anc biimpa opelxpi dvhvscacl eleq1a rexlimdva pm4.71rd - syl abbidv 3eqtr4a clmod dvhlmod dvhelvbasei lspsn eqtr4d ) JUIUJMHUJUKZC - AUJCMKULUMUKZUKZCIUNZUCUOZUDUOZGUPDUQZURZEUSUNZUTZVAZUDEVBUNZVCUNZVDZUCVE - ZUVBVFLUNZUUQUVHUCDMJVGUNUNZVHZVIZUUSUVLUJZUVHUKZUCVEUURUVIUVHUCUVLVJUUQU - URVOZUVMVOZUUQUURUVMVAUUQUVPUEUOGUFUOZUNVAUVRUVKUJUKZUEUFVKZVOUVSUEUFVLUU - QUURUVTABCDUEFUVKGHIJKUIMUFNOPQRUVKVPZSUBVMVNVQUVQUUQUVMUVLVRUVLVOUVQUVHU - CUVLVSDUVKVTUVMUVLWAWBWCUUQWDUUQUGUHUURUVMUUQUGUOZUHUOZURZUURUJUWBGUWCUNZ - VAZUWCUVKUJZUKZUWDUVMUJZABCUWCDFUVKUWBGHIJKUIMNOPQRUWASUBUGWEZUHWEZWFUUQU - WHUWBDUJZUWGUWDUVDVAZUDUVGVDZWHZUWIUUQUWHUWLUWGUWFWHZUWOUUQUWHUWPUUQUWHUK - ZUWLUWGUWFUWQUWBUWEDUUQUWFUWGWGZUWQUUOUWGGDUJZUWEDUJUUOUUPUWHWIUUQUWFUWGW - JZUUQUWSUWHUUQUUOBAUJBMKULUMUKZUUPUWSUUOUUPWKZUUOUXAUUPABHJKMNOPQWLWMUUOU - UPWNABCDFGHJKMNOPRUBWOWPZWMUWCDUVKGHJUIMPRUWAWQWPWRUWTUWRWSUUQUWPUKUWFUWG - UUQUWLUWGUWFWTUUQUWLUWGUWFXAXBXCUUQUWOUWLUWGUUTUWCVAZUWBGUUTUNZVAZUKZUDUV - KVDZWHZUWPUUQUWNUXHUWLUWGUUQUWNUWMUDUVKVDUXHUUQUWMUDUVGUVKUUOUVGUVKVAUUPU - VGEUVKUVFHJMUIPUWATUVFVPZUVGVPZXDWMZXEUUQUWMUXGUDUVKUUQUUTUVKUJZUKZUWMUXF - UXDUKZUXGUXNUWMUXFUWCUUTUVAXHZVAZUKZUXOUXNUWMUWDUXEUXPURZVAUXRUXNUVDUXSUW - DUXNUUOUXMUWSUVAUVKUJZUVDUXSVAUUOUUPUXMWIUUQUXMWNUUQUWSUXMUXCWMUUOUXTUUPU - XMDUVKHJMPRUWAXFZXGUUTDUVCEUVKGHJUIMUVAPRUWATUVCVPZXIXJXKUWBUWCUXEUXPUWJU - WKXLXMUXNUXQUXDUXFUXNUXQUWCUUTVAUXDUXNUXPUUTUWCUUOUXMUXPUUTVAUUPDUUTUVKHJ - MPRUWAXNXRXKUHUDXOXMXPXQUXFUXDXSXMXTXQYAUWLUWGUXHUKZUKUWLUWGUWFUKZUKUXIUW - PUYCUYDUWLUWGUXHUWFUXFUWFUDUWCUVKUXDUXEUWEUWBGUUTUWCYBXKYCYDYEUWLUWGUXHYF - UWLUWGUWFYFYHYIXQUWIUWDUWOUGUHVKZUJUWOUVMUYEUWDUVHUWNUCUGUHDUVKUUSUWDVAUV - EUWMUDUVGUUSUWDUVDYGYJYRYKUWOUGUHYLYMXMXQYNYOUUQUVHUVOUCUUQUVHUVNUUQUVEUV - NUDUVGUUQUUTUVGUJZUKZUVDUVLUJZUVEUVNYPUYGUUOUXMUVBUVLUJZUYHUUOUUPUYFWIUUQ - UYFUXMUUQUVGUVKUUTUXLYQUUAUUQUYIUYFUUQUWSUXTUYIUXCUUOUXTUUPUYAWMZGUVADUVK - UUBYSWMUUTDUVCEUVKUVBHJMPRUWATUYBUUCYTUVDUVLUUSUUDUUGUUEUUFUUHUUIUUQEUUJU - JUVBEVCUNZUJZUVJUVIVAUUQEHJMPTUXBUUKUUQUUOUWSUXTUYLUXBUXCUYJUVADEUVKGHJUY - KMUIPRUWATUYKVPZUULYTUCUVCUDUVFUVGLUYKEUVBUXJUXKUYMUYBUAUUMYSUUN $. + 3bitr4i syl6rbb rexbidv rabxp eleq2i opabidw bitr2i eqrelrdv2 syl21anc wi + eleq2d syl2anc syl12anc biimpa dvhvscacl eleq1a rexlimdva pm4.71rd abbidv + opelxpi syl 3eqtr4a clmod dvhlmod dvhelvbasei lspsn eqtr4d ) JUIUJMHUJUKZ + CAUJCMKULUMUKZUKZCIUNZUCUOZUDUOZGUPDUQZURZEUSUNZUTZVAZUDEVBUNZVCUNZVDZUCV + EZUVBVFLUNZUUQUVHUCDMJVGUNUNZVHZVIZUUSUVLUJZUVHUKZUCVEUURUVIUVHUCUVLVJUUQ + UURVOZUVMVOZUUQUURUVMVAUUQUVPUEUOGUFUOZUNVAUVRUVKUJUKZUEUFVKZVOUVSUEUFVLU + UQUURUVTABCDUEFUVKGHIJKUIMUFNOPQRUVKVPZSUBVMVNVQUVQUUQUVMUVLVRUVLVOUVQUVH + UCUVLVSDUVKVTUVMUVLWAWBWCUUQWDUUQUGUHUURUVMUUQUGUOZUHUOZURZUURUJUWBGUWCUN + ZVAZUWCUVKUJZUKZUWDUVMUJZABCUWCDFUVKUWBGHIJKUIMNOPQRUWASUBUGWEZUHWEZWFUUQ + UWHUWBDUJZUWGUWDUVDVAZUDUVGVDZWHZUWIUUQUWHUWLUWGUWFWHZUWOUUQUWHUWPUUQUWHU + KZUWLUWGUWFUWQUWBUWEDUUQUWFUWGWGZUWQUUOUWGGDUJZUWEDUJUUOUUPUWHWIUUQUWFUWG + WJZUUQUWSUWHUUQUUOBAUJBMKULUMUKZUUPUWSUUOUUPWKZUUOUXAUUPABHJKMNOPQWLWMUUO + UUPWNABCDFGHJKMNOPRUBWOWPZWMUWCDUVKGHJUIMPRUWAWQWPWRUWTUWRWSUUQUWPUKUWFUW + GUUQUWLUWGUWFWTUUQUWLUWGUWFXAXBXCUUQUWOUWLUWGUUTUWCVAZUWBGUUTUNZVAZUKZUDU + VKVDZWHZUWPUUQUWNUXHUWLUWGUUQUWNUWMUDUVKVDUXHUUQUWMUDUVGUVKUUOUVGUVKVAUUP + UVGEUVKUVFHJMUIPUWATUVFVPZUVGVPZXDWMZXEUUQUWMUXGUDUVKUUQUUTUVKUJZUKZUWMUX + FUXDUKZUXGUXNUWMUXFUWCUUTUVAXHZVAZUKZUXOUXNUWMUWDUXEUXPURZVAUXRUXNUVDUXSU + WDUXNUUOUXMUWSUVAUVKUJZUVDUXSVAUUOUUPUXMWIUUQUXMWNUUQUWSUXMUXCWMUUOUXTUUP + UXMDUVKHJMPRUWAXFZXGUUTDUVCEUVKGHJUIMUVAPRUWATUVCVPZXIXJXKUWBUWCUXEUXPUWJ + UWKXLXMUXNUXQUXDUXFUXNUXQUWCUUTVAUXDUXNUXPUUTUWCUUOUXMUXPUUTVAUUPDUUTUVKH + JMPRUWAXNXRXKUHUDXOXMXPXQUXFUXDXSXMXTXQYAUWLUWGUXHUKZUKUWLUWGUWFUKZUKUXIU + WPUYCUYDUWLUWGUXHUWFUXFUWFUDUWCUVKUXDUXEUWEUWBGUUTUWCYBXKYCYDYEUWLUWGUXHY + FUWLUWGUWFYFYHYIXQUWIUWDUWOUGUHVKZUJUWOUVMUYEUWDUVHUWNUCUGUHDUVKUUSUWDVAU + VEUWMUDUVGUUSUWDUVDYGYJYKYLUWOUGUHYMYNXMXQYOYPUUQUVHUVOUCUUQUVHUVNUUQUVEU + VNUDUVGUUQUUTUVGUJZUKZUVDUVLUJZUVEUVNYQUYGUUOUXMUVBUVLUJZUYHUUOUUPUYFWIUU + QUYFUXMUUQUVGUVKUUTUXLYRUUAUUQUYIUYFUUQUWSUXTUYIUXCUUOUXTUUPUYAWMZGUVADUV + KUUGYSWMUUTDUVCEUVKUVBHJMPRUWATUYBUUBYTUVDUVLUUSUUCUUHUUDUUEUUFUUIUUQEUUJ + UJUVBEVCUNZUJZUVJUVIVAUUQEHJMPTUXBUUKUUQUUOUWSUXTUYLUXBUXCUYJUVADEUVKGHJU + YKMUIPRUWATUYKVPZUULYTUCUVCUDUVFUVGLUYKEUVBUXJUXKUYMUYBUAUUMYSUUN $. $} ${ @@ -614417,28 +614417,28 @@ of phi(x) is independent of the atom q." (Contributed by NM, w3a ccla syl wceq wrex crab ssrab2 eqsstri clatglbcl sylancl adantr simpr simpl2 sseldd simpl1r lhpbase latmcl syl3anc eqidd oveq1 rspceeqv syl2anc clat eqeq1 rexbidv elrab sylanbrc eleqtrrdi clatglble mp3an2 latmle1 wral - lattrd weq eqeq2d cbvrexv syl6bb elrab2 simp3 simp13 breq2 rspcva simp11l - wi 3ad2ant1 simp12 simp112 simp11r wb clatleglb simp113 latlem12 syl13anc - mpbird mpbi2and 3expia biimprcd syl6 rexlimdv expimpd syl5bi simp2 mp3an3 - ralrimiv isglbd ) HUERZKGRZUFZDCUGZDFUHZKISZUNZUAUBCDFEFUHZHILMOYEUBTZDRZ - UFZCHIYFYGKJUIZYGLMYIHXSXTYBYDYHUJZUKZYEYFCRZYHYEHUORZECUGZYMYEXSYNXSXTYB - YDULHUMZUPZEBTZATZKJUIZUQZADURZBCUSZCQUUBBCUTVAZCEFHLOVBVCZVDYIHVPRZYGCRZ - KCRZYJCRZYLYIDCYGYAYBYDYHVFYEYHVEZVGZYIXTUUHXSXTYBYDYHVHCGHKLPVIZUPZCHJYG - KLNVJVKZUUKYIYNYJERZYFYJISZYIXSYNYKYPUPYIYJUUCEYIUUIYJYTUQZADURZYJUUCRUUN - YIYHYJYJUQUURUUJYIYJVLAYGDYTYJYJYSYGKJVMVNVOUUBUURBYJCYRYJUQUUAUUQADYRYJY - TVQVRVSVTQWAYNYOUUOUUPUUDCEFHIYJLMOWBWCVOYIUUFUUGUUHYJYGISYLUUKUUMCHIJYGK - LMNWDVKWFYEUATZCRZUUSYGISZUBDWEZUNZUUSYFISZUUSUCTZISZUCEWEZUVCUVFUCEUVEER - UVECRZUVEUDTZKJUIZUQZUDDURZUFUVCUVFUUBUVLBUVECEBUCWGZUUBUVEYTUQZADURUVLUV - MUUAUVNADYRUVEYTVQVRUVNUVKAUDDAUDWGYTUVJUVEYSUVIKJVMWHWIWJQWKUVCUVHUVLUVF - UVCUVHUFZUVKUVFUDDUVOUVIDRZUUSUVJISZUVKUVFWQUVCUVHUVPUVQUVCUVHUVPUNZUUSUV - IISZUUSKISZUVQUVRUVPUVBUVSUVCUVHUVPWLZYEUUTUVBUVHUVPWMZUVAUVSUBUVIDYGUVIU - USIWNWOVOUVRCHIUUSYCKLMUVRHUVCUVHXSUVPXSXTYBYDUUTUVBWPZWRZUKZYEUUTUVBUVHU - VPWSZUVRYNYBYCCRUVRXSYNUWDYPUPZYAYBYDUUTUVBUVHUVPWTZCDFHLOVBVOUVRXTUUHUVC - UVHXTUVPXSXTYBYDUUTUVBXAWRUULUPZUVRUUSYCISZUVBUWBUVRYNUUTYBUWJUVBXBUWGUWF - UWHUBCDFHIUUSLMOXCVKXGYAYBYDUUTUVBUVHUVPXDWFUVRUUFUUTUVICRUUHUVSUVTUFUVQX - BUWEUWFUVRDCUVIUWHUWAVGUWICHIJUUSUVIKLMNXEXFXHXIUVKUVFUVQUVEUVJUUSIWNXJXK - XLXMXNXQUVCYNUUTUVDUVGXBZUVCXSYNUWCYPUPYEUUTUVBXOYNUUTYOUWKUUDUCCEFHIUUSL - MOXCXPVOXGYQYAYBYDXOUUEXR $. + lattrd eqeq2d cbvrexvw syl6bb elrab2 wi simp3 simp13 breq2 rspcva simp11l + weq 3ad2ant1 simp12 simp112 simp11r wb clatleglb mpbird latlem12 syl13anc + simp113 mpbi2and 3expia biimprcd syl6 rexlimdv syl5bi simp2 mp3an3 isglbd + expimpd ralrimiv ) HUERZKGRZUFZDCUGZDFUHZKISZUNZUAUBCDFEFUHZHILMOYEUBTZDR + ZUFZCHIYFYGKJUIZYGLMYIHXSXTYBYDYHUJZUKZYEYFCRZYHYEHUORZECUGZYMYEXSYNXSXTY + BYDULHUMZUPZEBTZATZKJUIZUQZADURZBCUSZCQUUBBCUTVAZCEFHLOVBVCZVDYIHVPRZYGCR + ZKCRZYJCRZYLYIDCYGYAYBYDYHVFYEYHVEZVGZYIXTUUHXSXTYBYDYHVHCGHKLPVIZUPZCHJY + GKLNVJVKZUUKYIYNYJERZYFYJISZYIXSYNYKYPUPYIYJUUCEYIUUIYJYTUQZADURZYJUUCRUU + NYIYHYJYJUQUURUUJYIYJVLAYGDYTYJYJYSYGKJVMVNVOUUBUURBYJCYRYJUQUUAUUQADYRYJ + YTVQVRVSVTQWAYNYOUUOUUPUUDCEFHIYJLMOWBWCVOYIUUFUUGUUHYJYGISYLUUKUUMCHIJYG + KLMNWDVKWFYEUATZCRZUUSYGISZUBDWEZUNZUUSYFISZUUSUCTZISZUCEWEZUVCUVFUCEUVEE + RUVECRZUVEUDTZKJUIZUQZUDDURZUFUVCUVFUUBUVLBUVECEBUCWQZUUBUVEYTUQZADURUVLU + VMUUAUVNADYRUVEYTVQVRUVNUVKAUDDAUDWQYTUVJUVEYSUVIKJVMWGWHWIQWJUVCUVHUVLUV + FUVCUVHUFZUVKUVFUDDUVOUVIDRZUUSUVJISZUVKUVFWKUVCUVHUVPUVQUVCUVHUVPUNZUUSU + VIISZUUSKISZUVQUVRUVPUVBUVSUVCUVHUVPWLZYEUUTUVBUVHUVPWMZUVAUVSUBUVIDYGUVI + UUSIWNWOVOUVRCHIUUSYCKLMUVRHUVCUVHXSUVPXSXTYBYDUUTUVBWPZWRZUKZYEUUTUVBUVH + UVPWSZUVRYNYBYCCRUVRXSYNUWDYPUPZYAYBYDUUTUVBUVHUVPWTZCDFHLOVBVOUVRXTUUHUV + CUVHXTUVPXSXTYBYDUUTUVBXAWRUULUPZUVRUUSYCISZUVBUWBUVRYNUUTYBUWJUVBXBUWGUW + FUWHUBCDFHIUUSLMOXCVKXDYAYBYDUUTUVBUVHUVPXGWFUVRUUFUUTUVICRUUHUVSUVTUFUVQ + XBUWEUWFUVRDCUVIUWHUWAVGUWICHIJUUSUVIKLMNXEXFXHXIUVKUVFUVQUVEUVJUUSIWNXJX + KXLXQXMXRUVCYNUUTUVDUVGXBZUVCXSYNUWCYPUPYEUUTUVBXNYNUUTYOUWKUUDUCCEFHIUUS + LMOXCXOVOXDYQYAYBYDXNUUEXP $. $d u v .<_ $. $d v B $. $d u v G $. $d u v H $. $d u v K $. dihglblem.i $e |- J = ( ( DIsoB ` K ) ` W ) $. @@ -619024,24 +619024,24 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane). ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) ) $= ( vy vz vu vl wcel cfv wceq cv co csn wrex crio cmpt cdif wo lcfl6 wa weq wreu wi wral chlt ad2antrr simplrl simplrr simprl eqeq1 rexbidv riotabidv - oveq1 oveq2d eqeq2d cbvrexv syl6bb cbvriotav syl6eq cbvmptv simprr eqtr3d - eqid lcfl7lem ex ralrimivva a1d ancld sneq fveq2d rexeqbidv mpteq2dv reu4 - oveq2 syl6ibr reurex impbid1 orbi2d bitrd ) ANEUTNQVASVBZNDSDVCZCVCZLVCZB - VCZIVDZFVDZVBZCXPVEZRVAZVFZLGVGZVHZVBZBSUAVEVIZVFZVJXLYEBYFVNZVJABCDEFGHI - JKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOVKAYGYHXLAYGYHAYGYGYENDSXMXNXOUP - VCZIVDZFVDZVBZCYIVEZRVAZVFZLGVGZVHZVBZVLZBUPVMZVOZUPYFVPBYFVPZVLYHAYGUUBA - UUBYGAUUABUPYFYFAXPYFUTZYIYFUTZVLZVLZYSYTUUFYSVLZUQURFGHIJUSMURSURVCZUQVC - ZUSVCZXPIVDZFVDZVBZUQYAVFZUSGVGZVHZOURSUUHUUIUUJYIIVDZFVDZVBZUQYNVFZUSGVG - ZVHZPQRSTXPYIUAUBUCUDUEUFUGUHUIUJUKULAPVQUTTOUTVLUUEYSUNVRUUPWOUVBWOAUUCU - UDYSVSAUUCUUDYSVTUUGNUUPUVBUUGNYDUUPUUFYEYRWADURSYCUUODURVMZYCUUHXRVBZCYA - VFZLGVGUUOUVCYBUVELGUVCXSUVDCYAXMUUHXRWBWCWDUVEUUNLUSGLUSVMZUVEUUHXNUUKFV - DZVBZCYAVFUUNUVFUVDUVHCYAUVFXRUVGUUHUVFXQUUKXNFXOUUJXPIWEWFWGWCUVHUUMCUQY - ACUQVMZUVGUULUUHXNUUIUUKFWEWGWHWIWJWKWLWKUUGNYQUVBUUFYEYRWMDURSYPUVAUVCYP - UUHYKVBZCYNVFZLGVGUVAUVCYOUVKLGUVCYLUVJCYNXMUUHYKWBWCWDUVKUUTLUSGUVFUVKUU - HXNUUQFVDZVBZCYNVFUUTUVFUVJUVMCYNUVFYKUVLUUHUVFYJUUQXNFXOUUJYIIWEWFWGWCUV - MUUSCUQYNUVIUVLUURUUHXNUUIUUQFWEWGWHWIWJWKWLWKWNWPWQWRWSWTYEYRBUPYFYTYDYQ - NYTDSYCYPYTYBYOLGYTXSYLCYAYNYTXTYMRXPYIXAXBYTXRYKXMYTXQYJXNFXPYIXOIXFWFWG - XCWDXDWGXEXGYEBYFXHXIXJXK $. + eqid oveq1 oveq2d eqeq2d cbvrexvw syl6bb cbvriotavw syl6eq cbvmptv simprr + eqtr3d lcfl7lem ralrimivva a1d ancld sneq fveq2d oveq2 rexeqbidv mpteq2dv + ex reu4 syl6ibr reurex impbid1 orbi2d bitrd ) ANEUTNQVASVBZNDSDVCZCVCZLVC + ZBVCZIVDZFVDZVBZCXPVEZRVAZVFZLGVGZVHZVBZBSUAVEVIZVFZVJXLYEBYFVNZVJABCDEFG + HIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOVKAYGYHXLAYGYHAYGYGYENDSXMXNXO + UPVCZIVDZFVDZVBZCYIVEZRVAZVFZLGVGZVHZVBZVLZBUPVMZVOZUPYFVPBYFVPZVLYHAYGUU + BAUUBYGAUUABUPYFYFAXPYFUTZYIYFUTZVLZVLZYSYTUUFYSVLZUQURFGHIJUSMURSURVCZUQ + VCZUSVCZXPIVDZFVDZVBZUQYAVFZUSGVGZVHZOURSUUHUUIUUJYIIVDZFVDZVBZUQYNVFZUSG + VGZVHZPQRSTXPYIUAUBUCUDUEUFUGUHUIUJUKULAPVQUTTOUTVLUUEYSUNVRUUPWEUVBWEAUU + CUUDYSVSAUUCUUDYSVTUUGNUUPUVBUUGNYDUUPUUFYEYRWADURSYCUUODURVMZYCUUHXRVBZC + YAVFZLGVGUUOUVCYBUVELGUVCXSUVDCYAXMUUHXRWBWCWDUVEUUNLUSGLUSVMZUVEUUHXNUUK + FVDZVBZCYAVFUUNUVFUVDUVHCYAUVFXRUVGUUHUVFXQUUKXNFXOUUJXPIWFWGWHWCUVHUUMCU + QYACUQVMZUVGUULUUHXNUUIUUKFWFWHWIWJWKWLWMWLUUGNYQUVBUUFYEYRWNDURSYPUVAUVC + YPUUHYKVBZCYNVFZLGVGUVAUVCYOUVKLGUVCYLUVJCYNXMUUHYKWBWCWDUVKUUTLUSGUVFUVK + UUHXNUUQFVDZVBZCYNVFUUTUVFUVJUVMCYNUVFYKUVLUUHUVFYJUUQXNFXOUUJYIIWFWGWHWC + UVMUUSCUQYNUVIUVLUURUUHXNUUIUUQFWFWHWIWJWKWLWMWLWOWPXEWQWRWSYEYRBUPYFYTYD + YQNYTDSYCYPYTYBYOLGYTXSYLCYAYNYTXTYMRXPYIWTXAYTXRYKXMYTXQYJXNFXPYIXOIXBWG + WHXCWDXDWHXFXGYEBYFXHXIXJXK $. $} ${ @@ -620296,17 +620296,17 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane). ` V ` to nonzero functionals with closed kernels ` C ` . (Contributed by NM, 22-Feb-2015.) $) lcf1o $p |- ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) ) $= - ( vy vz vu vl csn cdif cv co wceq cfv wrex crio cmpt weq eqeq2d cbvrexv - oveq1 oveq2d rexbidv syl5bb cbvriotav eqeq1 riotabidv syl5eq sneq oveq2 - cbvmptv fveq2d rexeqbidv mpteq2dv eqtri lcfrlem9 ) AUTVAVBEFGHIJKLMVCOP - QRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOUPUQQBUAUCVDVEZDUADVFZCVFZNVFZBVFZKVG - ZGVGZVHZCWPVDZTVIZVJZNIVKZVLZVLUTWLVBUAVBVFZVAVFZVCVFZUTVFZKVGZGVGZVHZV - AXHVDZTVIZVJZVCIVKZVLZVLURBUTWLXDXPBUTVMZXDVBUAXEXFXGWPKVGZGVGZVHZVAXAV - JZVCIVKZVLXPDVBUAXCYBDVBVMZXCWMXSVHZVAXAVJZVCIVKYBXBYENVCIXBWMXFWQGVGZV - HZVAXAVJNVCVMZYEWSYGCVAXACVAVMWRYFWMWNXFWQGVPVNVOYHYGYDVAXAYHYFXSWMYHWQ - XRXFGWOXGWPKVPVQVNVRVSVTYCYEYAVCIYCYDXTVAXAWMXEXSWAVRWBWCWFXQVBUAYBXOXQ - YAXNVCIXQXTXKVAXAXMXQWTXLTWPXHWDWGXQXSXJXEXQXRXIXFGWPXHXGKWEVQVNWHWBWIW - CWFWJUSWK $. + ( vy vz vu vl csn cdif cv co wceq cfv wrex crio cmpt weq oveq1 cbvrexvw + eqeq2d oveq2d rexbidv syl5bb cbvriotavw riotabidv syl5eq cbvmptv fveq2d + eqeq1 sneq oveq2 rexeqbidv mpteq2dv eqtri lcfrlem9 ) AUTVAVBEFGHIJKLMVC + OPQRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOUPUQQBUAUCVDVEZDUADVFZCVFZNVFZBVFZK + VGZGVGZVHZCWPVDZTVIZVJZNIVKZVLZVLUTWLVBUAVBVFZVAVFZVCVFZUTVFZKVGZGVGZVH + ZVAXHVDZTVIZVJZVCIVKZVLZVLURBUTWLXDXPBUTVMZXDVBUAXEXFXGWPKVGZGVGZVHZVAX + AVJZVCIVKZVLXPDVBUAXCYBDVBVMZXCWMXSVHZVAXAVJZVCIVKYBXBYENVCIXBWMXFWQGVG + ZVHZVAXAVJNVCVMZYEWSYGCVAXACVAVMWRYFWMWNXFWQGVNVPVOYHYGYDVAXAYHYFXSWMYH + WQXRXFGWOXGWPKVNVQVPVRVSVTYCYEYAVCIYCYDXTVAXAWMXEXSWEVRWAWBWCXQVBUAYBXO + XQYAXNVCIXQXTXKVAXAXMXQWTXLTWPXHWFWDXQXSXJXEXQXRXIXFGWPXHXGKWGVQVPWHWAW + IWBWCWJUSWK $. $} ${ @@ -620864,12 +620864,12 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane). 11-Mar-2015.) $) lcfrlem39 $p |- ( ph -> ( X .+ Y ) e. E ) $= ( vx vw vv vk vj csca cfv cbs cvsca csn cdif cv wceq wrex crio cmpt - co eqid weq oveq1 oveq2d eqeq2d rexbidv cbvriotav mpteq2i lcfrlem38 - ) AVFVGVHBCDEFGVKVLZVMVLZWLGVNVLZGHIVIJKLMNVFGVMVLZUBVOVPZVHWOVHVQZ - VGVQZVJVQZVFVQZWNWBZEWBZVRZVGWTVORVLZVSZVJWMVTZWAZWAOPQRWOSTUAUBUCU - DUEUFUGUHUIUJUKULUMUNUOUPUQURUSUTVAVBVCVDVEWOWCWNWCWLWCWMWCVFWPXGVH - WOWQWRVIVQZWTWNWBZEWBZVRZVGXDVSZVIWMVTZWAVHWOXFXMXEXLVJVIWMVJVIWDZX - CXKVGXDXNXBXJWQXNXAXIWREWSXHWTWNWEWFWGWHWIWJWJWK $. + eqid weq oveq1 oveq2d eqeq2d rexbidv cbvriotavw mpteq2i lcfrlem38 + co ) AVFVGVHBCDEFGVKVLZVMVLZWLGVNVLZGHIVIJKLMNVFGVMVLZUBVOVPZVHWOVH + VQZVGVQZVJVQZVFVQZWNWKZEWKZVRZVGWTVORVLZVSZVJWMVTZWAZWAOPQRWOSTUAUB + UCUDUEUFUGUHUIUJUKULUMUNUOUPUQURUSUTVAVBVCVDVEWOWBWNWBWLWBWMWBVFWPX + GVHWOWQWRVIVQZWTWNWKZEWKZVRZVGXDVSZVIWMVTZWAVHWOXFXMXEXLVJVIWMVJVIW + CZXCXKVGXDXNXBXJWQXNXAXIWREWSXHWTWNWDWEWFWGWHWIWIWJ $. $} $d i E $. $d g i N $. $d i ._|_ $. $d i .+ $. $d i U $. $d i X $. @@ -626034,15 +626034,15 @@ first fundamental theorem of projective geometry (see ~ mapdpg ). @) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) ) ) $= ( c2nd cfv wceq csn c1st fveq2d cvv cv co wa crio cmpt fveq2 eqeq1d sneqd cif 2fveq3 oveq12d oveq1d eqeq12d anbi12d riotabidv ifbieq2d cbvmptv sneq - weq eqeq2d oveq2 cbvriotav ifeq2 ax-mp mpteq2i 3eqtri ) IAUAAUBZOPZMQZDVI - RZLPZJPZFUBZRZHPZQZVHSPZSPZVIKUCZRZLPZJPZVROPZVNEUCZRZHPZQZUDZFCUEZUJZUFB - UABUBZOPZMQZDWMRZLPZJPZVPQZWLSPZSPZWMKUCZRZLPZJPZWSOPZVNEUCZRZHPZQZUDZFCU - EZUJZUFBUAWNDWQGUBZRZHPZQZXDXEXMEUCZRZHPZQZUDZGCUEZUJZUFNABUAWKXLABUTZVJW - NWJXKDYDVIWMMVHWLOUGZUHYDWIXJFCYDVQWRWHXIYDVMWQVPYDVLWPJYDVKWOLYDVIWMYEUI - TTUHYDWCXDWGXHYDWBXCJYDWAXBLYDVTXAYDVSWTVIWMKVHWLSSUKYEULUITTYDWFXGHYDWEX - FYDWDXEVNEVHWLOSUKUMUITUNUOUPUQURBUAXLYCXKYBQXLYCQXJYAFGCFGUTZWRXPXIXTYFV - PXOWQYFVOXNHVNXMUSTVAYFXHXSXDYFXGXRHYFXFXQVNXMXEEVBUITVAUOVCWNXKYBDVDVEVF - VG $. + weq eqeq2d oveq2 cbvriotavw ifeq2 ax-mp mpteq2i 3eqtri ) IAUAAUBZOPZMQZDV + IRZLPZJPZFUBZRZHPZQZVHSPZSPZVIKUCZRZLPZJPZVROPZVNEUCZRZHPZQZUDZFCUEZUJZUF + BUABUBZOPZMQZDWMRZLPZJPZVPQZWLSPZSPZWMKUCZRZLPZJPZWSOPZVNEUCZRZHPZQZUDZFC + UEZUJZUFBUAWNDWQGUBZRZHPZQZXDXEXMEUCZRZHPZQZUDZGCUEZUJZUFNABUAWKXLABUTZVJ + WNWJXKDYDVIWMMVHWLOUGZUHYDWIXJFCYDVQWRWHXIYDVMWQVPYDVLWPJYDVKWOLYDVIWMYEU + ITTUHYDWCXDWGXHYDWBXCJYDWAXBLYDVTXAYDVSWTVIWMKVHWLSSUKYEULUITTYDWFXGHYDWE + XFYDWDXEVNEVHWLOSUKUMUITUNUOUPUQURBUAXLYCXKYBQXLYCQXJYAFGCFGUTZWRXPXIXTYF + VPXOWQYFVOXNHVNXMUSTVAYFXHXSXDYFXGXRHYFXFXQVNXMXEEVBUITVAUOVCWNXKYBDVDVEV + FVG $. $} ${ @@ -631361,8 +631361,8 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove (Contributed by Steven Nguyen, 7-Jan-2023.) $) resubf $p |- -R : ( RR X. RR ) --> RR $= ( vy vz vx cv caddc co wceq cr crio wcel wral cresub wf resubval rersubcl - cxp wa eqeltrrd rgen2a df-resub fmpo mpbi ) ADZBDEFCDZGBHIZHJZAHKCHKHHPHL - MUFCAHUDHJUCHJQUDUCLFUEHBUDUCNUDUCORSCAHHUEHLCABTUAUB $. + cxp wa eqeltrrd rgen2 df-resub fmpo mpbi ) ADZBDEFCDZGBHIZHJZAHKCHKHHPHLM + UFCAHHUDHJUCHJQUDUCLFUEHBUDUCNUDUCORSCAHHUEHLCABTUAUB $. $} $( Addition and subtraction of equals. Compare ~ pncan2 . (Contributed by @@ -632258,140 +632258,140 @@ standardize vectors to a length (norm) of one, but such definitions require ltnsymd simp-5l nncn 2cnd 2ne0 divcan2d cdvds nndivdvds mvrraddd mvlraddd nnnn0 subcld pncan3d addcld negidd addassd addid2d 3eqtr3d pncand negnegd eqtr3d 3rspcedvd rexlimdva2 reximia 3imtr3i con4i wi c0 0nnn disjsn mpbir - cin disj3 mpbi nnssz ssdif eqsstri ssel ss2ralv imim12d ralimdv2 cbvral3v - neeq2d sylib ralimi impbii ) AUAZDUAZHIZBUAZUXBHIZJIZCUAZUXBHIZUBZCKUDZBK - UDZAKUDZDUCUEUFZUDZEUAZUXBHIZFUAZUXBHIZJIZGUAZUXBHIZUBZGLMUGZUHZUDZFUYDUD - ZEUYDUDZDUXMUDZUYHUXNUXSUYANZGUYDUIZFUYDUIZEUYDUIZDUXMUIZUXFUXHNZCKUIZBKU - IZAKUIZDUXMUIZUYHOZUXNOZUYLUYQDUXMUXBUXMPZUYKUYQEUYDVUAUXOUYDPZQZUYJUYQFU - YDVUCUXQUYDPZQZUYIUYQGUYDVUEUXTUYDPZQZUYIQZUYNUXBUJUKIZKPZUXOULUFZMUXOUMU - NZMUXQUMUNZUXOMUXTUMUNZUXQUOZUXOUPZUPZVUMVUNUXOUOZUXQUPZVURUPZUPZUPZUXBHI - ZUXEJIZUXHNZVVCVUJUXQULUFZVULVUMUXQVUNUXTUXTUOZUPZUPZVUMVVHVUOUPZUPZUPZUX - BHIZJIZUXHNZVVNVUJUXTULUFZVULVUMUXTVUNUXOVUOUPZUPZVUMVUNUXQVURUPZVVGUPZUP - ZUPZUXBHIZNZABCVVBVVLVWBKVUHVUJVUKVVAKVUHVUBUXOLPZUXOMUBZQVUKKPVUAVUBVUDV - UFUYIUQVUBVWEVWFUXOLUYCUSZUXOLMURZUTUXOVAVHVUHVULVUQVUTKVUHVULQZVUMUXOVUP - KVWIVUMQZVWEVULUXOKPZVWJUXOLUYCVUAVUBVUDVUFUYIVULVUMVBVCVUHVULVUMVDUXOVIZ - VEVWIVUMOZQZVUNVUOUXOKVWNVUNQZUXQVUDUXQMUBZVUCVUFUYIVULVWMVUNUXQLMURZVFVW - IVWMVUNVDVUDUXQLPZVUCVUFUYIVULVWMVUNUXQLUYCUSZVFVGVWNVUNOZQZVWEVULVWKVXAU - XOLUYCVUAVUBVUDVUFUYIVULVWMVWTVJVCVUHVULVWMVWTVKVWLVEVLVLVUHVULOZQZVUMVUS - VURKVXCVUMQZVUNVURUXQKVXDVUNQZUXOVUBVWFVUAVUDVUFUYIVXBVUMVUNVWHVMVUHVXBVU - MVUNVKVUBVWEVUAVUDVUFUYIVXBVUMVUNVWGVMVGVXDVWTQZVWRVUMUXQKPZVXFUXQLUYCVUC - VUDVUFUYIVXBVUMVWTVBVCVXCVUMVWTVDUXQVIZVEVLVXCVWMQZUXOVUBVWFVUAVUDVUFUYIV - XBVWMVWHVFVUHVXBVWMVDVUBVWEVUAVUDVUFUYIVXBVWMVWGVFVGVLVLVNVUHVUJVVFVVKKVU - HVUDVWRVWPQVVFKPVUCVUDVUFUYIVKVUDVWRVWPVWSVWQUTUXQVAVHVUHVULVVIVVJKVWIVUM - UXQVVHKVWJVWRVUMVXGVWJUXQLUYCVUCVUDVUFUYIVULVUMVOVCVWIVUMVRVXHVEVWNVUNUXT - VVGKVWOUXTLPZVUNUXTKPZVWOUXTLUYCVUEVUFUYIVULVWMVUNVOVCVWNVUNVRUXTVIZVEVXA - UXTVUFUXTMUBZVUEUYIVULVWMVWTUXTLMURZVPVWNVWTVRVUFVXJVUEUYIVULVWMVWTUXTLUY - CUSZVPVGVLVLVXCVUMVVHVUOKVXDVUNUXTVVGKVXEVXJVUNVXKVXEUXTLUYCVUEVUFUYIVXBV - UMVUNVOVCVXDVUNVRVXLVEVXFUXTVUFVXMVUEUYIVXBVUMVWTVXNVPVXDVWTVRVUFVXJVUEUY - IVXBVUMVWTVXOVPVGVLVXIUXQVUDVWPVUCVUFUYIVXBVWMVWQVPVXCVWMVRVUDVWRVUCVUFUY - IVXBVWMVWSVPVGVLVLVNVUHVUJVVPVWAKVUHVUJQZVXJVXMVVPKPVXPUXTLUYCVUEVUFUYIVU - JVKZVCZVXPVUFVXMVXQVXNVSUXTVAVQVUHVUJOZQZVULVVRVVTKVXTVULQZVUMUXTVVQKVYAV - UMQZVXJVUNVXKVYBUXTLUYCVUEVUFUYIVXSVULVUMVOVCZVYBVUNMUYAUMUNZVYBMUXSUYAUM - VYBUXPUXRVYBUXOUXBVYBUXOVYBUXOLUYCVUAVUBVUDVUFUYIVXSVULVUMVJVCVTZVYBUXBVU - AUXBKPZVUBVUDVUFUYIVXSVULVUMUXBWAZWBZWCZWDVYBUXQUXBVYBUXQVYBUXQLUYCVUCVUD - VUFUYIVXSVULVUMVBVCVTZVYIWDVYBVULMUXPUMUNZVXTVULVUMVDVYBUXBUXOVYEVYHVUHVX - SVULVUMVKZWEWFVYBVUMMUXRUMUNZVYAVUMVRVYBUXBUXQVYJVYHVYLWEWFUUAVUGUYIVXSVU - LVUMUQZUUBVYBUXBUXTVYBUXTVYCVTVYHVYLWEWHVXLVEVYAVWMQZVUNUXOVUOKVYOVUNQZVW - EVULVWKVYPUXOLUYCVUAVUBVUDVUFUYIVXSVULVWMVUNWGZVCVXTVULVWMVUNVKVWLVEVYOVW - TQZUXQVYRVUDVWPVUCVUDVUFUYIVXSVULVWMVWTVJZVWQVSVYAVWMVWTVDVYRUXQLUYCVYSVC - VGVLVLVXTVXBQZVUMVVSVVGKVYTVUMQZVUNUXQVURKWUAVUNQZVWRVUMVXGWUBUXQLUYCVUCV - UDVUFUYIVXSVXBVUMVUNVJZVCVYTVUMVUNVDVXHVEWUAVWTQZUXOWUDVUBVWFVUAVUBVUDVUF - UYIVXSVXBVUMVWTWGZVWHVSVXTVXBVUMVWTVKWUDUXOLUYCWUEVCVGVLVYTVWMQZUXTWUFVUF - VXMVUEVUFUYIVXSVXBVWMVOZVXNVSWUFVUNVYDWUFVYDMUXSUMUNWUFUXSMWUFUXPUXRWUFUX - OUXBWUFUXOWUFUXOLUYCVUAVUBVUDVUFUYIVXSVXBVWMVJZVCVTZWUFUXBVUAVYFVUBVUDVUF - UYIVXSVXBVWMVYGWBZWCZWDZWUFUXQUXBWUFUXQWUFUXQLUYCVUCVUDVUFUYIVXSVXBVWMVBZ - VCVTZWUKWDZUUCWUFUUDZWUFUXSMMJIMUMWUFUXPUXRMMWULWUOWUPWUPWUFUXPMUMUNUXPMN - ZVYKWIOZWUFWUQOVYKOWURWUFWUQUXOMNZWUFVUBWUSOWUHVUBUXOMVWHWJVSWUFUXOWKPZVY - FWUQWUSWLWUFVUBVWEWUTWUHVWGUXOWMZVHZWUJUXOUXBUUEVQWNWUFVULVYKVXTVXBVWMVDW - UFUXBUXOWUIWUJVUHVXSVXBVWMVKZWEWOWUQVYKWPVEWUFUXPMWULWUPWQWHWUFUXRMUMUNUX - RMNZVYMWIOZWUFWVDOVYMOWVEWUFUXRMWUFUXQUXBWUFVUDVWRUXQWKPZWUMVWSUXQWMZVHZW - UFVUDVWPWUMVWQVSZVUAUXBLPVUBVUDVUFUYIVXSVXBVWMUCUXBUUFWBZUUGWJWUFVUMVYMVY - TVWMVRWUFUXBUXQWUNWUJWVCWEWOWVDVYMWPVEWUFUXRMWUOWUPWQWHUUHUUIUUJUUOWUFUYA - UXSMUMWUFUXSUYAVUGUYIVXSVXBVWMUQZWRUUKWNWUFUXBUXTWUFUXTWUFUXTLUYCWUGVCZVT - WUJWVCWEWNWVLVGVLVLVLUXAVVBNZUYNVVEWLVUHWVMUXFVVDUXHWVMUXCVVCUXEJUXAVVBUX - BHXARWSSUXDVVLNZVVEVVOWLVUHWVNVVDVVNUXHWVNUXEVVMVVCJUXDVVLUXBHXAWTWSSUXGV - WBNZVVOVWDWLVUHWVOUXHVWCVVNUXGVWBUXBHXAUULSVUHVUJVWDVXPVUKUXBHIZVVFUXBHIZ - JIZVVPUXBHIZVVNVWCVXPUXSUYAWVRWVSVUGUYIVUJVDVXPWVPUXPWVQUXRJVXPVUKUJVUIUU - MIZHIZUXOWVTHIZWVPUXPVXPVUKUJHIZVUIHIUXOUJHIZVUIHIWWAWWBVXPWWCWWDVUIHVXPU - XOXBPWWCWWDNVXPUXOVXPUXOLUYCVUAVUBVUDVUFUYIVUJVOZVCVTUXOXCVSRVXPVUKUJVUIV - XPVUKVXPUXOVXPVUBVWEWUTWWEVWGWVAVHZXDXEVXPVUIVUHVUJVRWCZUJXFPVXPUUNXGZXHV - XPUXOUJVUIWWFWWGWWHXHTVXPUXBWVTVUKHVXPWVTUXBVXPUXBUJVXPVUAVYFUXBWKPVUAVUB - VUDVUFUYIVUJUUPVYGUXBUUQVHVXPUURUJMUBVXPUUSXGUUTWRZWTVXPUXBWVTUXOHWWIWTTV - XPVVFWVTHIZUXQWVTHIZWVQUXRVXPVVFUJHIZVUIHIUXQUJHIZVUIHIWWJWWKVXPWWLWWMVUI - HVXPUXQXBPWWLWWMNVXPUXQVXPUXQLUYCVUCVUDVUFUYIVUJUQZVCVTUXQXCVSRVXPVVFUJVU - IVXPVVFVXPUXQVXPVUDVWRWVFWWNVWSWVGVHZXDXEWWGWWHXHVXPUXQUJVUIWWOWWGWWHXHTV - XPUXBWVTVVFHWWIWTVXPUXBWVTUXQHWWIWTTXIVXPVVPWVTHIZUXTWVTHIZWVSUYAVXPVVPUJ - HIZVUIHIUXTUJHIZVUIHIWWPWWQVXPWWRWWSVUIHVXPUXTXBPWWRWWSNVXPUXTVXRVTUXTXCV - SRVXPVVPUJVUIVXPVVPVXPUXTVXPVUFVXJUXTWKPZVXQVXOUXTWMZVHZXDXEWWGWWHXHVXPUX - TUJVUIWXBWWGWWHXHTVXPUXBWVTVVPHWWIWTVXPUXBWVTUXTHWWIWTTTVUJVVNWVRNVUHVUJV - VCWVPVVMWVQJVUJVVBVUKUXBHVUJVUKVVAXJRVUJVVLVVFUXBHVUJVVFVVKXJRXISVUJVWCWV - SNVUHVUJVWBVVPUXBHVUJVVPVWAXJRSTVXTVVAUXBHIZVVKUXBHIZJIZVWAUXBHIZVVNVWCVX - TVULWXEWXFNVYAVUQUXBHIZVVIUXBHIZJIZVVRUXBHIZWXEWXFVYAVUMWXIWXJNVYBUXSUYAW - XIWXJVYNVUMWXIUXSNVYAVUMWXGUXPWXHUXRJVUMVUQUXOUXBHVUMUXOVUPXJRVUMVVIUXQUX - BHVUMUXQVVHXJRXISVUMWXJUYANVYAVUMVVRUXTUXBHVUMUXTVVQXJRSTVYOVUPUXBHIZVVHU - XBHIZJIZVVQUXBHIZWXIWXJVYOVUNWXMWXNNVYPVUOUXBHIZUYAJIZUXPWXMWXNVYPWXPUXRU - OZUYAJIZUYAUXRXKIZUXPVYPWXOWXQUYAJVYPWVFVYFUJUXBUVAUNZOZWXOWXQNZVYPVUDVWR - WVFVUCVUDVUFUYIVXSVULVWMVUNVJVWSWVGVHZVYPVUAVYFVUAVUBVUDVUFUYIVXSVULVWMVU - NXLZVYGVSZVYPWXTVUJVUHVXSVULVWMVUNUQVYPVYFUJKPZWXTVUJWLZWYEXMUXBUJUVBZXNW - NUXQUXBXOZXPRVYPWXRUYAWXQJIZWXSVYPWXQUYAVYPUXRVYPUXQUXBWYCVYPVUAVYFUXBXFP - ZWYDVYGUXBUVEZVHZXQZXRVYPUXTUXBVYPVUFVXJWWTVUEVUFUYIVXSVULVWMVUNVBVXOWXAV - HWYMXQZXSVYPUYAUXRWYOWYNXTYCVYPUYAUXPUXRVYPUXOUXBVYPVUBVWEWUTVYQVWGWVAVHW - YMXQWYNVYPUXSUYAVUGUYIVXSVULVWMVUNVOWRUVCYAVUNWXMWXPNVYOVUNWXKWXOWXLUYAJV - UNVUPVUOUXBHVUNVUOUXOXJRVUNVVHUXTUXBHVUNUXTVVGXJRZXISVUNWXNUXPNVYOVUNVVQU - XOUXBHVUNUXOVUOXJRSTVYRUXPVVGUXBHIZJIZWXOWXMWXNVYRUXPUYAUOZJIZWXQWYRWXOVY - RWYTUXPUYAXKIZWXQVYRUXPUYAVYRUXOUXBVYRVUBVWEWUTVUAVUBVUDVUFUYIVXSVULVWMVW - TWGVWGWVAVHVYRUXBVUAVYFVUBVUDVUFUYIVXSVULVWMVWTVYGYDZWCZXQZVYRUXTUXBVYRVU - FVXJWWTVUEVUFUYIVXSVULVWMVWTVBVXOWXAVHZXUCXQZXTVYRUYAXUAWXQXUFVYRUXPUYAXU - DXUFUVFVYRUXRVYRUXQUXBVYRVUDVWRWVFVYSVWSWVGVHZXUCXQZXRVYRUXPWXSUYAXUAJIWY - JVYRUXPUXRUYAXUDXUHVUGUYIVXSVULVWMVWTVOUVDVYRUYAUXPXUFXUDUVGVYRUYAUXRXUFX - UHXTTYBYCVYRWYQWYSUXPJVYRWWTVYFWYAWYQWYSNZXUEXUBVYRWXTVUJVUHVXSVULVWMVWTU - QVYRVYFWYFWYGXUBXMWYHXNWNZUXTUXBXOZXPWTVYRWVFVYFWYAWYBXUGXUBXUJWYIXPTVWTW - XMWYRNVYOVWTWXKUXPWXLWYQJVWTVUPUXOUXBHVUNVUOUXOYERVWTVVHVVGUXBHVUNUXTVVGY - ERZXISVWTWXNWXONVYOVWTVVQVUOUXBHVUNUXOVUOYERSTYFVWMWXIWXMNVYAVWMWXGWXKWXH - WXLJVWMVUQVUPUXBHVUMUXOVUPYERVWMVVIVVHUXBHVUMUXQVVHYERXISVWMWXJWXNNVYAVWM - VVRVVQUXBHVUMUXTVVQYERSTYFVULWXEWXINVXTVULWXCWXGWXDWXHJVULVVAVUQUXBHVULVU - QVUTXJRVULVVKVVIUXBHVULVVIVVJXJRXISVULWXFWXJNVXTVULVWAVVRUXBHVULVVRVVTXJR - STVYTVUTUXBHIZVVJUXBHIZJIZVVTUXBHIZWXEWXFVYTVUMXUOXUPNWUAVUSUXBHIZWXLJIZV - VSUXBHIZXUOXUPWUAVUNXURXUSNWUBVURUXBHIZUYAJIZUXRXURXUSWUBXVAUXPUOZUYAJIZU - XRWUBXUTXVBUYAJWUBWUTVYFWYAXUTXVBNZWUBVUBVWEWUTVUAVUBVUDVUFUYIVXSVXBVUMVU - NWGVWGWVAVHZVUAVYFVUBVUDVUFUYIVXSVXBVUMVUNVYGYDZWUBWXTVUJVUHVXSVXBVUMVUNU - QWUBVYFWYFWYGXVFXMWYHXNWNUXOUXBXOZXPRWUBUXPXVCUXRWUBUXOUXBXVEWUBUXBXVFWCZ - XQZWUBXVBUYAWUBUXPXVIXRZWUBUXTUXBWUBVUFVXJWWTVUEVUFUYIVXSVXBVUMVUNVBVXOWX - AVHXVHXQZUVHWUBUXQUXBWUBVUDVWRWVFWUCVWSWVGVHXVHXQWUBUXPXVCJIZUYAUXSWUBUXP - XVBJIZUYAJIMUYAJIXVLUYAWUBXVMMUYAJWUBUXPXVIUVIRWUBUXPXVBUYAXVIXVJXVKUVJWU - BUYAXVKUVKUVLVUGUYIVXSVXBVUMVUNVOYGYBYCVUNXURXVANWUAVUNXUQXUTWXLUYAJVUNVU - SVURUXBHVUNVURUXQXJRWYPXISVUNXUSUXRNWUAVUNVVSUXQUXBHVUNUXQVURXJRSTWUDUXRW - YQJIZXUTXURXUSWUDWXRUOZXVBXVNXUTWUDWXRUXPWUDWXRWYJWXSUXPWUDWXQUYAWUDUXRWU - DUXQUXBWUDVUDVWRWVFVUCVUDVUFUYIVXSVXBVUMVWTVJVWSWVGVHWUDVUAVYFWYKVUAVUBVU - DVUFUYIVXSVXBVUMVWTXLZVYGWYLVHZXQZXRZWUDUXTUXBWUDVUFVXJWWTVUEVUFUYIVXSVXB - VUMVWTVBVXOWXAVHZXVQXQZXSWUDUYAUXRXWAXVRXTWUDUXSUXRXKIWXSUXPWUDUXSUYAUXRX - KVUGUYIVXSVXBVUMVWTVORWUDUXPUXRWUDUXOUXBWUDVUBVWEWUTWUEVWGWVAVHZXVQXQXVRU - VMUVOYAYHWUDUXRWYSJIWXQUOZWYSJIXVNXVOWUDUXRXWCWYSJWUDXWCUXRWUDUXRXVRUVNWR - RWUDWYQWYSUXRJWUDWWTVYFWYAXUIXVTWUDVUAVYFXVPVYGVSZWUDWXTVUJVUHVXSVXBVUMVW - TUQWUDVYFWYFWYGXWDXMWYHXNWNZXUKXPWTWUDWXQUYAXVSXWAYITWUDWUTVYFWYAXVDXWBXW - DXWEXVGXPTVWTXURXVNNWUAVWTXUQUXRWXLWYQJVWTVUSUXQUXBHVUNVURUXQYERXULXISVWT - XUSXUTNWUAVWTVVSVURUXBHVUNUXQVURYERSTYFVUMXUOXURNVYTVUMXUMXUQXUNWXLJVUMVU - TVUSUXBHVUMVUSVURXJRVUMVVJVVHUXBHVUMVVHVUOXJRXISVUMXUPXUSNVYTVUMVVTVVSUXB - HVUMVVSVVGXJRSTWUFXUTWXOJIZWYQXUOXUPWUFUXSUOZWYSXWFWYQWUFUXSUYAWVKYHWUFXW - FXVBWXQJIXWGWUFXUTXVBWXOWXQJWUFWUTVYFWYAXVDWVBWUJWUFWXTVUJWVCWUFVYFWYFWYG - WUJXMWYHXNWNZXVGXPWUFWVFVYFWYAWYBWVHWUJXWHWYIXPXIWUFUXPUXRWUFUXOUXBWVBWUF - VUBVWFWUHVWHVSWVJYMWUFUXQUXBWVHWVIWVJYMYIYGWUFWWTVYFWYAXUIWUFVUFVXJWWTWUG - VXOWXAVHWUJXWHXUKXPTVWMXUOXWFNVYTVWMXUMXUTXUNWXOJVWMVUTVURUXBHVUMVUSVURYE - RVWMVVJVUOUXBHVUMVVHVUOYERXISVWMXUPWYQNVYTVWMVVTVVGUXBHVUMVVSVVGYERSTYFVX - BWXEXUONVXTVXBWXCXUMWXDXUNJVXBVVAVUTUXBHVULVUQVUTYERVXBVVKVVJUXBHVULVVIVV - JYERXISVXBWXFXUPNVXTVXBVWAVVTUXBHVULVVRVVTYERSTYFVXSVVNWXENVUHVXSVVCWXCVV - MWXDJVXSVVBVVAUXBHVUJVUKVVAYERVXSVVLVVKUXBHVUJVVFVVKYERXISVXSVWCWXFNVUHVX - SVWBVWAUXBHVUJVVPVWAYERSTYFUVPUVQYJYJUVRUYMUYGOZDUXMUIUYSUYLXWIDUXMUYLUYF - OZEUYDUIXWIUYKXWJEUYDUYKUYEOZFUYDUIXWJUYJXWKFUYDUYJUYBOZGUYDUIXWKUYIXWLGU - YDXWLUYIUXSUYAYKYLYNUYBGUYDYOYPYNUYEFUYDYOYPYNUYFEUYDYOYPYNUYGDUXMYOYPUYR - UXLOZDUXMUIUYTUYQXWMDUXMUYQUXKOZAKUIXWMUYPXWNAKUYPUXJOZBKUIXWNUYOXWOBKUYO - UXIOZCKUIXWOUYNXWPCKXWPUYNUXFUXHYKYLYNUXICKYOYPYNUXJBKYOYPYNUXKAKYOYPYNUX - LDUXMYOYPUVSUVTUYGUXLDUXMUYGUYBGKUDFKUDZEKUDZUXLKUYDYQZUYGXWRUWAKKUYCUHZU - YDKUYCUWFUWBNZKXWTNXXAMKPOUWCKMUWDUWEKUYCUWGUWHKLYQXWTUYDYQUWIKLUYCUWJYRU - WKXWSUYFXWQEUYDKXWSVWKVUBUYFXWQKUYDUXOUWLUYBFGKUYDUWMUWNUWOYRUYBUXIUXCUXR - JIZUYAUBUXFUYAUBEFGABCKKKEAYSZUXSXXBUYAXXCUXPUXCUXRJUXOUXAUXBHXARYTFBYSZX - XBUXFUYAXXDUXRUXEUXCJUXQUXDUXBHXAWTYTGCYSUYAUXHUXFUXTUXGUXBHXAUWQUWPUWRUW - SUWT $. + cin disj3 mpbi nnssz ssdif eqsstri ssel ss2ralv ralimdv2 neeq2d cbvral3vw + imim12d sylib ralimi impbii ) AUAZDUAZHIZBUAZUXBHIZJIZCUAZUXBHIZUBZCKUDZB + KUDZAKUDZDUCUEUFZUDZEUAZUXBHIZFUAZUXBHIZJIZGUAZUXBHIZUBZGLMUGZUHZUDZFUYDU + DZEUYDUDZDUXMUDZUYHUXNUXSUYANZGUYDUIZFUYDUIZEUYDUIZDUXMUIZUXFUXHNZCKUIZBK + UIZAKUIZDUXMUIZUYHOZUXNOZUYLUYQDUXMUXBUXMPZUYKUYQEUYDVUAUXOUYDPZQZUYJUYQF + UYDVUCUXQUYDPZQZUYIUYQGUYDVUEUXTUYDPZQZUYIQZUYNUXBUJUKIZKPZUXOULUFZMUXOUM + UNZMUXQUMUNZUXOMUXTUMUNZUXQUOZUXOUPZUPZVUMVUNUXOUOZUXQUPZVURUPZUPZUPZUXBH + IZUXEJIZUXHNZVVCVUJUXQULUFZVULVUMUXQVUNUXTUXTUOZUPZUPZVUMVVHVUOUPZUPZUPZU + XBHIZJIZUXHNZVVNVUJUXTULUFZVULVUMUXTVUNUXOVUOUPZUPZVUMVUNUXQVURUPZVVGUPZU + PZUPZUXBHIZNZABCVVBVVLVWBKVUHVUJVUKVVAKVUHVUBUXOLPZUXOMUBZQVUKKPVUAVUBVUD + VUFUYIUQVUBVWEVWFUXOLUYCUSZUXOLMURZUTUXOVAVHVUHVULVUQVUTKVUHVULQZVUMUXOVU + PKVWIVUMQZVWEVULUXOKPZVWJUXOLUYCVUAVUBVUDVUFUYIVULVUMVBVCVUHVULVUMVDUXOVI + ZVEVWIVUMOZQZVUNVUOUXOKVWNVUNQZUXQVUDUXQMUBZVUCVUFUYIVULVWMVUNUXQLMURZVFV + WIVWMVUNVDVUDUXQLPZVUCVUFUYIVULVWMVUNUXQLUYCUSZVFVGVWNVUNOZQZVWEVULVWKVXA + UXOLUYCVUAVUBVUDVUFUYIVULVWMVWTVJVCVUHVULVWMVWTVKVWLVEVLVLVUHVULOZQZVUMVU + SVURKVXCVUMQZVUNVURUXQKVXDVUNQZUXOVUBVWFVUAVUDVUFUYIVXBVUMVUNVWHVMVUHVXBV + UMVUNVKVUBVWEVUAVUDVUFUYIVXBVUMVUNVWGVMVGVXDVWTQZVWRVUMUXQKPZVXFUXQLUYCVU + CVUDVUFUYIVXBVUMVWTVBVCVXCVUMVWTVDUXQVIZVEVLVXCVWMQZUXOVUBVWFVUAVUDVUFUYI + VXBVWMVWHVFVUHVXBVWMVDVUBVWEVUAVUDVUFUYIVXBVWMVWGVFVGVLVLVNVUHVUJVVFVVKKV + UHVUDVWRVWPQVVFKPVUCVUDVUFUYIVKVUDVWRVWPVWSVWQUTUXQVAVHVUHVULVVIVVJKVWIVU + MUXQVVHKVWJVWRVUMVXGVWJUXQLUYCVUCVUDVUFUYIVULVUMVOVCVWIVUMVRVXHVEVWNVUNUX + TVVGKVWOUXTLPZVUNUXTKPZVWOUXTLUYCVUEVUFUYIVULVWMVUNVOVCVWNVUNVRUXTVIZVEVX + AUXTVUFUXTMUBZVUEUYIVULVWMVWTUXTLMURZVPVWNVWTVRVUFVXJVUEUYIVULVWMVWTUXTLU + YCUSZVPVGVLVLVXCVUMVVHVUOKVXDVUNUXTVVGKVXEVXJVUNVXKVXEUXTLUYCVUEVUFUYIVXB + VUMVUNVOVCVXDVUNVRVXLVEVXFUXTVUFVXMVUEUYIVXBVUMVWTVXNVPVXDVWTVRVUFVXJVUEU + YIVXBVUMVWTVXOVPVGVLVXIUXQVUDVWPVUCVUFUYIVXBVWMVWQVPVXCVWMVRVUDVWRVUCVUFU + YIVXBVWMVWSVPVGVLVLVNVUHVUJVVPVWAKVUHVUJQZVXJVXMVVPKPVXPUXTLUYCVUEVUFUYIV + UJVKZVCZVXPVUFVXMVXQVXNVSUXTVAVQVUHVUJOZQZVULVVRVVTKVXTVULQZVUMUXTVVQKVYA + VUMQZVXJVUNVXKVYBUXTLUYCVUEVUFUYIVXSVULVUMVOVCZVYBVUNMUYAUMUNZVYBMUXSUYAU + MVYBUXPUXRVYBUXOUXBVYBUXOVYBUXOLUYCVUAVUBVUDVUFUYIVXSVULVUMVJVCVTZVYBUXBV + UAUXBKPZVUBVUDVUFUYIVXSVULVUMUXBWAZWBZWCZWDVYBUXQUXBVYBUXQVYBUXQLUYCVUCVU + DVUFUYIVXSVULVUMVBVCVTZVYIWDVYBVULMUXPUMUNZVXTVULVUMVDVYBUXBUXOVYEVYHVUHV + XSVULVUMVKZWEWFVYBVUMMUXRUMUNZVYAVUMVRVYBUXBUXQVYJVYHVYLWEWFUUAVUGUYIVXSV + ULVUMUQZUUBVYBUXBUXTVYBUXTVYCVTVYHVYLWEWHVXLVEVYAVWMQZVUNUXOVUOKVYOVUNQZV + WEVULVWKVYPUXOLUYCVUAVUBVUDVUFUYIVXSVULVWMVUNWGZVCVXTVULVWMVUNVKVWLVEVYOV + WTQZUXQVYRVUDVWPVUCVUDVUFUYIVXSVULVWMVWTVJZVWQVSVYAVWMVWTVDVYRUXQLUYCVYSV + CVGVLVLVXTVXBQZVUMVVSVVGKVYTVUMQZVUNUXQVURKWUAVUNQZVWRVUMVXGWUBUXQLUYCVUC + VUDVUFUYIVXSVXBVUMVUNVJZVCVYTVUMVUNVDVXHVEWUAVWTQZUXOWUDVUBVWFVUAVUBVUDVU + FUYIVXSVXBVUMVWTWGZVWHVSVXTVXBVUMVWTVKWUDUXOLUYCWUEVCVGVLVYTVWMQZUXTWUFVU + FVXMVUEVUFUYIVXSVXBVWMVOZVXNVSWUFVUNVYDWUFVYDMUXSUMUNWUFUXSMWUFUXPUXRWUFU + XOUXBWUFUXOWUFUXOLUYCVUAVUBVUDVUFUYIVXSVXBVWMVJZVCVTZWUFUXBVUAVYFVUBVUDVU + FUYIVXSVXBVWMVYGWBZWCZWDZWUFUXQUXBWUFUXQWUFUXQLUYCVUCVUDVUFUYIVXSVXBVWMVB + ZVCVTZWUKWDZUUCWUFUUDZWUFUXSMMJIMUMWUFUXPUXRMMWULWUOWUPWUPWUFUXPMUMUNUXPM + NZVYKWIOZWUFWUQOVYKOWURWUFWUQUXOMNZWUFVUBWUSOWUHVUBUXOMVWHWJVSWUFUXOWKPZV + YFWUQWUSWLWUFVUBVWEWUTWUHVWGUXOWMZVHZWUJUXOUXBUUEVQWNWUFVULVYKVXTVXBVWMVD + WUFUXBUXOWUIWUJVUHVXSVXBVWMVKZWEWOWUQVYKWPVEWUFUXPMWULWUPWQWHWUFUXRMUMUNU + XRMNZVYMWIOZWUFWVDOVYMOWVEWUFUXRMWUFUXQUXBWUFVUDVWRUXQWKPZWUMVWSUXQWMZVHZ + WUFVUDVWPWUMVWQVSZVUAUXBLPVUBVUDVUFUYIVXSVXBVWMUCUXBUUFWBZUUGWJWUFVUMVYMV + YTVWMVRWUFUXBUXQWUNWUJWVCWEWOWVDVYMWPVEWUFUXRMWUOWUPWQWHUUHUUIUUJUUOWUFUY + AUXSMUMWUFUXSUYAVUGUYIVXSVXBVWMUQZWRUUKWNWUFUXBUXTWUFUXTWUFUXTLUYCWUGVCZV + TWUJWVCWEWNWVLVGVLVLVLUXAVVBNZUYNVVEWLVUHWVMUXFVVDUXHWVMUXCVVCUXEJUXAVVBU + XBHXARWSSUXDVVLNZVVEVVOWLVUHWVNVVDVVNUXHWVNUXEVVMVVCJUXDVVLUXBHXAWTWSSUXG + VWBNZVVOVWDWLVUHWVOUXHVWCVVNUXGVWBUXBHXAUULSVUHVUJVWDVXPVUKUXBHIZVVFUXBHI + ZJIZVVPUXBHIZVVNVWCVXPUXSUYAWVRWVSVUGUYIVUJVDVXPWVPUXPWVQUXRJVXPVUKUJVUIU + UMIZHIZUXOWVTHIZWVPUXPVXPVUKUJHIZVUIHIUXOUJHIZVUIHIWWAWWBVXPWWCWWDVUIHVXP + UXOXBPWWCWWDNVXPUXOVXPUXOLUYCVUAVUBVUDVUFUYIVUJVOZVCVTUXOXCVSRVXPVUKUJVUI + VXPVUKVXPUXOVXPVUBVWEWUTWWEVWGWVAVHZXDXEVXPVUIVUHVUJVRWCZUJXFPVXPUUNXGZXH + VXPUXOUJVUIWWFWWGWWHXHTVXPUXBWVTVUKHVXPWVTUXBVXPUXBUJVXPVUAVYFUXBWKPVUAVU + BVUDVUFUYIVUJUUPVYGUXBUUQVHVXPUURUJMUBVXPUUSXGUUTWRZWTVXPUXBWVTUXOHWWIWTT + VXPVVFWVTHIZUXQWVTHIZWVQUXRVXPVVFUJHIZVUIHIUXQUJHIZVUIHIWWJWWKVXPWWLWWMVU + IHVXPUXQXBPWWLWWMNVXPUXQVXPUXQLUYCVUCVUDVUFUYIVUJUQZVCVTUXQXCVSRVXPVVFUJV + UIVXPVVFVXPUXQVXPVUDVWRWVFWWNVWSWVGVHZXDXEWWGWWHXHVXPUXQUJVUIWWOWWGWWHXHT + VXPUXBWVTVVFHWWIWTVXPUXBWVTUXQHWWIWTTXIVXPVVPWVTHIZUXTWVTHIZWVSUYAVXPVVPU + JHIZVUIHIUXTUJHIZVUIHIWWPWWQVXPWWRWWSVUIHVXPUXTXBPWWRWWSNVXPUXTVXRVTUXTXC + VSRVXPVVPUJVUIVXPVVPVXPUXTVXPVUFVXJUXTWKPZVXQVXOUXTWMZVHZXDXEWWGWWHXHVXPU + XTUJVUIWXBWWGWWHXHTVXPUXBWVTVVPHWWIWTVXPUXBWVTUXTHWWIWTTTVUJVVNWVRNVUHVUJ + VVCWVPVVMWVQJVUJVVBVUKUXBHVUJVUKVVAXJRVUJVVLVVFUXBHVUJVVFVVKXJRXISVUJVWCW + VSNVUHVUJVWBVVPUXBHVUJVVPVWAXJRSTVXTVVAUXBHIZVVKUXBHIZJIZVWAUXBHIZVVNVWCV + XTVULWXEWXFNVYAVUQUXBHIZVVIUXBHIZJIZVVRUXBHIZWXEWXFVYAVUMWXIWXJNVYBUXSUYA + WXIWXJVYNVUMWXIUXSNVYAVUMWXGUXPWXHUXRJVUMVUQUXOUXBHVUMUXOVUPXJRVUMVVIUXQU + XBHVUMUXQVVHXJRXISVUMWXJUYANVYAVUMVVRUXTUXBHVUMUXTVVQXJRSTVYOVUPUXBHIZVVH + UXBHIZJIZVVQUXBHIZWXIWXJVYOVUNWXMWXNNVYPVUOUXBHIZUYAJIZUXPWXMWXNVYPWXPUXR + UOZUYAJIZUYAUXRXKIZUXPVYPWXOWXQUYAJVYPWVFVYFUJUXBUVAUNZOZWXOWXQNZVYPVUDVW + RWVFVUCVUDVUFUYIVXSVULVWMVUNVJVWSWVGVHZVYPVUAVYFVUAVUBVUDVUFUYIVXSVULVWMV + UNXLZVYGVSZVYPWXTVUJVUHVXSVULVWMVUNUQVYPVYFUJKPZWXTVUJWLZWYEXMUXBUJUVBZXN + WNUXQUXBXOZXPRVYPWXRUYAWXQJIZWXSVYPWXQUYAVYPUXRVYPUXQUXBWYCVYPVUAVYFUXBXF + PZWYDVYGUXBUVEZVHZXQZXRVYPUXTUXBVYPVUFVXJWWTVUEVUFUYIVXSVULVWMVUNVBVXOWXA + VHWYMXQZXSVYPUYAUXRWYOWYNXTYCVYPUYAUXPUXRVYPUXOUXBVYPVUBVWEWUTVYQVWGWVAVH + WYMXQWYNVYPUXSUYAVUGUYIVXSVULVWMVUNVOWRUVCYAVUNWXMWXPNVYOVUNWXKWXOWXLUYAJ + VUNVUPVUOUXBHVUNVUOUXOXJRVUNVVHUXTUXBHVUNUXTVVGXJRZXISVUNWXNUXPNVYOVUNVVQ + UXOUXBHVUNUXOVUOXJRSTVYRUXPVVGUXBHIZJIZWXOWXMWXNVYRUXPUYAUOZJIZWXQWYRWXOV + YRWYTUXPUYAXKIZWXQVYRUXPUYAVYRUXOUXBVYRVUBVWEWUTVUAVUBVUDVUFUYIVXSVULVWMV + WTWGVWGWVAVHVYRUXBVUAVYFVUBVUDVUFUYIVXSVULVWMVWTVYGYDZWCZXQZVYRUXTUXBVYRV + UFVXJWWTVUEVUFUYIVXSVULVWMVWTVBVXOWXAVHZXUCXQZXTVYRUYAXUAWXQXUFVYRUXPUYAX + UDXUFUVFVYRUXRVYRUXQUXBVYRVUDVWRWVFVYSVWSWVGVHZXUCXQZXRVYRUXPWXSUYAXUAJIW + YJVYRUXPUXRUYAXUDXUHVUGUYIVXSVULVWMVWTVOUVDVYRUYAUXPXUFXUDUVGVYRUYAUXRXUF + XUHXTTYBYCVYRWYQWYSUXPJVYRWWTVYFWYAWYQWYSNZXUEXUBVYRWXTVUJVUHVXSVULVWMVWT + UQVYRVYFWYFWYGXUBXMWYHXNWNZUXTUXBXOZXPWTVYRWVFVYFWYAWYBXUGXUBXUJWYIXPTVWT + WXMWYRNVYOVWTWXKUXPWXLWYQJVWTVUPUXOUXBHVUNVUOUXOYERVWTVVHVVGUXBHVUNUXTVVG + YERZXISVWTWXNWXONVYOVWTVVQVUOUXBHVUNUXOVUOYERSTYFVWMWXIWXMNVYAVWMWXGWXKWX + HWXLJVWMVUQVUPUXBHVUMUXOVUPYERVWMVVIVVHUXBHVUMUXQVVHYERXISVWMWXJWXNNVYAVW + MVVRVVQUXBHVUMUXTVVQYERSTYFVULWXEWXINVXTVULWXCWXGWXDWXHJVULVVAVUQUXBHVULV + UQVUTXJRVULVVKVVIUXBHVULVVIVVJXJRXISVULWXFWXJNVXTVULVWAVVRUXBHVULVVRVVTXJ + RSTVYTVUTUXBHIZVVJUXBHIZJIZVVTUXBHIZWXEWXFVYTVUMXUOXUPNWUAVUSUXBHIZWXLJIZ + VVSUXBHIZXUOXUPWUAVUNXURXUSNWUBVURUXBHIZUYAJIZUXRXURXUSWUBXVAUXPUOZUYAJIZ + UXRWUBXUTXVBUYAJWUBWUTVYFWYAXUTXVBNZWUBVUBVWEWUTVUAVUBVUDVUFUYIVXSVXBVUMV + UNWGVWGWVAVHZVUAVYFVUBVUDVUFUYIVXSVXBVUMVUNVYGYDZWUBWXTVUJVUHVXSVXBVUMVUN + UQWUBVYFWYFWYGXVFXMWYHXNWNUXOUXBXOZXPRWUBUXPXVCUXRWUBUXOUXBXVEWUBUXBXVFWC + ZXQZWUBXVBUYAWUBUXPXVIXRZWUBUXTUXBWUBVUFVXJWWTVUEVUFUYIVXSVXBVUMVUNVBVXOW + XAVHXVHXQZUVHWUBUXQUXBWUBVUDVWRWVFWUCVWSWVGVHXVHXQWUBUXPXVCJIZUYAUXSWUBUX + PXVBJIZUYAJIMUYAJIXVLUYAWUBXVMMUYAJWUBUXPXVIUVIRWUBUXPXVBUYAXVIXVJXVKUVJW + UBUYAXVKUVKUVLVUGUYIVXSVXBVUMVUNVOYGYBYCVUNXURXVANWUAVUNXUQXUTWXLUYAJVUNV + USVURUXBHVUNVURUXQXJRWYPXISVUNXUSUXRNWUAVUNVVSUXQUXBHVUNUXQVURXJRSTWUDUXR + WYQJIZXUTXURXUSWUDWXRUOZXVBXVNXUTWUDWXRUXPWUDWXRWYJWXSUXPWUDWXQUYAWUDUXRW + UDUXQUXBWUDVUDVWRWVFVUCVUDVUFUYIVXSVXBVUMVWTVJVWSWVGVHWUDVUAVYFWYKVUAVUBV + UDVUFUYIVXSVXBVUMVWTXLZVYGWYLVHZXQZXRZWUDUXTUXBWUDVUFVXJWWTVUEVUFUYIVXSVX + BVUMVWTVBVXOWXAVHZXVQXQZXSWUDUYAUXRXWAXVRXTWUDUXSUXRXKIWXSUXPWUDUXSUYAUXR + XKVUGUYIVXSVXBVUMVWTVORWUDUXPUXRWUDUXOUXBWUDVUBVWEWUTWUEVWGWVAVHZXVQXQXVR + UVMUVOYAYHWUDUXRWYSJIWXQUOZWYSJIXVNXVOWUDUXRXWCWYSJWUDXWCUXRWUDUXRXVRUVNW + RRWUDWYQWYSUXRJWUDWWTVYFWYAXUIXVTWUDVUAVYFXVPVYGVSZWUDWXTVUJVUHVXSVXBVUMV + WTUQWUDVYFWYFWYGXWDXMWYHXNWNZXUKXPWTWUDWXQUYAXVSXWAYITWUDWUTVYFWYAXVDXWBX + WDXWEXVGXPTVWTXURXVNNWUAVWTXUQUXRWXLWYQJVWTVUSUXQUXBHVUNVURUXQYERXULXISVW + TXUSXUTNWUAVWTVVSVURUXBHVUNUXQVURYERSTYFVUMXUOXURNVYTVUMXUMXUQXUNWXLJVUMV + UTVUSUXBHVUMVUSVURXJRVUMVVJVVHUXBHVUMVVHVUOXJRXISVUMXUPXUSNVYTVUMVVTVVSUX + BHVUMVVSVVGXJRSTWUFXUTWXOJIZWYQXUOXUPWUFUXSUOZWYSXWFWYQWUFUXSUYAWVKYHWUFX + WFXVBWXQJIXWGWUFXUTXVBWXOWXQJWUFWUTVYFWYAXVDWVBWUJWUFWXTVUJWVCWUFVYFWYFWY + GWUJXMWYHXNWNZXVGXPWUFWVFVYFWYAWYBWVHWUJXWHWYIXPXIWUFUXPUXRWUFUXOUXBWVBWU + FVUBVWFWUHVWHVSWVJYMWUFUXQUXBWVHWVIWVJYMYIYGWUFWWTVYFWYAXUIWUFVUFVXJWWTWU + GVXOWXAVHWUJXWHXUKXPTVWMXUOXWFNVYTVWMXUMXUTXUNWXOJVWMVUTVURUXBHVUMVUSVURY + ERVWMVVJVUOUXBHVUMVVHVUOYERXISVWMXUPWYQNVYTVWMVVTVVGUXBHVUMVVSVVGYERSTYFV + XBWXEXUONVXTVXBWXCXUMWXDXUNJVXBVVAVUTUXBHVULVUQVUTYERVXBVVKVVJUXBHVULVVIV + VJYERXISVXBWXFXUPNVXTVXBVWAVVTUXBHVULVVRVVTYERSTYFVXSVVNWXENVUHVXSVVCWXCV + VMWXDJVXSVVBVVAUXBHVUJVUKVVAYERVXSVVLVVKUXBHVUJVVFVVKYERXISVXSVWCWXFNVUHV + XSVWBVWAUXBHVUJVVPVWAYERSTYFUVPUVQYJYJUVRUYMUYGOZDUXMUIUYSUYLXWIDUXMUYLUY + FOZEUYDUIXWIUYKXWJEUYDUYKUYEOZFUYDUIXWJUYJXWKFUYDUYJUYBOZGUYDUIXWKUYIXWLG + UYDXWLUYIUXSUYAYKYLYNUYBGUYDYOYPYNUYEFUYDYOYPYNUYFEUYDYOYPYNUYGDUXMYOYPUY + RUXLOZDUXMUIUYTUYQXWMDUXMUYQUXKOZAKUIXWMUYPXWNAKUYPUXJOZBKUIXWNUYOXWOBKUY + OUXIOZCKUIXWOUYNXWPCKXWPUYNUXFUXHYKYLYNUXICKYOYPYNUXJBKYOYPYNUXKAKYOYPYNU + XLDUXMYOYPUVSUVTUYGUXLDUXMUYGUYBGKUDFKUDZEKUDZUXLKUYDYQZUYGXWRUWAKKUYCUHZ + UYDKUYCUWFUWBNZKXWTNXXAMKPOUWCKMUWDUWEKUYCUWGUWHKLYQXWTUYDYQUWIKLUYCUWJYR + UWKXWSUYFXWQEUYDKXWSVWKVUBUYFXWQKUYDUXOUWLUYBFGKUYDUWMUWQUWNYRUYBUXIUXCUX + RJIZUYAUBUXFUYAUBEFGABCKKKEAYSZUXSXXBUYAXXCUXPUXCUXRJUXOUXAUXBHXARYTFBYSZ + XXBUXFUYAXXDUXRUXEUXCJUXQUXDUXBHXAWTYTGCYSUYAUXHUXFUXTUXGUXBHXAUWOUWPUWRU + WSUWT $. $} ${ @@ -633562,9 +633562,9 @@ standardize vectors to a length (norm) of one, but such definitions require Stefan O'Rear, 12-Feb-2015.) $) moxfr $p |- ( E* x ph <-> E* y ps ) $= ( wex weu wi wmo cvv wrex wcel cv a1i wceq rexv moeu ax-mp rexxfr 3bitr3i - euex mpbir euxfr imbi12i 3bitr4i ) ACIZACJZKBDIZBDJZKACLBDLUIUKUJULACMNBD - MNUIUKABCDEMMEMODPMOFQCPZERZDMNZUMMOUOUNDIZUNDJUPGUNDUDUAUNDSUEQHUBACSBDS - UCABCDEFGHUFUGACTBDTUH $. + euex mpbir euxfrw imbi12i 3bitr4i ) ACIZACJZKBDIZBDJZKACLBDLUIUKUJULACMNB + DMNUIUKABCDEMMEMODPMOFQCPZERZDMNZUMMOUOUNDIZUNDJUPGUNDUDUAUNDSUEQHUBACSBD + SUCABCDEFGHUFUGACTBDTUH $. $} @@ -633742,19 +633742,19 @@ family of sets (implicit). (Contributed by Stefan O'Rear, wfn ismrcd1 eqid mrcf ffn 3syl cv mrcssvd elpwi mrcssid syl2an wal 3expib alrimivv vex fvex weq wb sseq1 adantl sseq12 anbi12d fveq2 imbi12d spc2gv mp2an syl mp2and mrccl elpw sylibr fnelfp syl2anc mpbid sseqtrd anbi2d id - sseq12d chvarv sylan2 2fveq3 eqeq12d mpbird mrcsscl syl3anc eqssd eqfnfvd - ffvelrnda ) ALDUAZEEUBUCUDZUEMZAWQWQEHUFZAWRDUGMNZWQWRWSUHWSWQUIABCDEFGHI - JKUJZWRWSDWSUKZULWQWRWSUMUNALUOZWQNZOZXDEMZXDWSMZXFXGXHEMZXHXFXHDPZXDXHPZ - XGXIPZAXJXEAWRXDWSDXBXCUPZQAXAXDDPZXKXEXBXDDUQZWRXDWSDXCURUSAXJXKOZXLRZXE - ABUOZDPZCUOZXRPZOZXTEMZXREMZPZRZBUTCUTZXQAYFCBAXSYAYEJVAVBXDSNXHSNYGXQRLV - CXDWSVDZYFXQCBXDXHSSCLVEZXRXHTZOZYBXPYEXLYKXSXJYAXKYJXSXJVFYIXRXHDVGVHXTX - DXRXHVIVJYIYCXGTYDXITYEXLVFYJXTXDEVKXRXHEVKYCXGYDXIVIUSVLVMVNVOQVPXFXHWRN - ZXIXHTZAXAXNYLXEXBXOWRXDWSDXCVQUSXFEWQUIZXHWQNZYLYMVFAYNXEWTQZAYOXEAXJYOX - MXHDYHVRVSQWQEXHVTWAWBWCXFXAXDXGPZXGWRNZXHXGPAXAXEXBQXEAXNYQXOAXSOZXRYDPZ - RAXNOZYQRBLBLVEZYSUUAYTYQUUBXSXNAXRXDDVGWDZUUBXRXDYDXGUUBWEXRXDEVKZWFVLIW - GWHXFYRXGEMZXGTZXEAXNUUFXOYSYDEMZYDTZRUUAUUFRBLUUBYSUUAUUHUUFUUCUUBUUGUUE - YDXGXRXDEEWIUUDWJVLKWGWHXFYNXGWQNYRUUFVFYPAWQWQXDEHWPWQEXGVTWAWKWRXDWSXGD - XCWLWMWNWO $. + sseq12d chvarvv sylan2 2fveq3 eqeq12d ffvelrnda mrcsscl syl3anc eqfnfvd + mpbird eqssd ) ALDUAZEEUBUCUDZUEMZAWQWQEHUFZAWRDUGMNZWQWRWSUHWSWQUIABCDEF + GHIJKUJZWRWSDWSUKZULWQWRWSUMUNALUOZWQNZOZXDEMZXDWSMZXFXGXHEMZXHXFXHDPZXDX + HPZXGXIPZAXJXEAWRXDWSDXBXCUPZQAXAXDDPZXKXEXBXDDUQZWRXDWSDXCURUSAXJXKOZXLR + ZXEABUOZDPZCUOZXRPZOZXTEMZXREMZPZRZBUTCUTZXQAYFCBAXSYAYEJVAVBXDSNXHSNYGXQ + RLVCXDWSVDZYFXQCBXDXHSSCLVEZXRXHTZOZYBXPYEXLYKXSXJYAXKYJXSXJVFYIXRXHDVGVH + XTXDXRXHVIVJYIYCXGTYDXITYEXLVFYJXTXDEVKXRXHEVKYCXGYDXIVIUSVLVMVNVOQVPXFXH + WRNZXIXHTZAXAXNYLXEXBXOWRXDWSDXCVQUSXFEWQUIZXHWQNZYLYMVFAYNXEWTQZAYOXEAXJ + YOXMXHDYHVRVSQWQEXHVTWAWBWCXFXAXDXGPZXGWRNZXHXGPAXAXEXBQXEAXNYQXOAXSOZXRY + DPZRAXNOZYQRBLBLVEZYSUUAYTYQUUBXSXNAXRXDDVGWDZUUBXRXDYDXGUUBWEXRXDEVKZWFV + LIWGWHXFYRXGEMZXGTZXEAXNUUFXOYSYDEMZYDTZRUUAUUFRBLUUBYSUUAUUHUUFUUCUUBUUG + UUEYDXGXRXDEEWIUUDWJVLKWGWHXFYNXGWQNYRUUFVFYPAWQWQXDEHWKWQEXGVTWAWOWRXDWS + XGDXCWLWMWPWN $. $} ${ @@ -634175,15 +634175,15 @@ family of sets (implicit). (Contributed by Stefan O'Rear, /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } ) $= ( vv va vc vb cz cv cmap co wcel wral cmpt wa eleq1d csn cxp cfv cof cmul caddc cpw crab cvv cmzpcl wceq oveq2 oveq2d pweqd xpeq1d ralbidv weq sneq - xpeq2d cbvralv syl6bb mpteq1d fveq2 mpteq2dv fveq1 cbvmptv eleq1i anbi12d - raleqbi1dv anbi1d rabeqbidv df-mzpcl ovex pwex rabex fvmpt ) HFLHMZNOZIMZ - UAZUBZGMZPZILQZJVRKMZJMZUCZRZWBPZKVQQZSZBMZCMZUFUDOWBPWLWMUEUDOWBPSCWBQBW - BQZSZGLVRNOZUGZUHLFNOZDMZUAZUBZWBPZDLQZAWREMZAMZUCZRZWBPZEFQZSZWNSZGLWRNO - ZUGZUHUIUJVQFUKZWOXKGWQXMXNWPXLXNVRWRLNVQFLNULZUMUNXNWKXJWNXNWDXCWJXIXNWD - WRVTUBZWBPZILQXCXNWCXQILXNWAXPWBXNVRWRVTXOUOTUPXQXBIDLIDUQZXPXAWBXRVTWTWR - VSWSURUSTUTVAXNWJJWRWGRZWBPZKFQXIWIXTKVQFXNWHXSWBXNJVRWRWGXOVBTVIXTXHKEFK - EUQZXTJWRXDWFUCZRZWBPXHYAXSYCWBYAJWRWGYBWEXDWFVCVDTYCXGWBJAWRYBXFXDWFXEVE - VFVGVAUTVAVHVJVKJHBCIKGVLXKGXMXLLWRNVMVNVOVP $. + xpeq2d cbvralvw syl6bb mpteq1d raleqbi1dv mpteq2dv cbvmptv eleq1i anbi12d + fveq2 fveq1 anbi1d rabeqbidv df-mzpcl ovex pwex rabex fvmpt ) HFLHMZNOZIM + ZUAZUBZGMZPZILQZJVRKMZJMZUCZRZWBPZKVQQZSZBMZCMZUFUDOWBPWLWMUEUDOWBPSCWBQB + WBQZSZGLVRNOZUGZUHLFNOZDMZUAZUBZWBPZDLQZAWREMZAMZUCZRZWBPZEFQZSZWNSZGLWRN + OZUGZUHUIUJVQFUKZWOXKGWQXMXNWPXLXNVRWRLNVQFLNULZUMUNXNWKXJWNXNWDXCWJXIXNW + DWRVTUBZWBPZILQXCXNWCXQILXNWAXPWBXNVRWRVTXOUOTUPXQXBIDLIDUQZXPXAWBXRVTWTW + RVSWSURUSTUTVAXNWJJWRWGRZWBPZKFQXIWIXTKVQFXNWHXSWBXNJVRWRWGXOVBTVCXTXHKEF + KEUQZXTJWRXDWFUCZRZWBPXHYAXSYCWBYAJWRWGYBWEXDWFVHVDTYCXGWBJAWRYBXFXDWFXEV + IVEVFVAUTVAVGVJVKJHBCIKGVLXKGXMXLLWRNVMVNVOVP $. $} ${ @@ -634216,16 +634216,16 @@ family of sets (implicit). (Contributed by Stefan O'Rear, ( vv vf vg va vb cz cv cmap co cmzpcl cfv wcel cvv wral wa caddc wf elmap zex wceq oveq2 fveq2 eleq12d wss csn cxp cmpt cof cmul ssid ovex constmap oveq2d vex ffvelrn sylanb ancoms fmpttd sylibr pm3.2i zaddcl adantl simpl - rgen simpr ovexd inidm off zmulcl anbi12i 3imtr4i rgen2a wb elmzpcl ax-mp - jca mpbir2an vtoclg ) GGBHZIJZIJZVTKLZMZGGAIJZIJZAKLZMBANVTAUAZWBWFWCWGWH - WAWEGIVTAGIUBUNVTAKUCUDWDWBWBUEZWACHZUFUGWBMZCGOZDWAWJDHZLZUHZWBMZCVTOZPZ - WJWMQUIJZWBMZWJWMUJUIJZWBMZPZDWBOCWBOZPZWBUKWRXDWLWQWKCGWAWJGGVTIULZTUMVE - WPCVTWJVTMZWAGWORWPXGDWAWNGWMWAMZXGWNGMZXHVTGWMRXGXIGVTWMTBUOZSVTGWJWMUPU - QURUSGWAWOTXFSUTVEVAXCCDWBWAGWJRZWAGWMRZPZWAGWSRZWAGXARZPWJWBMZWMWBMZPXCX - MXNXOXMEFWAWAWAQGGGWJWMNNEHZGMFHZGMPZXRXSQJGMXMXRXSVBVCXKXLVDZXKXLVFZXMGV - TIVGZYCWAVHZVIXMEFWAWAWAUJGGGWJWMNNXTXRXSUJJGMXMXRXSVJVCYAYBYCYCYDVIVQXPX - KXQXLGWAWJTXFSGWAWMTXFSVKWTXNXBXOGWAWSTXFSGWAXATXFSVKVLVMVAVTNMWDWIXEPVNX - JDWBCDCCVTVOVPVRVS $. + rgen simpr ovexd inidm off zmulcl jca anbi12i 3imtr4i rgen2 elmzpcl ax-mp + wb mpbir2an vtoclg ) GGBHZIJZIJZVTKLZMZGGAIJZIJZAKLZMBANVTAUAZWBWFWCWGWHW + AWEGIVTAGIUBUNVTAKUCUDWDWBWBUEZWACHZUFUGWBMZCGOZDWAWJDHZLZUHZWBMZCVTOZPZW + JWMQUIJZWBMZWJWMUJUIJZWBMZPZDWBOCWBOZPZWBUKWRXDWLWQWKCGWAWJGGVTIULZTUMVEW + PCVTWJVTMZWAGWORWPXGDWAWNGWMWAMZXGWNGMZXHVTGWMRXGXIGVTWMTBUOZSVTGWJWMUPUQ + URUSGWAWOTXFSUTVEVAXCCDWBWBWAGWJRZWAGWMRZPZWAGWSRZWAGXARZPWJWBMZWMWBMZPXC + XMXNXOXMEFWAWAWAQGGGWJWMNNEHZGMFHZGMPZXRXSQJGMXMXRXSVBVCXKXLVDZXKXLVFZXMG + VTIVGZYCWAVHZVIXMEFWAWAWAUJGGGWJWMNNXTXRXSUJJGMXMXRXSVJVCYAYBYCYCYDVIVKXP + XKXQXLGWAWJTXFSGWAWMTXFSVLWTXNXBXOGWAWSTXFSGWAXATXFSVLVMVNVAVTNMWDWIXEPVQ + XJDWBCDCCVTVOVPVRVS $. $( Corrolary of ~ mzpclall : polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.) $) @@ -634593,75 +634593,75 @@ theorem and the several that follow ( ~ mzpaddmpt , ~ mzpmulmpt , adantl simpl snssd syl2anc eqid fvex fvmpt fvres ax-mp syl6req syl5eq w3a wf cun simplll simprll unfi unex ssun1 simpllr mzpresrename syl3anc ssun2 wi simprlr mzpaddmpt simplr simprr wfn ovex mzpf ffn 3syl ofmpteq oveq12d - reseq1 resabs1 fveq2i oveq12i eqtrd eqeq1d rexbidv eqeq1 2rexbidv cbvrexv - weq syl6bb unssd elmapi fssres syl2anr zex elmap sylibr adantlrr adantrrr - mzpmulmpt simplrr mpbird r19.40 exp32 rexlimdvv ex rexlimivv imp ad2ant2l - simprrr 3adant1 simpld simprd mzpindd eqeq2i anbi2i 2rexbii sylib ) ABHIZ - JZCKZBUJZAGLBUDMZGKZUVKUKZDKZIZNZOZPZDUVKHIZQCRQZUVLAEUVMEKZUVKUKZUVPIZNZ - OZPZDUWAQCRQULUVJUWBUMULUVLUAKZUVROZPZDUWAQCRQZUVLUVMUBKZUNZUOZUVROZPZDUW - AQZCRQZUVLUCUVMUWMUCKZIZNZUVROZPZDUWAQZCRQZUEKZBUJZUWMGUVMUVNUXGUKZUFKZIZ - NZOZPZUFUXGHIZQZUERQZUGKZBUJZUWTGUVMUVNUXRUKZUHKZIZNZOZPZUHUXRHIZQZUGRQZU - VLUWMUWTUPUQZMZUVROZPZDUWAQZCRQZUVLUWMUWTURUQZMZUVROZPZDUWAQZCRQZUWBUAAUB - UCBUWMLJZUWSULVUASRJSBUJZUWOGUVMUVNSUKZUVPIZNZOZPZDSHIZQZUWSUSVUALSUDMZUW - NUOZVUHJZVUBUWOGUVMVUCVUKIZNZOZVUISUTJVUAVULVBUWMSVAWCVUBVUABVCZVDVUAVUNG - UVMUWMNUWOVUAGUVMVUMUWMVUAUVNUVMJZPZVUCVUJJZVUMUWMOVURVUQVUBVUSVUAVUQVEVU - PUVNLBSVFVGVUJUWMVUCUBVHVIVJVKGUVMUWMVLVMVUGVUBVUOPDVUKVUHUVPVUKOZVUFVUOV - UBVUTVUEVUNUWOVUTGUVMVUDVUMVUCUVPVUKVNVOVPTVQVRUWRVUICSRUVKSOZUWQVUGDUWAV - UHUVKSHVSVVAUVLVUBUWPVUFUVKSBVTVVAUVRVUEUWOVVAGUVMUVQVUDVVAUVOVUCUVPUVKSU - VNWAWDVOVPWBWEVQWFWNUWMBJZUXFULVVBUWNRJUWNBUJZUXBGUVMUVNUWNUKZUVPIZNZOZPZ - DUWNHIZQZUXFUWMWGVVBUCLUWNUDMZUXANZVVIJZVVCUXBGUVMVVDVVLIZNZOZVVJVVMVVBUW - NUTJUWMUWNJZVVMUWMWHUBWIZUCUWNUWMWJWKVDUWMBWLVVBUXBGUVMUWMUVNIZNVVOUCGUVM - UXAVVSUWMUWTUVNVNWMVVBGUVMVVSVVNVVBVUQPZVVNUWMVVDIZVVSVVTVVDVVKJZVVNVWAOV - VTVUQVVCVWBVVBVUQVEVVTUWMBVVBVUQWOWPUVNLBUWNVFWQUCVVDUXAVWAVVKVVLUWMUWTVV - DVNVVLWRUWMVVDWSWTVJVVQVWAVVSOVVRUWMUWNUVNXAXBXCVKXDVVHVVCVVPPDVVLVVIUVPV - VLOZVVGVVPVVCVWCVVFVVOUXBVWCGUVMVVEVVNVVDUVPVVLVNVOVPTVQVRUXEVVJCUWNRUVKU - WNOZUXDVVHDUWAVVIUVKUWNHVSVWDUVLVVCUXCVVGUVKUWNBVTVWDUVRVVFUXBVWDGUVMUVQV - VEVWDUVOVVDUVPUVKUWNUVNWAWDVOVPWBWEVQWFWNULUVMLUWMXFZUXQPZUVMLUWTXFZUYHPZ - XEZUYNUYTVWFVWHUYNUYTPZULUXQUYHVWJVWEVWGUXQUYHVWJUXNUYHVWJXQZUEUFRUXOUXGR - JZUXJUXOJZPZUXNVWKVWNUXNPZUYEVWJUGUHRUYFVWOUXRRJZUYAUYFJZPZUYEVWJVWOVWRUY - EPZPZUYMUYSPZCRQZVWJVWTVXBUVLUXLUYCUYIMZUVROZPZDUWAQZUVLUXLUYCUYOMZUVROZP - ZDUWAQZPZCRQZVWOVWRUXSVXLUYDVWNUXHVWRUXSPZVXLUXMVWNUXHPZVXMPZUXGUXRXGZRJZ - VXPBUJZVXCGUVMUVNVXPUKZUVPIZNZOZPZDVXPHIZQZVXRVXGVYAOZPZDVYDQZVXLVXOVWLVW - PVXQVWLVWMUXHVXMXHVXNVWPVWQUXSXIUXGUXRXJWQVXOUILVXPUDMZUIKZUXGUKZUXJIZVYJ - UXRUKZUYAIZUPMZNZVYDJZVXRVXCGUVMVXSVYPIZNZOZVYEVXOUIVYIVYLNVYDJZUIVYIVYNN - VYDJZVYQVXOVXPUTJZUXGVXPUJZVWMWUAWUCVXOUXGUXRUEVHUGVHXKZVDZWUDVXOUXGUXRXL - ZVDVWLVWMUXHVXMXMZUIUXJUXGVXPXNXOZVXOWUCUXRVXPUJZVWQWUBWUFWUJVXOUXRUXGXPZ - VDVXNVWPVWQUXSXRZUIUYAUXRVXPXNXOZUIVYLVYNVXPXSWQVXOUXGUXRBVWNUXHVXMXTZVXN - VWRUXSYAZUUAZVXOVXCGUVMUXKUYBUPMZNZVYSVXOUVMUTJZUXLUVMYBZUYCUVMYBZVXCWURO - WUSVXOLBUDYCVDZVXOUXLUVIJZUVMLUXLXFWUTVXOBUTJZUXHVWMWVCWVDVXOFVDZWUNWUHGU - XJUXGBXNXOUXLBYDUVMLUXLYEYFZVXOUYCUVIJZUVMLUYCXFWVAVXOWVDUXSVWQWVGWVEWUOW - ULGUYAUXRBXNXOUYCBYDUVMLUYCYEYFZGUVMUXKUYBUPUTYGXOVXOGUVMWUQVYRVXOVUQPZVY - RVXSUXGUKZUXJIZVXSUXRUKZUYAIZUPMZWUQWVIVXSVYIJZVYRWVNOWVIVXPLVXSXFZWVOVUQ - BLUVNXFVXRWVPVXOUVNLBUUBWUPBLVXPUVNUUCUUDLVXPVXSUUEWUEUUFUUGZUIVXSVYOWVNV - YIVYPVYJVXSOZVYLWVKVYNWVMUPWVRVYKWVJUXJVYJVXSUXGYIWDZWVRVYMWVLUYAVYJVXSUX - RYIWDZYHVYPWRWVKWVMUPYCWTVJWVKUXKWVMUYBUPWVJUXIUXJWUDWVJUXIOWUGUVNUXGVXPY - JXBYKZWVLUXTUYAWUJWVLUXTOWUKUVNUXRVXPYJXBYKZYLXCVKYMVYCVXRVYTPDVYPVYDUVPV - YPOZVYBVYTVXRWWCVYAVYSVXCWWCGUVMVXTVYRVXSUVPVYPVNVOVPTVQVRVXOUIVYIVYLVYNU - RMZNZVYDJZVXRVXGGUVMVXSWWEIZNZOZVYHVXOWUAWUBWWFWUIWUMUIVYLVYNVXPUUJWQWUPV - XOVXGGUVMUXKUYBURMZNZWWHVXOWUSWUTWVAVXGWWKOWVBWVFWVHGUVMUXKUYBURUTYGXOVXO - GUVMWWJWWGWVIWWGWVKWVMURMZWWJWVIWVOWWGWWLOWVQUIVXSWWDWWLVYIWWEWVRVYLWVKVY - NWVMURWVSWVTYHWWEWRWVKWVMURYCWTVJWVKUXKWVMUYBURWWAWWBYLXCVKYMVYGVXRWWIPDW - WEVYDUVPWWEOZVYFWWIVXRWWMVYAWWHVXGWWMGUVMVXTWWGVXSUVPWWEVNVOVPTVQVRVXKVYE - VYHPCVXPRUVKVXPOZVXFVYEVXJVYHWWNVXEVYCDUWAVYDUVKVXPHVSZWWNUVLVXRVXDVYBUVK - VXPBVTZWWNUVRVYAVXCWWNGUVMUVQVXTWWNUVOVXSUVPUVKVXPUVNWAWDVOZVPWBWEWWNVXIV - YGDUWAVYDWWOWWNUVLVXRVXHVYFWWPWWNUVRVYAVXGWWQVPWBWEWBVQVRUUHUUIVWTVXAVXKC - RVWTUYMVXFUYSVXJVWTUYLVXEDUWAVWTUYKVXDUVLVWTUYJVXCUVRVWTUWMUXLUWTUYCUYIVW - NUXHUXMVWSUUKZVWOVWRUXSUYDUUTZYHYNTYOVWTUYRVXIDUWAVWTUYQVXHUVLVWTUYPVXGUV - RVWTUWMUXLUWTUYCUYOWWRWWSYHYNTYOWBYOUULUYMUYSCRUUMVJUUNUUOUUPUUQUURUUSUVA - ZUVBVWIUYNUYTWWTUVCUWIUWOOZUWKUWQCDRUWAWXAUWJUWPUVLUWIUWOUVRYPTYQUWIUXBOZ - UWKUXDCDRUWAWXBUWJUXCUVLUWIUXBUVRYPTYQUAUBYSZUWLUVLUWMUVROZPZDUWAQZCRQUXQ - WXCUWKWXECDRUWAWXCUWJWXDUVLUWIUWMUVRYPTYQWXFUXPCUERCUEYSZWXFUXHUWMGUVMUXI - UVPIZNZOZPZDUXOQUXPWXGWXEWXKDUWAUXOUVKUXGHVSWXGUVLUXHWXDWXJUVKUXGBVTWXGUV - RWXIUWMWXGGUVMUVQWXHWXGUVOUXIUVPUVKUXGUVNWAWDVOVPWBWEWXKUXNDUFUXODUFYSZWX - JUXMUXHWXLWXIUXLUWMWXLGUVMWXHUXKUXIUVPUXJVNVOVPTYRYTYRYTUAUCYSZUWLUVLUWTU - VROZPZDUWAQZCRQUYHWXMUWKWXOCDRUWAWXMUWJWXNUVLUWIUWTUVRYPTYQWXPUYGCUGRCUGY - SZWXPUXSUWTGUVMUXTUVPIZNZOZPZDUYFQUYGWXQWXOWYADUWAUYFUVKUXRHVSWXQUVLUXSWX - NWXTUVKUXRBVTWXQUVRWXSUWTWXQGUVMUVQWXRWXQUVOUXTUVPUVKUXRUVNWAWDVOVPWBWEWY - AUYEDUHUYFDUHYSZWXTUYDUXSWYBWXSUYCUWTWYBGUVMWXRUYBUXTUVPUYAVNVOVPTYRYTYRY - TUWIUYJOZUWKUYLCDRUWAWYCUWJUYKUVLUWIUYJUVRYPTYQUWIUYPOZUWKUYRCDRUWAWYDUWJ - UYQUVLUWIUYPUVRYPTYQUWIAOZUWKUVTCDRUWAWYEUWJUVSUVLUWIAUVRYPTYQUVDWCUVTUWH - CDRUWAUVSUWGUVLUVRUWFAGEUVMUVQUWEGEYSUVOUWDUVPUVNUWCUVKYIWDWMUVEUVFUVGUVH - $. + reseq1 resabs1 fveq2i oveq12i eqtrd eqeq1d eqeq1 2rexbidv cbvrexvw syl6bb + rexbidv weq unssd elmapi fssres syl2anr elmap mzpmulmpt adantlrr adantrrr + zex sylibr simplrr simprrr mpbird r19.40 exp32 rexlimdvv ex rexlimivv imp + ad2ant2l 3adant1 simpld simprd mzpindd eqeq2i anbi2i 2rexbii sylib ) ABHI + ZJZCKZBUJZAGLBUDMZGKZUVKUKZDKZIZNZOZPZDUVKHIZQCRQZUVLAEUVMEKZUVKUKZUVPIZN + ZOZPZDUWAQCRQULUVJUWBUMULUVLUAKZUVROZPZDUWAQCRQZUVLUVMUBKZUNZUOZUVROZPZDU + WAQZCRQZUVLUCUVMUWMUCKZIZNZUVROZPZDUWAQZCRQZUEKZBUJZUWMGUVMUVNUXGUKZUFKZI + ZNZOZPZUFUXGHIZQZUERQZUGKZBUJZUWTGUVMUVNUXRUKZUHKZIZNZOZPZUHUXRHIZQZUGRQZ + UVLUWMUWTUPUQZMZUVROZPZDUWAQZCRQZUVLUWMUWTURUQZMZUVROZPZDUWAQZCRQZUWBUAAU + BUCBUWMLJZUWSULVUASRJSBUJZUWOGUVMUVNSUKZUVPIZNZOZPZDSHIZQZUWSUSVUALSUDMZU + WNUOZVUHJZVUBUWOGUVMVUCVUKIZNZOZVUISUTJVUAVULVBUWMSVAWCVUBVUABVCZVDVUAVUN + GUVMUWMNUWOVUAGUVMVUMUWMVUAUVNUVMJZPZVUCVUJJZVUMUWMOVURVUQVUBVUSVUAVUQVEV + UPUVNLBSVFVGVUJUWMVUCUBVHVIVJVKGUVMUWMVLVMVUGVUBVUOPDVUKVUHUVPVUKOZVUFVUO + VUBVUTVUEVUNUWOVUTGUVMVUDVUMVUCUVPVUKVNVOVPTVQVRUWRVUICSRUVKSOZUWQVUGDUWA + VUHUVKSHVSVVAUVLVUBUWPVUFUVKSBVTVVAUVRVUEUWOVVAGUVMUVQVUDVVAUVOVUCUVPUVKS + UVNWAWDVOVPWBWEVQWFWNUWMBJZUXFULVVBUWNRJUWNBUJZUXBGUVMUVNUWNUKZUVPIZNZOZP + ZDUWNHIZQZUXFUWMWGVVBUCLUWNUDMZUXANZVVIJZVVCUXBGUVMVVDVVLIZNZOZVVJVVMVVBU + WNUTJUWMUWNJZVVMUWMWHUBWIZUCUWNUWMWJWKVDUWMBWLVVBUXBGUVMUWMUVNIZNVVOUCGUV + MUXAVVSUWMUWTUVNVNWMVVBGUVMVVSVVNVVBVUQPZVVNUWMVVDIZVVSVVTVVDVVKJZVVNVWAO + VVTVUQVVCVWBVVBVUQVEVVTUWMBVVBVUQWOWPUVNLBUWNVFWQUCVVDUXAVWAVVKVVLUWMUWTV + VDVNVVLWRUWMVVDWSWTVJVVQVWAVVSOVVRUWMUWNUVNXAXBXCVKXDVVHVVCVVPPDVVLVVIUVP + VVLOZVVGVVPVVCVWCVVFVVOUXBVWCGUVMVVEVVNVVDUVPVVLVNVOVPTVQVRUXEVVJCUWNRUVK + UWNOZUXDVVHDUWAVVIUVKUWNHVSVWDUVLVVCUXCVVGUVKUWNBVTVWDUVRVVFUXBVWDGUVMUVQ + VVEVWDUVOVVDUVPUVKUWNUVNWAWDVOVPWBWEVQWFWNULUVMLUWMXFZUXQPZUVMLUWTXFZUYHP + ZXEZUYNUYTVWFVWHUYNUYTPZULUXQUYHVWJVWEVWGUXQUYHVWJUXNUYHVWJXQZUEUFRUXOUXG + RJZUXJUXOJZPZUXNVWKVWNUXNPZUYEVWJUGUHRUYFVWOUXRRJZUYAUYFJZPZUYEVWJVWOVWRU + YEPZPZUYMUYSPZCRQZVWJVWTVXBUVLUXLUYCUYIMZUVROZPZDUWAQZUVLUXLUYCUYOMZUVROZ + PZDUWAQZPZCRQZVWOVWRUXSVXLUYDVWNUXHVWRUXSPZVXLUXMVWNUXHPZVXMPZUXGUXRXGZRJ + ZVXPBUJZVXCGUVMUVNVXPUKZUVPIZNZOZPZDVXPHIZQZVXRVXGVYAOZPZDVYDQZVXLVXOVWLV + WPVXQVWLVWMUXHVXMXHVXNVWPVWQUXSXIUXGUXRXJWQVXOUILVXPUDMZUIKZUXGUKZUXJIZVY + JUXRUKZUYAIZUPMZNZVYDJZVXRVXCGUVMVXSVYPIZNZOZVYEVXOUIVYIVYLNVYDJZUIVYIVYN + NVYDJZVYQVXOVXPUTJZUXGVXPUJZVWMWUAWUCVXOUXGUXRUEVHUGVHXKZVDZWUDVXOUXGUXRX + LZVDVWLVWMUXHVXMXMZUIUXJUXGVXPXNXOZVXOWUCUXRVXPUJZVWQWUBWUFWUJVXOUXRUXGXP + ZVDVXNVWPVWQUXSXRZUIUYAUXRVXPXNXOZUIVYLVYNVXPXSWQVXOUXGUXRBVWNUXHVXMXTZVX + NVWRUXSYAZUUAZVXOVXCGUVMUXKUYBUPMZNZVYSVXOUVMUTJZUXLUVMYBZUYCUVMYBZVXCWUR + OWUSVXOLBUDYCVDZVXOUXLUVIJZUVMLUXLXFWUTVXOBUTJZUXHVWMWVCWVDVXOFVDZWUNWUHG + UXJUXGBXNXOUXLBYDUVMLUXLYEYFZVXOUYCUVIJZUVMLUYCXFWVAVXOWVDUXSVWQWVGWVEWUO + WULGUYAUXRBXNXOUYCBYDUVMLUYCYEYFZGUVMUXKUYBUPUTYGXOVXOGUVMWUQVYRVXOVUQPZV + YRVXSUXGUKZUXJIZVXSUXRUKZUYAIZUPMZWUQWVIVXSVYIJZVYRWVNOWVIVXPLVXSXFZWVOVU + QBLUVNXFVXRWVPVXOUVNLBUUBWUPBLVXPUVNUUCUUDLVXPVXSUUIWUEUUEUUJZUIVXSVYOWVN + VYIVYPVYJVXSOZVYLWVKVYNWVMUPWVRVYKWVJUXJVYJVXSUXGYIWDZWVRVYMWVLUYAVYJVXSU + XRYIWDZYHVYPWRWVKWVMUPYCWTVJWVKUXKWVMUYBUPWVJUXIUXJWUDWVJUXIOWUGUVNUXGVXP + YJXBYKZWVLUXTUYAWUJWVLUXTOWUKUVNUXRVXPYJXBYKZYLXCVKYMVYCVXRVYTPDVYPVYDUVP + VYPOZVYBVYTVXRWWCVYAVYSVXCWWCGUVMVXTVYRVXSUVPVYPVNVOVPTVQVRVXOUIVYIVYLVYN + URMZNZVYDJZVXRVXGGUVMVXSWWEIZNZOZVYHVXOWUAWUBWWFWUIWUMUIVYLVYNVXPUUFWQWUP + VXOVXGGUVMUXKUYBURMZNZWWHVXOWUSWUTWVAVXGWWKOWVBWVFWVHGUVMUXKUYBURUTYGXOVX + OGUVMWWJWWGWVIWWGWVKWVMURMZWWJWVIWVOWWGWWLOWVQUIVXSWWDWWLVYIWWEWVRVYLWVKV + YNWVMURWVSWVTYHWWEWRWVKWVMURYCWTVJWVKUXKWVMUYBURWWAWWBYLXCVKYMVYGVXRWWIPD + WWEVYDUVPWWEOZVYFWWIVXRWWMVYAWWHVXGWWMGUVMVXTWWGVXSUVPWWEVNVOVPTVQVRVXKVY + EVYHPCVXPRUVKVXPOZVXFVYEVXJVYHWWNVXEVYCDUWAVYDUVKVXPHVSZWWNUVLVXRVXDVYBUV + KVXPBVTZWWNUVRVYAVXCWWNGUVMUVQVXTWWNUVOVXSUVPUVKVXPUVNWAWDVOZVPWBWEWWNVXI + VYGDUWAVYDWWOWWNUVLVXRVXHVYFWWPWWNUVRVYAVXGWWQVPWBWEWBVQVRUUGUUHVWTVXAVXK + CRVWTUYMVXFUYSVXJVWTUYLVXEDUWAVWTUYKVXDUVLVWTUYJVXCUVRVWTUWMUXLUWTUYCUYIV + WNUXHUXMVWSUUKZVWOVWRUXSUYDUULZYHYNTYSVWTUYRVXIDUWAVWTUYQVXHUVLVWTUYPVXGU + VRVWTUWMUXLUWTUYCUYOWWRWWSYHYNTYSWBYSUUMUYMUYSCRUUNVJUUOUUPUUQUURUUSUUTUV + AZUVBVWIUYNUYTWWTUVCUWIUWOOZUWKUWQCDRUWAWXAUWJUWPUVLUWIUWOUVRYOTYPUWIUXBO + ZUWKUXDCDRUWAWXBUWJUXCUVLUWIUXBUVRYOTYPUAUBYTZUWLUVLUWMUVROZPZDUWAQZCRQUX + QWXCUWKWXECDRUWAWXCUWJWXDUVLUWIUWMUVRYOTYPWXFUXPCUERCUEYTZWXFUXHUWMGUVMUX + IUVPIZNZOZPZDUXOQUXPWXGWXEWXKDUWAUXOUVKUXGHVSWXGUVLUXHWXDWXJUVKUXGBVTWXGU + VRWXIUWMWXGGUVMUVQWXHWXGUVOUXIUVPUVKUXGUVNWAWDVOVPWBWEWXKUXNDUFUXODUFYTZW + XJUXMUXHWXLWXIUXLUWMWXLGUVMWXHUXKUXIUVPUXJVNVOVPTYQYRYQYRUAUCYTZUWLUVLUWT + UVROZPZDUWAQZCRQUYHWXMUWKWXOCDRUWAWXMUWJWXNUVLUWIUWTUVRYOTYPWXPUYGCUGRCUG + YTZWXPUXSUWTGUVMUXTUVPIZNZOZPZDUYFQUYGWXQWXOWYADUWAUYFUVKUXRHVSWXQUVLUXSW + XNWXTUVKUXRBVTWXQUVRWXSUWTWXQGUVMUVQWXRWXQUVOUXTUVPUVKUXRUVNWAWDVOVPWBWEW + YAUYEDUHUYFDUHYTZWXTUYDUXSWYBWXSUYCUWTWYBGUVMWXRUYBUXTUVPUYAVNVOVPTYQYRYQ + YRUWIUYJOZUWKUYLCDRUWAWYCUWJUYKUVLUWIUYJUVRYOTYPUWIUYPOZUWKUYRCDRUWAWYDUW + JUYQUVLUWIUYPUVRYOTYPUWIAOZUWKUVTCDRUWAWYEUWJUVSUVLUWIAUVRYOTYPUVDWCUVTUW + HCDRUWAUVSUWGUVLUVRUWFAGEUVMUVQUWEGEYTUVOUWDUVPUVNUWCUVKYIWDWMUVEUVFUVGUV + H $. $} ${ @@ -635034,13 +635034,13 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, ` N ) ) $= ( va vb vp cn0 wcel cn cfv wa cv co cres wceq cc0 wrex cab rexbidv c1 cfz cmzp cdioph simpl simpr eqidd fveq1 eqeq1d anbi2d abbidv weq eqeq1 anbi1d - cmap reseq1 eqeq2d fveqeq2 anbi12d cbvrexv syl6bb cbvabv rspceeqv syl2anc - syl6eq eldioph3b sylanbrc ) DHIZCJUCKZIZLZVHBMZAMZUADUBNZOZPZVMCKQPZLZAHJ - UONZRZBSZEMZFMZVNOZPZWCGMZKZQPZLZFVSRZESZPGVIRZWADUDKIVHVJUEVKVJWAWAPWLVH - VJUFVKWAUGGCVIWKWAWAWFCPZWKWEWCCKZQPZLZFVSRZESWAWMWJWQEWMWIWPFVSWMWHWOWEW - MWGWNQWCWFCUHUIUJTUKWQVTEBEBULZWQVLWDPZWOLZFVSRVTWRWPWTFVSWRWEWSWOWBVLWDU - MUNTWTVRFAVSFAULZWSVPWOVQXAWDVOVLWCVMVNUPUQWCVMQCURUSUTVAVBVEVCVDFEWADGVF - VG $. + cmap reseq1 eqeq2d fveqeq2 anbi12d cbvrexvw syl6bb cbvabv syl6eq rspceeqv + syl2anc eldioph3b sylanbrc ) DHIZCJUCKZIZLZVHBMZAMZUADUBNZOZPZVMCKQPZLZAH + JUONZRZBSZEMZFMZVNOZPZWCGMZKZQPZLZFVSRZESZPGVIRZWADUDKIVHVJUEVKVJWAWAPWLV + HVJUFVKWAUGGCVIWKWAWAWFCPZWKWEWCCKZQPZLZFVSRZESWAWMWJWQEWMWIWPFVSWMWHWOWE + WMWGWNQWCWFCUHUIUJTUKWQVTEBEBULZWQVLWDPZWOLZFVSRVTWRWPWTFVSWRWEWSWOWBVLWD + UMUNTWTVRFAVSFAULZWSVPWOVQXAWDVOVLWCVMVNUPUQWCVMQCURUSUTVAVBVCVDVEFEWADGV + FVG $. $} @@ -635258,19 +635258,19 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, diophrex $p |- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. ( Dioph ` M ) ) -> { t | E. u e. S t = ( u |` ( 1 ... N ) ) } e. ( Dioph ` N ) ) $= ( va vb vd ve vc cn0 wcel cfv cv cres wceq wrex cab wa wex cuz cdioph w3a - c1 cfz co eqeq1 rexbidv reseq1 eqeq2d cbvrexv syl6bb cbvabv cc0 cmap cmzp - cn rexeq abbidv adantl anbi1d rexab r19.41v exbii rexcom4 anass vex resex - anbi2d ceqsexv bitri ancom wss simpl2 fzss2 resabs1 3syl syl5bbr eldioph3 - syl5bb 3ad2antl1 eqeltrd eldioph3b simprbi 3ad2ant3 r19.29a eqeltrrid + c1 cfz co eqeq1 rexbidv reseq1 eqeq2d cbvrexvw syl6bb cbvabv cn cmap cmzp + rexeq abbidv adantl anbi1d rexab r19.41v exbii rexcom4 anass resex anbi2d + cc0 vex ceqsexv bitri ancom wss simpl2 fzss2 resabs1 3syl syl5bb eldioph3 + syl5bbr 3ad2antl1 eqeltrd eldioph3b simprbi 3ad2ant3 r19.29a eqeltrrid adantr ) EKLZDEUAMLZCDUBMLZUCZBNZANZUDEUEUFZOZPZACQZBRFNZGNZWOOZPZGCQZFRZ EUBMZXCWRFBWSWMPZXCWMXAPZGCQWRXFXBXGGCWSWMXAUGUHXGWQGACWTWNPXAWPWMWTWNWOU - IUJUKULUMWLCHNZINZUDDUEUFZOZPZXIJNZMUNPZSZIKUQUOUFZQZHRZPZXDXELJUQUPMZWLX - MXTLZSZXSSXDXBGXRQZFRZXEXSXDYDPYBXSXCYCFXBGCXRURUSUTYBYDXELXSYBYDWSXIWOOZ + IUJUKULUMWLCHNZINZUDDUEUFZOZPZXIJNZMVHPZSZIKUNUOUFZQZHRZPZXDXELJUNUPMZWLX + MXTLZSZXSSXDXBGXRQZFRZXEXSXDYDPYBXSXCYCFXBGCXRUQURUSYBYDXELXSYBYDWSXIWOOZ PZXNSZIXPQZFRZXEYBYCYHFYCWTXKPZXNSZIXPQZXBSZGTZYBYHXQYLXBGHXHWTPZXOYKIXPY - OXLYJXNXHWTXKUGVAUHVBYNYKXBSZIXPQZGTZYBYHYQYMGYKXBIXPVCVDYRYPGTZIXPQYBYHY - PIGXPVEYBYSYGIXPYSXNWSXKWOOZPZSZYBYGYSYJXNXBSZSZGTUUBYPUUDGYJXNXBVFVDUUCU - UBGXKXIXJIVGVHYJXBUUAXNYJXAYTWSWTXKWOUIUJVIVJVKUUBUUAXNSYBYGXNUUAVLYBUUAY - FXNYBYTYEWSYBWJWOXJVMYTYEPWIWJWKYAVNEUDDVOXIWOXJVPVQUJVAVTVTUHVRVRVTUSWIW + OXLYJXNXHWTXKUGUTUHVAYNYKXBSZIXPQZGTZYBYHYQYMGYKXBIXPVBVCYRYPGTZIXPQYBYHY + PIGXPVDYBYSYGIXPYSXNWSXKWOOZPZSZYBYGYSYJXNXBSZSZGTUUBYPUUDGYJXNXBVEVCUUCU + UBGXKXIXJIVIVFYJXBUUAXNYJXAYTWSWTXKWOUIUJVGVJVKUUBUUAXNSYBYGXNUUAVLYBUUAY + FXNYBYTYEWSYBWJWOXJVMYTYEPWIWJWKYAVNEUDDVOXIWOXJVPVQUJUTVRVRUHVTVTVRURWIW JYAYIXELWKIFXMEVSWAWBWHWBWKWIXSJXTQZWJWKDKLUUEIHCDJWCWDWEWFWG $. $} @@ -635288,18 +635288,18 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, ( va vb cn0 wcel cz co cmap cfv wa cc0 wceq crab cv wrex cab nfv syl6eq c1 cfz cmpt cmzp cres cdioph wb wral nfmpt1 nfel1 nfan cvv wss zex nn0ssz mapss mp2an sseli adantl wf mzpf mptfcl imp syl2an adantll fvmpt2 syl2anc - eqid eqcomd eqeq1d ralrimi rabbi sylib nfcv nffvmpt1 nfeq1 fveqeq2 cbvrab - ex df-rab wfn elmapi ffn fnresdm 3syl eqeq2d equcom syl6bb anbi1d rexbiia - ceqsrexbv bitr2i abbii cuz simpl nn0z uzid adantr eldioph syl3anc eqeltrd - syl simpr ) CFGZAHUACUBIZJIZBUCZXEUDKZGZLZBMNZAFXEJIZOZDPZEPZXEUEZNZXOXGK - MNZLZEXLQZDRZCUFKZXJXMXNXLGXNXGKZMNZLZDRZYAXJXMYDDXLOZYFXJXMAPZXGKZMNZAXL - OZYGXJXKYJUGZAXLUHXMYKNXJYLAXLXDXIAXDASAXGXHAXFBUIUJUKXJYHXLGZYLXJYMLZBYI - MYNYIBYNYHXFGZBHGZYIBNYMYOXJXLXFYHHULGFHUMXLXFUMUNUOFHXEULUPUQURZUSXIYMYP - XDXIXFHXGUTZYOYPYMXGXEVAYQYRYOYPAXFBHVBVCVDVEAXFBHXGXGVHVFVGVIVJVSVKXKYJA - XLVLVMYJYDADXLAXLVNDXLVNYJDSAYCMAXFBXNVOVPYHXNMXGVQVRTYDDXLVTTYEXTDXTXOXN - NZXRLZEXLQYEXSYTEXLXOXLGZXQYSXRUUAXQXNXONYSUUAXPXOXNUUAXEFXOUTXOXEWAXPXON - XOFXEWBXEFXOWCXEXOWDWEWFDEWGWHWIWJXRYDEXNXLXOXNMXGVQWKWLWMTXJXDCCWNKGZXIY - AYBGXDXIWOXDUUBXIXDCHGUUBCWPCWQXBWRXDXIXCEDXGCCWSWTXA $. + eqid eqcomd eqeq1d ralrimi rabbi sylib nfcv nffvmpt1 nfeq1 fveqeq2 df-rab + cbvrabw wfn elmapi ffn fnresdm 3syl eqeq2d equcom syl6bb anbi1d ceqsrexbv + rexbiia bitr2i abbii cuz simpl nn0z uzid syl adantr simpr eldioph syl3anc + ex eqeltrd ) CFGZAHUACUBIZJIZBUCZXEUDKZGZLZBMNZAFXEJIZOZDPZEPZXEUEZNZXOXG + KMNZLZEXLQZDRZCUFKZXJXMXNXLGXNXGKZMNZLZDRZYAXJXMYDDXLOZYFXJXMAPZXGKZMNZAX + LOZYGXJXKYJUGZAXLUHXMYKNXJYLAXLXDXIAXDASAXGXHAXFBUIUJUKXJYHXLGZYLXJYMLZBY + IMYNYIBYNYHXFGZBHGZYIBNYMYOXJXLXFYHHULGFHUMXLXFUMUNUOFHXEULUPUQURZUSXIYMY + PXDXIXFHXGUTZYOYPYMXGXEVAYQYRYOYPAXFBHVBVCVDVEAXFBHXGXGVHVFVGVIVJXBVKXKYJ + AXLVLVMYJYDADXLAXLVNDXLVNYJDSAYCMAXFBXNVOVPYHXNMXGVQVSTYDDXLVRTYEXTDXTXOX + NNZXRLZEXLQYEXSYTEXLXOXLGZXQYSXRUUAXQXNXONYSUUAXPXOXNUUAXEFXOUTXOXEVTXPXO + NXOFXEWAXEFXOWBXEXOWCWDWEDEWFWGWHWJXRYDEXNXLXOXNMXGVQWIWKWLTXJXDCCWMKGZXI + YAYBGXDXIWNXDUUBXIXDCHGUUBCWOCWPWQWRXDXIWSEDXGCCWTXAXC $. $( Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so @@ -635485,7 +635485,7 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) $) sbccomieg $p |- ( [. A / a ]. [. B / b ]. ph <-> [. C / b ]. [. A / a ]. ph ) $= - ( wsbc cvv wcel sbcex wex spesbc exlimiv syl nfcv nfsbc1v nfsbc cv wceq + ( wsbc cvv wcel sbcex wex spesbc exlimiv syl nfcv nfsbc1v nfsbcw cv wceq sbceq1a sbceqbid sbciegf pm5.21nii ) AFCHZEBHBIJZAEBHZFDHZUEEBKUHUGFLUFUG FDMUGUFFAEBKNOUEUHEBIUGEFDEDPAEBQRESBTAUGFCDGAEBUAUBUCUD $. $} @@ -635945,12 +635945,12 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } e. ( Dioph ` N ) ) $= ( va vb vp cn0 wcel co cun cfv cv cc0 wceq wrex cfz cmzp cmap crab cdioph - c1 weq uneq1 fveqeq2d rexbidv uneq2 cbvrexv syl6bb cbvrabv eqeq1d rabbidv - wa fveq1 rspceeqv mpan2 anim2i eldioph4b sylibr ) DLMZCEUFDUANZOUBPZMZUQV - DBQZAQZOZCPRSZALEUCNZTZBLVEUCNZUDZIQZJQZOZKQZPZRSZJVLTZIVNUDZSKVFTZUQVODU - EPMVGWDVDVGVOVRCPZRSZJVLTZIVNUDZSWDVMWGBIVNBIUGZVMVPVIOZCPRSZAVLTWGWIVKWK - AVLWIVJWJRCVHVPVIUHUIUJWKWFAJVLAJUGWJVRRCVIVQVPUKUIULUMUNKCVFWCWHVOVSCSZW - BWGIVNWLWAWFJVLWLVTWERVRVSCURUOUJUPUSUTVAJIVODEKFGHVBVC $. + c1 weq uneq1 fveqeq2d rexbidv uneq2 cbvrexvw syl6bb cbvrabv fveq1 rabbidv + wa eqeq1d rspceeqv mpan2 anim2i eldioph4b sylibr ) DLMZCEUFDUANZOUBPZMZUQ + VDBQZAQZOZCPRSZALEUCNZTZBLVEUCNZUDZIQZJQZOZKQZPZRSZJVLTZIVNUDZSKVFTZUQVOD + UEPMVGWDVDVGVOVRCPZRSZJVLTZIVNUDZSWDVMWGBIVNBIUGZVMVPVIOZCPRSZAVLTWGWIVKW + KAVLWIVJWJRCVHVPVIUHUIUJWKWFAJVLAJUGWJVRRCVIVQVPUKUIULUMUNKCVFWCWHVOVSCSZ + WBWGIVNWLWAWFJVLWLVTWERVRVSCUOURUJUPUSUTVAJIVODEKFGHVBVC $. $} ${ @@ -636074,18 +636074,18 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, fphpd $p |- ( ph -> E. x e. A E. y e. A ( x =/= y /\ C = D ) ) $= ( va wceq cv wi wral wn wa wrex wcel csb vb wne cdom wbr csdm domnsym cvv nsyl3 relsdom brrelex1i syl adantr nfv nfcsb1v nfim eleq1w anbi2d csbeq1a - nfel1 eleq1d imbi12d chvar ex csbid vex csbie eqeq12i imbi1i 2ralbii nfeq - wb csbeq1 eqeq1d equequ1 eqeq2d equequ2 rspc2 com12 sylbir impbid1 adantl - id syl6 dom2d mtand ancom df-ne anbi1i pm4.61 3bitr4i rexbii rexnal bitri - mpd sylibr ) AFGLZBMZCMZLZNZCDOZBDOZPZWQWRUBZWPQZCDRZBDRZAXBDEUCUDZXHEDUE - UDZADEUFHUHAXBQZEUGSZXHAXKXBAXIXKHEDUEUIUJUKULXJKUADEBKMZFTZBUAMZFTZUGAXL - DSZXMESZNXBAXPXQAWQDSZQZFESZNAXPQZXQNBKYAXQBYABUMBXMEBXLFUNZUSUOWQXLLZXSY - AXTXQYCXRXPABKDUPUQYCFXMEBXLFURUTVAIVBVCULXBXPXNDSQZXMXOLZXLXNLZVKZNAXBYD - YEYFNZYGXBBWQFTZBWRFTZLZWSNZCDOBDOZYDYHNYLWTBCDDYKWPWSYIFYJGBFVDBWRFGCVEJ - VFVGVHVIYDYMYHYLYHXMYJLZXLWRLZNBCXLXNDDYNYOBBXMYJYBBWRFUNVJYOBUMUOYHCUMYC - YKYNWSYOYCYIXMYJBWQXLFVLVMBKCVNVAWRXNLZYNYEYOYFYPYJXOXMBWRXNFVLVOCUAKVPVA - VQVRVSYHYEYFYHWBBXLXNFVLVTWCWAWDWNWEXGXAPZBDRXCXFYQBDXFWTPZCDRYQXEYRCDWSP - ZWPQWPYSQXEYRYSWPWFXDYSWPWQWRWGWHWPWSWIWJWKWTCDWLWMWKXABDWLWMWO $. + nfel1 eleq1d imbi12d chvarfv ex wb csbid vex csbie eqeq12i imbi1i 2ralbii + nfeq csbeq1 eqeq1d equequ1 eqeq2d equequ2 rspc2 com12 sylbir impbid1 syl6 + id adantl dom2d mpd mtand ancom df-ne anbi1i pm4.61 3bitr4i rexbii rexnal + bitri sylibr ) AFGLZBMZCMZLZNZCDOZBDOZPZWQWRUBZWPQZCDRZBDRZAXBDEUCUDZXHED + UEUDZADEUFHUHAXBQZEUGSZXHAXKXBAXIXKHEDUEUIUJUKULXJKUADEBKMZFTZBUAMZFTZUGA + XLDSZXMESZNXBAXPXQAWQDSZQZFESZNAXPQZXQNBKYAXQBYABUMBXMEBXLFUNZUSUOWQXLLZX + SYAXTXQYCXRXPABKDUPUQYCFXMEBXLFURUTVAIVBVCULXBXPXNDSQZXMXOLZXLXNLZVDZNAXB + YDYEYFNZYGXBBWQFTZBWRFTZLZWSNZCDOBDOZYDYHNYLWTBCDDYKWPWSYIFYJGBFVEBWRFGCV + FJVGVHVIVJYDYMYHYLYHXMYJLZXLWRLZNBCXLXNDDYNYOBBXMYJYBBWRFUNVKYOBUMUOYHCUM + YCYKYNWSYOYCYIXMYJBWQXLFVLVMBKCVNVAWRXNLZYNYEYOYFYPYJXOXMBWRXNFVLVOCUAKVP + VAVQVRVSYHYEYFYHWBBXLXNFVLVTWAWCWDWEWFXGXAPZBDRXCXFYQBDXFWTPZCDRYQXEYRCDW + SPZWPQWPYSQXEYRYSWPWGXDYSWPWQWRWHWIWPWSWJWKWLWTCDWMWNWLXABDWMWNWO $. $} ${ @@ -636103,21 +636103,21 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, ( vb vc wa clt wcel cv wne cmpt cfv wceq wbr fmpttd ffvelrnda fveq2 fphpd wo cr sselda adantrr adantr adantrl lttri2d simprl ad2antrr simprr simplr wrex simpr breq1 fveqeq2 anbi12d breq2 eqeq2d rspc2ev syl112anc ex eqcomd - weq jaod eqid eleq1w anbi2d eleq1d imbi12d chvarv fvmptd3 adantlr eqeq12d - wi biimpd anim2d reximdva syld sylbid expimpd ancomsd rexlimdvva mpd ) AP - UAZQUAZUBZWNDEGUCZUDZWOWQUDZUEZRZQEVBPEVBBUAZCUAZSUFZHIUEZRZCEVBZBEVBZAPQ - EFWRWSLAEFWNWQADEGFMUGUHWNWOWQUIUJAXAXHPQEEAWNETZWOETZRZRZWTWPXHXLWTWPXHX - LWTRZWPWNWOSUFZWOWNSUFZUKZXHXMWNWOXLWNULTZWTAXIXQXJAEULWNJUMUNUOXLWOULTZW - TAXJXRXIAEULWOJUMUPUOUQXMXPXDXBWQUDZXCWQUDZUEZRZCEVBZBEVBZXHXMXNYDXOXMXNY - DXMXNRXIXJXNWTYDXLXIWTXNAXIXJURZUSXLXJWTXNAXIXJUTZUSXMXNVCXLWTXNVAYBXNWTR - WNXCSUFZWRXTUEZRBCWNWOEEBPVMXDYGYAYHXBWNXCSVDXBWNXTWQVEVFCQVMZYGXNYHWTXCW - OWNSVGYIXTWSWRXCWOWQUIVHVFVIVJVKXMXOYDXMXORZXJXIXOWSWRUEZYDXLXJWTXOYFUSXL - XIWTXOYEUSXMXOVCYJWRWSXLWTXOVAVLYBXOYKRWOXCSUFZWSXTUEZRBCWOWNEEBQVMXDYLYA - YMXBWOXCSVDXBWOXTWQVEVFCPVMZYLXOYMYKXCWNWOSVGYNXTWRWSXCWNWQUIVHVFVIVJVKVN - AYDXHWDXKWTAYCXGBEAXBETZRZYBXFCEYPXCETZRZYAXEXDYRYAXEYRXSHXTIYRDXBGHEWQFW - QVOZNAYOYQVAYPHFTZYQADUAETZRZGFTZWDZYPYTWDDBDBVMZUUBYPUUCYTUUEUUAYOADBEVP - VQUUEGHFNVRVSMVTUOWAYRDXCGIEWQFYSOYPYQVCAYQIFTZYOUUDAYQRZUUFWDDCDCVMZUUBU - UGUUCUUFUUHUUAYQADCEVPVQUUHGIFOVRVSMVTWBWAWCWEWFWGWGUSWHWIWJWKWLWM $. + jaod wi eqid eleq1w anbi2d eleq1d imbi12d chvarvv fvmptd3 adantlr eqeq12d + weq biimpd anim2d reximdva syld sylbid expimpd ancomsd rexlimdvva mpd ) A + PUAZQUAZUBZWNDEGUCZUDZWOWQUDZUEZRZQEVBPEVBBUAZCUAZSUFZHIUEZRZCEVBZBEVBZAP + QEFWRWSLAEFWNWQADEGFMUGUHWNWOWQUIUJAXAXHPQEEAWNETZWOETZRZRZWTWPXHXLWTWPXH + XLWTRZWPWNWOSUFZWOWNSUFZUKZXHXMWNWOXLWNULTZWTAXIXQXJAEULWNJUMUNUOXLWOULTZ + WTAXJXRXIAEULWOJUMUPUOUQXMXPXDXBWQUDZXCWQUDZUEZRZCEVBZBEVBZXHXMXNYDXOXMXN + YDXMXNRXIXJXNWTYDXLXIWTXNAXIXJURZUSXLXJWTXNAXIXJUTZUSXMXNVCXLWTXNVAYBXNWT + RWNXCSUFZWRXTUEZRBCWNWOEEBPWDXDYGYAYHXBWNXCSVDXBWNXTWQVEVFCQWDZYGXNYHWTXC + WOWNSVGYIXTWSWRXCWOWQUIVHVFVIVJVKXMXOYDXMXORZXJXIXOWSWRUEZYDXLXJWTXOYFUSX + LXIWTXOYEUSXMXOVCYJWRWSXLWTXOVAVLYBXOYKRWOXCSUFZWSXTUEZRBCWOWNEEBQWDXDYLY + AYMXBWOXCSVDXBWOXTWQVEVFCPWDZYLXOYMYKXCWNWOSVGYNXTWRWSXCWNWQUIVHVFVIVJVKV + MAYDXHVNXKWTAYCXGBEAXBETZRZYBXFCEYPXCETZRZYAXEXDYRYAXEYRXSHXTIYRDXBGHEWQF + WQVOZNAYOYQVAYPHFTZYQADUAETZRZGFTZVNZYPYTVNDBDBWDZUUBYPUUCYTUUEUUAYOADBEV + PVQUUEGHFNVRVSMVTUOWAYRDXCGIEWQFYSOYPYQVCAYQIFTZYOUUDAYQRZUUFVNDCDCWDZUUB + UUGUUCUUFUUHUUAYQADCEVPVQUUHGIFOVRVSMVTWBWAWCWEWFWGWGUSWHWIWJWKWLWM $. $} $( An infinite subset of a countable set is countable, without using choice. @@ -638364,36 +638364,37 @@ group element in (1,2), contradicting ~ pell14qrgapw . (Contributed by by Stefan O'Rear, 24-Sep-2014.) $) monotuz $p |- ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( A < B <-> D < E ) ) $= ( wcel va vb vc vd wa clt wbr csb cv csbeq1 cuz cr cz uzssz zssre eqsstri - cfv sstri wi nfv nfcsb1v nfel1 nfim weq eleq1 anbi2d csbeq1a eleq1d chvar - imbi12d simpl adantlrr simplrl sseldi simplrr simpr c1 wceq breq2d imbi2d - caddc co vex csbie syl5eqr ovex oveq1 csbeq1d breq12d vtoclg w3a 3ad2ant2 - simp2l cle zre 3ad2ant1 simp3 wb simp11 simp12 eluz syl2anc mpbird simp2r - ltled syl6eleq uztrn eleqtrrdi peano2uz syl vtoclf lttrd 3exp a2d syl3anc - uzind2 mpd ex ltord1 nfcvd csbiegf breqan12d adantl bitrd ) ADKTZEKTZUEZU - EDEUFUGBDFUHZBEFUHZUFUGZGHUFUGZAUAUBBUAUIZFUHZBUBUIZFUHZDEKYHYIBYLYNFUJBY - LDFUJBYLEFUJKLUKUQZULOYPUMULLUNZUOURUPABUIZKTZUEZFULTZUSZAYLKTZUEZYMULTZU - SBUAUUDUUEBUUDBUTBYMULBYLFVAVBVCBUAVDZYTUUDUUAUUEUUFYSUUCAYRYLKVEVFUUFFYM - ULBYLFVGVHVJNVIZAUUCYNKTZUEUEZYLYNUFUGZYMYOUFUGZUUIUUJUEZUUDUUKAUUCUUJUUD - UUHUUDUUJVKVLUULYLUMTZYNUMTUUJUUDUUKUSZUULKUMYLKYPUMOYQUPZAUUCUUHUUJVMVNU - ULKUMYNUUOAUUCUUHUUJVOVNUUIUUJVPUUDYMBUCUIZFUHZUFUGZUSUUDYMBYLVQWAWBZFUHZ - UFUGZUSZUUDYMBUDUIZFUHZUFUGZUSUUDYMBUVCVQWAWBZFUHZUFUGZUSUUNUCUDYLYNUUPUU - SVRZUURUVAUUDUVIUUQUUTYMUFBUUPUUSFUJVSVTUCUDVDZUURUVEUUDUVJUUQUVDYMUFBUUP - UVCFUJVSVTUUPUVFVRZUURUVHUUDUVKUUQUVGYMUFBUUPUVFFUJVSVTUCUBVDZUURUUKUUDUV - LUUQYOYMUFBUUPYNFUJVSVTACUIZKTZUEZIJUFUGZUSZUVBCYLUMCUAVDZUVOUUDUVPUVAUVR - UVNUUCAUVMYLKVEVFUVRIYMJUUTUFUVRIBUVMFUHZYMBUVMFICWCQWDZBUVMYLFUJWEUVRJBU - VMVQWAWBZFUHZUUTBUWAFJUVMVQWAWFPWDZUVRBUWAUUSFUVMYLVQWAWGWHWEWIVJMWJUUMUV - CUMTZYLUVCUFUGZWKZUUDUVEUVHUWFUUDUVEUVHUWFUUDUVEWKZYMUVDUVGUUDUWFUUEUVEUU - GWLUWGAUVCKTZUVDULTZUWFAUUCUVEWMZUWGUVCYPKUWGUVCYLUKUQTZYLYPTUVCYPTZUWGUW - KYLUVCWNUGZUWFUUDUWMUVEUWFYLUVCUUMUWDYLULTUWEYLWOWPUWDUUMUVCULTUWEUVCWOWL - UUMUWDUWEWQXEWPUWGUUMUWDUWKUWMWRUUMUWDUWEUUDUVEWSUUMUWDUWEUUDUVEWTYLUVCXA - XBXCUWGYLKYPUWFAUUCUVEXDOXFYLUVCLXGXBZOXHZUUBAUWHUEZUWIUSBUDUWPUWIBUWPBUT - BUVDULBUVCFVAVBVCBUDVDZYTUWPUUAUWIUWQYSUWHAYRUVCKVEVFUWQFUVDULBUVCFVGVHVJ - NVIXBUWGAUVFKTZUVGULTZUWJUWGUVFYPKUWGUWLUVFYPTUWNLUVCXIXJOXHUUBAUWRUEZUWS - USBUVFUWTUWSBUWTBUTBUVGULBUVFFVAVBVCUVCVQWAWFYRUVFVRZYTUWTUUAUWSUXAYSUWRA - YRUVFKVEVFUXAFUVGULBUVFFVGVHVJNXKXBUWFUUDUVEWQUWGAUWHUVDUVGUFUGZUWJUWOUVQ - UWPUXBUSZCUDUXCCUTCUDVDZUVOUWPUVPUXBUXDUVNUWHAUVMUVCKVEVFUXDIUVDJUVGUFUXD - IUVSUVDUVTBUVMUVCFUJWEUXDJUWBUVGUWCUXDBUWAUVFFUVMUVCVQWAWGWHWEWIVJMVIXBXL - XMXNXPXOXQXRXSYGYJYKWRAYEYFYHGYIHUFBDFGKYEBGXTRYABEFHKYFBHXTSYAYBYCYD $. + cfv sstri nfv nfcsb1v nfel1 nfim weq eleq1 anbi2d csbeq1a imbi12d chvarfv + wi eleq1d simpl adantlrr simplrl sseldi simplrr simpr caddc breq2d imbi2d + c1 co wceq vex csbie syl5eqr ovex oveq1 csbeq1d breq12d vtoclg w3a simp2l + 3ad2ant2 cle zre 3ad2ant1 simp3 ltled wb simp11 simp12 eluz mpbird simp2r + syl2anc syl6eleq uztrn eleqtrrdi peano2uz syl vtoclf lttrd uzind2 syl3anc + 3exp a2d mpd ex ltord1 nfcvd csbiegf breqan12d adantl bitrd ) ADKTZEKTZUE + ZUEDEUFUGBDFUHZBEFUHZUFUGZGHUFUGZAUAUBBUAUIZFUHZBUBUIZFUHZDEKYHYIBYLYNFUJ + BYLDFUJBYLEFUJKLUKUQZULOYPUMULLUNZUOURUPABUIZKTZUEZFULTZVIZAYLKTZUEZYMULT + ZVIBUAUUDUUEBUUDBUSBYMULBYLFUTVAVBBUAVCZYTUUDUUAUUEUUFYSUUCAYRYLKVDVEUUFF + YMULBYLFVFVJVGNVHZAUUCYNKTZUEUEZYLYNUFUGZYMYOUFUGZUUIUUJUEZUUDUUKAUUCUUJU + UDUUHUUDUUJVKVLUULYLUMTZYNUMTUUJUUDUUKVIZUULKUMYLKYPUMOYQUPZAUUCUUHUUJVMV + NUULKUMYNUUOAUUCUUHUUJVOVNUUIUUJVPUUDYMBUCUIZFUHZUFUGZVIUUDYMBYLVTVQWAZFU + HZUFUGZVIZUUDYMBUDUIZFUHZUFUGZVIUUDYMBUVCVTVQWAZFUHZUFUGZVIUUNUCUDYLYNUUP + UUSWBZUURUVAUUDUVIUUQUUTYMUFBUUPUUSFUJVRVSUCUDVCZUURUVEUUDUVJUUQUVDYMUFBU + UPUVCFUJVRVSUUPUVFWBZUURUVHUUDUVKUUQUVGYMUFBUUPUVFFUJVRVSUCUBVCZUURUUKUUD + UVLUUQYOYMUFBUUPYNFUJVRVSACUIZKTZUEZIJUFUGZVIZUVBCYLUMCUAVCZUVOUUDUVPUVAU + VRUVNUUCAUVMYLKVDVEUVRIYMJUUTUFUVRIBUVMFUHZYMBUVMFICWCQWDZBUVMYLFUJWEUVRJ + BUVMVTVQWAZFUHZUUTBUWAFJUVMVTVQWFPWDZUVRBUWAUUSFUVMYLVTVQWGWHWEWIVGMWJUUM + UVCUMTZYLUVCUFUGZWKZUUDUVEUVHUWFUUDUVEUVHUWFUUDUVEWKZYMUVDUVGUUDUWFUUEUVE + UUGWMUWGAUVCKTZUVDULTZUWFAUUCUVEWLZUWGUVCYPKUWGUVCYLUKUQTZYLYPTUVCYPTZUWG + UWKYLUVCWNUGZUWFUUDUWMUVEUWFYLUVCUUMUWDYLULTUWEYLWOWPUWDUUMUVCULTUWEUVCWO + WMUUMUWDUWEWQWRWPUWGUUMUWDUWKUWMWSUUMUWDUWEUUDUVEWTUUMUWDUWEUUDUVEXAYLUVC + XBXEXCUWGYLKYPUWFAUUCUVEXDOXFYLUVCLXGXEZOXHZUUBAUWHUEZUWIVIBUDUWPUWIBUWPB + USBUVDULBUVCFUTVAVBBUDVCZYTUWPUUAUWIUWQYSUWHAYRUVCKVDVEUWQFUVDULBUVCFVFVJ + VGNVHXEUWGAUVFKTZUVGULTZUWJUWGUVFYPKUWGUWLUVFYPTUWNLUVCXIXJOXHUUBAUWRUEZU + WSVIBUVFUWTUWSBUWTBUSBUVGULBUVFFUTVAVBUVCVTVQWFYRUVFWBZYTUWTUUAUWSUXAYSUW + RAYRUVFKVDVEUXAFUVGULBUVFFVFVJVGNXKXEUWFUUDUVEWQUWGAUWHUVDUVGUFUGZUWJUWOU + VQUWPUXBVIZCUDUXCCUSCUDVCZUVOUWPUVPUXBUXDUVNUWHAUVMUVCKVDVEUXDIUVDJUVGUFU + XDIUVSUVDUVTBUVMUVCFUJWEUXDJUWBUVGUWCUXDBUWAUVFFUVMUVCVTVQWGWHWEWIVGMVHXE + XLXOXPXMXNXQXRXSYGYJYKWSAYEYFYHGYIHUFBDFGKYEBGXTRYABEFHKYFBHXTSYAYBYCYD + $. $} ${