HomeTheorem List (p. 318 of 429)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 318 of 429) | < 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: | Metamath Proof Explorer
(1-27903) |
Hilbert Space Explorer
(27904-29428) |
Users' Mathboxes
(29429-42879) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | abs2sqlt 31701 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2))) | ||
| Theorem | abs2difi 31702 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)) | ||
| Theorem | abs2difabsi 31703 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)) | ||
| Theorem | axextprim 31704 | ax-ext 2631 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧)) | ||
| Theorem | axrepprim 31705 | ax-rep 4804 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥))) | ||
| Theorem | axunprim 31706 | ax-un 6991 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
| Theorem | axpowprim 31707 | ax-pow 4873 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦) | ||
| Theorem | axregprim 31708 | ax-reg 8538 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
| Theorem | axinfprim 31709 | ax-inf 8573 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | ||
| Theorem | axacprim 31710 | ax-ac 9319 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
| ⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥)))))) | ||
| Theorem | untelirr 31711* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 31821). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011.) |
| ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴) | ||
| Theorem | untuni 31712* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
| ⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥) | ||
| Theorem | untsucf 31713* | If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦) | ||
| Theorem | unt0 31714 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥 | ||
| Theorem | untint 31715* | If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
| ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀𝑦 ∈ ∩ 𝐴 ¬ 𝑦 ∈ 𝑦) | ||
| Theorem | efrunt 31716* | If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
| ⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥) | ||
| Theorem | untangtr 31717* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
| ⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦)) | ||
| Theorem | 3orel2 31718 | Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
| ⊢ (¬ 𝜓 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
| Theorem | 3orel3 31719 | Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) |
| ⊢ (¬ 𝜒 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜓))) | ||
| Theorem | 3pm3.2ni 31720 | Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 & ⊢ ¬ 𝜒 ⇒ ⊢ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
| Theorem | 3jaodd 31721 | Double deduction form of 3jaoi 1431. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂))) | ||
| Theorem | 3orit 31722 | Closed form of 3ori 1428. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)) | ||
| Theorem | biimpexp 31723 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
| ⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒))) | ||
| Theorem | 3orel13 31724 | Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.) |
| ⊢ ((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜓)) | ||
| Theorem | nepss 31725 | Two classes are inequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
| ⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵)) | ||
| Theorem | 3ccased 31726 | Triple disjunction form of ccased 1007. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓)) ⇒ ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓)) | ||
| Theorem | dfso3 31727* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
| ⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
| Theorem | brtpid1 31728 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵 | ||
| Theorem | brtpid2 31729 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵 | ||
| Theorem | brtpid3 31730 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
| ⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵 | ||
| Theorem | ceqsrexv2 31731* | Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
| Theorem | iota5f 31732* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
| Theorem | ceqsralv2 31733* | Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)) | ||
| Theorem | dford5 31734 | A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.) |
| ⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴)) | ||
| Theorem | jath 31735 | Closed form of ja 173. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
| ⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) | ||
| Theorem | sqdivzi 31736 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
| Theorem | subdivcomb1 31737 | Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) − 𝐵) / 𝐶) = (𝐴 − (𝐵 / 𝐶))) | ||
| Theorem | subdivcomb2 31738 | Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − (𝐶 · 𝐵)) / 𝐶) = ((𝐴 / 𝐶) − 𝐵)) | ||
| Theorem | supfz 31739 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
| Theorem | inffz 31740 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
| Theorem | inffzOLD 31741 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) Obsolete version of inffz 31740 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, ◡ < ) = 𝑀) | ||
| Theorem | fz0n 31742 | The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0)) | ||
| Theorem | shftvalg 31743 | Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
| Theorem | divcnvlin 31744* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
| Theorem | climlec3 31745* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | logi 31746 | Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
| ⊢ (log‘i) = (i · (π / 2)) | ||
| Theorem | iexpire 31747 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
| ⊢ (i↑𝑐i) ∈ ℝ | ||
| Theorem | bcneg1 31748 | The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0) | ||
| Theorem | bcm1nt 31749 | The proportion of one bionmial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾)))) | ||
| Theorem | bcprod 31750* | A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) | ||
| Theorem | bccolsum 31751* | A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1))) | ||
| Theorem | iprodefisumlem 31752 | Lemma for iprodefisum 31753. (Contributed by Scott Fenton, 11-Feb-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹))) | ||
| Theorem | iprodefisum 31753* | Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (exp‘𝐵) = (exp‘Σ𝑘 ∈ 𝑍 𝐵)) | ||
| Theorem | iprodgam 31754* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
| ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) | ||
| Theorem | faclimlem1 31755* | Lemma for faclim 31758. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))) | ||
| Theorem | faclimlem2 31756* | Lemma for faclim 31758. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1)) | ||
| Theorem | faclimlem3 31757 | Lemma for faclim 31758. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵))))) | ||
| Theorem | faclim 31758* | An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))) ⇒ ⊢ (𝐴 ∈ ℕ0 → seq1( · , 𝐹) ⇝ (!‘𝐴)) | ||
| Theorem | iprodfac 31759* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
| ⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘)))) | ||
| Theorem | faclim2 31760* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) ⇒ ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1) | ||
| Theorem | pdivsq 31761 | Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃 ∥ 𝑀 ↔ 𝑃 ∥ (𝑀↑2))) | ||
| Theorem | dvdspw 31762 | Exponentiation law for divisibility. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀↑𝑁))) | ||
| Theorem | gcd32 31763 | Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐶) = ((𝐴 gcd 𝐶) gcd 𝐵)) | ||
| Theorem | gcdabsorb 31764 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵)) | ||
| Theorem | brtp 31765 | A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹))) | ||
| Theorem | dftr6 31766 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E ))) | ||
| Theorem | coep 31767* | Composition with epsilon. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥) | ||
| Theorem | coepr 31768* | Composition with the converse of epsilon. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵) | ||
| Theorem | dffr5 31769 | A quantifier free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.) |
| ⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅))) | ||
| Theorem | dfso2 31770 | Quantifier free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
| ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) | ||
| Theorem | dfpo2 31771 | Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.) |
| ⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) | ||
| Theorem | br8 31772* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌)) | ||
| Theorem | br6 31773* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁)) | ||
| Theorem | br4 31774* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
| ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏)) | ||
| Theorem | cnvco1 31775 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴) | ||
| Theorem | cnvco2 31776 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴) | ||
| Theorem | eldm3 31777 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
| ⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) | ||
| Theorem | elrn3 31778 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
| ⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅) | ||
| Theorem | pocnv 31779 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
| Theorem | socnv 31780 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) | ||
| Theorem | sotrd 31781 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) & ⊢ (𝜑 → 𝑌𝑅𝑍) ⇒ ⊢ (𝜑 → 𝑋𝑅𝑍) | ||
| Theorem | sotr3 31782 | Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → ((𝑋𝑅𝑌 ∧ ¬ 𝑍𝑅𝑌) → 𝑋𝑅𝑍)) | ||
| Theorem | soasym 31783 | Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋)) | ||
| Theorem | sotrine 31784 | Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ≠ 𝐶 ↔ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
| Theorem | eqfunresadj 31785 | Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌}))) | ||
| Theorem | eqfunressuc 31786 | Law for equality of restriction to successors. This is primarily useful when 𝑋 is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑋 ∈ dom 𝐹 ∧ 𝑋 ∈ dom 𝐺 ∧ (𝐹‘𝑋) = (𝐺‘𝑋))) → (𝐹 ↾ suc 𝑋) = (𝐺 ↾ suc 𝑋)) | ||
| Theorem | funeldmb 31787 | If ∅ is not part of the range of a function 𝐹, then 𝐴 is in the domain of 𝐹 iff (𝐹‘𝐴) ≠ ∅. (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹) → (𝐴 ∈ dom 𝐹 ↔ (𝐹‘𝐴) ≠ ∅)) | ||
| Theorem | elintfv 31788* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ 𝑋 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦))) | ||
| Theorem | funpsstri 31789 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
| ⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹)) | ||
| Theorem | fundmpss 31790 | If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.) |
| ⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺)) | ||
| Theorem | fvresval 31791 | The value of a function at a restriction is either null or the same as the function itself. (Contributed by Scott Fenton, 4-Sep-2011.) |
| ⊢ (((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴) ∨ ((𝐹 ↾ 𝐵)‘𝐴) = ∅) | ||
| Theorem | funsseq 31792 | Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺)) | ||
| Theorem | fununiq 31793 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
| Theorem | funbreq 31794 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶)) | ||
| Theorem | fprb 31795* | A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩})) | ||
| Theorem | br1steq 31796 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴) | ||
| Theorem | br2ndeq 31797 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵) | ||
| Theorem | br1steqgOLD 31798 | Obsolete version of br1steqg 7232 as of 9-Feb-2022. (Contributed by Scott Fenton, 2-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴)) | ||
| Theorem | br2ndeqgOLD 31799 | Obsolete version of br2ndeqg 7233 as of 9-Feb-2022. (Contributed by Scott Fenton, 2-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵)) | ||
| Theorem | dfdm5 31800 | Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |