diff --git a/discouraged b/discouraged index dfab6de8ac..abe0c3a359 100644 --- a/discouraged +++ b/discouraged @@ -19235,11 +19235,14 @@ New usage of "sbco" is discouraged (2 uses). New usage of "sbco2" is discouraged (6 uses). New usage of "sbco2d" is discouraged (1 uses). New usage of "sbco3" is discouraged (1 uses). +New usage of "sbco4OLD" is discouraged (0 uses). New usage of "sbco4lemOLD" is discouraged (0 uses). +New usage of "sbco4lemOLDOLD" is discouraged (0 uses). New usage of "sbcom" is discouraged (0 uses). New usage of "sbcom3" is discouraged (3 uses). New usage of "sbcoreleleq" is discouraged (2 uses). New usage of "sbcoreleleqVD" is discouraged (0 uses). +New usage of "sbcovOLD" is discouraged (0 uses). New usage of "sbcrexgOLD" is discouraged (2 uses). New usage of "sbcssgVD" is discouraged (0 uses). New usage of "sbel2x" is discouraged (0 uses). @@ -19254,6 +19257,8 @@ New usage of "sbidm" is discouraged (0 uses). New usage of "sbie" is discouraged (20 uses). New usage of "sbied" is discouraged (3 uses). New usage of "sbiedv" is discouraged (1 uses). +New usage of "sbievOLD" is discouraged (0 uses). +New usage of "sbievwOLD" is discouraged (0 uses). New usage of "sbn1ALT" is discouraged (0 uses). New usage of "sbnfOLD" is discouraged (0 uses). New usage of "sbralieALT" is discouraged (0 uses). @@ -19574,6 +19579,7 @@ New usage of "syl5imp" is discouraged (0 uses). New usage of "syl5impVD" is discouraged (0 uses). New usage of "symgsubmefmndALT" is discouraged (0 uses). New usage of "symgvalstructOLD" is discouraged (0 uses). +New usage of "tan4thpiOLD" is discouraged (0 uses). New usage of "tarski-bernays-ax2" is discouraged (0 uses). New usage of "taylply2OLD" is discouraged (0 uses). New usage of "taylthlem2OLD" is discouraged (0 uses). @@ -21628,12 +21634,17 @@ Proof modification of "sbcim1OLD" is discouraged (33 steps). Proof modification of "sbcim2g" is discouraged (83 steps). Proof modification of "sbcim2gVD" is discouraged (139 steps). Proof modification of "sbcimdvOLD" is discouraged (52 steps). -Proof modification of "sbco4lemOLD" is discouraged (98 steps). +Proof modification of "sbco4OLD" is discouraged (79 steps). +Proof modification of "sbco4lemOLD" is discouraged (66 steps). +Proof modification of "sbco4lemOLDOLD" is discouraged (98 steps). Proof modification of "sbcoreleleq" is discouraged (91 steps). Proof modification of "sbcoreleleqVD" is discouraged (176 steps). +Proof modification of "sbcovOLD" is discouraged (32 steps). Proof modification of "sbcrexgOLD" is discouraged (77 steps). Proof modification of "sbcssgVD" is discouraged (229 steps). Proof modification of "sbhypfOLD" is discouraged (58 steps). +Proof modification of "sbievOLD" is discouraged (24 steps). +Proof modification of "sbievwOLD" is discouraged (23 steps). Proof modification of "sbn1ALT" is discouraged (41 steps). Proof modification of "sbnfOLD" is discouraged (82 steps). Proof modification of "sbralieALT" is discouraged (98 steps). @@ -21728,6 +21739,7 @@ Proof modification of "syl5impVD" is discouraged (57 steps). Proof modification of "symgsubmefmndALT" is discouraged (129 steps). Proof modification of "symgvalstructOLD" is discouraged (651 steps). Proof modification of "symrefref3" is discouraged (75 steps). +Proof modification of "tan4thpiOLD" is discouraged (135 steps). Proof modification of "tarski-bernays-ax2" is discouraged (557 steps). Proof modification of "taylply2OLD" is discouraged (657 steps). Proof modification of "taylthlem2OLD" is discouraged (2711 steps). diff --git a/set.mm b/set.mm index 5b2d5a2d35..a9b3292be5 100644 --- a/set.mm +++ b/set.mm @@ -17631,14 +17631,32 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the ACDGZBEZCHZEZABCDFZEQRPEZCHASEZCHUAPCDIUDUCCARBJKASCLMUBTABCDINO $. $} + ${ + $d t x $. + sbbiiev.1 $e |- ( x = t -> ( ph <-> ps ) ) $. + $( An equivalence of substitutions (as in ~ sbbii ) allowing the additional + information that ` x = t ` . Version of ~ sbiev and ~ sbievw without a + disjoint variable condition on ` ps ` , useful for substituting only + part of ` ph ` . (Contributed by SN, 24-Aug-2025.) $) + sbbiiev $p |- ( [ t / x ] ph <-> [ t / x ] ps ) $= + ( weq wi wal wsb pm5.74i albii sb6 3bitr4i ) CDFZAGZCHNBGZCHACDIBCDIOPCNA + BEJKACDLBCDLM $. + $} + ${ $d x y $. $d x ps $. sbievw.is $e |- ( x = y -> ( ph <-> ps ) ) $. $( Conversion of implicit substitution to explicit substitution. Version of ~ sbie and ~ sbiev with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, - 18-Jul-2023.) $) + 18-Jul-2023.) (Proof shortened by SN, 24-Aug-2025.) $) sbievw $p |- ( [ y / x ] ph <-> ps ) $= + ( wsb sbbiiev sbv bitri ) ACDFBCDFBABCDEGBCDHI $. + + $( Obsolete version of ~ sbievw as of 24-Aug-2025. (Contributed by NM, + 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + sbievwOLD $p |- ( [ y / x ] ph <-> ps ) $= ( wsb weq wi wal sb6 equsalvw bitri ) ACDFCDGAHCIBACDJABCDEKL $. $} @@ -17673,8 +17691,7 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the 27-May-1997.) (Revised by Giovanni Mascellani, 8-Apr-2018.) (Revised by BJ, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 19-Jan-2023.) $) sbcom3vv $p |- ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph ) $= - ( weq wsb wi wal sbequ pm5.74i albii sb6 3bitr4i ) CDEZABCFZGZCHNABDFZGZC - HOCDFQCDFPRCNOQACDBIJKOCDLQCDLM $. + ( wsb sbequ sbbiiev ) ABCEABDECDACDBFG $. $} ${ @@ -17699,6 +17716,43 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the ( vw wsb sbequ sbievw2 ) ABDFABCFABEFDCEADEBGAECBGH $. $} + ${ + $d x y $. $d ph y $. $d ps x $. + cbvsbv.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Change the bound variable (i.e. the substituted one) in wff's linked by + implicit substitution. The proof was extracted from a former ~ cbvabv + version. (Contributed by Wolf Lammen, 16-Mar-2025.) $) + cbvsbv $p |- ( [ z / x ] ph <-> [ z / y ] ps ) $= + ( wsb sbco2vv sbievw sbbii bitr3i ) ACEGACDGZDEGBDEGACEDHLBDEABCDFIJK $. + $( $j usage 'cbvsbv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + + ${ + $d v w ph $. $d v w x $. $d v w y $. + $( Lemma for ~ sbco4 . It replaces the temporary variable ` v ` with + another temporary variable ` w ` . (Contributed by Jim Kingdon, + 26-Sep-2018.) (Proof shortened by Wolf Lammen, 12-Oct-2024.) Avoid + ~ ax-11 . (Revised by SN, 3-Sep-2025.) $) + sbco4lem $p |- ( [ x / v ] [ y / x ] [ v / y ] ph <-> + [ x / w ] [ y / x ] [ w / y ] ph ) $= + ( wsb weq sbequ sbbidv cbvsbv ) ACEFZBCFACDFZBCFEDBEDGKLBCAEDCHIJ $. + $( $j usage 'sbco4lem' avoids 'ax-11'; $) + $} + + ${ + $d t u v ph $. $d t u v x $. $d t u v y $. $d w ph $. $d w x $. + $d w y $. $d t w $. + $( Two ways of exchanging two variables. Both sides of the biconditional + exchange ` x ` and ` y ` , either via two temporary variables ` u ` and + ` v ` , or a single temporary ` w ` . (Contributed by Jim Kingdon, + 25-Sep-2018.) Avoid ~ ax-11 . (Revised by SN, 3-Sep-2025.) $) + sbco4 $p |- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> + [ x / w ] [ y / x ] [ w / y ] ph ) $= + ( vt wsb weq sbequ sbbidv sbievw sbco4lem bitri ) ACEHZBFHZEBHZFCHOBCHZEB + HZACDHBCHDBHZQSFCFCIPREBOFCBJKLSACGHBCHGBHTABCGEMABCDGMNN $. + $( $j usage 'sbco4' avoids 'ax-11'; $) + $} + ${ $d x w z $. $d y w $. $( Substitution in an equality. (Contributed by Raph Levien and FL, @@ -18569,10 +18623,10 @@ scheme is logically redundant (see ~ ax10w ) but is used as an auxiliary ${ $d v w ph $. $d v w x $. $d v w y $. - $( Lemma for ~ sbco4 . It replaces the temporary variable ` v ` with - another temporary variable ` w ` . (Contributed by Jim Kingdon, - 26-Sep-2018.) (Proof shortened by Wolf Lammen, 12-Oct-2024.) $) - sbco4lem $p |- ( [ x / v ] [ y / x ] [ v / y ] ph <-> + $( Obsolete version of ~ sbco4lem as of 3-Sep-2025. (Contributed by Jim + Kingdon, 26-Sep-2018.) (Proof shortened by Wolf Lammen, 12-Oct-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + sbco4lemOLD $p |- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph ) $= ( wsb sbcom2 sbbii sbco2vv 2sbbii 3bitr3i ) ACDFZDEFZBCFZEBFLBCFZDEFZEBFA CEFZBCFEBFODBFNPEBLDEBCGHMQEBCBACEDIJODBEIK $. @@ -18581,11 +18635,10 @@ scheme is logically redundant (see ~ ax10w ) but is used as an auxiliary ${ $d t u v ph $. $d t u v x $. $d t u v y $. $d w ph $. $d w x $. $d w y $. $d t w $. - $( Two ways of exchanging two variables. Both sides of the biconditional - exchange ` x ` and ` y ` , either via two temporary variables ` u ` and - ` v ` , or a single temporary ` w ` . (Contributed by Jim Kingdon, - 25-Sep-2018.) $) - sbco4 $p |- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> + $( Obsolete version of ~ sbco4 as of 3-Sep-2025. (Contributed by Jim + Kingdon, 25-Sep-2018.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + sbco4OLD $p |- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph ) $= ( vt wsb sbcom2 sbco2vv sbbii bitr3i sbco4lem 3bitri ) ACEHZBFHZEBHFCHZOB CHZEBHZACGHBCHGBHACDHBCHDBHQPFCHZEBHSPFCEBITREBOBCFJKLABCGEMABCDGMN $. @@ -19383,8 +19436,16 @@ disjoint variable condition if we allow more axioms (see ~ equs4 ). $d x y $. $( A composition law for substitution. Version of ~ sbco with a disjoint variable condition using fewer axioms. (Contributed by NM, - 14-May-1993.) (Revised by GG, 7-Aug-2023.) $) + 14-May-1993.) (Revised by GG, 7-Aug-2023.) (Proof shortened by SN, + 26-Aug-2025.) $) sbcov $p |- ( [ y / x ] [ x / y ] ph <-> [ y / x ] ph ) $= + ( wsb sbequ12r sbbiiev ) ACBDABCABCEF $. + $( $j usage 'sbcov' avoids 'ax-10' 'ax-11' 'ax-13'; $) + + $( Obsolete version of ~ sbcov as of 26-Aug-2025. (Contributed by NM, + 14-May-1993.) (Revised by GG, 7-Aug-2023.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + sbcovOLD $p |- ( [ y / x ] [ x / y ] ph <-> [ y / x ] ph ) $= ( wsb sbcom3vv sbid sbbii bitri ) ACBDBCDACCDZBCDABCDACBCEIABCACFGH $. $( $j usage 'sbcov' avoids 'ax-10' 'ax-11' 'ax-13'; $) $} @@ -19612,7 +19673,7 @@ any disjoint variable condition (but the version with a disjoint $( Obsolete version of ~ sbco4lem as of 12-Oct-2024. (Contributed by Jim Kingdon, 26-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) $) - sbco4lemOLD $p |- ( [ x / v ] [ y / x ] [ v / y ] ph <-> + sbco4lemOLDOLD $p |- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph ) $= ( wsb sbcom2 sbbii sbco2vv 2sbbii bitri sbid2vw 3bitr3i ) ACDFZDEFZBCFZED FZDBFZOEDFZBCFZDBFACEFZBCFZEBFZNBCFDBFQTDBOBCEDGHRUBEDFDBFUCPUBDEDBOUABCA @@ -19938,8 +19999,16 @@ any disjoint variable condition (but the version with a disjoint See ~ sbievw for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ~ ax-10 and shorten proof. - (Revised by BJ, 18-Jul-2023.) $) + (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Jul-2025.) $) sbiev $p |- ( [ y / x ] ph <-> ps ) $= + ( wsb sbbiiev sbf bitri ) ACDGBCDGBABCDFHBCDEIJ $. + $( $j usage 'sbiev' avoids 'ax-10' 'ax-13'; $) + + $( Obsolete version of ~ sbiev as of 24-Aug-2025. (Contributed by NM, + 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence + on ~ ax-10 and shorten proof. (Revised by BJ, 18-Jul-2023.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + sbievOLD $p |- ( [ y / x ] ph <-> ps ) $= ( wsb weq wi wal sb6 equsalv bitri ) ACDGCDHAICJBACDKABCDEFLM $. $} @@ -20461,17 +20530,6 @@ Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM, ( nfv sbbib ) ABCDADEBCEF $. $} - ${ - $d x y $. $d ph y $. $d ps x $. - cbvsbv.1 $e |- ( x = y -> ( ph <-> ps ) ) $. - $( Change the bound variable (i.e. the substituted one) in wff's linked by - implicit substitution. The proof was extracted from a former ~ cbvabv - version. (Contributed by Wolf Lammen, 16-Mar-2025.) $) - cbvsbv $p |- ( [ z / x ] ph <-> [ z / y ] ps ) $= - ( wsb sbco2vv sbievw sbbii bitr3i ) ACEGACDGZDEGBDEGACEDHLBDEABCDFIJK $. - $( $j usage 'cbvsbv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) - $} - ${ $d x y w $. $d ph w $. $d ps w $. $d w z $. cbvsbvf.1 $e |- F/ y ph $. @@ -30819,10 +30877,9 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) Avoid ~ ax-10 , ~ ax-12 . (Revised by SN, 21-Aug-2025.) $) cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $= - ( cv wcel wi wal wsb wral sb8v df-ral weq eleq1w imbi1d pm5.74i albii sb6 - 3bitr4i sbrimvw bitr2i bitri ) BEDFZAGZBHUDBCIZCHZABDJABCIZCDJZUDBCKABDLU - HCEDFZUGGZCHUFUGCDLUJUECUEUIAGZBCIZUJBCMZUDGZBHUMUKGZBHUEULUNUOBUMUDUKUMU - CUIABCDNOPQUDBCRUKBCRSUIABCTUAQUBS $. + ( cv wcel wi wal wsb wral df-ral weq eleq1w imbi1d sbbiiev sbrimvw bitr2i + sb8v albii bitri 3bitr4i ) BEDFZAGZBHUCBCIZCHZABDJABCIZCDJZUCBCRABDKUGCED + FZUFGZCHUEUFCDKUIUDCUDUHAGZBCIUIUCUJBCBCLUBUHABCDMNOUHABCPQSTUA $. $( $j usage 'cbvralsvw' avoids 'ax-10' 'ax-12' 'ax-13'; $) $( Change bound variable by using a substitution. Version of ~ cbvrexsv @@ -382044,9 +382101,19 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is WMABBOVEVEWIWNWOBBVERVFWPWQWRQWSMGVKMUUHYTUUIUUJWTWCXGWKQGXHXAWAXBXHXCNWRXI UUBXDNZXEXKXIXLXKXNXIUUGUUMUNYBYDXIXLYJYOYAXHUAYNUOVAXEWE $. - $( The tangent of ` _pi / 4 ` . (Contributed by Mario Carneiro, - 5-Apr-2015.) $) + $( The tangent of ` _pi / 4 ` . (Contributed by Mario Carneiro, 5-Apr-2015.) + (Proof shortened by SN, 2-Sep-2025.) $) tan4thpi $p |- ( tan ` ( _pi / 4 ) ) = 1 $= + ( cpi c4 cdiv co ctan cfv csin ccos c1 c2 csqrt cc wcel cc0 wne sincos4thpi + wceq picn sqrt2re mp2an 4cn 4ne0 divcli simpri recni 2re sqrtgt0ii gt0ne0ii + 2pos recne0 eqnetri tanval simpli oveq12i reccli dividi 3eqtri ) ABCDZEFZUR + GFZURHFZCDZIJKFZCDZVDCDIURLMVANOUSVBQABRUAUBUCVAVDNUTVDQZVAVDQZPUDZVCLMVCNO + VDNOVCSUEZVCSJUFUIUGUHZVCUJTZUKURULTUTVDVAVDCVEVFPUMVGUNVDVCVHVIUOVJUPUQ $. + + $( Obsolete version of ~ tan4thpi as of 2-Sep-2025. (Contributed by Mario + Carneiro, 5-Apr-2015.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + tan4thpiOLD $p |- ( tan ` ( _pi / 4 ) ) = 1 $= ( cpi c4 cdiv co ctan cfv csin ccos c1 c2 cc wcel cc0 wne mp2an sincos4thpi wceq cr recni eqnetri csqrt cn pire 4nn nndivre simpri sqrt2re cexp cle wbr 2re 0le2 resqrtth 2ne0 sqne0 ax-mp mpbi recne0 tanval simpli oveq12i reccli @@ -695855,6 +695922,17 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove 1t1e1ALT $p |- ( 1 x. 1 ) = 1 $= ( c1 cr wcel cmul co wceq 1re ax-1rid ax-mp ) ABCAADEAFGAHI $. + ${ + lttrii.a $e |- A e. RR $. + lttrii.b $e |- B e. RR $. + lttrii.c $e |- C e. RR $. + lttrii.1 $e |- A < B $. + lttrii.2 $e |- B < C $. + $( 'Less than' is transitive. (Contributed by SN, 26-Aug-2025.) $) + lttrii $p |- A < C $= + ( clt wbr lttri mp2an ) ABIJBCIJACIJGHABCDEFKL $. + $} + ${ $d A x $. $d B x $. $d C x $. $d ph x $. remulcan2d.1 $e |- ( ph -> A e. RR ) $. @@ -696262,11 +696340,58 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove 4t5e20 $p |- ( 4 x. 5 ) = ; 2 0 $= ( c5 c4 c2 cc0 cdc 5cn 4cn 5t4e20 mulcomli ) ABCDEFGHI $. + $( The square of 4 is 16. (Contributed by SN, 26-Aug-2025.) $) + sq4 $p |- ( 4 ^ 2 ) = ; 1 6 $= + ( c4 c2 cexp co cmul c1 c6 cdc 4cn sqvali 4t4e16 eqtri ) ABCDAAEDFGHAIJKL + $. + + $( The square of 5 is 25. (Contributed by SN, 26-Aug-2025.) $) + sq5 $p |- ( 5 ^ 2 ) = ; 2 5 $= + ( c5 c2 cexp co cmul cdc 5cn sqvali 5t5e25 eqtri ) ABCDAAEDBAFAGHIJ $. + + $( The square of 6 is 36. (Contributed by SN, 26-Aug-2025.) $) + sq6 $p |- ( 6 ^ 2 ) = ; 3 6 $= + ( c6 c2 cexp co cmul c3 cdc 6cn sqvali 6t6e36 eqtri ) ABCDAAEDFAGAHIJK $. + + $( The square of 7 is 49. (Contributed by SN, 26-Aug-2025.) $) + sq7 $p |- ( 7 ^ 2 ) = ; 4 9 $= + ( c7 c2 cexp co cmul c4 c9 cdc 7cn sqvali 7t7e49 eqtri ) ABCDAAEDFGHAIJKL + $. + + $( The square of 8 is 64. (Contributed by SN, 26-Aug-2025.) $) + sq8 $p |- ( 8 ^ 2 ) = ; 6 4 $= + ( c8 c2 cexp co cmul c6 c4 cdc 8cn sqvali 8t8e64 eqtri ) ABCDAAEDFGHAIJKL + $. + $( The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) $) sq9 $p |- ( 9 ^ 2 ) = ; 8 1 $= ( c9 c2 cexp co cmul c8 c1 cdc 9cn sqvali 9t9e81 eqtri ) ABCDAAEDFGHAIJKL $. + $( 4 is a positive real. (Contributed by SN, 26-Aug-2025.) $) + 4rp $p |- 4 e. RR+ $= + ( c4 4re 4pos elrpii ) ABCD $. + + $( 5 is a positive real. (Contributed by SN, 26-Aug-2025.) $) + 5rp $p |- 5 e. RR+ $= + ( c5 5re 5pos elrpii ) ABCD $. + + $( 6 is a positive real. (Contributed by SN, 26-Aug-2025.) $) + 6rp $p |- 6 e. RR+ $= + ( c6 6re 6pos elrpii ) ABCD $. + + $( 7 is a positive real. (Contributed by SN, 26-Aug-2025.) $) + 7rp $p |- 7 e. RR+ $= + ( c7 7re 7pos elrpii ) ABCD $. + + $( 8 is a positive real. (Contributed by SN, 26-Aug-2025.) $) + 8rp $p |- 8 e. RR+ $= + ( c8 8re 8pos elrpii ) ABCD $. + + $( 9 is a positive real. (Contributed by SN, 26-Aug-2025.) $) + 9rp $p |- 9 e. RR+ $= + ( c9 9re 9pos elrpii ) ABCD $. + $( Calculate a product by long multiplication as a base comparison with other multiplication algorithms. @@ -696884,6 +697009,60 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Trigonometry +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + tanhalfpim.a $e |- ( ph -> A e. CC ) $. + tanhalfpim.1 $e |- ( ph -> ( sin ` A ) =/= 0 ) $. + $( The tangent of ` _pi / 2 ` minus a number is the cotangent, here + represented by ` cos A / sin A ` . (Contributed by SN, 2-Sep-2025.) $) + tanhalfpim $p |- ( ph -> + ( tan ` ( ( _pi / 2 ) - A ) ) = ( ( cos ` A ) / ( sin ` A ) ) ) $= + ( cpi c2 cdiv co cmin ctan cfv csin ccos cc wcel cc0 wne wceq picn syl + 2cn 2ne0 divcli subcld coshalfpim eqnetrd tanval syl2anc sinhalfpim eqtrd + a1i oveq12d ) AEFGHZBIHZJKZUNLKZUNMKZGHZBMKZBLKZGHZAUNNOUQPQUOURRAUMBUMNO + AEFSUAUBUCUKCUDAUQUTPABNOZUQUTRCBUEZTDUFUNUGUHAVBURVARCVBUPUSUQUTGBUIVCUL + TUJ $. + $} + + $( The tangent of ` _pi / 3 ` is ` sqrt 3 ` . (Contributed by SN, + 2-Sep-2025.) $) + tan3rdpi $p |- ( tan ` ( _pi / 3 ) ) = ( sqrt ` 3 ) $= + ( cpi c3 cdiv co ctan cfv csin ccos csqrt c2 c1 cc wcel cc0 wne sincos3rdpi + wceq 3cn wtru a1i picn 3ne0 divcli simpri 0re halfgt0 gtneii eqnetri tanval + mp2an simpli oveq12i sqrtcld 1cnd ax-1ne0 divcan7d div1d eqtrd mptru 3eqtri + 2cnd 2ne0 ) ABCDZEFZVCGFZVCHFZCDZBIFZJCDZKJCDZCDZVHVCLMVFNOVDVGQABUARUBUCVF + VJNVEVIQZVFVJQZPUDZNVJUEUFUGUHVCUIUJVEVIVFVJCVLVMPUKVNULVKVHQSVKVHKCDVHSVHK + JSBBLMSRTUMZSUNSVAKNOSUOTJNOSVBTUPSVHVOUQURUSUT $. + + $( The arcsine of ` 1 / 2 ` is ` _pi / 6 ` . (Contributed by SN, + 31-Aug-2025.) $) + asin1half $p |- ( arcsin ` ( 1 / 2 ) ) = ( _pi / 6 ) $= + ( cpi c6 cdiv co cfv casin c2 wceq wcel cr cle wbr pire cc0 neghalfpire clt + halfpire wtru crp a1i csin c1 ccos csqrt sincos6thpi simpli fveq2i cneg 6re + c3 cicc 0re 6pos gtneii redivcli 2re pipos 2pos divgt0ii mpbii ax-mp lttrii + lt0neg2 ltleii 2lt6 2rp 6rp ltdiv2d mptru elicc2i mpbir3an reasinsin eqtr3i + pirp ) ABCDZUAEZFEZUBGCDZFEVOVPVRFVPVRHVOUCEUJUDEGCDHUEUFUGVOAGCDZUHZVSUKDI + ZVQVOHWAVOJIVTVOKLVOVSKLABMUINBULUMUNUOZVTVOOWBVTNVOOULWBVSJIZVTNPLZQWCNVSP + LWDAGMUPUQURUSVSVCUTVAABMUIUQUMUSVBVDVOVSWBQVOVSPLZRGBPLWEVERGBAGSIRVFTBSIR + VGTASIRVNTVHUTVIVDVTVSVOOQVJVKVOVLVAVM $. + + $( The arccosine of ` 1 / 2 ` is ` _pi / 3 ` . (Contributed by SN, + 31-Aug-2024.) $) + acos1half $p |- ( arccos ` ( 1 / 2 ) ) = ( _pi / 3 ) $= + ( cpi c3 cdiv co cfv cacos c1 c2 wceq wcel cc0 pire 3re cxr clt rexri pipos + wbr 3pos mp2an ccos csin csqrt sincos3rdpi simpri fveq2i cioo 3ne0 redivcli + cc recni cr rere ax-mp divgt0ii picn gt0ne0ii dividi 1lt3 eqbrtri ltdiv23ii + cre mpbir w3a wb 0xr elioo1 mpbir3an eqeltri acoscos eqtr3i ) ABCDZUAEZFEZG + HCDZFEVLVMVOFVLUBEBUCEHCDIVMVOIUDUEUFVLUJJVLVBEZKAUGDZJVNVLIVLABLMUHUIZUKVP + VLVQVLULJVPVLIVRVLUMUNVLVQJZVLNJZKVLORZVLAORZVLVRPABLMQSUOWBAACDZBORWCGBOAU + PALQUQURUSUTABALMLSQVAVCKNJANJVSVTWAWBVDVEVFALPKAVLVGTVHVIVLVJTVK $. + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Real subtraction @@ -702936,17 +703115,6 @@ evaluates to zero (the "zero set"). (In other words, scalar multiples BWCWFURWGWHWKWLXOWIWJ $. $} - $( The arccosine of ` 1 / 2 ` is ` _pi / 3 ` . (Contributed by SN, - 31-Aug-2024.) $) - acos1half $p |- ( arccos ` ( 1 / 2 ) ) = ( _pi / 3 ) $= - ( cpi c3 cdiv co cfv cacos c1 c2 wceq wcel cc0 pire 3re cxr clt rexri pipos - wbr 3pos mp2an ccos csin csqrt sincos3rdpi simpri fveq2i cioo 3ne0 redivcli - cc recni cr rere ax-mp divgt0ii picn gt0ne0ii dividi 1lt3 eqbrtri ltdiv23ii - cre mpbir w3a wb 0xr elioo1 mpbir3an eqeltri acoscos eqtr3i ) ABCDZUAEZFEZG - HCDZFEVLVMVOFVLUBEBUCEHCDIVMVOIUDUEUFVLUJJVLVBEZKAUGDZJVNVLIVLABLMUHUIZUKVP - VLVQVLULJVPVLIVRVLUMUNVLVQJZVLNJZKVLORZVLAORZVLVRPABLMQSUOWBAACDZBORWCGBOAU - PALQUQURUSUTABALMLSQVAVCKNJANJVSVTWAWBVDVEVFALPKAVLVGTVHVIVLVJTVK $. - $( An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.) $) aprilfools2025 $p |- { <" A p r i l "> , <" f o o l s ! "> } e. _V $= @@ -702979,12 +703147,9 @@ This strategy (which I will call a "standard replacement" of axioms) has a $d x y $. $d ph y $. $d ps x $. nfa1w.x $e |- ( x = y -> ( ph <-> ps ) ) $. $( Replace ~ ax-10 in ~ nfa1 with a substitution hypothesis. (Contributed - by SN, 7-Jun-2025.) $) + by SN, 2-Sep-2025.) $) nfa1w $p |- F/ x A. x ph $= - ( wal wn wex alex wi wnf exim df-ex wb weq notbid cbvexvw a1i hbn1w con1i - sylbi syl6 nfd hbe1w mpg nfn nfxfr ) ACFAGZCHZGCACIUICUIUICFZJZUICKCUKCFZ - UICULUICHUJCHZUJUIUJCLUMUJGCFZGUJUJCMUJUNUIBGZDHZCDUIUPNCDOZUHUOCDUQABEPZ - QRSTUAUBUCUHUOCDURUDUEUFUG $. + ( wal cbvalvw nfv nfxfr ) ACFBDFZCABCDEGJCHI $. $( $j usage 'nfa1w' avoids 'ax-10'; $) $} @@ -837187,9 +837352,9 @@ Reciprocal trigonometric functions (sec, csc, cot) 0cn mp2an oveq2i 1div1e1 3eqtri ) ABCZDAECZFGZDDFGDAHIUBAJUAUCKPUBDALMNAOQU BDDFLRST $. - $( Prove the tangent squared secant squared identity ` ( 1 + ( ( tan ` A ) ^ - 2 ) ) = ( ( sec ` A ) ^ 2 ) ) ` . (Contributed by David A. Wheeler, - 25-May-2015.) $) + $( Prove the tangent squared secant squared identity + ` ( 1 + ( ( tan `` A ) ^ 2 ) ) = ( ( sec `` A ) ^ 2 ) ) ` . (Contributed + by David A. Wheeler, 25-May-2015.) $) onetansqsecsq $p |- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( ( sec ` A ) ^ 2 ) ) $= ( cc wcel cfv cc0 wne wa c1 c2 cexp co caddc cdiv wceq sqcld oveq1d syl3an2 @@ -837205,9 +837370,9 @@ Reciprocal trigonometric functions (sec, csc, cot) WHHVOWGWBXIWSVEAVMVFPVGTVRWEHVPMKZIJKZWCVRWDXJIJAVHPVRXKHIJKZWBMKZWCVOWOVQX KXMNZWPHBCXCXDXNVIUOHVPIUQVJRXLHWBMVNVKVLTVD $. - $( Prove the tangent squared cosecant squared identity ` ( 1 + ( ( cot ` A ) - ^ 2 ) ) = ( ( csc ` A ) ^ 2 ) ) ` . (Contributed by David A. Wheeler, - 27-May-2015.) $) + $( Prove the tangent squared cosecant squared identity + ` ( 1 + ( ( cot `` A ) ^ 2 ) ) = ( ( csc `` A ) ^ 2 ) ) ` . (Contributed + by David A. Wheeler, 27-May-2015.) $) cotsqcscsq $p |- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( cot ` A ) ^ 2 ) ) = ( ( csc ` A ) ^ 2 ) ) $= ( cc wcel cfv cc0 wne wa c1 c2 cexp co caddc cdiv oveq1d oveq2d wceq adantr