Home | Metamath
Proof Explorer Theorem List (p. 330 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-gfoo 32901* | Define the Galois field of order 𝑝↑+∞, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ GF∞ = (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)}))) | ||
Definition | df-eqp 32902* | Define an equivalence relation on ℤ-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum Σ𝑘 ≤ 𝑛𝑓(𝑘)(𝑝↑𝑘) is a multiple of 𝑝↑(𝑛 + 1) for every 𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ ~Qp = (𝑝 ∈ ℙ ↦ {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}) | ||
Definition | df-rqp 32903* | There is a unique element of (ℤ ↑m (0...(𝑝 − 1))) ~Qp -equivalent to any element of (ℤ ↑m ℤ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))))) | ||
Definition | df-qp 32904* | Define the 𝑝-adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 10-Oct-2021.) |
⊢ Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < )))))) | ||
Definition | df-zp 32905 | Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ Zp = (ZRing ∘ Qp) | ||
Definition | df-qpa 32906* | Define the completion of the 𝑝-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the 𝑛-th set the collection of polynomials with degree less than 𝑛 and with coefficients < (𝑝↑𝑛)). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial 𝑥↑(𝑝↑𝑛) − 𝑥, which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ _Qp = (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟 deg1 𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))}))) | ||
Definition | df-cp 32907 | Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ Cp = ( cplMetSp ∘ _Qp) | ||
I hope someone will enjoy solving (proving) the simple equations, inequalities, and calculations from this mathbox. I have proved these problems (theorems) using the Milpgame proof assistant. (It can be downloaded from https://us.metamath.org/other/milpgame/milpgame.html.) | ||
Theorem | problem1 32908 | Practice problem 1. Clues: 5p4e9 11796 3p2e5 11789 eqtri 2844 oveq1i 7166. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ ((3 + 2) + 4) = 9 | ||
Theorem | problem2 32909 | Practice problem 2. Clues: oveq12i 7168 adddiri 10654 add4i 10864 mulcli 10648 recni 10655 2re 11712 3eqtri 2848 10re 12118 5re 11725 1re 10641 4re 11722 eqcomi 2830 5p4e9 11796 oveq1i 7166 df-3 11702. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.) |
⊢ (((2 · ;10) + 5) + ((1 · ;10) + 4)) = ((3 · ;10) + 9) | ||
Theorem | problem3 32910 | Practice problem 3. Clues: eqcomi 2830 eqtri 2844 subaddrii 10975 recni 10655 4re 11722 3re 11718 1re 10641 df-4 11703 addcomi 10831. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ (𝐴 + 3) = 4 ⇒ ⊢ 𝐴 = 1 | ||
Theorem | problem4 32911 | Practice problem 4. Clues: pm3.2i 473 eqcomi 2830 eqtri 2844 subaddrii 10975 recni 10655 7re 11731 6re 11728 ax-1cn 10595 df-7 11706 ax-mp 5 oveq1i 7166 3cn 11719 2cn 11713 df-3 11702 mulid2i 10646 subdiri 11090 mp3an 1457 mulcli 10648 subadd23 10898 oveq2i 7167 oveq12i 7168 3t2e6 11804 mulcomi 10649 subcli 10962 biimpri 230 subadd2i 10974. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 3 & ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7 ⇒ ⊢ (𝐴 = 1 ∧ 𝐵 = 2) | ||
Theorem | problem5 32912 | Practice problem 5. Clues: 3brtr3i 5095 mpbi 232 breqtri 5091 ltaddsubi 11201 remulcli 10657 2re 11712 3re 11718 9re 11737 eqcomi 2830 mvlladdi 10904 3cn 6cn 11729 eqtr3i 2846 6p3e9 11798 addcomi 10831 ltdiv1ii 11569 6re 11728 nngt0i 11677 2nn 11711 divcan3i 11386 recni 10655 2cn 11713 2ne0 11742 mpbir 233 eqtri 2844 mulcomi 10649 3t2e6 11804 divmuli 11394. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℝ & ⊢ ((2 · 𝐴) + 3) < 9 ⇒ ⊢ 𝐴 < 3 | ||
Theorem | quad3 32913 | Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.) |
⊢ 𝑋 ∈ ℂ & ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ⇒ ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) | ||
Theorem | climuzcnv 32914* | Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑)))) | ||
Theorem | sinccvglem 32915* | ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖ {0})) & ⊢ (𝜑 → 𝐹 ⇝ 0) & ⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) & ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1) | ||
Theorem | sinccvg 32916* | ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
⊢ ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝐹 ⇝ 0) → ((𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) ∘ 𝐹) ⇝ 1) | ||
Theorem | circum 32917* | The circumference of a circle of radius 𝑅, defined as the limit as 𝑛 ⇝ +∞ of the perimeter of an inscribed n-sided isogons, is ((2 · π) · 𝑅). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.) |
⊢ 𝐴 = ((2 · π) / 𝑛) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ ((2 · 𝑛) · (𝑅 · (sin‘(𝐴 / 2))))) & ⊢ 𝑅 ∈ ℝ ⇒ ⊢ 𝑃 ⇝ ((2 · π) · 𝑅) | ||
Theorem | elfzm12 32918 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁))) | ||
Theorem | nn0seqcvg 32919* | A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ 𝐹:ℕ0⟶ℕ0 & ⊢ 𝑁 = (𝐹‘0) & ⊢ (𝑘 ∈ ℕ0 → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘))) ⇒ ⊢ (𝐹‘𝑁) = 0 | ||
Theorem | lediv2aALT 32920 | Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) | ||
Theorem | abs2sqlei 32921 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2)) | ||
Theorem | abs2sqlti 32922 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)) | ||
Theorem | abs2sqle 32923 | The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2))) | ||
Theorem | abs2sqlt 32924 | 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 32925 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)) | ||
Theorem | abs2difabsi 32926 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)) | ||
Theorem | axextprim 32927 | ax-ext 2793 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧)) | ||
Theorem | axrepprim 32928 | ax-rep 5190 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥))) | ||
Theorem | axunprim 32929 | ax-un 7461 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axpowprim 32930 | ax-pow 5266 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦) | ||
Theorem | axregprim 32931 | ax-reg 9056 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | axinfprim 32932 | ax-inf 9101 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | ||
Theorem | axacprim 32933 | ax-ac 9881 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥)))))) | ||
Theorem | untelirr 32934* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 33037). 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 32935* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥) | ||
Theorem | untsucf 32936* | 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 32937 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥 | ||
Theorem | untint 32938* | 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 32939* | If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥) | ||
Theorem | untangtr 32940* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦)) | ||
Theorem | 3orel2 32941 | 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 32942 | Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) |
⊢ (¬ 𝜒 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜓))) | ||
Theorem | 3pm3.2ni 32943 | Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 & ⊢ ¬ 𝜒 ⇒ ⊢ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Theorem | 3jaodd 32944 | Double deduction form of 3jaoi 1423. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂))) | ||
Theorem | 3orit 32945 | Closed form of 3ori 1420. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)) | ||
Theorem | biimpexp 32946 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒))) | ||
Theorem | 3orel13 32947 | Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜓)) | ||
Theorem | nepss 32948 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵)) | ||
Theorem | 3ccased 32949 | Triple disjunction form of ccased 1033. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓)) ⇒ ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓)) | ||
Theorem | dfso3 32950* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | brtpid1 32951 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
⊢ 𝐴{〈𝐴, 𝐵〉, 𝐶, 𝐷}𝐵 | ||
Theorem | brtpid2 32952 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
⊢ 𝐴{𝐶, 〈𝐴, 𝐵〉, 𝐷}𝐵 | ||
Theorem | brtpid3 32953 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
⊢ 𝐴{𝐶, 𝐷, 〈𝐴, 𝐵〉}𝐵 | ||
Theorem | ceqsrexv2 32954* | Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | iota5f 32955* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
Theorem | ceqsralv2 32956* | Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)) | ||
Theorem | dford5 32957 | 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 32958 | Closed form of ja 188. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) | ||
Theorem | sqdivzi 32959 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
Theorem | supfz 32960 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
Theorem | inffz 32961 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
Theorem | fz0n 32962 | The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0)) | ||
Theorem | shftvalg 32963 | Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
Theorem | divcnvlin 32964* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
Theorem | climlec3 32965* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | logi 32966 | Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
⊢ (log‘i) = (i · (π / 2)) | ||
Theorem | iexpire 32967 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
⊢ (i↑𝑐i) ∈ ℝ | ||
Theorem | bcneg1 32968 | The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0) | ||
Theorem | bcm1nt 32969 | 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 32970* | A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) | ||
Theorem | bccolsum 32971* | A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1))) | ||
Theorem | iprodefisumlem 32972 | Lemma for iprodefisum 32973. (Contributed by Scott Fenton, 11-Feb-2018.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹))) | ||
Theorem | iprodefisum 32973* | 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 32974* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) | ||
Theorem | faclimlem1 32975* | Lemma for faclim 32978. 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 32976* | Lemma for faclim 32978. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1)) | ||
Theorem | faclimlem3 32977 | Lemma for faclim 32978. 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 32978* | 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 32979* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘)))) | ||
Theorem | faclim2 32980* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) ⇒ ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1) | ||
Theorem | pdivsq 32981 | Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃 ∥ 𝑀 ↔ 𝑃 ∥ (𝑀↑2))) | ||
Theorem | dvdspw 32982 | Exponentiation law for divisibility. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀↑𝑁))) | ||
Theorem | gcd32 32983 | 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 32984 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵)) | ||
Theorem | brtp 32985 | A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ (𝑋{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹))) | ||
Theorem | dftr6 32986 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E ))) | ||
Theorem | coep 32987* | Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥) | ||
Theorem | coepr 32988* | Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵) | ||
Theorem | dffr5 32989 | A quantifier free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅))) | ||
Theorem | dfso2 32990 | Quantifier free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) | ||
Theorem | dfpo2 32991 | Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) | ||
Theorem | br8 32992* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑅〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ 𝜌)) | ||
Theorem | br6 32993* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (〈𝐴, 〈𝐵, 𝐶〉〉𝑅〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 𝜁)) | ||
Theorem | br4 32994* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ 𝜏)) | ||
Theorem | cnvco1 32995 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴) | ||
Theorem | cnvco2 32996 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴) | ||
Theorem | eldm3 32997 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) | ||
Theorem | elrn3 32998 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅) | ||
Theorem | pocnv 32999 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
Theorem | socnv 33000 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |