HomeHome 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  Metamath Proof Explorer
(1-27903)
  Hilbert Space Explorer  Hilbert Space Explorer
(27904-29428)
  Users' Mathboxes  Users' Mathboxes
(29429-42879)
 

Theorem List for Metamath Proof Explorer - 31701-31800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremabs2sqlt 31701 The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)))
 
Theoremabs2difi 31702 Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴𝐵))
 
Theoremabs2difabsi 31703 Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴𝐵))
 
20.8  Mathbox for Scott Fenton
 
20.8.1  ZFC Axioms in primitive form
 
Theoremaxextprim 31704 ax-ext 2631 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
¬ ∀𝑥 ¬ ((𝑥𝑦𝑥𝑧) → ((𝑥𝑧𝑥𝑦) → 𝑦 = 𝑧))
 
Theoremaxrepprim 31705 ax-rep 4804 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧𝑥 → ¬ ∀𝑥(∀𝑧 𝑥𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧𝑥)))
 
Theoremaxunprim 31706 ax-un 6991 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦𝑥 → ¬ 𝑥𝑧) → 𝑦𝑥)
 
Theoremaxpowprim 31707 ax-pow 4873 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
(∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥𝑦 → ∀𝑦 𝑥𝑧) → 𝑦𝑥) → 𝑥 = 𝑦)
 
Theoremaxregprim 31708 ax-reg 8538 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
(𝑥𝑦 → ¬ ∀𝑥(𝑥𝑦 → ¬ ∀𝑧(𝑧𝑥 → ¬ 𝑧𝑦)))
 
Theoremaxinfprim 31709 ax-inf 8573 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.)
¬ ∀𝑥 ¬ (𝑦𝑧 → ¬ (𝑦𝑥 → ¬ ∀𝑦(𝑦𝑥 → ¬ ∀𝑧(𝑦𝑧 → ¬ 𝑧𝑥))))
 
Theoremaxacprim 31710 ax-ac 9319 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
¬ ∀𝑥 ¬ ∀𝑦𝑧(∀𝑥 ¬ (𝑦𝑧 → ¬ 𝑧𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦𝑧 → (𝑧𝑤 → (𝑦𝑤 → ¬ 𝑤𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦𝑧 → (𝑧𝑤 → (𝑦𝑤 → ¬ 𝑤𝑥))))))
 
20.8.2  Untangled classes
 
Theoremuntelirr 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.)
(∀𝑥𝐴 ¬ 𝑥𝑥 → ¬ 𝐴𝐴)
 
Theoremuntuni 31712* The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
(∀𝑥 𝐴 ¬ 𝑥𝑥 ↔ ∀𝑦𝐴𝑥𝑦 ¬ 𝑥𝑥)
 
Theoremuntsucf 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 𝐴 ¬ 𝑦𝑦)
 
Theoremunt0 31714 The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
𝑥 ∈ ∅ ¬ 𝑥𝑥
 
Theoremuntint 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.)
(∃𝑥𝐴𝑦𝑥 ¬ 𝑦𝑦 → ∀𝑦 𝐴 ¬ 𝑦𝑦)
 
Theoremefrunt 31716* If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
( E Fr 𝐴 → ∀𝑥𝐴 ¬ 𝑥𝑥)
 
Theoremuntangtr 31717* A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
(Tr 𝐴 → (∀𝑥𝐴 ¬ 𝑥𝑥 ↔ ∀𝑥𝐴𝑦𝑥 ¬ 𝑦𝑦))
 
20.8.3  Extra propositional calculus theorems
 
Theorem3orel2 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.)
𝜓 → ((𝜑𝜓𝜒) → (𝜑𝜒)))
 
Theorem3orel3 31719 Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
𝜒 → ((𝜑𝜓𝜒) → (𝜑𝜓)))
 
Theorem3pm3.2ni 31720 Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.)
¬ 𝜑    &    ¬ 𝜓    &    ¬ 𝜒        ¬ (𝜑𝜓𝜒)
 
Theorem3jaodd 31721 Double deduction form of 3jaoi 1431. (Contributed by Scott Fenton, 20-Apr-2011.)
(𝜑 → (𝜓 → (𝜒𝜂)))    &   (𝜑 → (𝜓 → (𝜃𝜂)))    &   (𝜑 → (𝜓 → (𝜏𝜂)))       (𝜑 → (𝜓 → ((𝜒𝜃𝜏) → 𝜂)))
 
Theorem3orit 31722 Closed form of 3ori 1428. (Contributed by Scott Fenton, 20-Apr-2011.)
((𝜑𝜓𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒))
 
Theorembiimpexp 31723 A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
(((𝜑𝜓) → 𝜒) ↔ ((𝜑𝜓) → ((𝜓𝜑) → 𝜒)))
 
Theorem3orel13 31724 Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.)
((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑𝜓𝜒) → 𝜓))
 
20.8.4  Misc. Useful Theorems
 
Theoremnepss 31725 Two classes are inequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
(𝐴𝐵 ↔ ((𝐴𝐵) ⊊ 𝐴 ∨ (𝐴𝐵) ⊊ 𝐵))
 
Theorem3ccased 31726 Triple disjunction form of ccased 1007. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
(𝜑 → ((𝜒𝜂) → 𝜓))    &   (𝜑 → ((𝜒𝜁) → 𝜓))    &   (𝜑 → ((𝜒𝜎) → 𝜓))    &   (𝜑 → ((𝜃𝜂) → 𝜓))    &   (𝜑 → ((𝜃𝜁) → 𝜓))    &   (𝜑 → ((𝜃𝜎) → 𝜓))    &   (𝜑 → ((𝜏𝜂) → 𝜓))    &   (𝜑 → ((𝜏𝜁) → 𝜓))    &   (𝜑 → ((𝜏𝜎) → 𝜓))       (𝜑 → (((𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜓))
 
Theoremdfso3 31727* Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
(𝑅 Or 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
 
Theorembrtpid1 31728 A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.)
𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵
 
Theorembrtpid2 31729 A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.)
𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵
 
Theorembrtpid3 31730 A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.)
𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵
 
Theoremceqsrexv2 31731* Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.)
(𝑥 = 𝐴 → (𝜑𝜓))       (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ (𝐴𝐵𝜓))
 
Theoremiota5f 31732* A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
𝑥𝜑    &   𝑥𝐴    &   ((𝜑𝐴𝑉) → (𝜓𝑥 = 𝐴))       ((𝜑𝐴𝑉) → (℩𝑥𝜓) = 𝐴)
 
Theoremceqsralv2 31733* Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.)
(𝑥 = 𝐴 → (𝜑𝜓))       (∀𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ (𝐴𝐵𝜓))
 
Theoremdford5 31734 A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.)
(Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴))
 
Theoremjath 31735 Closed form of ja 173. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
((¬ 𝜑𝜒) → ((𝜓𝜒) → ((𝜑𝜓) → 𝜒)))
 
20.8.5  Properties of real and complex numbers
 
Theoremsqdivzi 31736 Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
 
Theoremsubdivcomb1 31737 Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) − 𝐵) / 𝐶) = (𝐴 − (𝐵 / 𝐶)))
 
Theoremsubdivcomb2 31738 Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − (𝐶 · 𝐵)) / 𝐶) = ((𝐴 / 𝐶) − 𝐵))
 
Theoremsupfz 31739 The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.)
(𝑁 ∈ (ℤ𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)
 
Theoreminffz 31740 The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.)
(𝑁 ∈ (ℤ𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
 
TheoreminffzOLD 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((𝑀...𝑁), ℤ, < ) = 𝑀)
 
Theoremfz0n 31742 The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.)
(𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0))
 
Theoremshftvalg 31743 Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
((𝐹𝑉𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵𝐴)))
 
Theoremdivcnvlin 31744* Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℤ)    &   (𝜑𝐹𝑉)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵)))       (𝜑𝐹 ⇝ 1)
 
Theoremclimlec3 31745* Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐹𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ 𝐵)       (𝜑𝐴𝐵)
 
Theoremlogi 31746 Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.)
(log‘i) = (i · (π / 2))
 
Theoremiexpire 31747 i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
(i↑𝑐i) ∈ ℝ
 
Theorembcneg1 31748 The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
(𝑁 ∈ ℕ0 → (𝑁C-1) = 0)
 
Theorembcm1nt 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𝐾) · (𝑁 / (𝑁𝐾))))
 
Theorembcprod 31750* A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.)
(𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁)))
 
Theorembccolsum 31751* A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.)
((𝑁 ∈ ℕ0𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1)))
 
20.8.6  Infinite products
 
Theoremiprodefisumlem 31752 Lemma for iprodefisum 31753. (Contributed by Scott Fenton, 11-Feb-2018.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐹:𝑍⟶ℂ)       (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹)))
 
Theoremiprodefisum 31753* Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) = 𝐵)    &   ((𝜑𝑘𝑍) → 𝐵 ∈ ℂ)    &   (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )       (𝜑 → ∏𝑘𝑍 (exp‘𝐵) = (exp‘Σ𝑘𝑍 𝐵))
 
Theoremiprodgam 31754* An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
(𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))       (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴))
 
20.8.7  Factorial limits
 
Theoremfaclimlem1 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))))))
 
Theoremfaclimlem2 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))
 
Theoremfaclimlem3 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) / 𝐵)))))
 
Theoremfaclim 31758* An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.)
𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))       (𝐴 ∈ ℕ0 → seq1( · , 𝐹) ⇝ (!‘𝐴))
 
Theoremiprodfac 31759* An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.)
(𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘))))
 
Theoremfaclim2 31760* Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.)
𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀))))       (𝑀 ∈ ℕ0𝐹 ⇝ 1)
 
20.8.8  Greatest common divisor and divisibility
 
Theorempdivsq 31761 Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃𝑀𝑃 ∥ (𝑀↑2)))
 
Theoremdvdspw 31762 Exponentiation law for divisibility. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐾𝑀𝐾 ∥ (𝑀𝑁)))
 
Theoremgcd32 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 𝐵))
 
Theoremgcdabsorb 31764 Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵))
 
20.8.9  Properties of relationships
 
Theorembrtp 31765 A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.)
𝑋 ∈ V    &   𝑌 ∈ V       (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴𝑌 = 𝐵) ∨ (𝑋 = 𝐶𝑌 = 𝐷) ∨ (𝑋 = 𝐸𝑌 = 𝐹)))
 
Theoremdftr6 31766 A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.)
𝐴 ∈ V       (Tr 𝐴𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E )))
 
Theoremcoep 31767* Composition with epsilon. (Contributed by Scott Fenton, 18-Feb-2013.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥𝐵 𝐴𝑅𝑥)
 
Theoremcoepr 31768* Composition with the converse of epsilon. (Contributed by Scott Fenton, 18-Feb-2013.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴(𝑅 E )𝐵 ↔ ∃𝑥𝐴 𝑥𝑅𝐵)
 
Theoremdffr5 31769 A quantifier free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.)
(𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ 𝑅)))
 
Theoremdfso2 31770 Quantifier free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)
(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ 𝑅))))
 
Theoremdfpo2 31771 Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.)
(𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
 
Theorembr8 31772* Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
(𝑎 = 𝐴 → (𝜑𝜓))    &   (𝑏 = 𝐵 → (𝜓𝜒))    &   (𝑐 = 𝐶 → (𝜒𝜃))    &   (𝑑 = 𝐷 → (𝜃𝜏))    &   (𝑒 = 𝐸 → (𝜏𝜂))    &   (𝑓 = 𝐹 → (𝜂𝜁))    &   (𝑔 = 𝐺 → (𝜁𝜎))    &   ( = 𝐻 → (𝜎𝜌))    &   (𝑥 = 𝑋𝑃 = 𝑄)    &   𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)}       (((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
 
Theorembr6 31773* Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
(𝑎 = 𝐴 → (𝜑𝜓))    &   (𝑏 = 𝐵 → (𝜓𝜒))    &   (𝑐 = 𝐶 → (𝜒𝜃))    &   (𝑑 = 𝐷 → (𝜃𝜏))    &   (𝑒 = 𝐸 → (𝜏𝜂))    &   (𝑓 = 𝐹 → (𝜂𝜁))    &   (𝑥 = 𝑋𝑃 = 𝑄)    &   𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}       ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
 
Theorembr4 31774* Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)
(𝑎 = 𝐴 → (𝜑𝜓))    &   (𝑏 = 𝐵 → (𝜓𝜒))    &   (𝑐 = 𝐶 → (𝜒𝜃))    &   (𝑑 = 𝐷 → (𝜃𝜏))    &   (𝑥 = 𝑋𝑃 = 𝑄)    &   𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}       ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄)) → (⟨𝐴, 𝐵𝑅𝐶, 𝐷⟩ ↔ 𝜏))
 
Theoremcnvco1 31775 Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
(𝐴𝐵) = (𝐵𝐴)
 
Theoremcnvco2 31776 Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
(𝐴𝐵) = (𝐵𝐴)
 
Theoremeldm3 31777 Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
(𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)
 
Theoremelrn3 31778 Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.)
(𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅)
 
Theorempocnv 31779 The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
(𝑅 Po 𝐴𝑅 Po 𝐴)
 
Theoremsocnv 31780 The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
(𝑅 Or 𝐴𝑅 Or 𝐴)
 
Theoremsotrd 31781 Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.)
(𝜑𝑅 Or 𝐴)    &   (𝜑𝑋𝐴)    &   (𝜑𝑌𝐴)    &   (𝜑𝑍𝐴)    &   (𝜑𝑋𝑅𝑌)    &   (𝜑𝑌𝑅𝑍)       (𝜑𝑋𝑅𝑍)
 
Theoremsotr3 31782 Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.)
((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴𝑍𝐴)) → ((𝑋𝑅𝑌 ∧ ¬ 𝑍𝑅𝑌) → 𝑋𝑅𝑍))
 
Theoremsoasym 31783 Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.)
((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋))
 
Theoremsotrine 31784 Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝐶 ↔ (𝐵𝑅𝐶𝐶𝑅𝐵)))
 
Theoremeqfunresadj 31785 Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.)
(((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹𝑋) = (𝐺𝑋) ∧ (𝑌 ∈ dom 𝐹𝑌 ∈ dom 𝐺 ∧ (𝐹𝑌) = (𝐺𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌})))
 
Theoremeqfunressuc 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 𝑋))
 
Theoremfuneldmb 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 𝐹 ↔ (𝐹𝐴) ≠ ∅))
 
Theoremelintfv 31788* Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.)
𝑋 ∈ V       ((𝐹 Fn 𝐴𝐵𝐴) → (𝑋 (𝐹𝐵) ↔ ∀𝑦𝐵 𝑋 ∈ (𝐹𝑦)))
 
20.8.10  Properties of functions and mappings
 
Theoremfunpsstri 31789 A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
((Fun 𝐻 ∧ (𝐹𝐻𝐺𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹𝐺𝐹 = 𝐺𝐺𝐹))
 
Theoremfundmpss 31790 If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.)
(Fun 𝐺 → (𝐹𝐺 → dom 𝐹 ⊊ dom 𝐺))
 
Theoremfvresval 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.)
(((𝐹𝐵)‘𝐴) = (𝐹𝐴) ∨ ((𝐹𝐵)‘𝐴) = ∅)
 
Theoremfunsseq 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 𝐺) → (𝐹 = 𝐺𝐹𝐺))
 
Theoremfununiq 31793 The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V       (Fun 𝐹 → ((𝐴𝐹𝐵𝐴𝐹𝐶) → 𝐵 = 𝐶))
 
Theoremfunbreq 31794 An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V       ((Fun 𝐹𝐴𝐹𝐵) → (𝐴𝐹𝐶𝐵 = 𝐶))
 
Theoremfprb 31795* A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥𝑅𝑦𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}))
 
Theorembr1steq 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 𝐶𝐶 = 𝐴)
 
Theorembr2ndeq 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 𝐶𝐶 = 𝐵)
 
Theorembr1steqgOLD 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 𝐶𝐶 = 𝐴))
 
Theorembr2ndeqgOLD 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 𝐶𝐶 = 𝐵))
 
Theoremdfdm5 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 >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31500 316 31501-31600 317 31601-31700 318 31701-31800 319 31801-31900 320 31901-32000 321 32001-32100 322 32101-32200 323 32201-32300 324 32301-32400 325 32401-32500 326 32501-32600 327 32601-32700 328 32701-32800 329 32801-32900 330 32901-33000 331 33001-33100 332 33101-33200 333 33201-33300 334 33301-33400 335 33401-33500 336 33501-33600 337 33601-33700 338 33701-33800 339 33801-33900 340 33901-34000 341 34001-34100 342 34101-34200 343 34201-34300 344 34301-34400 345 34401-34500 346 34501-34600 347 34601-34700 348 34701-34800 349 34801-34900 350 34901-35000 351 35001-35100 352 35101-35200 353 35201-35300 354 35301-35400 355 35401-35500 356 35501-35600 357 35601-35700 358 35701-35800 359 35801-35900 360 35901-36000 361 36001-36100 362 36101-36200 363 36201-36300 364 36301-36400 365 36401-36500 366 36501-36600 367 36601-36700 368 36701-36800 369 36801-36900 370 36901-37000 371 37001-37100 372 37101-37200 373 37201-37300 374 37301-37400 375 37401-37500 376 37501-37600 377 37601-37700 378 37701-37800 379 37801-37900 380 37901-38000 381 38001-38100 382 38101-38200 383 38201-38300 384 38301-38400 385 38401-38500 386 38501-38600 387 38601-38700 388 38701-38800 389 38801-38900 390 38901-39000 391 39001-39100 392 39101-39200 393 39201-39300 394 39301-39400 395 39401-39500 396 39501-39600 397 39601-39700 398 39701-39800 399 39801-39900 400 39901-40000 401 40001-40100 402 40101-40200 403 40201-40300 404 40301-40400 405 40401-40500 406 40501-40600 407 40601-40700 408 40701-40800 409 40801-40900 410 40901-41000 411 41001-41100 412 41101-41200 413 41201-41300 414 41301-41400 415 41401-41500 416 41501-41600 417 41601-41700 418 41701-41800 419 41801-41900 420 41901-42000 421 42001-42100 422 42101-42200 423 42201-42300 424 42301-42400 425 42401-42500 426 42501-42600 427 42601-42700 428 42701-42800 429 42801-42879
  Copyright terms: Public domain < Previous  Next >