Home | Metamath
Proof ExplorerTheorem List
(p. 282 of 324)
| < 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-22370) |
Hilbert Space Explorer
(22371-23893) |
Users' Mathboxes
(23894-32378) |

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

Statement | ||

Theorem | usgreg2spot 28101* | 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 28102* | 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 28103* | 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 28104* | 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 28105 | If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1758. (Contributed by DAW, 13-Feb-2017.) |

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

Theorem | sbidd-misc 28107 | An identity theorem for substitution. See sbid 1943. 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 28108 | Extend wff notation to include the 'greater than or equal to' relation, see df-gte 28110. |

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

Definition | df-gte 28110 |
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 9080.
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 28111), 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 28112 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 28111 |
The 'greater than' relation is merely the converse of the 'less than or
equal to' relation defined by df-lt 8957. Defined in ISO 80000-2:2009(E)
operation 2-7.12. See df-gte 28110 for a discussion on why this approach is
used for the definition. See gt-lt 28113 and gt-lth 28115 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 28112 | Simple relationship between and . (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

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

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

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

Theorem | ex-gt 28116 | 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 28117 | 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 28118 | Extend class notation to include the hyperbolic sine function, see df-sinh 28121. |

sinh | ||

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

cosh | ||

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

tanh | ||

Definition | df-sinh 28121 | Define the hyperbolic sine function (sinh). We define it this way for cmpt 4224, which requires the form . See sinhval-named 28124 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 28127 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 28122 | Define the hyperbolic cosine function (cosh). We define it this way for cmpt 4224, which requires the form . (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

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

tanh cosh | ||

Theorem | sinhval-named 28124 | 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 28121. See sinhval 12706 for a theorem to convert this further. See sinh-conventional 28127 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 28125 | 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 28122. See coshval 12707 for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

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

cosh tanh | ||

Theorem | sinh-conventional 28127 | 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 28128 | 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 28129 | Extend class notation to include the secant function, see df-sec 28132. |

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

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

Definition | df-sec 28132* | Define the secant function. We define it this way for cmpt 4224, 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 28133* | Define the cosecant function. We define it this way for cmpt 4224, 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 28134* | Define the cotangent function. We define it this way for cmpt 4224, 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 28135 | Value of the secant function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

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

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

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

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

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

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

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

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

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

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

Theorem | reccot 28146 | The reciprocal of cotangent is tangent. (Contributed by David A. Wheeler, 21-Mar-2014.) |

Theorem | rectan 28147 | The reciprocal of tangent is cotangent. (Contributed by David A. Wheeler, 21-Mar-2014.) |

Theorem | sec0 28148 | The value of the secant function at zero is one. (Contributed by David A. Wheeler, 16-Mar-2014.) |

Theorem | onetansqsecsq 28149 | Prove the tangent squared secant squared identity A ) ^ 2 ) ) = ( ( sec . (Contributed by David A. Wheeler, 25-May-2015.) |

Theorem | cotsqcscsq 28150 | Prove the tangent squared cosecant squared identity A ) ^ 2 ) ) = ( ( csc . (Contributed by David A. Wheeler, 27-May-2015.) |

19.23.5 Identities for "if"Utility theorems for "if". | ||

Theorem | ifnmfalse 28151 | 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 3704 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |

19.23.6 Not-member-of | ||

Theorem | AnelBC 28152 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using . (Contributed by David A. Wheeler, 10-May-2015.) |

19.23.7 Decimal pointDefine 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 28156 and df-dp2 28155 for more information; ~? dfpval provides a more convenient way to obtain a value. This is intentionally similar to df-dec 10337. TODO: Fix non-existent label dfpval. | ||

Syntax | cdp2 28153 | Constant used for decimal fraction constructor. See df-dp2 28155. |

_ | ||

Syntax | cdp 28154 | Decimal point operator. See df-dp 28156. |

Definition | df-dp2 28155 | Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 10337. (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Definition | df-dp 28156* |
Define the (decimal point) operator. For example,
, and
;__ ;;;; ;;;
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 , not ; this should simplify some proofs. The LHS is , 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 is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Theorem | dp2cl 28157 | Define the closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Theorem | dpval 28158 | Define the value of the decimal point operator. See df-dp 28156. (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Theorem | dpcl 28159 | Prove that the closure of the decimal point is as we have defined it. See df-dp 28156. (Contributed by David A. Wheeler, 15-May-2015.) |

Theorem | dpfrac1 28160 | Prove a simple equivalence involving the decimal point. See df-dp 28156 and dpcl 28159. (Contributed by David A. Wheeler, 15-May-2015.) |

; | ||

19.23.8 Signum (sgn or sign)
function | ||

Syntax | csgn 28161 | Extend class notation to include the Signum function. |

sgn | ||

Definition | df-sgn 28162 | Signum function. Pronounced "signum" , otherwise it might be confused with "sine". Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. We define this over (df-xr 9078) instead of so that it can accept and . Note that df-psgn 27274 defines the sign of a permutation, which is different. Value shown in sgnval 28163. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgnval 28163 | Value of Signum function. Pronounced "signum" . See df-sgn 28162. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgn0 28164 | Proof that signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgnp 28165 | Proof that signum of positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgnrrp 28166 | Proof that signum of positive reals is 1. (Contributed by David A. Wheeler, 18-May-2015.) |

sgn | ||

Theorem | sgn1 28167 | Proof that the signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |

sgn | ||

Theorem | sgnpnf 28168 | Proof that the signum of is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |

sgn | ||

Theorem | sgnn 28169 | Proof that signum of negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgnmnf 28170 | Proof that the signum of is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |

sgn | ||

19.23.9 Ceiling function | ||

Syntax | ccei 28171 | Extend class notation to include the ceiling function. |

⌈ | ||

Definition | df-ceiling 28172 |
The ceiling function. Defined in ISO 80000-2:2009(E) operation 2-9.18 and
the "NIST Digital Library of Mathematical Functions" , front
introduction,
"Common Notations and Definitions" section at
http://dlmf.nist.gov/front/introduction#Sx4.
By convention metamath users tend to expand this construct directly, instead of using the definition. However, we want to make sure this is separately and formally defined. Proof ceicl 11183 shows that the ceiling function returns an integer when provided a real. Formalized by David A. Wheeler. (Contributed by David A. Wheeler, 19-May-2015.) |

⌈ | ||

Theorem | ceilingval 28173 | The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) |

⌈ | ||

Theorem | ceilingcl 28174 | Closure of the ceiling function; the real work is in ceicl 11183. (Contributed by David A. Wheeler, 19-May-2015.) |

⌈ | ||

19.23.10 Logarithms generalized to arbitrary
base using ` logb ` | ||

Theorem | ene0 28175 | is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |

Theorem | ene1 28176 | is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |

Theorem | elogb 28177 | Using as the base is the same as . (Contributed by David A. Wheeler, 17-Oct-2017.) |

logb | ||

19.23.11 Logarithm laws generalized to an
arbitrary base - log_Define "log using an arbitrary base" function and then prove some of its properties. This builds on previous work by Stefan O'Rear. This supports the notational form log_; that looks a little more like traditional notation, but is different from other 2-parameter functions. E.G., log_;; This form is less convenient to work with inside metamath as compared to the logb form defined separately. | ||

Syntax | clog_ 28178 | Extend class notation to include the logarithm generalized to an arbitrary base. |

log_ | ||

Definition | df-log_ 28179* | Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as log_ for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.) |

log_ | ||

19.23.12 MiscellaneousMiscellaneous proofs. | ||

Theorem | 5m4e1 28180 | Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.) |

Theorem | 2p2ne5 28181 | Prove that . In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.) |

Theorem | resolution 28182 | Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.) |

19.24 Mathbox for Alan Sare | ||

19.24.1 Supplementary "adant"
deductions | ||

Theorem | ad4ant13 28183 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant14 28184 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant123 28185 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant124 28186 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant134 28187 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant23 28188 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant24 28189 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad4ant234 28190 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant12 28191 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant13 28192 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant14 28193 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant15 28194 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant23 28195 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant24 28196 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant25 28197 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant245 28198 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant234 28199 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

Theorem | ad5ant235 28200 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |