![]() |
Metamath
Proof Explorer Theorem List (p. 303 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
These 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 30200 and mmnatded.html 30200. Since these examples should not be used within proofs of other theorems, especially in mathboxes, they are marked with "(New usage is discouraged.)". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.2 30201 |
Theorem 5.2 of [Clemente] 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 30202. A proof without context is shown in ex-natded5.2i 30203. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜓)) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝜃) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.2-2 30202 | A more efficient proof of Theorem 5.2 of [Clemente] p. 15. Compare with ex-natded5.2 30201 and ex-natded5.2i 30203. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜓)) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝜃) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.2i 30203 | The same as ex-natded5.2 30201 and ex-natded5.2-2 30202 but with no context. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝜓 ∧ 𝜒) → 𝜃) & ⊢ (𝜒 → 𝜓) & ⊢ 𝜒 ⇒ ⊢ 𝜃 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.3 30204 |
Theorem 5.3 of [Clemente] 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 30205.
A proof without context is shown in ex-natded5.3i 30206.
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. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.3-2 30205 | A more efficient proof of Theorem 5.3 of [Clemente] p. 16. Compare with ex-natded5.3 30204 and ex-natded5.3i 30206. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.3i 30206 | The same as ex-natded5.3 30204 and ex-natded5.3-2 30205 but with no context. Identical to jccir 521, which should be used instead. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜓 → 𝜒) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜓 → (𝜒 ∧ 𝜃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.5 30207 |
Theorem 5.5 of [Clemente] 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 480; simpr 484 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 197; a proof without context is shown in mto 196. (Contributed by David A. Wheeler, 19-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.7 30208 |
Theorem 5.7 of [Clemente] 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 30209.
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. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ∨ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.7-2 30209 | A more efficient proof of Theorem 5.7 of [Clemente] p. 19. Compare with ex-natded5.7 30208. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ∨ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.8 30210 |
Theorem 5.8 of [Clemente] 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 480; simpr 484 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 30211. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ¬ 𝜃)) & ⊢ (𝜑 → (𝜏 → 𝜃)) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.8-2 30211 | A more efficient proof of Theorem 5.8 of [Clemente] p. 20. For a longer line-by-line translation, see ex-natded5.8 30210. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ¬ 𝜃)) & ⊢ (𝜑 → (𝜏 → 𝜃)) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.13 30212 |
Theorem 5.13 of [Clemente] 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 30213.
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 480; simpr 484 is useful when you want to depend directly on the new assumption). (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (¬ 𝜏 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 ∨ 𝜏)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded5.13-2 30213 | A more efficient proof of Theorem 5.13 of [Clemente] p. 20. Compare with ex-natded5.13 30212. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (¬ 𝜏 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 ∨ 𝜏)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded9.20 30214 |
Theorem 9.20 of [Clemente] 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 480; simpr 484 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 30215. (Contributed by David A. Wheeler, 19-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded9.20-2 30215 | A more efficient proof of Theorem 9.20 of [Clemente] p. 45. Compare with ex-natded9.20 30214. (Contributed by David A. Wheeler, 19-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded9.26 30216* |
Theorem 9.26 of [Clemente] 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 30217. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∃𝑥∀𝑦𝜓) ⇒ ⊢ (𝜑 → ∀𝑦∃𝑥𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-natded9.26-2 30217* | A more efficient proof of Theorem 9.26 of [Clemente] p. 45. Compare with ex-natded9.26 30216. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∃𝑥∀𝑦𝜓) ⇒ ⊢ (𝜑 → ∀𝑦∃𝑥𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-or 30218 | Example for df-or 847. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (2 = 3 ∨ 4 = 4) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-an 30219 | Example for df-an 396. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (2 = 2 ∧ 3 = 3) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-dif 30220 | Example for df-dif 3947. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({1, 3} ∖ {1, 8}) = {3} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-un 30221 | Example for df-un 3949. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({1, 3} ∪ {1, 8}) = {1, 3, 8} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-in 30222 | Example for df-in 3951. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({1, 3} ∩ {1, 8}) = {1} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-uni 30223 | Example for df-uni 4904. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ∪ {{1, 3}, {1, 8}} = {1, 3, 8} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-ss 30224 | Example for df-ss 3961. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ {1, 2} ⊆ {1, 2, 3} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-pss 30225 | Example for df-pss 3963. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ {1, 2} ⊊ {1, 2, 3} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-pw 30226 | Example for df-pw 4600. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐴 = {3, 5, 7} → 𝒫 𝐴 = (({∅} ∪ {{3}, {5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}} ∪ {{3, 5, 7}}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-pr 30227 | Example for df-pr 4627. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ {1, -1} → (𝐴↑2) = 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-br 30228 | Example for df-br 5143. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-opab 30229* | Example for df-opab 5205. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-eprel 30230 | Example for df-eprel 5576. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 5 E {1, 5} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-id 30231 | Example for df-id 5570. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (5 I 5 ∧ ¬ 4 I 5) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-po 30232 | Example for df-po 5584. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ( < Po ℝ ∧ ¬ ≤ Po ℝ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-xp 30233 | Example for df-xp 5678. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({1, 5} × {2, 7}) = ({⟨1, 2⟩, ⟨1, 7⟩} ∪ {⟨5, 2⟩, ⟨5, 7⟩}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-cnv 30234 | Example for df-cnv 5680. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ◡{⟨2, 6⟩, ⟨3, 9⟩} = {⟨6, 2⟩, ⟨9, 3⟩} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-co 30235 | Example for df-co 5681. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((exp ∘ cos)‘0) = e | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-dm 30236 | Example for df-dm 5682. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → dom 𝐹 = {2, 3}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-rn 30237 | Example for df-rn 5683. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-res 30238 | Example for df-res 5684. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-ima 30239 | Example for df-ima 5685. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 “ 𝐵) = {6}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-fv 30240 | Example for df-fv 6550. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-1st 30241 | Example for df-1st 7987. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (1st ‘⟨3, 4⟩) = 3 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-2nd 30242 | Example for df-2nd 7988. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (2nd ‘⟨3, 4⟩) = 4 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1kp2ke3k 30243 |
Example for df-dec 12700, 1000 + 2000 = 3000.
This proof disproves (by counterexample) 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, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.) This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision." The proof here starts with (2 + 1) = 3, 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 12700 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (;;;1000 + ;;;2000) = ;;;3000 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-fl 30244 | Example for df-fl 13781. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((⌊‘(3 / 2)) = 1 ∧ (⌊‘-(3 / 2)) = -2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-ceil 30245 | Example for df-ceil 13782. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-mod 30246 | Example for df-mod 13859. (Contributed by AV, 3-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((5 mod 3) = 2 ∧ (-7 mod 2) = 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-exp 30247 | Example for df-exp 14051. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((5↑2) = ;25 ∧ (-3↑-2) = (1 / 9)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-fac 30248 | Example for df-fac 14257. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (!‘5) = ;;120 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-bc 30249 | Example for df-bc 14286. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (5C3) = ;10 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-hash 30250 | Example for df-hash 14314. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (♯‘{0, 1, 2}) = 3 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-sqrt 30251 | Example for df-sqrt 15206. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (√‘;25) = 5 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-abs 30252 | Example for df-abs 15207. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (abs‘-2) = 2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-dvds 30253 | Example for df-dvds 16223: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 3 ∥ 6 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-gcd 30254 | Example for df-gcd 16461. (Contributed by AV, 5-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (-6 gcd 9) = 3 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-lcm 30255 | Example for df-lcm 16552. (Contributed by AV, 5-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (6 lcm 9) = ;18 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-prmo 30256 | Example for df-prmo 16992: (#p‘10) = 2 · 3 · 5 · 7. (Contributed by AV, 6-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (#p‘;10) = ;;210 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | aevdemo 30257* | Proof illustrating the comment of aev2 2054. (Contributed by BJ, 30-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑥 𝑥 = 𝑦 → ((∃𝑎∀𝑏 𝑐 = 𝑑 ∨ ∃𝑒 𝑓 = 𝑔) ∧ ∀ℎ(𝑖 = 𝑗 → 𝑘 = 𝑙))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-ind-dvds 30258 | Example of a proof by induction (divisibility result). (Contributed by Stanislas Polu, 9-Mar-2020.) (Revised by BJ, 24-Mar-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ0 → 3 ∥ ((4↑𝑁) + 2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ex-fpar 30259 | Formalized example provided in the comment for fpar 8115. (Contributed by AV, 3-Jan-2024.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V))))) & ⊢ 𝐴 = (0[,)+∞) & ⊢ 𝐵 = ℝ & ⊢ 𝐹 = (√ ↾ 𝐴) & ⊢ 𝐺 = (sin ↾ 𝐵) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋( + ∘ 𝐻)𝑌) = ((√‘𝑋) + (sin‘𝑌))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | avril1 30260 |
Poisson d'Avril's Theorem. This theorem is noted for its
Selbstdokumentieren property, which means, literally,
"self-documenting" and recalls the principle of quidquid
german 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.)
A reply to skeptics can be found at mmnotes.txt, under the 1-Apr-2006 entry. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2bornot2b 30261 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | helloworld 30262 | The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://helloworldcollection.de. 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 to put it to rest with a remarkably short proof only four lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ¬ (ℎ ∈ (𝐿𝐿0) ∧ 𝑊∅(R1𝑑)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1p1e2apr1 30263 | One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel L. 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (1 + 1) = 2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eqid1 30264 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). It is one of the three axioms of Ayn Rand's philosophy (Atlas Shrugged, Part Three, Chapter VII). While some have proposed extending Rand's axiomatization to include Compassion and Kindness, others fear that such an extension may flirt with logical inconsistency. (Contributed by Stefan Allan, 1-Apr-2009.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = 𝐴 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1div0apr 30265 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (1 / 0) = ∅ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topnfbey 30266 | Nothing seems to be impossible to Prof. Lirpa. After years of intensive research, he managed to find a proof that when given a chance to reach infinity, one could indeed go beyond, thus giving formal soundness to Buzz Lightyear's motto "To infinity... and beyond!" (Contributed by Prof. Loof Lirpa, 1-Apr-2020.) (Revised by Thierry Arnoux, 2-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ (0...+∞) → +∞ < 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9p10ne21 30267 | 9 + 10 is not equal to 21. This disproves a popular meme which asserts that 9 + 10 does equal 21. See https://www.quora.com/Can-someone-try-to-prove-to-me-that-9+10-21 for attempts to prove that 9 + 10 = 21, and see https://tinyurl.com/9p10e21 for the history of the 9 + 10 = 21 meme. (Contributed by BTernaryTau, 25-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (9 + ;10) ≠ ;21 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9p10ne21fool 30268 | 9 + 10 equals 21. This astonishing thesis lives as a meme on the internet, and may be believed by quite some people. At least repeated requests to falsify it are a permanent part of the story. Prof. Loof Lirpa did not rest until he finally came up with a computer verifiable mathematical proof, that only a fool can think so. (Contributed by Prof. Loof Lirpa, 26-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((9 + ;10) = ;21 → 𝐹∅(0 · 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Axiom | ax-flt 30269 | This factoid is e.g. useful for nrt2irr 30270. Andrew has a proof, I'll have a go at formalizing it after my coffee break. In the mean time let's add it as an axiom. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ)) → ((𝑋↑𝑁) + (𝑌↑𝑁)) ≠ (𝑍↑𝑁)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nrt2irr 30270 | The 𝑁-th root of 2 is irrational for 𝑁 greater than 2. For 𝑁 = 2, see sqrt2irr 16217. This short and rather elegant proof has the minor disadvantage that it refers to ax-flt 30269, which is still to be formalized. For a proof not requiring ax-flt 30269, see rtprmirr 41828. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ (ℤ≥‘3) → ¬ (2↑𝑐(1 / 𝑁)) ∈ ℚ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cplig 30271 | Extend class notation with the class of all planar incidence geometries. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Plig | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-plig 30272* |
Define the class of planar incidence geometries. We use Hilbert's
axioms and adapt them to planar geometry. We use ∈ for the
incidence relation. We could have used a generic binary relation, but
using ∈ allows to reuse previous results.
Much of what follows is
directly borrowed from Aitken, Incidence-Betweenness Geometry,
2008,
http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf.
The class Plig is the class of planar incidence geometries, where a planar incidence geometry is defined as a set of lines satisfying three axioms. In the definition below, 𝑥 denotes a planar incidence geometry, so ∪ 𝑥 denotes the union of its lines, that is, the set of points in the plane, 𝑙 denotes a line, and 𝑎, 𝑏, 𝑐 denote points. Therefore, the axioms are: 1) for all pairs of (distinct) points, there exists a unique line containing them; 2) all lines contain at least two points; 3) there exist three non-collinear points. (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Plig = {𝑥 ∣ (∀𝑎 ∈ ∪ 𝑥∀𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝑥 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝑥 ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥∃𝑐 ∈ ∪ 𝑥∀𝑙 ∈ 𝑥 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isplig 30273* | The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ispligb 30274* | The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ Plig ↔ (𝐺 ∈ V ∧ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tncp 30275* | In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ Plig → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | l2p 30276* | For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | lpni 30277* | For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nsnlplig 30278 | There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021.) (Proof shortened by AV, 5-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ Plig → ¬ {𝐴} ∈ 𝐺) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nsnlpligALT 30279 | Alternate version of nsnlplig 30278 using the predicate ∉ instead of ¬ ∈ and whose proof is shorter. (Contributed by AV, 5-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ Plig → {𝐴} ∉ 𝐺) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | n0lplig 30280 | There is no "empty line" in a planar incidence geometry. (Contributed by AV, 28-Nov-2021.) (Proof shortened by BJ, 2-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | n0lpligALT 30281 | Alternate version of n0lplig 30280 using the predicate ∉ instead of ¬ ∈ and whose proof bypasses nsnlplig 30278. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ Plig → ∅ ∉ 𝐺) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eulplig 30282* | Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ 𝐴 ≠ 𝐵)) → ∃!𝑙 ∈ 𝐺 (𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pliguhgr 30283 | Any planar incidence geometry 𝐺 can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 28879 for a generalization of this case for arbitrary incidence structures (planar incidence geometries are such incidence structures). (Proposed by Gerard Lang, 24-Nov-2021.) (Contributed by AV, 28-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ Plig → ⟨∪ 𝐺, ( I ↾ 𝐺)⟩ ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
This section contains a few aliases that we temporarily keep to prevent broken links. If you land on any of these, please let the originating site and/or us know that the link that made you land here should be changed. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dummylink 30284 |
Alias for a1ii 2 that may be referenced in some older works, and
kept
here to prevent broken links.
If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to a1ii 2. (Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜑 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | id1 30285 |
Alias for idALT 23 that may be referenced in some older works, and
kept
here to prevent broken links.
If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to idALT 23. (Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e., theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it is not useful), and if so, delete it. Then, repeat this recursively. One way to search for terminal theorems is to log the output ("MM> OPEN LOG xxx.txt") of "MM> SHOW USAGE <label-match>" in the Metamath program and search for "(None)". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
This section contains an earlier development of groups that was defined before extensible structures were introduced. The intent is for this deprecated section to be deleted once the corresponding definitions and theorems for complex topological vector spaces, which are using them, are revised accordingly. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgr 30286 | Extend class notation with the class of all group operations. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GrpOp | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgi 30287 | Extend class notation with a function mapping a group operation to the group's identity element. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgn 30288 | Extend class notation with a function mapping a group operation to the inverse function for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class inv | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgs 30289 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class /𝑔 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-grpo 30290* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gid 30291* | 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 = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-ginv 30292* | Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gdiv 30293* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgrpo 30294* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgrpoi 30295* | Properties that determine a group operation. Read 𝑁 as 𝑁(𝑥). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ V & ⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋 & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ 𝑈 ∈ 𝑋 & ⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋) & ⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈) ⇒ ⊢ 𝐺 ∈ GrpOp | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grpofo 30296 | A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grpocl 30297 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grpolidinv 30298* | A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grpon0 30299 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑋 ≠ ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grpoass 30300 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |