Home | Metamath
Proof ExplorerTheorem List
(p. 285 of 328)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22421) |
Hilbert Space Explorer
(22422-23944) |
Users' Mathboxes
(23945-32762) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | 2pthfrgra 28401* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

FriendGrph PathOn | ||

Theorem | 3cyclfrgrarn1 28402* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |

FriendGrph | ||

Theorem | 3cyclfrgrarn 28403* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |

FriendGrph | ||

Theorem | 3cyclfrgrarn2 28404* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 10-Dec-2017.) |

FriendGrph | ||

Theorem | 3cyclfrgra 28405* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

FriendGrph Cycles | ||

Theorem | 4cycl2v2nb 28406 | In a (maybe degenerated) 4-cycle, two vertices have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

Theorem | 4cycl2vnunb 28407* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

Theorem | n4cyclfrgra 28408 | There is no 4-cycle in a friendship graph, see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

FriendGrph Cycles | ||

Theorem | 4cyclusnfrgra 28409 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

USGrph FriendGrph | ||

Theorem | frgranbnb 28410 | If two neighbors of a specific vertex have a common neighbor in a friendship graph, then this common neighbor must be the specific vertex. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

Neighbors FriendGrph | ||

Theorem | frconngra 28411 | A friendship graph is connected, see 1. remark after Proposition 1 of [MertziosUnger] p. 153 : "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

FriendGrph ConnGrph | ||

Theorem | vdfrgra0 28412 | A vertex in a friendship graph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgfrgra0 28413 | A vertex in a friendship graph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdn0frgrav2 28414 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgn0frgrav2 28415 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdn1frgrav2 28416 | Any vertex in a friendship graph does not have degree 1, see 2. remark after Proposition 1 of [MertziosUnger] p. 153 : "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgn1frgrav2 28417 | Any vertex in a friendship graph does not have degree 1, see 2. remark after Proposition 1 of [MertziosUnger] p. 153 : "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgfrgragt2 28418 | Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see 3. remark after Proposition 1 of [MertziosUnger] p. 153 : "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | frgrancvvdeqlem1 28419* | Lemma 1 for frgrancvvdeq 28431. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem2 28420* | Lemma 2 for frgrancvvdeq 28431. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem3 28421* | Lemma 3 for frgrancvvdeq 28431. In a friendship graph, for each neighbor of a vertex there is exacly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem4 28422* | Lemma 4 for frgrancvvdeq 28431. The restricted iota of a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) |

Neighbors Neighbors FriendGrph Neighbors | ||

Theorem | frgrancvvdeqlem5 28423* | Lemma 5 for frgrancvvdeq 28431. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem6 28424* | Lemma 6 for frgrancvvdeq 28431. The mapping of neighbors to neighbors applied on a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph Neighbors | ||

Theorem | frgrancvvdeqlem7 28425* | Lemma 7 for frgrancvvdeq 28431. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemA 28426* | Lemma A for frgrancvvdeq 28431. This corresponds to the following observation in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemB 28427* | Lemma B for frgrancvvdeq 28431. This corresponds to the following observation in [Huneke] p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemC 28428* | Lemma C for frgrancvvdeq 28431. This corresponds to the following observation in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem8 28429* | Lemma 8 for frgrancvvdeq 28431. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem9 28430* | Lemma 9 for frgrancvvdeq 28431. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

FriendGrph Neighbors Neighbors Neighbors | ||

Theorem | frgrancvvdeq 28431* | In a finite friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to the first Lemma ("claim") of the proof of the (friendship) theorem in [Huneke] p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph Neighbors VDeg VDeg | ||

Theorem | frgrancvvdgeq 28432* | In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to the first Lemma ("claim") of the proof of the (friendship) theorem in [Huneke] p. 1: "If x,y, are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph Neighbors VDeg VDeg | ||

Theorem | frgrawopreglem1 28433* | Lemma 1 for frgrawopreg 28438. In a friendship graph, the classes A and B are sets. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem2 28434* | Lemma 2 for frgrawopreg 28438. In a friendship graph with at least 2 vertices, the degree of a vertex must be at least 2. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem3 28435* | Lemma 3 for frgrawopreg 28438. The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

VDeg VDeg VDeg | ||

Theorem | frgrawopreglem4 28436* | Lemma 4 for frgrawopreg 28438. In a friendship graph each vertex with degree K is connected with a vertex with degree other than K. This corresponds to the observation in the proof of [Huneke] p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B." (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem5 28437* | Lemma 5 for frgrawopreg 28438. If A as well as B contain at least two vertices in a friendship graph, there is a 4-cycle in the graph. This corresponds to the observation in the proof of [Huneke] p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreg 28438* | In a friendship graph there are either no vertices or exactly one vertex having degree K, or all or all except one vertices have degree K. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreg1 28439* | According to the proof of the friendship theorem in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

VDeg FriendGrph | ||

Theorem | frgrawopreg2 28440* | According to the proof of the friendship theorem in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

VDeg FriendGrph | ||

Theorem | frgraregorufr0 28441* | For each nonnegative integer K there are either no edges having degree K, or all vertices have degree K in a friendship graph, unless there is a universal friend. This corresponds to the second claim in the proof of the friendship theorem in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

FriendGrph VDeg VDeg | ||

Theorem | frgraregorufr 28442* | For each nonnegative integer K there are either no edges having degree K, or all vertices have degree K in a friendship graph, unless there is a universal friend. This corresponds to the second claim in the proof of the friendship theorem in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

FriendGrph VDeg VDeg | ||

Theorem | frgraeu 28443* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

FriendGrph | ||

Theorem | frg2woteu 28444* | For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

FriendGrph 2WalksOnOt | ||

Theorem | frg2wotn0 28445 | In a friendship graph, there is always a path/walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

FriendGrph 2WalksOnOt | ||

Theorem | frg2wot1 28446 | In a friendship graph, there is exactly one walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |

FriendGrph 2WalksOnOt | ||

Theorem | frg2spot1 28447 | In a friendship graph, there is exactly one simple path of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |

FriendGrph 2SPathOnOt | ||

Theorem | frg2woteqm 28448 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 20-Feb-2018.) |

FriendGrph 2WalksOnOt 2WalksOnOt | ||

Theorem | frg2woteq 28449 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 14-Feb-2018.) |

FriendGrph 2WalksOnOt 2WalksOnOt | ||

Theorem | 2spotdisj 28450* | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |

Disj 2SPathOnOt | ||

Theorem | 2spotiundisj 28451* | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.) |

Disj
2SPathOnOt | ||

Theorem | frghash2spot 28452 | The number of simple paths of length 2 is n*(n-1) in a friendship graph with vertices. This corresponds to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, the order of vertices is not respected by Huneke, so he only counts half of the paths which are existing when respecting the order as it is the case for simple paths represented by orderes triples. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |

FriendGrph 2SPathOnOt | ||

Theorem | 2spot0 28453 | If there are no vertices, then there are no paths (of length 2), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

2SPathOnOt | ||

Theorem | usg2spot2nb 28454* | The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |

2SPathOnOt USGrph Neighbors Neighbors | ||

Theorem | usgreghash2spotv 28455* | According to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For simple paths of length 2 represented by ordered triples, we have again k*(k-1) such paths. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |

2SPathOnOt USGrph VDeg | ||

Theorem | usgreg2spot 28456* | In a finite k-regular graph the set of all paths of length two is the union of all the paths of length 2 over the vertices which are in the the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |

2SPathOnOt USGrph VDeg 2SPathOnOt | ||

Theorem | 2spotmdisj 28457* | The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

2SPathOnOt Disj | ||

Theorem | usgreghash2spot 28458* | In a finite k-regular graph with N vertices there are N times " choose 2 " paths with length 2, according to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by ordered triples, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

USGrph VDeg 2SPathOnOt | ||

Theorem | frgregordn0 28459* | If a nonempty friendship graph is k-regular, its order is k(k-1)+1. This corresponds to the third claim in the proof of the friendship theorem in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

FriendGrph VDeg | ||

19.23 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)
| ||

19.23.1 Natural deduction | ||

Theorem | 19.8ad 28460 | If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1762. (Contributed by DAW, 13-Feb-2017.) |

Theorem | sbidd 28461 | An identity theorem for substitution. See sbid 1947. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.) |

Theorem | sbidd-misc 28462 | An identity theorem for substitution. See sbid 1947. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.) |

19.23.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 28463 | Extend wff notation to include the 'greater than or equal to' relation, see df-gte 28465. |

Syntax | cgt 28464 | Extend wff notation to include the 'greater than' relation, see df-gt 28466. |

Definition | df-gte 28465 |
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 9126.
We do not write this as , and similarly we do
not write ` > ` as , 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:
and
but
these are very complicated. This definition of , and the similar
one for (df-gt 28466), 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 28467 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 (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

Definition | df-gt 28466 |
The 'greater than' relation is merely the converse of the 'less than or
equal to' relation defined by df-lt 9003. Defined in ISO 80000-2:2009(E)
operation 2-7.12. See df-gte 28465 for a discussion on why this approach is
used for the definition. See gt-lt 28468 and gt-lth 28470 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 (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.) |

Theorem | gte-lte 28467 | Simple relationship between and . (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

Theorem | gt-lt 28468 | Simple relationship between and . (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.) |

Theorem | gte-lteh 28469 | Relationship between and using hypotheses. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

Theorem | gt-lth 28470 | Relationship between and using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.) |

Theorem | ex-gt 28471 | 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.) |

Theorem | ex-gte 28472 | 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.) |

19.23.3 Hyperbolic trig functionsIt is a convention of set.mm to not use sinh and so on directly, and instead of use expansions such as . 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 28473 | Extend class notation to include the hyperbolic sine function, see df-sinh 28476. |

sinh | ||

Syntax | ccosh 28474 | Extend class notation to include the hyperbolic cosine function. see df-cosh 28477. |

cosh | ||

Syntax | ctanh 28475 | Extend class notation to include the hyperbolic tangent function, see df-tanh 28478. |

tanh | ||

Definition | df-sinh 28476 | Define the hyperbolic sine function (sinh). We define it this way for cmpt 4266, which requires the form . See sinhval-named 28479 for a simple way to evaluate it. We define this function by dividing by , which uses fewer operations than many conventional definitions (and thus is more convenient to use in metamath). See sinh-conventional 28482 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 | ||

Definition | df-cosh 28477 | Define the hyperbolic cosine function (cosh). We define it this way for cmpt 4266, which requires the form . (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

Definition | df-tanh 28478 | Define the hyperbolic tangent function (tanh). We define it this way for cmpt 4266, which requires the form . (Contributed by David A. Wheeler, 10-May-2015.) |

tanh cosh | ||

Theorem | sinhval-named 28479 | 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 28476. See sinhval 12755 for a theorem to convert this further. See sinh-conventional 28482 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 | ||

Theorem | coshval-named 28480 | 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 28477. See coshval 12756 for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

Theorem | tanhval-named 28481 | 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 28478. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh tanh | ||

Theorem | sinh-conventional 28482 | 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.) |

sinh | ||

Theorem | sinhpcosh 28483 | Prove that sinh cosh using the conventional hyperbolic trig functions. (Contributed by David A. Wheeler, 27-May-2015.) |

sinh cosh | ||

19.23.4 Reciprocal trig 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 28484 | Extend class notation to include the secant function, see df-sec 28487. |

Syntax | ccsc 28485 | Extend class notation to include the cosecant function, see df-csc 28488. |

Syntax | ccot 28486 | Extend class notation to include the cotangent function, see df-cot 28489. |

Definition | df-sec 28487* | Define the secant function. We define it this way for cmpt 4266, which requires the form . 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.) |

Definition | df-csc 28488* | Define the cosecant function. We define it this way for cmpt 4266, which requires the form . 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.) |

Definition | df-cot 28489* | Define the cotangent function. We define it this way for cmpt 4266, which requires the form . 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.) |

Theorem | secval 28490 | Value of the secant function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | cscval 28491 | Value of the cosecant function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | cotval 28492 | Value of the cotangent function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | seccl 28493 | The closure of the secant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | csccl 28494 | The closure of the cosecant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | cotcl 28495 | The closure of the cotangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | reseccl 28496 | The closure of the secant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | recsccl 28497 | The closure of the cosecant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | recotcl 28498 | The closure of the cotangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | recsec 28499 | The reciprocal of secant is cosine. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | reccsc 28500 | The reciprocal of cosecant is sine. (Contributed by David A. Wheeler, 14-Mar-2014.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |