Home | Metamath
Proof Explorer Theorem List (p. 412 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | monotoddzz 41101* | A function (given implicitly) which is odd and monotonic on โ0 is monotonic on โค. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
โข ((๐ โง ๐ฅ โ โ0 โง ๐ฆ โ โ0) โ (๐ฅ < ๐ฆ โ ๐ธ < ๐น)) & โข ((๐ โง ๐ฅ โ โค) โ ๐ธ โ โ) & โข ((๐ โง ๐ฆ โ โค) โ ๐บ = -๐น) & โข (๐ฅ = ๐ด โ ๐ธ = ๐ถ) & โข (๐ฅ = ๐ต โ ๐ธ = ๐ท) & โข (๐ฅ = ๐ฆ โ ๐ธ = ๐น) & โข (๐ฅ = -๐ฆ โ ๐ธ = ๐บ) โ โข ((๐ โง ๐ด โ โค โง ๐ต โ โค) โ (๐ด < ๐ต โ ๐ถ < ๐ท)) | ||
Theorem | oddcomabszz 41102* | An odd function which takes nonnegative values on nonnegative arguments commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ โง ๐ฅ โ โค) โ ๐ด โ โ) & โข ((๐ โง ๐ฅ โ โค โง 0 โค ๐ฅ) โ 0 โค ๐ด) & โข ((๐ โง ๐ฆ โ โค) โ ๐ถ = -๐ต) & โข (๐ฅ = ๐ฆ โ ๐ด = ๐ต) & โข (๐ฅ = -๐ฆ โ ๐ด = ๐ถ) & โข (๐ฅ = ๐ท โ ๐ด = ๐ธ) & โข (๐ฅ = (absโ๐ท) โ ๐ด = ๐น) โ โข ((๐ โง ๐ท โ โค) โ (absโ๐ธ) = ๐น) | ||
Theorem | 2nn0ind 41103* | Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข ๐ & โข ๐ & โข (๐ฆ โ โ โ ((๐ โง ๐) โ ๐)) & โข (๐ฅ = 0 โ (๐ โ ๐)) & โข (๐ฅ = 1 โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ โ 1) โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ + 1) โ (๐ โ ๐)) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) โ โข (๐ด โ โ0 โ ๐) | ||
Theorem | zindbi 41104* | Inductively transfer a property to the integers if it holds for zero and passes between adjacent integers in either direction. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (๐ฆ โ โค โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ + 1) โ (๐ โ ๐)) & โข (๐ฅ = 0 โ (๐ โ ๐)) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) โ โข (๐ด โ โค โ (๐ โ ๐)) | ||
Theorem | rmxypos 41105 | For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ (0 < (๐ด Xrm ๐) โง 0 โค (๐ด Yrm ๐))) | ||
Theorem | ltrmynn0 41106 | The Y-sequence is strictly monotonic on โ0. Strengthened by ltrmy 41110. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0 โง ๐ โ โ0) โ (๐ < ๐ โ (๐ด Yrm ๐) < (๐ด Yrm ๐))) | ||
Theorem | ltrmxnn0 41107 | The X-sequence is strictly monotonic on โ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0 โง ๐ โ โ0) โ (๐ < ๐ โ (๐ด Xrm ๐) < (๐ด Xrm ๐))) | ||
Theorem | lermxnn0 41108 | The X-sequence is monotonic on โ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0 โง ๐ โ โ0) โ (๐ โค ๐ โ (๐ด Xrm ๐) โค (๐ด Xrm ๐))) | ||
Theorem | rmxnn 41109 | The X-sequence is defined to range over โ0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค) โ (๐ด Xrm ๐) โ โ) | ||
Theorem | ltrmy 41110 | The Y-sequence is strictly monotonic over โค. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ โ โค) โ (๐ < ๐ โ (๐ด Yrm ๐) < (๐ด Yrm ๐))) | ||
Theorem | rmyeq0 41111 | Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค) โ (๐ = 0 โ (๐ด Yrm ๐) = 0)) | ||
Theorem | rmyeq 41112 | Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ โ โค) โ (๐ = ๐ โ (๐ด Yrm ๐) = (๐ด Yrm ๐))) | ||
Theorem | lermy 41113 | Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ (๐ด Yrm ๐) โค (๐ด Yrm ๐))) | ||
Theorem | rmynn 41114 | Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ) โ (๐ด Yrm ๐) โ โ) | ||
Theorem | rmynn0 41115 | Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ (๐ด Yrm ๐) โ โ0) | ||
Theorem | rmyabs 41116 | Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ต โ โค) โ (absโ(๐ด Yrm ๐ต)) = (๐ด Yrm (absโ๐ต))) | ||
Theorem | jm2.24nn 41117 | X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of [JonesMatijasevic] p. 697 restricted to โ. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ) โ ((๐ด Yrm (๐ โ 1)) + (๐ด Yrm ๐)) < (๐ด Xrm ๐)) | ||
Theorem | jm2.17a 41118 | First half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ (((2 ยท ๐ด) โ 1)โ๐) โค (๐ด Yrm (๐ + 1))) | ||
Theorem | jm2.17b 41119 | Weak form of the second half of lemma 2.17 of [JonesMatijasevic] p. 696, allowing induction to start lower. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ (๐ด Yrm (๐ + 1)) โค ((2 ยท ๐ด)โ๐)) | ||
Theorem | jm2.17c 41120 | Second half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ) โ (๐ด Yrm ((๐ + 1) + 1)) < ((2 ยท ๐ด)โ(๐ + 1))) | ||
Theorem | jm2.24 41121 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to โค. Could be eliminated with a more careful proof of jm2.26lem3 41159. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค) โ ((๐ด Yrm (๐ โ 1)) + (๐ด Yrm ๐)) < (๐ด Xrm ๐)) | ||
Theorem | rmygeid 41122 | Y(n) increases faster than n. Used implicitly without proof or comment in lemma 2.27 of [JonesMatijasevic] p. 697. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ ๐ โค (๐ด Yrm ๐)) | ||
Theorem | congtr 41123 | A wff of the form ๐ด โฅ (๐ต โ ๐ถ) is interpreted as a congruential equation. This is similar to (๐ต mod ๐ด) = (๐ถ mod ๐ด), but is defined such that behavior is regular for zero and negative values of ๐ด. To use this concept effectively, we need to show that congruential equations behave similarly to normal equations; first a transitivity law. Idea for the future: If there was a congruential equation symbol, it could incorporate type constraints, so that most of these would not need them. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ถ โ ๐ท))) โ ๐ด โฅ (๐ต โ ๐ท)) | ||
Theorem | congadd 41124 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ท โ โค โง ๐ธ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ท โ ๐ธ))) โ ๐ด โฅ ((๐ต + ๐ท) โ (๐ถ + ๐ธ))) | ||
Theorem | congmul 41125 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ท โ โค โง ๐ธ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ท โ ๐ธ))) โ ๐ด โฅ ((๐ต ยท ๐ท) โ (๐ถ ยท ๐ธ))) | ||
Theorem | congsym 41126 | Congruence mod ๐ด is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ด โฅ (๐ต โ ๐ถ))) โ ๐ด โฅ (๐ถ โ ๐ต)) | ||
Theorem | congneg 41127 | If two integers are congruent mod ๐ด, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ด โฅ (๐ต โ ๐ถ))) โ ๐ด โฅ (-๐ต โ -๐ถ)) | ||
Theorem | congsub 41128 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ท โ โค โง ๐ธ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ท โ ๐ธ))) โ ๐ด โฅ ((๐ต โ ๐ท) โ (๐ถ โ ๐ธ))) | ||
Theorem | congid 41129 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โฅ (๐ต โ ๐ต)) | ||
Theorem | mzpcong 41130* | Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.) |
โข ((๐น โ (mzPolyโ๐) โง (๐ โ (โค โm ๐) โง ๐ โ (โค โm ๐)) โง (๐ โ โค โง โ๐ โ ๐ ๐ โฅ ((๐โ๐) โ (๐โ๐)))) โ ๐ โฅ ((๐นโ๐) โ (๐นโ๐))) | ||
Theorem | congrep 41131* | Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข ((๐ด โ โ โง ๐ โ โค) โ โ๐ โ (0...(๐ด โ 1))๐ด โฅ (๐ โ ๐)) | ||
Theorem | congabseq 41132 | If two integers are congruent, they are either equal or separated by at least the congruence base. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (((๐ด โ โ โง ๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต โ ๐ถ)) โ ((absโ(๐ต โ ๐ถ)) < ๐ด โ ๐ต = ๐ถ)) | ||
Theorem | acongid 41133 |
A wff like that in this theorem will be known as an "alternating
congruence". A special symbol might be considered if more uses come
up.
They have many of the same properties as normal congruences, starting with
reflexivity.
JonesMatijasevic uses "a โก ยฑ b (mod c)" for this construction. The disjunction of divisibility constraints seems to adequately capture the concept, but it's rather verbose and somewhat inelegant. Use of an explicit equivalence relation might also work. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โฅ (๐ต โ ๐ต) โจ ๐ด โฅ (๐ต โ -๐ต))) | ||
Theorem | acongsym 41134 | Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ))) โ (๐ด โฅ (๐ถ โ ๐ต) โจ ๐ด โฅ (๐ถ โ -๐ต))) | ||
Theorem | acongneg2 41135 | Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ด โฅ (๐ต โ -๐ถ) โจ ๐ด โฅ (๐ต โ --๐ถ))) โ (๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ))) | ||
Theorem | acongtr 41136 | Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง ((๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ)) โง (๐ด โฅ (๐ถ โ ๐ท) โจ ๐ด โฅ (๐ถ โ -๐ท)))) โ (๐ด โฅ (๐ต โ ๐ท) โจ ๐ด โฅ (๐ต โ -๐ท))) | ||
Theorem | acongeq12d 41137 | Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข (๐ โ ๐ต = ๐ถ) & โข (๐ โ ๐ท = ๐ธ) โ โข (๐ โ ((๐ด โฅ (๐ต โ ๐ท) โจ ๐ด โฅ (๐ต โ -๐ท)) โ (๐ด โฅ (๐ถ โ ๐ธ) โจ ๐ด โฅ (๐ถ โ -๐ธ)))) | ||
Theorem | acongrep 41138* | Every integer is alternating-congruent to some number in the first half of the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข ((๐ด โ โ โง ๐ โ โค) โ โ๐ โ (0...๐ด)((2 ยท ๐ด) โฅ (๐ โ ๐) โจ (2 ยท ๐ด) โฅ (๐ โ -๐))) | ||
Theorem | fzmaxdif 41139 | Bound on the difference between two integers constrained to two possibly overlapping finite ranges. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (((๐ถ โ โค โง ๐ด โ (๐ต...๐ถ)) โง (๐น โ โค โง ๐ท โ (๐ธ...๐น)) โง (๐ถ โ ๐ธ) โค (๐น โ ๐ต)) โ (absโ(๐ด โ ๐ท)) โค (๐น โ ๐ต)) | ||
Theorem | fzneg 41140 | Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โ (๐ด โ (๐ต...๐ถ) โ -๐ด โ (-๐ถ...-๐ต))) | ||
Theorem | acongeq 41141 | Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 41160. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ โ โง ๐ต โ (0...๐ด) โง ๐ถ โ (0...๐ด)) โ (๐ต = ๐ถ โ ((2 ยท ๐ด) โฅ (๐ต โ ๐ถ) โจ (2 ยท ๐ด) โฅ (๐ต โ -๐ถ)))) | ||
Theorem | dvdsacongtr 41142 | Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง (๐ท โฅ ๐ด โง (๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ)))) โ (๐ท โฅ (๐ต โ ๐ถ) โจ ๐ท โฅ (๐ต โ -๐ถ))) | ||
Theorem | coprmdvdsb 41143 | Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐พ โ โค โง ๐ โ โค โง (๐ โ โค โง (๐พ gcd ๐) = 1)) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | modabsdifz 41144 | Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ ((๐ โ (๐ mod (absโ๐))) / ๐) โ โค) | ||
Theorem | dvdsabsmod0 41145 | Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 24-Sep-2014.) (Proof shortened by OpenAI, 3-Jul-2020.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โฅ ๐ โ (๐ mod (absโ๐)) = 0)) | ||
Theorem | jm2.18 41146 | Theorem 2.18 of [JonesMatijasevic] p. 696. Direct relationship of the exponential function to X and Y sequences. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐พ โ โ0 โง ๐ โ โ0) โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) โฅ (((๐ด Xrm ๐) โ ((๐ด โ ๐พ) ยท (๐ด Yrm ๐))) โ (๐พโ๐))) | ||
Theorem | jm2.19lem1 41147 | Lemma for jm2.19 41151. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค) โ ((๐ด Xrm ๐) gcd (๐ด Yrm ๐)) = 1) | ||
Theorem | jm2.19lem2 41148 | Lemma for jm2.19 41151. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + ๐)))) | ||
Theorem | jm2.19lem3 41149 | Lemma for jm2.19 41151. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) | ||
Theorem | jm2.19lem4 41150 | Lemma for jm2.19 41151. Extend to ZZ by symmetry. TODO: use zindbi 41104. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) | ||
Theorem | jm2.19 41151 | Lemma 2.19 of [JonesMatijasevic] p. 696. Transfer divisibility constraints between Y-values and their indices. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ด Yrm ๐) โฅ (๐ด Yrm ๐))) | ||
Theorem | jm2.21 41152 | Lemma for jm2.20nn 41155. Express X and Y values as a binomial. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ฝ โ โค) โ ((๐ด Xrm (๐ ยท ๐ฝ)) + ((โโ((๐ดโ2) โ 1)) ยท (๐ด Yrm (๐ ยท ๐ฝ)))) = (((๐ด Xrm ๐) + ((โโ((๐ดโ2) โ 1)) ยท (๐ด Yrm ๐)))โ๐ฝ)) | ||
Theorem | jm2.22 41153* | Lemma for jm2.20nn 41155. Applying binomial theorem and taking irrational part. (Contributed by Stefan O'Rear, 26-Sep-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ฝ โ โ0) โ (๐ด Yrm (๐ ยท ๐ฝ)) = ฮฃ๐ โ {๐ฅ โ (0...๐ฝ) โฃ ยฌ 2 โฅ ๐ฅ} ((๐ฝC๐) ยท (((๐ด Xrm ๐)โ(๐ฝ โ ๐)) ยท (((๐ด Yrm ๐)โ๐) ยท (((๐ดโ2) โ 1)โ((๐ โ 1) / 2)))))) | ||
Theorem | jm2.23 41154 | Lemma for jm2.20nn 41155. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ฝ โ โ) โ ((๐ด Yrm ๐)โ3) โฅ ((๐ด Yrm (๐ ยท ๐ฝ)) โ (๐ฝ ยท (((๐ด Xrm ๐)โ(๐ฝ โ 1)) ยท (๐ด Yrm ๐))))) | ||
Theorem | jm2.20nn 41155 | Lemma 2.20 of [JonesMatijasevic] p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ โง ๐ โ โ) โ (((๐ด Yrm ๐)โ2) โฅ (๐ด Yrm ๐) โ (๐ ยท (๐ด Yrm ๐)) โฅ ๐)) | ||
Theorem | jm2.25lem1 41156 | Lemma for jm2.26 41160. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง (๐ด โฅ (๐ถ โ ๐ท) โจ ๐ด โฅ (๐ถ โ -๐ท))) โ ((๐ด โฅ (๐ท โ ๐ต) โจ ๐ด โฅ (๐ท โ -๐ต)) โ (๐ด โฅ (๐ถ โ ๐ต) โจ ๐ด โฅ (๐ถ โ -๐ต)))) | ||
Theorem | jm2.25 41157 | Lemma for jm2.26 41160. Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โค) โ ((๐ด Xrm ๐) โฅ ((๐ด Yrm (๐ + (๐ผ ยท (2 ยท ๐)))) โ (๐ด Yrm ๐)) โจ (๐ด Xrm ๐) โฅ ((๐ด Yrm (๐ + (๐ผ ยท (2 ยท ๐)))) โ -(๐ด Yrm ๐)))) | ||
Theorem | jm2.26a 41158 | Lemma for jm2.26 41160. Reverse direction is required to prove forward direction, so do it separately. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ (โคโฅโ2) โง ๐ โ โค) โง (๐พ โ โค โง ๐ โ โค)) โ (((2 ยท ๐) โฅ (๐พ โ ๐) โจ (2 ยท ๐) โฅ (๐พ โ -๐)) โ ((๐ด Xrm ๐) โฅ ((๐ด Yrm ๐พ) โ (๐ด Yrm ๐)) โจ (๐ด Xrm ๐) โฅ ((๐ด Yrm ๐พ) โ -(๐ด Yrm ๐))))) | ||
Theorem | jm2.26lem3 41159 | Lemma for jm2.26 41160. Use acongrep 41138 to find K', M' ~ K, M in [ 0,N ]. Thus Y(K') ~ Y(M') and both are small; K' = M' on pain of contradicting 2.24, so K ~ M. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข (((๐ด โ (โคโฅโ2) โง ๐ โ โ) โง (๐พ โ (0...๐) โง ๐ โ (0...๐)) โง ((๐ด Xrm ๐) โฅ ((๐ด Yrm ๐พ) โ (๐ด Yrm ๐)) โจ (๐ด Xrm ๐) โฅ ((๐ด Yrm ๐พ) โ -(๐ด Yrm ๐)))) โ ๐พ = ๐) | ||
Theorem | jm2.26 41160 | Lemma 2.26 of [JonesMatijasevic] p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ (โคโฅโ2) โง ๐ โ โ) โง (๐พ โ โค โง ๐ โ โค)) โ (((๐ด Xrm ๐) โฅ ((๐ด Yrm ๐พ) โ (๐ด Yrm ๐)) โจ (๐ด Xrm ๐) โฅ ((๐ด Yrm ๐พ) โ -(๐ด Yrm ๐))) โ ((2 ยท ๐) โฅ (๐พ โ ๐) โจ (2 ยท ๐) โฅ (๐พ โ -๐)))) | ||
Theorem | jm2.15nn0 41161 | Lemma 2.15 of [JonesMatijasevic] p. 695. Yrm is a polynomial for fixed N, so has the expected congruence property. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ต โ (โคโฅโ2) โง ๐ โ โ0) โ (๐ด โ ๐ต) โฅ ((๐ด Yrm ๐) โ (๐ต Yrm ๐))) | ||
Theorem | jm2.16nn0 41162 | Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 41161 if Yrm is redefined as described in rmyluc 41095. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ (๐ด โ 1) โฅ ((๐ด Yrm ๐) โ ๐)) | ||
Theorem | jm2.27a 41163 | Lemma for jm2.27 41166. Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ0) & โข (๐ โ ๐ธ โ โ0) & โข (๐ โ ๐น โ โ0) & โข (๐ โ ๐บ โ โ0) & โข (๐ โ ๐ป โ โ0) & โข (๐ โ ๐ผ โ โ0) & โข (๐ โ ๐ฝ โ โ0) & โข (๐ โ ((๐ทโ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1) & โข (๐ โ ((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1) & โข (๐ โ ๐บ โ (โคโฅโ2)) & โข (๐ โ ((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1) & โข (๐ โ ๐ธ = ((๐ฝ + 1) ยท (2 ยท (๐ถโ2)))) & โข (๐ โ ๐น โฅ (๐บ โ ๐ด)) & โข (๐ โ (2 ยท ๐ถ) โฅ (๐บ โ 1)) & โข (๐ โ ๐น โฅ (๐ป โ ๐ถ)) & โข (๐ โ (2 ยท ๐ถ) โฅ (๐ป โ ๐ต)) & โข (๐ โ ๐ต โค ๐ถ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ท = (๐ด Xrm ๐)) & โข (๐ โ ๐ถ = (๐ด Yrm ๐)) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐น = (๐ด Xrm ๐)) & โข (๐ โ ๐ธ = (๐ด Yrm ๐)) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ผ = (๐บ Xrm ๐ )) & โข (๐ โ ๐ป = (๐บ Yrm ๐ )) โ โข (๐ โ ๐ถ = (๐ด Yrm ๐ต)) | ||
Theorem | jm2.27b 41164 | Lemma for jm2.27 41166. Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ0) & โข (๐ โ ๐ธ โ โ0) & โข (๐ โ ๐น โ โ0) & โข (๐ โ ๐บ โ โ0) & โข (๐ โ ๐ป โ โ0) & โข (๐ โ ๐ผ โ โ0) & โข (๐ โ ๐ฝ โ โ0) & โข (๐ โ ((๐ทโ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1) & โข (๐ โ ((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1) & โข (๐ โ ๐บ โ (โคโฅโ2)) & โข (๐ โ ((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1) & โข (๐ โ ๐ธ = ((๐ฝ + 1) ยท (2 ยท (๐ถโ2)))) & โข (๐ โ ๐น โฅ (๐บ โ ๐ด)) & โข (๐ โ (2 ยท ๐ถ) โฅ (๐บ โ 1)) & โข (๐ โ ๐น โฅ (๐ป โ ๐ถ)) & โข (๐ โ (2 ยท ๐ถ) โฅ (๐ป โ ๐ต)) & โข (๐ โ ๐ต โค ๐ถ) โ โข (๐ โ ๐ถ = (๐ด Yrm ๐ต)) | ||
Theorem | jm2.27c 41165 | Lemma for jm2.27 41166. Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ = (๐ด Yrm ๐ต)) & โข ๐ท = (๐ด Xrm ๐ต) & โข ๐ = (๐ต ยท (๐ด Yrm ๐ต)) & โข ๐ธ = (๐ด Yrm (2 ยท ๐)) & โข ๐น = (๐ด Xrm (2 ยท ๐)) & โข ๐บ = (๐ด + ((๐นโ2) ยท ((๐นโ2) โ ๐ด))) & โข ๐ป = (๐บ Yrm ๐ต) & โข ๐ผ = (๐บ Xrm ๐ต) & โข ๐ฝ = ((๐ธ / (2 ยท (๐ถโ2))) โ 1) โ โข (๐ โ (((๐ท โ โ0 โง ๐ธ โ โ0 โง ๐น โ โ0) โง (๐บ โ โ0 โง ๐ป โ โ0 โง ๐ผ โ โ0)) โง (๐ฝ โ โ0 โง (((((๐ทโ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐นโ2) โ (((๐ดโ2) โ 1) ยท (๐ธโ2))) = 1 โง ๐บ โ (โคโฅโ2)) โง (((๐ผโ2) โ (((๐บโ2) โ 1) ยท (๐ปโ2))) = 1 โง ๐ธ = ((๐ฝ + 1) ยท (2 ยท (๐ถโ2))) โง ๐น โฅ (๐บ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐บ โ 1) โง ๐น โฅ (๐ป โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (๐ป โ ๐ต) โง ๐ต โค ๐ถ)))))) | ||
Theorem | jm2.27 41166* | Lemma 2.27 of [JonesMatijasevic] p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a 41163 and jm2.27c 41165. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine". (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ = (๐ด Yrm ๐ต) โ โ๐ โ โ0 โ๐ โ โ0 โ๐ โ โ0 โ๐ โ โ0 โโ โ โ0 โ๐ โ โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐โ2))) = 1 โง ๐ โ (โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) | ||
Theorem | jm2.27dlem1 41167* | Lemma for rmydioph 41172. Substitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ด โ (1...๐ต) โ โข (๐ = (๐ โพ (1...๐ต)) โ (๐โ๐ด) = (๐โ๐ด)) | ||
Theorem | jm2.27dlem2 41168 | Lemma for rmydioph 41172. This theorem is used along with the next three to efficiently infer steps like 7 โ (1...;10). (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ด โ (1...๐ต) & โข ๐ถ = (๐ต + 1) & โข ๐ต โ โ โ โข ๐ด โ (1...๐ถ) | ||
Theorem | jm2.27dlem3 41169 | Lemma for rmydioph 41172. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ด โ โ โ โข ๐ด โ (1...๐ด) | ||
Theorem | jm2.27dlem4 41170 | Lemma for rmydioph 41172. Infer โ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ด โ โ & โข ๐ต = (๐ด + 1) โ โข ๐ต โ โ | ||
Theorem | jm2.27dlem5 41171 | Lemma for rmydioph 41172. Used with sselii 3940 to infer membership of midpoints of range; jm2.27dlem2 41168 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ต = (๐ด + 1) & โข (1...๐ต) โ (1...๐ถ) โ โข (1...๐ด) โ (1...๐ถ) | ||
Theorem | rmydioph 41172 | jm2.27 41166 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
โข {๐ โ (โ0 โm (1...3)) โฃ ((๐โ1) โ (โคโฅโ2) โง (๐โ3) = ((๐โ1) Yrm (๐โ2)))} โ (Diophโ3) | ||
Theorem | rmxdiophlem 41173* | X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0 โง ๐ โ โ0) โ (๐ = (๐ด Xrm ๐) โ โ๐ฆ โ โ0 (๐ฆ = (๐ด Yrm ๐) โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ฆโ2))) = 1))) | ||
Theorem | rmxdioph 41174 | X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
โข {๐ โ (โ0 โm (1...3)) โฃ ((๐โ1) โ (โคโฅโ2) โง (๐โ3) = ((๐โ1) Xrm (๐โ2)))} โ (Diophโ3) | ||
Theorem | jm3.1lem1 41175 | Lemma for jm3.1 41178. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐พ โ (โคโฅโ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) โ โข (๐ โ (๐พโ๐) < ๐ด) | ||
Theorem | jm3.1lem2 41176 | Lemma for jm3.1 41178. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐พ โ (โคโฅโ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) โ โข (๐ โ (๐พโ๐) < ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1)) | ||
Theorem | jm3.1lem3 41177 | Lemma for jm3.1 41178. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐พ โ (โคโฅโ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) โ โข (๐ โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) โ โ) | ||
Theorem | jm3.1 41178 | Diophantine expression for exponentiation. Lemma 3.1 of [JonesMatijasevic] p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข (((๐ด โ (โคโฅโ2) โง ๐พ โ (โคโฅโ2) โง ๐ โ โ) โง (๐พ Yrm (๐ + 1)) โค ๐ด) โ (๐พโ๐) = (((๐ด Xrm ๐) โ ((๐ด โ ๐พ) ยท (๐ด Yrm ๐))) mod ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1))) | ||
Theorem | expdiophlem1 41179* | Lemma for expdioph 41181. Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
โข (๐ถ โ โ0 โ (((๐ด โ (โคโฅโ2) โง ๐ต โ โ) โง ๐ถ = (๐ดโ๐ต)) โ โ๐ โ โ0 โ๐ โ โ0 โ๐ โ โ0 ((๐ด โ (โคโฅโ2) โง ๐ต โ โ) โง ((๐ด โ (โคโฅโ2) โง ๐ = (๐ด Yrm (๐ต + 1))) โง ((๐ โ (โคโฅโ2) โง ๐ = (๐ Yrm ๐ต)) โง ((๐ โ (โคโฅโ2) โง ๐ = (๐ Xrm ๐ต)) โง (๐ถ < ((((2 ยท ๐) ยท ๐ด) โ (๐ดโ2)) โ 1) โง ((((2 ยท ๐) ยท ๐ด) โ (๐ดโ2)) โ 1) โฅ ((๐ โ ((๐ โ ๐ด) ยท ๐)) โ ๐ถ)))))))) | ||
Theorem | expdiophlem2 41180 | Lemma for expdioph 41181. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
โข {๐ โ (โ0 โm (1...3)) โฃ (((๐โ1) โ (โคโฅโ2) โง (๐โ2) โ โ) โง (๐โ3) = ((๐โ1)โ(๐โ2)))} โ (Diophโ3) | ||
Theorem | expdioph 41181 | The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
โข {๐ โ (โ0 โm (1...3)) โฃ (๐โ3) = ((๐โ1)โ(๐โ2))} โ (Diophโ3) | ||
Theorem | setindtr 41182* | Set induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind 9604; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (โ๐ฅ(๐ฅ โ ๐ด โ ๐ฅ โ ๐ด) โ (โ๐ฆ(Tr ๐ฆ โง ๐ต โ ๐ฆ) โ ๐ต โ ๐ด)) | ||
Theorem | setindtrs 41183* | Set induction scheme without Infinity. See comments at setindtr 41182. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (โ๐ฆ โ ๐ฅ ๐ โ ๐) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = ๐ต โ (๐ โ ๐)) โ โข (โ๐ง(Tr ๐ง โง ๐ต โ ๐ง) โ ๐) | ||
Theorem | dford3lem1 41184* | Lemma for dford3 41186. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข ((Tr ๐ โง โ๐ฆ โ ๐ Tr ๐ฆ) โ โ๐ โ ๐ (Tr ๐ โง โ๐ฆ โ ๐ Tr ๐ฆ)) | ||
Theorem | dford3lem2 41185* | Lemma for dford3 41186. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข ((Tr ๐ฅ โง โ๐ฆ โ ๐ฅ Tr ๐ฆ) โ ๐ฅ โ On) | ||
Theorem | dford3 41186* | Ordinals are precisely the hereditarily transitive classes. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (Ord ๐ โ (Tr ๐ โง โ๐ฅ โ ๐ Tr ๐ฅ)) | ||
Theorem | dford4 41187* | dford3 41186 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (Ord ๐ โ โ๐โ๐โ๐((๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐ โง (๐ โ ๐ โ ๐ โ ๐)))) | ||
Theorem | wopprc 41188 | Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
โข ((๐ด โ V โง ๐ต โ V) โ ยฌ 1o โ {{{๐ด}, โ }, {{๐ต}}}) | ||
Theorem | rpnnen3lem 41189* | Lemma for rpnnen3 41190. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข (((๐ โ โ โง ๐ โ โ) โง ๐ < ๐) โ {๐ โ โ โฃ ๐ < ๐} โ {๐ โ โ โฃ ๐ < ๐}) | ||
Theorem | rpnnen3 41190 | Dedekind cut injection of โ into ๐ซ โ. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข โ โผ ๐ซ โ | ||
Theorem | axac10 41191 | Characterization of choice similar to dffin1-5 10258. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
โข ( โ โ On) = V | ||
Theorem | harinf 41192 | The Hartogs number of an infinite set is at least ฯ. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
โข ((๐ โ ๐ โง ยฌ ๐ โ Fin) โ ฯ โ (harโ๐)) | ||
Theorem | wdom2d2 41193* | Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข ((๐ โง ๐ฅ โ ๐ด) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ฅ = ๐) โ โข (๐ โ ๐ด โผ* (๐ต ร ๐ถ)) | ||
Theorem | ttac 41194 | Tarski's theorem about choice: infxpidm 10432 is equivalent to ax-ac 10329. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.) |
โข (CHOICE โ โ๐(ฯ โผ ๐ โ (๐ ร ๐) โ ๐)) | ||
Theorem | pw2f1ocnv 41195* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8957, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.) |
โข ๐น = (๐ฅ โ (2o โm ๐ด) โฆ (โก๐ฅ โ {1o})) โ โข (๐ด โ ๐ โ (๐น:(2o โm ๐ด)โ1-1-ontoโ๐ซ ๐ด โง โก๐น = (๐ฆ โ ๐ซ ๐ด โฆ (๐ง โ ๐ด โฆ if(๐ง โ ๐ฆ, 1o, โ ))))) | ||
Theorem | pw2f1o2 41196* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8957, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐น = (๐ฅ โ (2o โm ๐ด) โฆ (โก๐ฅ โ {1o})) โ โข (๐ด โ ๐ โ ๐น:(2o โm ๐ด)โ1-1-ontoโ๐ซ ๐ด) | ||
Theorem | pw2f1o2val 41197* | Function value of the pw2f1o2 41196 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
โข ๐น = (๐ฅ โ (2o โm ๐ด) โฆ (โก๐ฅ โ {1o})) โ โข (๐ โ (2o โm ๐ด) โ (๐นโ๐) = (โก๐ โ {1o})) | ||
Theorem | pw2f1o2val2 41198* | Membership in a mapped set under the pw2f1o2 41196 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
โข ๐น = (๐ฅ โ (2o โm ๐ด) โฆ (โก๐ฅ โ {1o})) โ โข ((๐ โ (2o โm ๐ด) โง ๐ โ ๐ด) โ (๐ โ (๐นโ๐) โ (๐โ๐) = 1o)) | ||
Theorem | soeq12d 41199 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ โ ๐ = ๐) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ Or ๐ด โ ๐ Or ๐ต)) | ||
Theorem | freq12d 41200 | Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ โ ๐ = ๐) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ Fr ๐ด โ ๐ Fr ๐ต)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |