Home | Metamath
Proof Explorer Theorem List (p. 329 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-rqp 32801* | 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 32802* | 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 32803 | Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ Zp = (ZRing ∘ Qp) | ||
Definition | df-qpa 32804* | 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 32805 | 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 32806 | Practice problem 1. Clues: 5p4e9 11784 3p2e5 11777 eqtri 2844 oveq1i 7155. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ ((3 + 2) + 4) = 9 | ||
Theorem | problem2 32807 | Practice problem 2. Clues: oveq12i 7157 adddiri 10643 add4i 10853 mulcli 10637 recni 10644 2re 11700 3eqtri 2848 10re 12106 5re 11713 1re 10630 4re 11710 eqcomi 2830 5p4e9 11784 oveq1i 7155 df-3 11690. (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 32808 | Practice problem 3. Clues: eqcomi 2830 eqtri 2844 subaddrii 10964 recni 10644 4re 11710 3re 11706 1re 10630 df-4 11691 addcomi 10820. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ (𝐴 + 3) = 4 ⇒ ⊢ 𝐴 = 1 | ||
Theorem | problem4 32809 | Practice problem 4. Clues: pm3.2i 471 eqcomi 2830 eqtri 2844 subaddrii 10964 recni 10644 7re 11719 6re 11716 ax-1cn 10584 df-7 11694 ax-mp 5 oveq1i 7155 3cn 11707 2cn 11701 df-3 11690 mulid2i 10635 subdiri 11079 mp3an 1452 mulcli 10637 subadd23 10887 oveq2i 7156 oveq12i 7157 3t2e6 11792 mulcomi 10638 subcli 10951 biimpri 229 subadd2i 10963. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 3 & ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7 ⇒ ⊢ (𝐴 = 1 ∧ 𝐵 = 2) | ||
Theorem | problem5 32810 | Practice problem 5. Clues: 3brtr3i 5087 mpbi 231 breqtri 5083 ltaddsubi 11190 remulcli 10646 2re 11700 3re 11706 9re 11725 eqcomi 2830 mvlladdi 10893 3cn 6cn 11717 eqtr3i 2846 6p3e9 11786 addcomi 10820 ltdiv1ii 11558 6re 11716 nngt0i 11665 2nn 11699 divcan3i 11375 recni 10644 2cn 11701 2ne0 11730 mpbir 232 eqtri 2844 mulcomi 10638 3t2e6 11792 divmuli 11383. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ ℝ & ⊢ ((2 · 𝐴) + 3) < 9 ⇒ ⊢ 𝐴 < 3 | ||
Theorem | quad3 32811 | 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 32812* | Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.) |
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑)))) | ||
Theorem | sinccvglem 32813* | ((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 32814* | ((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 32815* | 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 32816 | Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁))) | ||
Theorem | nn0seqcvg 32817* | 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 32818 | 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 32819 | 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 32820 | 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 32821 | 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 32822 | 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 32823 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)) | ||
Theorem | abs2difabsi 32824 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)) | ||
Theorem | axextprim 32825 | ax-ext 2793 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧)) | ||
Theorem | axrepprim 32826 | ax-rep 5182 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥))) | ||
Theorem | axunprim 32827 | ax-un 7450 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axpowprim 32828 | ax-pow 5258 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦) | ||
Theorem | axregprim 32829 | ax-reg 9045 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | axinfprim 32830 | ax-inf 9090 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | ||
Theorem | axacprim 32831 | ax-ac 9870 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.) |
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥)))))) | ||
Theorem | untelirr 32832* | We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 32935). 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 32833* | The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥) | ||
Theorem | untsucf 32834* | 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 32835 | The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥 | ||
Theorem | untint 32836* | 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 32837* | If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.) |
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥) | ||
Theorem | untangtr 32838* | A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.) |
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦)) | ||
Theorem | 3orel2 32839 | 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 32840 | Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) |
⊢ (¬ 𝜒 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜓))) | ||
Theorem | 3pm3.2ni 32841 | Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 & ⊢ ¬ 𝜒 ⇒ ⊢ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Theorem | 3jaodd 32842 | Double deduction form of 3jaoi 1419. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂))) | ||
Theorem | 3orit 32843 | Closed form of 3ori 1416. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)) | ||
Theorem | biimpexp 32844 | A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒))) | ||
Theorem | 3orel13 32845 | Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜓)) | ||
Theorem | nepss 32846 | Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.) |
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵)) | ||
Theorem | 3ccased 32847 | Triple disjunction form of ccased 1030. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓)) & ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓)) ⇒ ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓)) | ||
Theorem | dfso3 32848* | Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.) |
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | brtpid1 32849 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
⊢ 𝐴{〈𝐴, 𝐵〉, 𝐶, 𝐷}𝐵 | ||
Theorem | brtpid2 32850 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
⊢ 𝐴{𝐶, 〈𝐴, 𝐵〉, 𝐷}𝐵 | ||
Theorem | brtpid3 32851 | A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.) |
⊢ 𝐴{𝐶, 𝐷, 〈𝐴, 𝐵〉}𝐵 | ||
Theorem | ceqsrexv2 32852* | Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | iota5f 32853* | A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
Theorem | ceqsralv2 32854* | Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)) | ||
Theorem | dford5 32855 | 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 32856 | Closed form of ja 187. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.) |
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) | ||
Theorem | sqdivzi 32857 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
Theorem | supfz 32858 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
Theorem | inffz 32859 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
Theorem | fz0n 32860 | The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0)) | ||
Theorem | shftvalg 32861 | Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
Theorem | divcnvlin 32862* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
Theorem | climlec3 32863* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | logi 32864 | Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
⊢ (log‘i) = (i · (π / 2)) | ||
Theorem | iexpire 32865 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
⊢ (i↑𝑐i) ∈ ℝ | ||
Theorem | bcneg1 32866 | The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0) | ||
Theorem | bcm1nt 32867 | 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 32868* | A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) | ||
Theorem | bccolsum 32869* | A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1))) | ||
Theorem | iprodefisumlem 32870 | Lemma for iprodefisum 32871. (Contributed by Scott Fenton, 11-Feb-2018.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℂ) ⇒ ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹))) | ||
Theorem | iprodefisum 32871* | 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 32872* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) | ||
Theorem | faclimlem1 32873* | Lemma for faclim 32876. 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 32874* | Lemma for faclim 32876. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1)) | ||
Theorem | faclimlem3 32875 | Lemma for faclim 32876. 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 32876* | 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 32877* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘)))) | ||
Theorem | faclim2 32878* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) ⇒ ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1) | ||
Theorem | pdivsq 32879 | Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃 ∥ 𝑀 ↔ 𝑃 ∥ (𝑀↑2))) | ||
Theorem | dvdspw 32880 | Exponentiation law for divisibility. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀↑𝑁))) | ||
Theorem | gcd32 32881 | 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 32882 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵)) | ||
Theorem | brtp 32883 | A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ (𝑋{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹))) | ||
Theorem | dftr6 32884 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E ))) | ||
Theorem | coep 32885* | Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥) | ||
Theorem | coepr 32886* | Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵) | ||
Theorem | dffr5 32887 | A quantifier free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅))) | ||
Theorem | dfso2 32888 | Quantifier free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) | ||
Theorem | dfpo2 32889 | 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 32890* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑅〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ 𝜌)) | ||
Theorem | br6 32891* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (〈𝐴, 〈𝐵, 𝐶〉〉𝑅〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 𝜁)) | ||
Theorem | br4 32892* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ 𝜏)) | ||
Theorem | cnvco1 32893 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴) | ||
Theorem | cnvco2 32894 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴) | ||
Theorem | eldm3 32895 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) | ||
Theorem | elrn3 32896 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅) | ||
Theorem | pocnv 32897 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
Theorem | socnv 32898 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) | ||
Theorem | sotrd 32899 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) & ⊢ (𝜑 → 𝑌𝑅𝑍) ⇒ ⊢ (𝜑 → 𝑋𝑅𝑍) | ||
Theorem | sotr3 32900 | Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → ((𝑋𝑅𝑌 ∧ ¬ 𝑍𝑅𝑌) → 𝑋𝑅𝑍)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |