Skip to content

Commit e1fad28

Browse files
author
icecream17
authored
partial work
1 parent 46f582f commit e1fad28

File tree

2 files changed

+204
-16
lines changed

2 files changed

+204
-16
lines changed

‎changes-set.txt‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -99,9 +99,10 @@ make a github issue.)
9999

100100
DONE:
101101
Date Old New Notes
102-
20-Aug-24 brsnop [same] moved from TA's mathbox to main set.mm
102+
20-Aug-24 uzssre [same] moved from GS's mathbox to main set.mm
103+
20-Aug-24 brsnop [same] moved from TA's mathbox to main set.mm
103104
19-Aug-24 dfrp2 [same] moved from TA's mathbox to main set.mm
104-
19-Aug-24 rabeqcda [same] moved from SN's mathbox to main set.mm
105+
19-Aug-24 rabeqcda [same] moved from SN's mathbox to main set.mm
105106
18-Aug-24 prdsco [same] revised - compatibility with new df-prds
106107
18-Aug-24 prdshom [same] revised - compatibility with new df-prds
107108
18-Aug-24 prdstset [same] revised - compatibility with new df-prds

‎set.mm‎

Lines changed: 201 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -131784,15 +131784,20 @@ nonnegative integers (cont.)". $)
131784131784
EZBJEZUHUGKZABLZABMZUIAQEBQEUKUJANBNABROPSUCUJUIUFUGKZUMULUJUEJEUDJEUNUIBTA
131785131785
TUEUDUAOPUB $.
131786131786

131787+
$( An upper set of integers is a subset of all integers. (Contributed by NM,
131788+
2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) $)
131789+
uzssz $p |- ( ZZ>= ` M ) C_ ZZ $=
131790+
( cuz cdm wcel cfv cz wss cpw ffvelrni elpwid fdmi eleq2s wn ndmfv eqsstrdi
131791+
uzf c0 0ss pm2.61i ) ABCZDZABEZFGZUCAFTAFDUBFFFHZABPIJFUDBPKLUAMUBQFABNFROS
131792+
$.
131793+
131794+
$( An upper set of integers is a subset of the reals. (Contributed by Glauco
131795+
Siliprandi, 23-Oct-2021.) $)
131796+
uzssre $p |- ( ZZ>= ` M ) C_ RR $=
131797+
( cuz cfv cz cr uzssz zssre sstri ) ABCDEAFGH $.
131798+
131787131799
${
131788131800
$d k M $. $d k N $.
131789-
$( An upper set of integers is a subset of all integers. (Contributed by
131790-
NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) $)
131791-
uzssz $p |- ( ZZ>= ` M ) C_ ZZ $=
131792-
( cuz cdm wcel cfv cz wss cpw uzf ffvelrni elpwid fdmi eleq2s wn c0 ndmfv
131793-
0ss eqsstrdi pm2.61i ) ABCZDZABEZFGZUCAFTAFDUBFFFHZABIJKFUDBILMUANUBOFABP
131794-
FQRS $.
131795-
131796131801
$( Subset relationship for two sets of upper integers. (Contributed by NM,
131797131802
5-Sep-2005.) $)
131798131803
uzss $p |- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) ) $=
@@ -643213,6 +643218,18 @@ D Fn ( I ... ( M - 1 ) ) /\
643213643218
$( $j usage '19.9dev' avoids 'ax-10'; $)
643214643219
$}
643215643220

643221+
${
643222+
$d A x $. $d B x $. $d ch x $.
643223+
rspcedvdw.s $e |- ( x = A -> ( ps <-> ch ) ) $.
643224+
rspcedvdw.1 $e |- ( ph -> A e. B ) $.
643225+
rspcedvdw.2 $e |- ( ph -> ch ) $.
643226+
$( Version of ~ rspcedvd where the implicit substitution hypothesis does
643227+
not have an antecedent, which also avoids a disjoint variable condition
643228+
on ` ph , x ` . (Contributed by SN, 20-Aug-2024.) $)
643229+
rspcedvdw $p |- ( ph -> E. x e. B ps ) $=
643230+
( wcel wrex rspcev syl2anc ) AEFJCBDFKHIBCDEFGLM $.
643231+
$}
643232+
643216643233
${
643217643234
$d ph x y z $. $d ch x $. $d th y $. $d ta z $. $d D x y z $.
643218643235
$d A x y z $. $d B y z $. $d C z $.
@@ -645688,8 +645705,10 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
645688645705
exp11d.3 $e |- ( ph -> N e. ZZ ) $.
645689645706
exp11d.4 $e |- ( ph -> N =/= 0 ) $.
645690645707
exp11d.5 $e |- ( ph -> ( A ^ N ) = ( B ^ N ) ) $.
645691-
$( ~ sq11d for positive real bases and nonzero exponents. (Contributed by
645692-
Steven Nguyen, 6-Apr-2023.) $)
645708+
$( ~ sq11d for positive real bases and nonzero exponents. The base cannot
645709+
be generalized much further, since if ` N ` is even then we have
645710+
` A ^ N = -u A ^ N ` . TODO-SN: Avoid ~ df-cxp . (Contributed by SN,
645711+
6-Apr-2023.) $)
645693645712
exp11d $p |- ( ph -> A = B ) $=
645694645713
( ccxp co c1 cexp rpcnd rpne0d cxpexpzd oveq2d cxpmuld cxp1d 3eqtr3d cdiv
645695645714
3eqtr4d oveq1d cmul zcnd recidd zred reccld ) ABDJKZLDUAKZJKZCDJKZUJJKZBC
@@ -645698,6 +645717,20 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
645698645717
USUTRACUOSTT $.
645699645718
$}
645700645719

645720+
$( ~ dvdssqlem generalized to positive integer exponents. (Contributed by
645721+
SN, 20-Aug-2024.) $)
645722+
dvdsexplem $p |- ( ( A e. NN /\ B e. NN /\ N e. NN ) ->
645723+
( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) $=
645724+
( cn wcel w3a cdvds wbr cexp co cz cn0 nnz wa nnrpd 3adant3 adantr nnexpcld
645725+
cgcd wceq wi nnnn0 dvdsexpim syl3an crp gcdnncl simpl1 simpl3 nnne0d expgcd
645726+
nnzd syl3an3 simp1 3ad2ant3 simp2 gcdeq syl2anc biimpar eqtrd exp11d simprd
645727+
wb gcddvds syl2an eqbrtrrd ex impbid ) ADEZBDEZCDEZFZABGHZACIJZBCIJZGHZVHAK
645728+
EZVIBKEZVJCLEZVLVOUAAMZBMZCUBZABCUCUDVKVOVLVKVONZABSJZABGWBWCACVKWCUEEZVOVH
645729+
VIWDVJVHVINWCABUFOPQWBAVHVIVJVOUGOWBCVHVIVJVOUHZUKWBCWEUIWBWCCIJZVMVNSJZVMV
645730+
KWFWGTZVOVJVHVIVRWHWAABCUJULQVKWGVMTZVOVKVMDEVNDEWIVOVBVKACVHVIVJUMVJVHVRVI
645731+
WAUNZRVKBCVHVIVJUOWJRVMVNUPUQURUSUTVKWCBGHZVOVHVIWKVJVHVPVQWKVIVSVTVPVQNWCA
645732+
GHWKABVCVAVDPQVEVFVG $.
645733+
645701645734
${
645702645735
ltexp1d.1 $e |- ( ph -> A e. RR+ ) $.
645703645736
ltexp1d.2 $e |- ( ph -> B e. RR+ ) $.
@@ -647466,7 +647499,7 @@ standardize vectors to a length (norm) of one, but such definitions require
647466647499
prjspnenm1.g $e |- G = ??? $.
647467647500
@( A bijection between an n-dimensional projective space and its
647468647501
(n-1)-dimensional affine and projective spaces. (Contributed by Steven
647469-
Nguyen, ??-??-2023.) @)
647502+
Nguyen, ??-???-202?.) @)
647470647503
prjspnf1om1 @p |- ( ( N e. NN /\ K e. DivRing ) ->
647471647504
( F u. G ) : ( N PrjSpn K ) -1-1-onto-> (
647472647505
( ( K ^m ( 0 ..^ ( N - 1 ) ) ) |_| ( ( N - 1 ) PrjSpn K ) ) ) @=
@@ -647669,6 +647702,164 @@ standardize vectors to a length (norm) of one, but such definitions require
647669647702
IUWJUWKUWLUWM $.
647670647703
$}
647671647704

647705+
${
647706+
fltmul.s $e |- ( ph -> S e. CC ) $.
647707+
fltmul.a $e |- ( ph -> A e. CC ) $.
647708+
fltmul.b $e |- ( ph -> B e. CC ) $.
647709+
fltmul.c $e |- ( ph -> C e. CC ) $.
647710+
fltmul.n $e |- ( ph -> N e. NN0 ) $.
647711+
fltmul.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
647712+
$( A counterexample to FLT stays valid when scaled. The hypotheses are
647713+
more general than they need to be for convenience. (There does not seem
647714+
to be a standard term for Fermat or Pythagorean triples extended to any
647715+
` N e. NN0 ` , hence the label is more about the context in which this
647716+
theorem is used). (Contributed by SN, 20-Aug-2024.) $)
647717+
fltmul $p |- ( ph
647718+
-> ( ( ( S x. A ) ^ N ) + ( ( S x. B ) ^ N ) ) = ( ( S x. C ) ^ N ) ) $=
647719+
( cexp co cmul caddc expcld adddid oveq2d mulexpd eqtr3d oveq12d 3eqtr4d
647720+
) AEFMNZBFMNZONZUDCFMNZONZPNZUDDFMNZONZEBONFMNZECONFMNZPNEDONFMNAUDUEUGPN
647721+
ZONUIUKAUDUEUGAEFGKQABFHKQACFIKQRAUNUJUDOLSUAAULUFUMUHPAEBFGHKTAECFGIKTUB
647722+
AEDFGJKTUC $.
647723+
$}
647724+
647725+
${
647726+
fltdiv.s $e |- ( ph -> S e. CC ) $.
647727+
fltdiv.0 $e |- ( ph -> S =/= 0 ) $.
647728+
fltdiv.a $e |- ( ph -> A e. CC ) $.
647729+
fltdiv.b $e |- ( ph -> B e. CC ) $.
647730+
fltdiv.c $e |- ( ph -> C e. CC ) $.
647731+
fltdiv.n $e |- ( ph -> N e. NN0 ) $.
647732+
fltdiv.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
647733+
$( A counterexample to FLT stays valid when scaled. The hypotheses are
647734+
more general than they need to be for convenience. (Contributed by SN,
647735+
20-Aug-2024.) $)
647736+
fltdiv $p |- ( ph
647737+
-> ( ( ( A / S ) ^ N ) + ( ( B / S ) ^ N ) ) = ( ( C / S ) ^ N ) ) $=
647738+
( cexp co cdiv caddc expcld nn0zd expdivd expne0d divdird oveq12d 3eqtr4d
647739+
oveq1d eqtr3d ) ABFNOZEFNOZPOZCFNOZUHPOZQOZDFNOZUHPOZBEPOFNOZCEPOFNOZQODE
647740+
POFNOAUGUJQOZUHPOULUNAUGUJUHABFILRACFJLRAEFGLRAEFGHAFLSUAUBAUQUMUHPMUEUFA
647741+
UOUIUPUKQABEFIGHLTACEFJGHLTUCADEFKGHLTUD $.
647742+
$}
647743+
647744+
${
647745+
flt0.a $e |- ( ph -> A e. CC ) $.
647746+
flt0.b $e |- ( ph -> B e. CC ) $.
647747+
flt0.c $e |- ( ph -> C e. CC ) $.
647748+
flt0.n $e |- ( ph -> N e. NN0 ) $.
647749+
flt0.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
647750+
$( A counterexample for FLT does not exist for ` N = 0 ` . (Contributed by
647751+
SN, 20-Aug-2024.) $)
647752+
flt0 $p |- ( ph -> N e. NN ) $=
647753+
( wcel cc0 wne cexp co caddc c1 exp0d wceq oveq2 cn0 cn c2 sn-1ne2 necomi
647754+
1p1e2 eqnetri a1i oveq12d 3netr4d eqeq12d syl5ibcom imp mteqand sylanbrc
647755+
elnnne0 ) AEUAKELMEUBKIAELBLNOZCLNOZPOZDLNOZAQQPOZQUSUTVAQMAVAUCQUFQUCUDU
647756+
EUGUHAUQQURQPABFRACGRUIADHRUJAELSZUSUTSZABENOZCENOZPOZDENOZSVBVCJVBVFUSVG
647757+
UTVBVDUQVEURPELBNTELCNTUIELDNTUKULUMUNEUPUO $.
647758+
$}
647759+
647760+
${
647761+
fltabcoprm.s $e |- ( ph -> S e. NN ) $.
647762+
fltabcoprm.a $e |- ( ph -> A e. NN ) $.
647763+
fltabcoprm.b $e |- ( ph -> B e. NN ) $.
647764+
fltabcoprm.c $e |- ( ph -> C e. NN ) $.
647765+
fltabcoprm.n $e |- ( ph -> N e. NN0 ) $.
647766+
fltabcoprm.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
647767+
$( A counterexample to FLT implies a counterexample to FLT with ` A , B `
647768+
(assigned to ` A / ( A gcd B ) ` and ` B / ( A gcd B ) ` ) coprime (by
647769+
~ divgcdcoprm0 ). (Contributed by SN, 20-Aug-2024.) $)
647770+
fltabcoprm $p |- ( ph -> ( ( ( A / ( A gcd B ) ) ^ N )
647771+
+ ( ( B / ( A gcd B ) ) ^ N ) )
647772+
= ( ( C / ( A gcd B ) ) ^ N ) ) $=
647773+
( cgcd co cn wcel gcdnncl syl2anc nncnd nnne0d fltdiv ) ABCDBCMNZFAUBABOP
647774+
COPUBOPHIBCQRZSAUBUCTABHSACISADJSKLUA $.
647775+
647776+
$d A i $. $d B i $. $d C i $. $d ph i $.
647777+
fltaccoprm.1 $e |- ( ph -> ( A gcd B ) = 1 ) $.
647778+
$( A counterexample to FLT with ` A , B ` coprime also has ` A , C `
647779+
coprime (and by commutativity, ` B , C ` ). (Contributed by SN,
647780+
20-Aug-2024.) $)
647781+
fltaccoprm $p |- ( ph -> ( A gcd C ) = 1 ) $=
647782+
( vi cdvds wbr cn co wcel cz cv wa c1 wceq wi wral cgcd coprmgcdb syl2anc
647783+
wb mpbird simprl cexp cmin simpr adantr dvdsexpim syl3anc anim12d ancomsd
647784+
cn0 imp nnexpcld ad2antrr dvds2sub mpd nncnd expcld caddc eqcomd mvrladdd
647785+
nnzd breqtrd simplr flt0 dvdsexplem jca ex imim1d ralimdva mpbid ) ANUAZB
647786+
OPZWBDOPZUBZWBUCUDZUEZNQUFZBDUGRUCUDZAWCWBCOPZUBZWFUEZNQUFZWHAWMBCUGRUCUD
647787+
ZMABQSZCQSZWMWNUJHIBCNUHUIUKAWLWGNQAWBQSZUBZWEWKWFWRWEWKWRWEUBZWCWJWRWCWD
647788+
ULWSWJWBFUMRZCFUMRZOPZWSWTDFUMRZBFUMRZUNRZXAOWSWTXCOPZWTXDOPZUBZWTXEOPZWR
647789+
WEXHWRWDWCXHWRWDXFWCXGWRWBTSZDTSZFVASZWDXFUEWRWBAWQUOZVLZAXKWQADJVLUPAXLW
647790+
QKUPZWBDFUQURWRXJBTSZXLWCXGUEXNAXPWQABHVLUPXOWBBFUQURUSUTVBWSWTTSZXCTSZXD
647791+
TSZXHXIUEWRXQWEWRWTWRWBFXMXOVCVLUPAXRWQWEAXCADFJKVCVLVDAXSWQWEAXDABFHKVCV
647792+
LVDWTXCXDVEURVFAXEXAUDWQWEAXCXDXAABFABHVGZKVHACFACIVGZKVHAXDXAVIRXCLVJVKV
647793+
DVMWSWQWPFQSZWJXBUJAWQWEVNAWPWQWEIVDAYBWQWEABCDFXTYAADJVGKLVOVDWBCFVPURUK
647794+
VQVRVSVTVFAWODQSWHWIUJHJBDNUHUIWA $.
647795+
$}
647796+
647797+
${
647798+
$d ph x z $. $d ps x z $. $d ch y $. $d th y $. $d A y z $.
647799+
$d S x y z $.
647800+
flt4lem.1 $e |- ( y = x -> ( ps <-> ch ) ) $.
647801+
flt4lem.2 $e |- ( y = A -> ( ps <-> th ) ) $.
647802+
flt4lem.3 $e |- ( ph -> S C_ ( ZZ>= ` M ) ) $.
647803+
flt4lem.4 $e |- ( ( ph /\ ( x e. S /\ ch ) ) -> A e. S ) $.
647804+
flt4lem.5 $e |- ( ( ph /\ ( x e. S /\ ch ) ) -> th ) $.
647805+
flt4lem.6 $e |- ( ( ph /\ ( x e. S /\ ch ) ) -> A < x ) $.
647806+
$( Infinite descent. The hypotheses say that ` S ` is lower bounded, and
647807+
that if ` ps ` holds for an integer in ` S ` , it holds for a smaller
647808+
integer in ` S ` . By infinite descent, eventually we cannot go any
647809+
smaller, therefore ` ps ` holds for no integer in ` S ` . (Contributed
647810+
by SN, 20-Aug-2024.) $)
647811+
flt4lem $p |- ( ph -> { y e. S | ps } = (/) ) $=
647812+
( vz c0 wn wa cr crab wceq wne df-ne cle wbr wral wrex cuz cfv wss ssrab2
647813+
sstrid uzwo sylan wcel elrab breq2 notbid elrabd clt uzssre sstrdi adantr
647814+
cv sseldd sselda adantrr ltnled rspcedvdw sylan2b ralrimiva rexnal ralbii
647815+
mpbid ralnex bitri sylib pm2.21dd sylan2br pm2.18da ) ABFHUAZQUBZWCRAWBQU
647816+
CZWCWBQUDAWDSEVEZPVEZUEUFZPWBUGZEWBUHZWCAWBIUIUJZUKWDWIAWBHWJBFHULLUMWBEP
647817+
IUNUOAWIRZWDAWGRZPWBUHZEWBUGZWKAWMEWBWEWBUPAWEHUPZCSZWMBCFWEHJUQAWPSZWLWE
647818+
GUEUFZRZPGWBWFGUBWGWRWFGWEUEURUSWQBDFGHKMNUTWQGWEVAUFWSOWQGWEWQHTGAHTUKWP
647819+
AHWJTLIVBVCZVDMVFAWOWETUPCAHTWEWTVGVHVIVOVJVKVLWNWHRZEWBUGWKWMXAEWBWGPWBV
647820+
MVNWHEWBVPVQVRVDVSVTWA $.
647821+
$}
647822+
647823+
${
647824+
flt4lem2.a $e |- ( ph -> A e. NN ) $.
647825+
flt4lem2.b $e |- ( ph -> B e. NN ) $.
647826+
flt4lem2.c $e |- ( ph -> C e. NN ) $.
647827+
flt4lem2.1 $e |- ( ph -> A < B ) $.
647828+
$( ~ pythagtrip in deduction form with the additional hypothesis ` A < B `
647829+
to separate ` { A , B } = { x , y } ` into ` A = x /\ B = y ` . This
647830+
hypothesis can be assumed without loss of generality because of ~ fltne
647831+
and the commutative property of addition. (Contributed by SN,
647832+
20-Aug-2024.) $)
647833+
flt4lem2 $p |- ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <->
647834+
E. n e. NN E. m e. NN E. k e. NN (
647835+
A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\
647836+
B = ( k x. ( 2 x. ( m x. n ) ) ) /\
647837+
C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) $=
647838+
( c2 cexp co wceq cmul wa cn wrex wcel cpr cv cmin w3a pythagtrip syl3anc
647839+
caddc wb pm5.21ndd anbi1d df-3an bicomi syl6bb rexbidva 2rexbidva bitrd )
647840+
ABLMNCLMNUGNDLMNOZBCUAEUBZFUBZLMNZGUBZLMNZUCNPNZURLUSVAPNPNPNZUAOZDURUTVB
647841+
UGNPNOZQZERSZFRSGRSZBVCOZCVDOZVFUDZERSZFRSGRSABRTCRTDRTUQVIUHHIJBCDEFGUEU
647842+
FAVHVMGFRRAVARTUSRTQQZVGVLERVNURRTQZVGVJVKQZVFQZVLVOVEVPVFVO?VEVP???UIUJV
647843+
LVQVJVKVFUKULUMUNUOUP $.
647844+
$}
647845+
647846+
${
647847+
flt4lem3.a $e |- ( ph -> A e. NN ) $.
647848+
flt4lem3.b $e |- ( ph -> B e. NN ) $.
647849+
flt4lem3.c $e |- ( ph -> C e. NN ) $.
647850+
flt4lem3.1 $e |- ( ph -> A < B ) $.
647851+
flt4lem3.2 $e |- ( ph -> ( A gcd B ) = 1 ) $.
647852+
$( Add a coprime requirement, converting ~ pythagtrip into a
647853+
characterization of primitive Pythagorean triples. (Contributed by SN,
647854+
20-Aug-2024.) $)
647855+
flt4lem3 $p |- ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <->
647856+
E. n e. NN E. m e. NN (
647857+
A = ( ( m ^ 2 ) - ( n ^ 2 ) /\
647858+
B = ( 2 x. ( m x. n ) ) /\
647859+
C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) $=
647860+
? $.
647861+
$}
647862+
647672647863
${
647673647864
fltne.a $e |- ( ph -> A e. NN ) $.
647674647865
fltne.b $e |- ( ph -> B e. NN ) $.
@@ -690622,10 +690813,6 @@ not even needed (it can be any class). (Contributed by Glauco
690622690813
23-Oct-2021.) $)
690623690814
mnfnre2 $p |- -. -oo e. RR $=
690624690815
( cmnf cr mnfnre neli ) ABCD $.
690625-
$( An upper set of integers is a subset of the Reals. (Contributed by Glauco
690626-
Siliprandi, 23-Oct-2021.) $)
690627-
uzssre $p |- ( ZZ>= ` M ) C_ RR $=
690628-
( cuz cfv cz cr uzssz zssre sstri ) ABCDEAFGH $.
690629690816
$( The integers are a subset of the extended reals. (Contributed by Glauco
690630690817
Siliprandi, 23-Oct-2021.) $)
690631690818
zssxr $p |- ZZ C_ RR* $=

0 commit comments

Comments
 (0)