P. 410 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40901-41000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnpw2blenfzo2 40901	A positive integer is either 2 to the power of the binary length of the integer minus 1, or between 2 to the power of the binary length of the integer minus 1, increased by 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.)
|- ( N e. NN -> ( N = ( 2 ^ ( (#b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( (#b ` N ) - 1 ) ) + 1 )..^ ( 2 ^ (#b ` N ) ) ) ) )
Theorem	nnpw2pmod 40902	Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.)
|- ( N e. NN -> N = ( ( 2 ^ ( (#b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( (#b ` N ) - 1 ) ) ) ) )
Theorem	blen1 40903	The binary length of 1. (Contributed by AV, 21-May-2020.)
|- (#b ` 1 ) = 1
Theorem	blen2 40904	The binary length of 2. (Contributed by AV, 21-May-2020.)
|- (#b ` 2 ) = 2
Theorem	nnpw2p 40905*	Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.)
|- ( N e. NN -> E. i e. NN0 E. r e. ( 0..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) )
Theorem	nnpw2pb 40906*	A number is a positive integer iff it can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.)
|- ( N e. NN <-> E. i e. NN0 E. r e. ( 0..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) )
Theorem	blen1b 40907	The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020.)
|- ( N e. NN0 -> ( (#b ` N ) = 1 <-> ( N = 0 \/ N = 1 ) ) )
Theorem	blennnt2 40908	The binary length of a positive integer, doubled and increased by 1, is the binary length of the integer plus 1. (Contributed by AV, 30-May-2010.)
|- ( N e. NN -> (#b ` ( 2 x. N ) ) = ( (#b ` N ) + 1 ) )
Theorem	nnolog2flm1 40909	The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
Theorem	blennn0em1 40910	The binary length of the half of an even positive integer is the binary length of the integer minus 1. (Contributed by AV, 30-May-2010.)
|- ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> (#b ` ( N / 2 ) ) = ( (#b ` N ) - 1 ) )
Theorem	blennngt2o2 40911	The binary length of an odd integer greater than 1 is the binary length of the half of the integer decreased by 1, increased by 1. (Contributed by AV, 3-Jun-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> (#b ` N ) = ( (#b ` ( ( N - 1 ) / 2 ) ) + 1 ) )
Theorem	blengt1fldiv2p1 40912	The binary length of an integer greater than 1 is the binary length of the integer divided by 2, increased by one. (Contributed by AV, 3-Jun-2020.)
|- ( N e. ( ZZ>= ` 2 ) -> (#b ` N ) = ( (#b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )
Theorem	blennn0e2 40913	The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020.)
|- ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> (#b ` N ) = ( (#b ` ( N / 2 ) ) + 1 ) )
21.33.16.10  Digits Generalisation of df-bits 14474. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 40933: ( ( K (digit 2 ) N ) = 1 <-> K e. ( bits N ) ).
Syntax	cdig 40914	Extend class notation with the class of the digit extraction operation.
class digit
Definition	df-dig 40915*	Definition of an operation to obtain the k th digit of a nonnegative real number r in the positional system with base b. k = - 1 corresponds to the first digit of the fractional part (for b = 10 the first digit after the decimal point), k = 0 corresponds to the last digit of the integer part (for b = 10 the first digit before the decimal point). See also digit1 12444. Examples (not formal): ( 234.567 ( digit ` 10 ) 0 ) = 4; ( 2.567 ( digit ` 10 ) -2 ) = 6; ( 2345.67 ( digit ` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020.)
|- digit = ( b e. NN |-> ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( b ^ -u k ) x. r ) ) mod b ) ) )
Theorem	digfval 40916*	Operation to obtain the k th digit of a nonnegative real number r in the positional system with base B. (Contributed by AV, 23-May-2020.)
|- ( B e. NN -> (digit ` B ) = ( k e. ZZ , r e. ( 0 [,) +oo ) |-> ( ( |_ ` ( ( B ^ -u k ) x. r ) ) mod B ) ) )
Theorem	digval 40917	The K th digit of a nonnegative real number R in the positional system with base B. (Contributed by AV, 23-May-2020.)
|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K (digit ` B ) R ) = ( ( |_ ` ( ( B ^ -u K ) x. R ) ) mod B ) )
Theorem	digvalnn0 40918	The K th digit of a nonnegative real number R in the positional system with base B is a nonnegative integer. (Contributed by AV, 28-May-2020.)
|- ( ( B e. NN /\ K e. ZZ /\ R e. ( 0 [,) +oo ) ) -> ( K (digit ` B ) R ) e. NN0 )
Theorem	nn0digval 40919	The K th digit of a nonnegative real number R in the positional system with base B. (Contributed by AV, 23-May-2020.)
|- ( ( B e. NN /\ K e. NN0 /\ R e. ( 0 [,) +oo ) ) -> ( K (digit ` B ) R ) = ( ( |_ ` ( R / ( B ^ K ) ) ) mod B ) )
Theorem	dignn0fr 40920	The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.)
|- ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ N e. NN0 ) -> ( K (digit ` B ) N ) = 0 )
Theorem	dignn0ldlem 40921	Lemma for dignnld 40922. (Contributed by AV, 25-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> N < ( B ^ K ) )
Theorem	dignnld 40922	The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( K (digit ` B ) N ) = 0 )
Theorem	dig2nn0ld 40923	The leading digits of a positive integer in a binary system are 0. (Contributed by AV, 25-May-2020.)
|- ( ( N e. NN /\ K e. ( ZZ>= ` (#b ` N ) ) ) -> ( K (digit ` 2 ) N ) = 0 )
Theorem	dig2nn1st 40924	The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020.)
|- ( N e. NN -> ( ( (#b ` N ) - 1 ) (digit ` 2 ) N ) = 1 )
Theorem	dig0 40925	All digits of 0 are 0. (Contributed by AV, 24-May-2020.)
|- ( ( B e. NN /\ K e. ZZ ) -> ( K (digit ` B ) 0 ) = 0 )
Theorem	digexp 40926	The K th digit of a power to the base is either 1 or 0. (Contributed by AV, 24-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ N e. NN0 ) -> ( K (digit ` B ) ( B ^ N ) ) = if ( K = N , 1 , 0 ) )
Theorem	dig1 40927	All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( K (digit ` B ) 1 ) = if ( K = 0 , 1 , 0 ) )
Theorem	0dig1 40928	The 0 th digit of 1 is 1 in any positional system. (Contributed by AV, 28-May-2020.)
|- ( B e. ( ZZ>= ` 2 ) -> ( 0 (digit ` B ) 1 ) = 1 )
Theorem	0dig2pr01 40929	The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.)
|- ( N e. { 0 , 1 } -> ( 0 (digit ` 2 ) N ) = N )
Theorem	dig2nn0 40930	A digit of a nonnegative integer N in a binary system is either 0 or 1. (Contributed by AV, 24-May-2020.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( K (digit ` 2 ) N ) e. { 0 , 1 } )
Theorem	0dig2nn0e 40931	The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.)
|- ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( 0 (digit ` 2 ) N ) = 0 )
Theorem	0dig2nn0o 40932	The last bit of an odd integer is 1. (Contributed by AV, 3-Jun-2010.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 0 (digit ` 2 ) N ) = 1 )
Theorem	dig2bits 40933	The K th digit of a nonnegative integer N in a binary system is its K th bit. (Contributed by AV, 24-May-2020.)
|- ( ( N e. NN0 /\ K e. NN0 ) -> ( ( K (digit ` 2 ) N ) = 1 <-> K e. (bits ` N ) ) )
21.33.16.11  Nonnegative integer as sum of its shifted digits
Theorem	dignn0flhalflem1 40934	Lemma 1 for dignn0flhalf 40937. (Contributed by AV, 7-Jun-2012.)
|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( |_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) < ( |_ ` ( ( A - 1 ) / ( 2 ^ N ) ) ) )
Theorem	dignn0flhalflem2 40935	Lemma 2 for dignn0flhalf 40937. (Contributed by AV, 7-Jun-2012.)
|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN0 ) -> ( |_ ` ( A / ( 2 ^ ( N + 1 ) ) ) ) = ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ N ) ) ) )
Theorem	dignn0ehalf 40936	The digits of the half of an even nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 3-Jun-2010.)
|- ( ( ( A / 2 ) e. NN0 /\ A e. NN0 /\ I e. NN0 ) -> ( ( I + 1 ) (digit ` 2 ) A ) = ( I (digit ` 2 ) ( A / 2 ) ) )
Theorem	dignn0flhalf 40937	The digits of the rounded half of a nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 7-Jun-2010.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ I e. NN0 ) -> ( ( I + 1 ) (digit ` 2 ) A ) = ( I (digit ` 2 ) ( |_ ` ( A / 2 ) ) ) )
Theorem	nn0sumshdiglemA 40938*	Lemma for nn0sumshdig 40942 (induction step, even multiplicant). (Contributed by AV, 3-Jun-2020.)
|- ( ( ( a e. NN /\ ( a / 2 ) e. NN ) /\ y e. NN ) -> ( A. x e. NN0 ( (#b ` x ) = y -> x = sum_ k e. ( 0..^ y ) ( ( k (digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( (#b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0..^ ( y + 1 ) ) ( ( k (digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
Theorem	nn0sumshdiglemB 40939*	Lemma for nn0sumshdig 40942 (induction step, odd multiplicant). (Contributed by AV, 7-Jun-2020.)
|- ( ( ( a e. NN /\ ( ( a - 1 ) / 2 ) e. NN0 ) /\ y e. NN ) -> ( A. x e. NN0 ( (#b ` x ) = y -> x = sum_ k e. ( 0..^ y ) ( ( k (digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( (#b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0..^ ( y + 1 ) ) ( ( k (digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
Theorem	nn0sumshdiglem1 40940*	Lemma 1 for nn0sumshdig 40942 (induction step). (Contributed by AV, 7-Jun-2020.)
|- ( y e. NN -> ( A. a e. NN0 ( (#b ` a ) = y -> a = sum_ k e. ( 0..^ y ) ( ( k (digit ` 2 ) a ) x. ( 2 ^ k ) ) ) -> A. a e. NN0 ( (#b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0..^ ( y + 1 ) ) ( ( k (digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )
Theorem	nn0sumshdiglem2 40941*	Lemma 2 for nn0sumshdig 40942. (Contributed by AV, 7-Jun-2020.)
|- ( L e. NN -> A. a e. NN0 ( (#b ` a ) = L -> a = sum_ k e. ( 0..^ L ) ( ( k (digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
Theorem	nn0sumshdig 40942*	A nonnegative integer can be represented as sum of its shifted bits. (Contributed by AV, 7-Jun-2020.)
|- ( A e. NN0 -> A = sum_ k e. ( 0..^ (#b ` A ) ) ( ( k (digit ` 2 ) A ) x. ( 2 ^ k ) ) )
21.33.16.12  Algorithms for the multiplication of nonnegative integers
Theorem	nn0mulfsum 40943*	Trivial algorithm to calculate the product of two nonnegative integers a and b by adding up b a times. (Contributed by AV, 17-May-2020.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = sum_ k e. ( 1 ... A ) B )
Theorem	nn0mullong 40944*	Standard algorithm (also known as "long multiplication" or "grade-school multiplication") to calculate the product of two nonnegative integers a and b by multiplying the multiplicand b by each digit of the multiplier a and then add up all the properly shifted results. Here, the binary representation of the multiplier a is used, i.e. the above mentioned "digits" are 0 or 1. This is a similar result as provided by smumul 14546. (Contributed by AV, 7-Jun-2020.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = sum_ k e. ( 0..^ (#b ` A ) ) ( ( ( k (digit ` 2 ) A ) x. ( 2 ^ k ) ) x. B ) )
21.34  Mathbox for David A. Wheeler This is the mathbox of David A. Wheeler, dwheeler at dwheeler dot com. Among other things, I have added a number of formal definitions for widely-used functions, e.g., those defined in ISO 80000-2:2009(E) Quantities and units - Part 2: Mathematical signs and symbols used in the natural sciences and technology and the NIST Digital Library of Mathematical Functions http://dlmf.nist.gov/.
21.34.1  Natural deduction
Theorem	19.8ad 40945	If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1955. (Contributed by DAW, 13-Feb-2017.)
|- ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	sbidd 40946	An identity theorem for substitution. See sbid 2101. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
|- ( ph -> [ x / x ] ps )   =>    |- ( ph -> ps )
Theorem	sbidd-misc 40947	An identity theorem for substitution. See sbid 2101. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
|- ( ( ph -> [ x / x ] ps ) <-> ( ph -> ps ) )
21.34.2  Greater than, greater than or equal to. As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Here we formally define the widely-used relations 'greater than' and 'greater than or equal to', so that we have formal definitions of them, as well as a few related theorems.
Syntax	cge-real 40948	Extend wff notation to include the 'greater than or equal to' relation, see df-gte 40950.
class >_
Syntax	cgt 40949	Extend wff notation to include the 'greater than' relation, see df-gt 40951.
class >
Definition	df-gte 40950	Define the 'greater than or equal' predicate over the reals. Defined in ISO 80000-2:2009(E) operation 2-7.10. It is used as a primitive in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. This relation is merely the converse of the 'less than or equal to' relation defined by df-le 9699. We do not write this as ( x >_ y <-> y <_ x ), and similarly we do not write ` > ` as ( x > y <-> y < x ), because these are not definitional axioms as understood by mmj2 (those definitions will be flagged as being "potentially non-conservative"). We could write them this way: |- > = { <. x , y >. | ( ( x e. RR* /\ y e. RR* ) /\ y < x ) } and |- >_ = { <. x , y >. | ( ( x e. RR* /\ y e. RR* ) /\ y <_ x ) } but these are very complicated. This definition of >_, and the similar one for > (df-gt 40951), are a bit strange when you see them for the first time, but these definitions are much simpler for us to process and are clearly conservative definitions. (My thanks to Mario Carneiro for pointing out this simpler approach.) See gte-lte 40952 for a more conventional expression of the relationship between < and >. As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Thus, we discourage its use, but include its definition so that there is a formal definition of this symbol. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
|- >_ = `' <_
Definition	df-gt 40951	The 'greater than' relation is merely the converse of the 'less than or equal to' relation defined by df-lt 9570. Defined in ISO 80000-2:2009(E) operation 2-7.12. See df-gte 40950 for a discussion on why this approach is used for the definition. See gt-lt 40953 and gt-lth 40955 for more conventional expression of the relationship between < and >. As a stylistic issue, set.mm prefers 'less than or equal' instead of 'greater than or equal' to reduce the number of conversion steps. Thus, we discourage its use, but include its definition so that there is a formal definition of this symbol. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
|- > = `' <
Theorem	gte-lte 40952	Simple relationship between <_ and >_. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
|- ( ( A e. _V /\ B e. _V ) -> ( A >_ B <-> B <_ A ) )
Theorem	gt-lt 40953	Simple relationship between < and >. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
|- ( ( A e. _V /\ B e. _V ) -> ( A > B <-> B < A ) )
Theorem	gte-lteh 40954	Relationship between <_ and >_ using hypotheses. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( A >_ B <-> B <_ A )
Theorem	gt-lth 40955	Relationship between < and > using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( A > B <-> B < A )
Theorem	ex-gt 40956	Simple example of >, in this case, 0 is not greater than 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017.) (New usage is discouraged.)
|- -. 0 > 0
Theorem	ex-gte 40957	Simple example of >_, in this case, 0 is greater than or equal to 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017.) (New usage is discouraged.)
|- 0 >_ 0
21.34.3  Hyperbolic trigonometric functions It is a convention of set.mm to not use sinh and so on directly, and instead of use expansions such as ( cos ` ( _i x. x ) ). However, I believe it's important to give formal definitions for these conventional functions as they are typically used, so here they are. A few related identities are also proved.
Syntax	csinh 40958	Extend class notation to include the hyperbolic sine function, see df-sinh 40961.
class sinh
Syntax	ccosh 40959	Extend class notation to include the hyperbolic cosine function. see df-cosh 40962.
class cosh
Syntax	ctanh 40960	Extend class notation to include the hyperbolic tangent function, see df-tanh 40963.
class tanh
Definition	df-sinh 40961	Define the hyperbolic sine function (sinh). We define it this way for cmpt 4454, which requires the form ( x e. A |-> B ). See sinhval-named 40964 for a simple way to evaluate it. We define this function by dividing by _i, which uses fewer operations than many conventional definitions (and thus is more convenient to use in metamath). See sinh-conventional 40967 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.)
|- sinh = ( x e. CC |-> ( ( sin ` ( _i x. x ) ) / _i ) )
Definition	df-cosh 40962	Define the hyperbolic cosine function (cosh). We define it this way for cmpt 4454, which requires the form ( x e. A |-> B ). (Contributed by David A. Wheeler, 10-May-2015.)
|- cosh = ( x e. CC |-> ( cos ` ( _i x. x ) ) )
Definition	df-tanh 40963	Define the hyperbolic tangent function (tanh). We define it this way for cmpt 4454, which requires the form ( x e. A |-> B ). (Contributed by David A. Wheeler, 10-May-2015.)
|- tanh = ( x e. ( `'cosh " ( CC \ { 0 } ) ) |-> ( ( tan ` ( _i x. x ) ) / _i ) )
Theorem	sinhval-named 40964	Value of the named sinh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-sinh 40961. See sinhval 14285 for a theorem to convert this further. See sinh-conventional 40967 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.)
|- ( A e. CC -> (sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
Theorem	coshval-named 40965	Value of the named cosh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-cosh 40962. See coshval 14286 for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015.)
|- ( A e. CC -> (cosh ` A ) = ( cos ` ( _i x. A ) ) )
Theorem	tanhval-named 40966	Value of the named tanh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-tanh 40963. (Contributed by David A. Wheeler, 10-May-2015.)
|- ( A e. ( `'cosh " ( CC \ { 0 } ) ) -> (tanh ` A ) = ( ( tan ` ( _i x. A ) ) / _i ) )
Theorem	sinh-conventional 40967	Conventional definition of sinh. Here we show that the sinh definition we're using has the same meaning as the conventional definition used in some other sources. We choose a slightly different definition of sinh because it has fewer operations, and thus is more convenient to manipulate using metamath. (Contributed by David A. Wheeler, 10-May-2015.)
|- ( A e. CC -> (sinh ` A ) = ( -u _i x. ( sin ` ( _i x. A ) ) ) )
Theorem	sinhpcosh 40968	Prove that (sinh ` A ) + (cosh ` A ) = ( exp ` A ) using the conventional hyperbolic trigonometric functions. (Contributed by David A. Wheeler, 27-May-2015.)
|- ( A e. CC -> ( (sinh ` A ) + (cosh ` A ) ) = ( exp ` A ) )
21.34.4  Reciprocal trigonometric functions (sec, csc, cot) Define the traditional reciprocal trigonometric functions secant (sec), cosecant (csc), and cotangent (cos), along with various identities involving them.
Syntax	csec 40969	Extend class notation to include the secant function, see df-sec 40972.
class sec
Syntax	ccsc 40970	Extend class notation to include the cosecant function, see df-csc 40973.
class csc
Syntax	ccot 40971	Extend class notation to include the cotangent function, see df-cot 40974.
class cot
Definition	df-sec 40972*	Define the secant function. We define it this way for cmpt 4454, which requires the form ( x e. A |-> B ). The sec function is defined in ISO 80000-2:2009(E) operation 2-13.6 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 (Contributed by David A. Wheeler, 14-Mar-2014.)
|- sec = ( x e. { y e. CC | ( cos ` y ) =/= 0 } |-> ( 1 / ( cos ` x ) ) )
Definition	df-csc 40973*	Define the cosecant function. We define it this way for cmpt 4454, which requires the form ( x e. A |-> B ). The csc function is defined in ISO 80000-2:2009(E) operation 2-13.7 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 (Contributed by David A. Wheeler, 14-Mar-2014.)
|- csc = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( 1 / ( sin ` x ) ) )
Definition	df-cot 40974*	Define the cotangent function. We define it this way for cmpt 4454, which requires the form ( x e. A |-> B ). The cot function is defined in ISO 80000-2:2009(E) operation 2-13.5 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 (Contributed by David A. Wheeler, 14-Mar-2014.)
|- cot = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( cos ` x ) / ( sin ` x ) ) )
Theorem	secval 40975	Value of the secant function. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )
Theorem	cscval 40976	Value of the cosecant function. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) = ( 1 / ( sin ` A ) ) )
Theorem	cotval 40977	Value of the cotangent function. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) = ( ( cos ` A ) / ( sin ` A ) ) )
Theorem	seccl 40978	The closure of the secant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) e. CC )
Theorem	csccl 40979	The closure of the cosecant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) e. CC )
Theorem	cotcl 40980	The closure of the cotangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) e. CC )
Theorem	reseccl 40981	The closure of the secant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
|- ( ( A e. RR /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) e. RR )
Theorem	recsccl 40982	The closure of the cosecant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
|- ( ( A e. RR /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) e. RR )
Theorem	recotcl 40983	The closure of the cotangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
|- ( ( A e. RR /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) e. RR )
Theorem	recsec 40984	The reciprocal of secant is cosine. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) = ( 1 / ( sec ` A ) ) )
Theorem	reccsc 40985	The reciprocal of cosecant is sine. (Contributed by David A. Wheeler, 14-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) = ( 1 / ( csc ` A ) ) )
Theorem	reccot 40986	The reciprocal of cotangent is tangent. (Contributed by David A. Wheeler, 21-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( 1 / ( cot ` A ) ) )
Theorem	rectan 40987	The reciprocal of tangent is cotangent. (Contributed by David A. Wheeler, 21-Mar-2014.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 /\ ( cos ` A ) =/= 0 ) -> ( cot ` A ) = ( 1 / ( tan ` A ) ) )
Theorem	sec0 40988	The value of the secant function at zero is one. (Contributed by David A. Wheeler, 16-Mar-2014.)
|- ( sec ` 0 ) = 1
Theorem	onetansqsecsq 40989	Prove the tangent squared secant squared identity ( 1 + ( ( tan A ) ^ 2 ) ) = ( ( sec A ) ^ 2 ) ). (Contributed by David A. Wheeler, 25-May-2015.)
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( ( sec ` A ) ^ 2 ) )
Theorem	cotsqcscsq 40990	Prove the tangent squared cosecant squared identity ( 1 + ( ( cot A ) ^ 2 ) ) = ( ( csc A ) ^ 2 ) ). (Contributed by David A. Wheeler, 27-May-2015.)
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( cot ` A ) ^ 2 ) ) = ( ( csc ` A ) ^ 2 ) )
21.34.5  Identities for "if" Utility theorems for "if".
Theorem	ifnmfalse 40991	If A is not a member of B, but an "if" condition requires it, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs vs. applying iffalse 3881 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( A e/ B -> if ( A e. B , C , D ) = D )
21.34.6  Decimal point Define the decimal point operator and the decimal fraction constructor. This can model traditional decimal point notation, and serve as a convenient way to write some fractional numbers. See df-dp 40995 and df-dp2 40994 for more information; ~? dfpval provides a more convenient way to obtain a value. This is intentionally similar to df-dec 11075. TODO: Fix non-existent label dfpval.
Syntax	cdp2 40992	Constant used for decimal fraction constructor. See df-dp2 40994.
class _ A B
Syntax	cdp 40993	Decimal point operator. See df-dp 40995.
class period
Definition	df-dp2 40994	Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 11075. (Contributed by David A. Wheeler, 15-May-2015.)
|- _ A B = ( A + ( B / 10 ) )
Definition	df-dp 40995*	Define the period (decimal point) operator. For example, ( 1 period 5 ) = ( 3 / 2 ), and -u (; 3 2 period_ 7_ 1 8 ) = -u (;;;; 3 2 7 1 8 / ;;; 1 0 0 0 ) Unary minus, if applied, should normally be applied in front of the parentheses. Metamath intentionally does not have a built-in construct for numbers, so it can show that numbers are something you can build based on set theory. However, that means that metamath has no built-in way to handle decimal numbers as traditionally written, e.g., "2.54", and its parsing system intentionally does not include the complexities necessary to define such a parsing system. Here we create a system for modeling traditional decimal point notation; it is not syntactically identical, but it is sufficiently similar so it is a reasonable model of decimal point notation. It should also serve as a convenient way to write some fractional numbers. The RHS is RR, not QQ; this should simplify some proofs. The LHS is NN0, since that is what is used in practice. The definition intentionally does not allow negative numbers on the LHS; if it did, nonzero fractions would produce the wrong results. (It would be possible to define the decimal point to do this, but using it would be more complicated, and the expression -u ( A period B ) is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.)
|- period = ( x e. NN0 , y e. RR |-> _ x y )
Theorem	dp2cl 40996	Define the closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR )
Theorem	dpval 40997	Define the value of the decimal point operator. See df-dp 40995. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( ( A e. NN0 /\ B e. RR ) -> ( A period B ) = _ A B )
Theorem	dpcl 40998	Prove that the closure of the decimal point is RR as we have defined it. See df-dp 40995. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( ( A e. NN0 /\ B e. RR ) -> ( A period B ) e. RR )
Theorem	dpfrac1 40999	Prove a simple equivalence involving the decimal point. See df-dp 40995 and dpcl 40998. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( ( A e. NN0 /\ B e. RR ) -> ( A period B ) = (; A B / 10 ) )
21.34.7  Logarithms generalized to arbitrary base using ` logb ` Most of this subsection was moved to main set.mm, section "Logarithms to an arbitrary base".
Theorem	logb2aval 41000	Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb <. B , X >. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( logb ` <. B , X >. ) = ( ( log ` X ) / ( log ` B ) ) )