Home | Metamath
Proof ExplorerTheorem List
(p. 207 of 309)
| < 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-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |

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

Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qdrng 20601 | The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrng0 20602 | The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrng1 20603 | The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrngneg 20604 | The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s}
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrngdiv 20605 | The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} /_{r} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qabvle 20606 | By using induction on , we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qabvexp 20607 | Induct the product rule abvmul 15429 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostthlem1 20608* | Lemma for ostth 20620. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostthlem2 20609* | Lemma for ostth 20620. Refine ostthlem1 20608 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qabsabv 20610 | The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicabv 20611* | The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicabvf 20612* | The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicabvcxp 20613* | All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth1 20614* | - Lemma for ostth 20620: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If is equal to on the primes, then by complete induction and the multiplicative property abvmul 15429 of the absolute value, is equal to on all the integers, and ostthlem1 20608 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem2 20615* | Lemma for ostth2 20618. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem3 20616* | Lemma for ostth2 20618. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem4 20617* | Lemma for ostth2 20618. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2 20618* | - Lemma for ostth 20620: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth3 20619* | - Lemma for ostth 20620: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth 20620* | Ostrowski's theorem, which classifies all absolute values on . Any such absolute value must either be the trivial absolute value , a constant exponent times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

PART 14 MISCELLANEA | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.1 Definitional Examples | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-or 20621 | Example for df-or 361. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-an 20622 | Example for df-an 362. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-dif 20623 | Example for df-dif 3081. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-un 20624 | Example for df-un 3083. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-in 20625 | Example for df-in 3085. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-uni 20626 | Example for df-uni 3728. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-ss 20627 | Example for df-ss 3089. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-pss 20628 | Example for df-pss 3091. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-pw 20629 | Example for df-pw 3532. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-pr 20630 | Example for df-pr 3551. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-br 20631 | Example for df-br 3921. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-opab 20632* | Example for df-opab 3975. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-eprel 20633 | Example for df-eprel 4198. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-id 20634 | Example for df-id 4202. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-po 20635 | Example for df-po 4207. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-xp 20636 | Example for df-xp 4594. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-cnv 20637 | Example for df-cnv 4596. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-co 20638 | Example for df-co 4597. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-dm 20639 | Example for df-dm 4598. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-rn 20640 | Example for df-rn 4599. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-res 20641 | Example for df-res 4600. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-ima 20642 | Example for df-ima 4601. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-fv 20643 | Example for df-fv 4608. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-1st 20644 | Example for df-1st 5974. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-2nd 20645 | Example for df-2nd 5975. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 1kp2ke3k 20646 |
Example for df-dec 10004, 1000 + 2000 = 3000.
This proof disproves (by counter-example) the assertion of Hao Wang, who
stated, "There is a theorem in the primitive notation of set theory
that
corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula
would be forbiddingly long... even if (one) knows the definitions and is
asked to simplify the long formula according to them, chances are he will
make errors and arrive at some incorrect result." (Hao Wang,
"Theory and
practice in mathematics" , In Thomas Tymoczko, editor,
This is noted in The proof here starts with , commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 10004 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

;;; ;;; ;;; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-fl 20647 | Example for df-fl 10803. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-dvds 20648 | 3 divides into 6. A demonstration of df-divides 12406. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.2 Natural deduction
examplesThese are examples of how natural deduction rules can be applied in metamath (both as line-for-line translations of ND rules, and as a way to apply deduction forms without being limited to applying ND rules). For more information, see natded 4 and http://us.metamath.org/mpegif/mmnatded.html. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.2 20649 |
Theorem 5.2 of [Laboreo] p. 15, translated line by line using the
interpretation of natural deduction in Metamath.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.2-2 20650. A proof without context is shown in ex-natded5.2i 20651. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.2-2 20650 | A more efficient proof of Theorem 5.2 of [Laboreo] p. 15. Compare with ex-natded5.2 20649 and ex-natded5.2i 20651. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.2i 20651 | The same as ex-natded5.2 20649 and ex-natded5.2-2 20650 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.3 20652 |
Theorem 5.3 of [Laboreo] p. 16, translated line by line using an
interpretation of natural deduction in Metamath.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.3-2 20653.
A proof without context is shown in ex-natded5.3i 20654.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.3-2 20653 | A more efficient proof of Theorem 5.3 of [Laboreo] p. 16. Compare with ex-natded5.3 20652 and ex-natded5.3i 20654. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.3i 20654 | The same as ex-natded5.3 20652 and ex-natded5.3-2 20653 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.5 20655 |
Theorem 5.5 of [Laboreo] p. 18, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof is mtod 170; a proof without context is shown in mto 169. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.7 20656 |
Theorem 5.7 of [Laboreo] p. 19, translated line by line using the
interpretation of natural deduction in Metamath.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.7-2 20657.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.7-2 20657 | A more efficient proof of Theorem 5.7 of [Laboreo] p. 19. Compare with ex-natded5.7 20656. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.8 20658 |
Theorem 5.8 of [Laboreo] p. 20, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.8-2 20659. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.8-2 20659 | A more efficient proof of Theorem 5.8 of [Laboreo] p. 20. For a longer line-by-line translation, see ex-natded5.8 20658. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.13 20660 |
Theorem 5.13 of [Laboreo] p. 20, translated line by line using the
interpretation of natural deduction in Metamath.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.13-2 20661.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.13-2 20661 | A more efficient proof of Theorem 5.13 of [Laboreo] p. 20. Compare with ex-natded5.13 20660. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.20 20662 |
Theorem 9.20 of [Laboreo] p. 43, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof is ex-natded9.20-2 20663. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.20-2 20663 | A more efficient proof of Theorem 9.20 of [Laboreo] p. 45. Compare with ex-natded9.20 20662. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.26 20664* |
Theorem 9.26 of [Laboreo] p. 45, translated line by line using an
interpretation of natural deduction in Metamath. This proof has some
additional complications due to the fact that Metamath's existential
elimination rule does not change bound variables, so we need to verify
that is bound in the conclusion.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). Note that in the original proof, has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 20665. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.26-2 20665* | A more efficient proof of Theorem 9.26 of [Laboreo] p. 45. Compare with ex-natded9.26 20664. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.3 Humor | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.3.1 April Fool's theorem | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | avril1 20666 |
Poisson d'Avril's Theorem. This theorem is noted for its
Selbstdokumentieren property, which means, literally,
"self-documenting" and recalls the principle of quidquid
germanus
dictum sit, altum viditur, often used in set theory. Starting with
the
seemingly simple yet profound fact that any object equals itself
(proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we
demonstrate that the power set of the real numbers, as a relation on the
value of the imaginary unit, does not conjoin with an empty relation on
the product of the additive and multiplicative identity elements,
leading to this startling conclusion that has left even seasoned
professional mathematicians scratching their heads. (Contributed by
Prof. Loof Lirpa, 1-Apr-2005.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 2bornot2b 20667 |
The law of excluded middle. Act III, Theorem 1 of Shakespeare, Hamlet,
Prince of Denmark (1602). Its author leaves its proof as an exercise
for
the reader - "To be, or not to be: that is the question" -
starting a
trend that has become standard in modern-day textbooks, serving to make
the frustrated reader feel inferior, or in some cases to mask the fact
that the author does not know its solution. (Contributed by Prof. Loof
Lirpa, 1-Apr-2006.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | helloworld 20668 | The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://www.roesler-ac.de/wolfram/hello.htm. However, for many years it eluded a proof that it is more than just a conjecture, even though a wily mathematician once claimed, "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." Using an IBM 709 mainframe, a team of mathematicians led by Prof. Loof Lirpa, at the New College of Tahiti, were finally able put it rest with a remarkably short proof only 4 lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 1p1e2apr1 20669 |
One plus one equals two. Using proof-shortening techniques pioneered by
Mr. Mel O'Cat, along with the latest supercomputer technology, Prof.
Loof Lirpa and colleagues were able to shorten Whitehead and Russell's
360-page proof that 1+1=2 in Principia Mathematica to this
remarkable
proof only two steps long, thus establishing a new world's record for this
famous theorem. (Contributed by Prof. Loof Lirpa, 1-Apr-2008.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | eqid1 20670 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle
( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 1div0apr 20671 | Division by zero is forbidden! If we try, we encounter the DO NOT ENTER sign, which in mathematics means it is foolhardy to venture any further, possibly putting the underlying fabric of reality at risk. Based on a dare by David A. Wheeler. (Contributed by Mario Carneiro, 1-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.4 (Future - to be reviewed and
classified) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.4.1 Planar incidence geometry | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cplig 20672 | Extend class notation with the class of all planar incidence geometries. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-plig 20673* | Planar incidence geometry. I use Hilbert's "axioms" adapted to planar geometry. is the incidence relation. I could take a generic incidence relation but I'm lazy and I'm not sure the gain is worth the extra work. Much of what follows is directly borrowed from Aitken. http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isplig 20674* | The predicate "is a planar incidence geometry". (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | tncp 20675* | There exist three non colinear points. (Contributed by FL, 3-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | lpni 20676* | For any line, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.4.2 Algebra preliminaries | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | crpm 20677 | Ring primes. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

RPrime | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-rprm 20678* | Define the set of prime elements in a ring. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 12661. (Contributed by Mario Carneiro, 17-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

RPrime Unit
_{r} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.4.3 Transitive closure | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | ctcl 20679 | Extend class notation to include the transitive closure symbol. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | crtcl 20680 | Extend class notation with transitive closure. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-trcl 20681* | Transitive closure of a relation. Experimental. (Contributed by FL, 27-Jun-2011.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-rtrcl 20682* | Reflexive-transitive closure of a relation. Experimental. (Contributed by FL, 27-Jun-2011.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

PART 15 DEPRECATED SECTIONS | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

15.1 Additional material on Group
theory | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

15.1.1 Definitions and basic properties for
groups | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgr 20683 | Extend class notation with the class of all group operations. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgi 20684 | Extend class notation with a function mapping a group operation to the group's identity element. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgn 20685 | Extend class notation with a function mapping a group operation to the inverse function for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgs 20686 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgx 20687 | Extend class notation with a function mapping a group operation to the power operation for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-grpo 20688* | Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-gid 20689* | Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-ginv 20690* | Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-gdiv 20691* | Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-gx 20692* | Define a function that maps a group operation to the group's power operation. (Contributed by Paul Chapman, 17-Apr-2009.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isgrpo 20693* | The predicate "is a group operation." Note that is the base set of the group. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isgrpo2 20694* | The predicate "is a group operation." (Contributed by NM, 23-Oct-2012.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isgrpoi 20695* | Properties that determine a group operation. Read as . (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpofo 20696 | A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpocl 20697 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpolidinv 20698* | A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpon0 20699 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoass 20700 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |