![]() |
Metamath
Proof Explorer Theorem List (p. 421 of 480) | < 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: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | jm2.24nn 42001 | 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 42002 | 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 42003 | 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 42004 | 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 42005 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to โค. Could be eliminated with a more careful proof of jm2.26lem3 42043. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค) โ ((๐ด Yrm (๐ โ 1)) + (๐ด Yrm ๐)) < (๐ด Xrm ๐)) | ||
Theorem | rmygeid 42006 | 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 42007 | 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 42008 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ท โ โค โง ๐ธ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ท โ ๐ธ))) โ ๐ด โฅ ((๐ต + ๐ท) โ (๐ถ + ๐ธ))) | ||
Theorem | congmul 42009 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ท โ โค โง ๐ธ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ท โ ๐ธ))) โ ๐ด โฅ ((๐ต ยท ๐ท) โ (๐ถ ยท ๐ธ))) | ||
Theorem | congsym 42010 | Congruence mod ๐ด is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ด โฅ (๐ต โ ๐ถ))) โ ๐ด โฅ (๐ถ โ ๐ต)) | ||
Theorem | congneg 42011 | If two integers are congruent mod ๐ด, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ด โฅ (๐ต โ ๐ถ))) โ ๐ด โฅ (-๐ต โ -๐ถ)) | ||
Theorem | congsub 42012 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ท โ โค โง ๐ธ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โง ๐ด โฅ (๐ท โ ๐ธ))) โ ๐ด โฅ ((๐ต โ ๐ท) โ (๐ถ โ ๐ธ))) | ||
Theorem | congid 42013 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โฅ (๐ต โ ๐ต)) | ||
Theorem | mzpcong 42014* | Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.) |
โข ((๐น โ (mzPolyโ๐) โง (๐ โ (โค โm ๐) โง ๐ โ (โค โm ๐)) โง (๐ โ โค โง โ๐ โ ๐ ๐ โฅ ((๐โ๐) โ (๐โ๐)))) โ ๐ โฅ ((๐นโ๐) โ (๐นโ๐))) | ||
Theorem | congrep 42015* | Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข ((๐ด โ โ โง ๐ โ โค) โ โ๐ โ (0...(๐ด โ 1))๐ด โฅ (๐ โ ๐)) | ||
Theorem | congabseq 42016 | 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 42017 |
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 42018 | Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ))) โ (๐ด โฅ (๐ถ โ ๐ต) โจ ๐ด โฅ (๐ถ โ -๐ต))) | ||
Theorem | acongneg2 42019 | Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โง (๐ด โฅ (๐ต โ -๐ถ) โจ ๐ด โฅ (๐ต โ --๐ถ))) โ (๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ))) | ||
Theorem | acongtr 42020 | Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง ((๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ)) โง (๐ด โฅ (๐ถ โ ๐ท) โจ ๐ด โฅ (๐ถ โ -๐ท)))) โ (๐ด โฅ (๐ต โ ๐ท) โจ ๐ด โฅ (๐ต โ -๐ท))) | ||
Theorem | acongeq12d 42021 | Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
โข (๐ โ ๐ต = ๐ถ) & โข (๐ โ ๐ท = ๐ธ) โ โข (๐ โ ((๐ด โฅ (๐ต โ ๐ท) โจ ๐ด โฅ (๐ต โ -๐ท)) โ (๐ด โฅ (๐ถ โ ๐ธ) โจ ๐ด โฅ (๐ถ โ -๐ธ)))) | ||
Theorem | acongrep 42022* | 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 42023 | 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 42024 | Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โค) โ (๐ด โ (๐ต...๐ถ) โ -๐ด โ (-๐ถ...-๐ต))) | ||
Theorem | acongeq 42025 | Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 42044. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข ((๐ด โ โ โง ๐ต โ (0...๐ด) โง ๐ถ โ (0...๐ด)) โ (๐ต = ๐ถ โ ((2 ยท ๐ด) โฅ (๐ต โ ๐ถ) โจ (2 ยท ๐ด) โฅ (๐ต โ -๐ถ)))) | ||
Theorem | dvdsacongtr 42026 | Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง (๐ท โฅ ๐ด โง (๐ด โฅ (๐ต โ ๐ถ) โจ ๐ด โฅ (๐ต โ -๐ถ)))) โ (๐ท โฅ (๐ต โ ๐ถ) โจ ๐ท โฅ (๐ต โ -๐ถ))) | ||
Theorem | coprmdvdsb 42027 | Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐พ โ โค โง ๐ โ โค โง (๐ โ โค โง (๐พ gcd ๐) = 1)) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | modabsdifz 42028 | 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 42029 | 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 42030 | 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 42031 | Lemma for jm2.19 42035. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค) โ ((๐ด Xrm ๐) gcd (๐ด Yrm ๐)) = 1) | ||
Theorem | jm2.19lem2 42032 | Lemma for jm2.19 42035. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + ๐)))) | ||
Theorem | jm2.19lem3 42033 | Lemma for jm2.19 42035. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) | ||
Theorem | jm2.19lem4 42034 | Lemma for jm2.19 42035. Extend to ZZ by symmetry. TODO: use zindbi 41988. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) | ||
Theorem | jm2.19 42035 | 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 42036 | Lemma for jm2.20nn 42039. 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 42037* | Lemma for jm2.20nn 42039. 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 42038 | Lemma for jm2.20nn 42039. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โค โง ๐ฝ โ โ) โ ((๐ด Yrm ๐)โ3) โฅ ((๐ด Yrm (๐ ยท ๐ฝ)) โ (๐ฝ ยท (((๐ด Xrm ๐)โ(๐ฝ โ 1)) ยท (๐ด Yrm ๐))))) | ||
Theorem | jm2.20nn 42039 | 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 42040 | Lemma for jm2.26 42044. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โค โง ๐ท โ โค) โง (๐ด โฅ (๐ถ โ ๐ท) โจ ๐ด โฅ (๐ถ โ -๐ท))) โ ((๐ด โฅ (๐ท โ ๐ต) โจ ๐ด โฅ (๐ท โ -๐ต)) โ (๐ด โฅ (๐ถ โ ๐ต) โจ ๐ด โฅ (๐ถ โ -๐ต)))) | ||
Theorem | jm2.25 42041 | Lemma for jm2.26 42044. 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 42042 | Lemma for jm2.26 42044. 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 42043 | Lemma for jm2.26 42044. Use acongrep 42022 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 42044 | 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 42045 | 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 42046 | Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 42045 if Yrm is redefined as described in rmyluc 41979. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ โ โ0) โ (๐ด โ 1) โฅ ((๐ด Yrm ๐) โ ๐)) | ||
Theorem | jm2.27a 42047 | Lemma for jm2.27 42050. 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 42048 | Lemma for jm2.27 42050. 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 42049 | Lemma for jm2.27 42050. 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 42050* | 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 42047 and jm2.27c 42049. 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 42051* | Lemma for rmydioph 42056. 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 42052 | Lemma for rmydioph 42056. 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 42053 | Lemma for rmydioph 42056. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ด โ โ โ โข ๐ด โ (1...๐ด) | ||
Theorem | jm2.27dlem4 42054 | Lemma for rmydioph 42056. Infer โ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ด โ โ & โข ๐ต = (๐ด + 1) โ โข ๐ต โ โ | ||
Theorem | jm2.27dlem5 42055 | Lemma for rmydioph 42056. Used with sselii 3979 to infer membership of midpoints of range; jm2.27dlem2 42052 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
โข ๐ต = (๐ด + 1) & โข (1...๐ต) โ (1...๐ถ) โ โข (1...๐ด) โ (1...๐ถ) | ||
Theorem | rmydioph 42056 | jm2.27 42050 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 42057* | 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 42058 | 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 42059 | Lemma for jm3.1 42062. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐พ โ (โคโฅโ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) โ โข (๐ โ (๐พโ๐) < ๐ด) | ||
Theorem | jm3.1lem2 42060 | Lemma for jm3.1 42062. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐พ โ (โคโฅโ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) โ โข (๐ โ (๐พโ๐) < ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1)) | ||
Theorem | jm3.1lem3 42061 | Lemma for jm3.1 42062. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
โข (๐ โ ๐ด โ (โคโฅโ2)) & โข (๐ โ ๐พ โ (โคโฅโ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) โ โข (๐ โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) โ โ) | ||
Theorem | jm3.1 42062 | 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 42063* | Lemma for expdioph 42065. 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 42064 | Lemma for expdioph 42065. 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 42065 | 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 42066* | 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 9733; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (โ๐ฅ(๐ฅ โ ๐ด โ ๐ฅ โ ๐ด) โ (โ๐ฆ(Tr ๐ฆ โง ๐ต โ ๐ฆ) โ ๐ต โ ๐ด)) | ||
Theorem | setindtrs 42067* | Set induction scheme without Infinity. See comments at setindtr 42066. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (โ๐ฆ โ ๐ฅ ๐ โ ๐) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = ๐ต โ (๐ โ ๐)) โ โข (โ๐ง(Tr ๐ง โง ๐ต โ ๐ง) โ ๐) | ||
Theorem | dford3lem1 42068* | Lemma for dford3 42070. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข ((Tr ๐ โง โ๐ฆ โ ๐ Tr ๐ฆ) โ โ๐ โ ๐ (Tr ๐ โง โ๐ฆ โ ๐ Tr ๐ฆ)) | ||
Theorem | dford3lem2 42069* | Lemma for dford3 42070. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข ((Tr ๐ฅ โง โ๐ฆ โ ๐ฅ Tr ๐ฆ) โ ๐ฅ โ On) | ||
Theorem | dford3 42070* | Ordinals are precisely the hereditarily transitive classes. Definition 1.2 of [Schloeder] p. 1. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (Ord ๐ โ (Tr ๐ โง โ๐ฅ โ ๐ Tr ๐ฅ)) | ||
Theorem | dford4 42071* | dford3 42070 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (Ord ๐ โ โ๐โ๐โ๐((๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐ โง (๐ โ ๐ โ ๐ โ ๐)))) | ||
Theorem | wopprc 42072 | Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
โข ((๐ด โ V โง ๐ต โ V) โ ยฌ 1o โ {{{๐ด}, โ }, {{๐ต}}}) | ||
Theorem | rpnnen3lem 42073* | Lemma for rpnnen3 42074. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข (((๐ โ โ โง ๐ โ โ) โง ๐ < ๐) โ {๐ โ โ โฃ ๐ < ๐} โ {๐ โ โ โฃ ๐ < ๐}) | ||
Theorem | rpnnen3 42074 | Dedekind cut injection of โ into ๐ซ โ. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข โ โผ ๐ซ โ | ||
Theorem | axac10 42075 | Characterization of choice similar to dffin1-5 10387. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
โข ( โ โ On) = V | ||
Theorem | harinf 42076 | The Hartogs number of an infinite set is at least ฯ. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
โข ((๐ โ ๐ โง ยฌ ๐ โ Fin) โ ฯ โ (harโ๐)) | ||
Theorem | wdom2d2 42077* | Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข ((๐ โง ๐ฅ โ ๐ด) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ฅ = ๐) โ โข (๐ โ ๐ด โผ* (๐ต ร ๐ถ)) | ||
Theorem | ttac 42078 | Tarski's theorem about choice: infxpidm 10561 is equivalent to ax-ac 10458. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.) |
โข (CHOICE โ โ๐(ฯ โผ ๐ โ (๐ ร ๐) โ ๐)) | ||
Theorem | pw2f1ocnv 42079* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 9083, 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 42080* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 9083, 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 42081* | Function value of the pw2f1o2 42080 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 42082* | Membership in a mapped set under the pw2f1o2 42080 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 42083 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ โ ๐ = ๐) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ Or ๐ด โ ๐ Or ๐ต)) | ||
Theorem | freq12d 42084 | Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ โ ๐ = ๐) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ Fr ๐ด โ ๐ Fr ๐ต)) | ||
Theorem | weeq12d 42085 | Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ โ ๐ = ๐) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ We ๐ด โ ๐ We ๐ต)) | ||
Theorem | limsuc2 42086 | Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
โข ((Ord ๐ด โง ๐ด = โช ๐ด) โ (๐ต โ ๐ด โ suc ๐ต โ ๐ด)) | ||
Theorem | wepwsolem 42087* | Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ด ((๐ง โ ๐ฆ โง ยฌ ๐ง โ ๐ฅ) โง โ๐ค โ ๐ด (๐ค๐ ๐ง โ (๐ค โ ๐ฅ โ ๐ค โ ๐ฆ)))} & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ด ((๐ฅโ๐ง) E (๐ฆโ๐ง) โง โ๐ค โ ๐ด (๐ค๐ ๐ง โ (๐ฅโ๐ค) = (๐ฆโ๐ค)))} & โข ๐น = (๐ โ (2o โm ๐ด) โฆ (โก๐ โ {1o})) โ โข (๐ด โ V โ ๐น Isom ๐, ๐ ((2o โm ๐ด), ๐ซ ๐ด)) | ||
Theorem | wepwso 42088* | A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove ๐ด โ ๐. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ โ๐ง โ ๐ด ((๐ง โ ๐ฆ โง ยฌ ๐ง โ ๐ฅ) โง โ๐ค โ ๐ด (๐ค๐ ๐ง โ (๐ค โ ๐ฅ โ ๐ค โ ๐ฆ)))} โ โข ((๐ด โ ๐ โง ๐ We ๐ด) โ ๐ Or ๐ซ ๐ด) | ||
Theorem | dnnumch1 42089* | Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 10029. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐น = recs((๐ง โ V โฆ (๐บโ(๐ด โ ran ๐ง)))) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ โ๐ฆ โ ๐ซ ๐ด(๐ฆ โ โ โ (๐บโ๐ฆ) โ ๐ฆ)) โ โข (๐ โ โ๐ฅ โ On (๐น โพ ๐ฅ):๐ฅโ1-1-ontoโ๐ด) | ||
Theorem | dnnumch2 42090* | Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐น = recs((๐ง โ V โฆ (๐บโ(๐ด โ ran ๐ง)))) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ โ๐ฆ โ ๐ซ ๐ด(๐ฆ โ โ โ (๐บโ๐ฆ) โ ๐ฆ)) โ โข (๐ โ ๐ด โ ran ๐น) | ||
Theorem | dnnumch3lem 42091* | Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐น = recs((๐ง โ V โฆ (๐บโ(๐ด โ ran ๐ง)))) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ โ๐ฆ โ ๐ซ ๐ด(๐ฆ โ โ โ (๐บโ๐ฆ) โ ๐ฆ)) โ โข ((๐ โง ๐ค โ ๐ด) โ ((๐ฅ โ ๐ด โฆ โฉ (โก๐น โ {๐ฅ}))โ๐ค) = โฉ (โก๐น โ {๐ค})) | ||
Theorem | dnnumch3 42092* | Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐น = recs((๐ง โ V โฆ (๐บโ(๐ด โ ran ๐ง)))) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ โ๐ฆ โ ๐ซ ๐ด(๐ฆ โ โ โ (๐บโ๐ฆ) โ ๐ฆ)) โ โข (๐ โ (๐ฅ โ ๐ด โฆ โฉ (โก๐น โ {๐ฅ})):๐ดโ1-1โOn) | ||
Theorem | dnwech 42093* | Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐น = recs((๐ง โ V โฆ (๐บโ(๐ด โ ran ๐ง)))) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ โ๐ฆ โ ๐ซ ๐ด(๐ฆ โ โ โ (๐บโ๐ฆ) โ ๐ฆ)) & โข ๐ป = {โจ๐ฃ, ๐คโฉ โฃ โฉ (โก๐น โ {๐ฃ}) โ โฉ (โก๐น โ {๐ค})} โ โข (๐ โ ๐ป We ๐ด) | ||
Theorem | fnwe2val 42094* | Lemma for fnwe2 42098. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ง = (๐นโ๐ฅ) โ ๐ = ๐) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐นโ๐ฅ)๐ (๐นโ๐ฆ) โจ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โง ๐ฅ๐๐ฆ))} โ โข (๐๐๐ โ ((๐นโ๐)๐ (๐นโ๐) โจ ((๐นโ๐) = (๐นโ๐) โง ๐โฆ(๐นโ๐) / ๐งโฆ๐๐))) | ||
Theorem | fnwe2lem1 42095* | Lemma for fnwe2 42098. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ง = (๐นโ๐ฅ) โ ๐ = ๐) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐นโ๐ฅ)๐ (๐นโ๐ฆ) โจ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โง ๐ฅ๐๐ฆ))} & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ We {๐ฆ โ ๐ด โฃ (๐นโ๐ฆ) = (๐นโ๐ฅ)}) โ โข ((๐ โง ๐ โ ๐ด) โ โฆ(๐นโ๐) / ๐งโฆ๐ We {๐ฆ โ ๐ด โฃ (๐นโ๐ฆ) = (๐นโ๐)}) | ||
Theorem | fnwe2lem2 42096* | Lemma for fnwe2 42098. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus ๐ is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ง = (๐นโ๐ฅ) โ ๐ = ๐) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐นโ๐ฅ)๐ (๐นโ๐ฆ) โจ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โง ๐ฅ๐๐ฆ))} & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ We {๐ฆ โ ๐ด โฃ (๐นโ๐ฆ) = (๐นโ๐ฅ)}) & โข (๐ โ (๐น โพ ๐ด):๐ดโถ๐ต) & โข (๐ โ ๐ We ๐ต) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐ โ โ ) โ โข (๐ โ โ๐ โ ๐ โ๐ โ ๐ ยฌ ๐๐๐) | ||
Theorem | fnwe2lem3 42097* | Lemma for fnwe2 42098. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ง = (๐นโ๐ฅ) โ ๐ = ๐) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐นโ๐ฅ)๐ (๐นโ๐ฆ) โจ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โง ๐ฅ๐๐ฆ))} & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ We {๐ฆ โ ๐ด โฃ (๐นโ๐ฆ) = (๐นโ๐ฅ)}) & โข (๐ โ (๐น โพ ๐ด):๐ดโถ๐ต) & โข (๐ โ ๐ We ๐ต) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐ โ ๐ด) โ โข (๐ โ (๐๐๐ โจ ๐ = ๐ โจ ๐๐๐)) | ||
Theorem | fnwe2 42098* | A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 8122 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
โข (๐ง = (๐นโ๐ฅ) โ ๐ = ๐) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐นโ๐ฅ)๐ (๐นโ๐ฆ) โจ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โง ๐ฅ๐๐ฆ))} & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ We {๐ฆ โ ๐ด โฃ (๐นโ๐ฆ) = (๐นโ๐ฅ)}) & โข (๐ โ (๐น โพ ๐ด):๐ดโถ๐ต) & โข (๐ โ ๐ We ๐ต) โ โข (๐ โ ๐ We ๐ด) | ||
Theorem | aomclem1 42099* |
Lemma for dfac11 42107. This is the beginning of the proof that
multiple
choice is equivalent to choice. Our goal is to construct, by
transfinite recursion, a well-ordering of (๐
1โ๐ด). In what
follows, ๐ด is the index of the rank we wish to
well-order, ๐ง is
the collection of well-orderings constructed so far, dom ๐ง is
the
set of ordinal indices of constructed ranks i.e. the next rank to
construct, and ๐ฆ is a postulated multiple-choice
function.
Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐ต = {โจ๐, ๐โฉ โฃ โ๐ โ (๐ 1โโช dom ๐ง)((๐ โ ๐ โง ยฌ ๐ โ ๐) โง โ๐ โ (๐ 1โโช dom ๐ง)(๐(๐งโโช dom ๐ง)๐ โ (๐ โ ๐ โ ๐ โ ๐)))} & โข (๐ โ dom ๐ง โ On) & โข (๐ โ dom ๐ง = suc โช dom ๐ง) & โข (๐ โ โ๐ โ dom ๐ง(๐งโ๐) We (๐ 1โ๐)) โ โข (๐ โ ๐ต Or (๐ 1โdom ๐ง)) | ||
Theorem | aomclem2 42100* | Lemma for dfac11 42107. Successor case 2, a choice function for subsets of (๐ 1โdom ๐ง). (Contributed by Stefan O'Rear, 18-Jan-2015.) |
โข ๐ต = {โจ๐, ๐โฉ โฃ โ๐ โ (๐ 1โโช dom ๐ง)((๐ โ ๐ โง ยฌ ๐ โ ๐) โง โ๐ โ (๐ 1โโช dom ๐ง)(๐(๐งโโช dom ๐ง)๐ โ (๐ โ ๐ โ ๐ โ ๐)))} & โข ๐ถ = (๐ โ V โฆ sup((๐ฆโ๐), (๐ 1โdom ๐ง), ๐ต)) & โข (๐ โ dom ๐ง โ On) & โข (๐ โ dom ๐ง = suc โช dom ๐ง) & โข (๐ โ โ๐ โ dom ๐ง(๐งโ๐) We (๐ 1โ๐)) & โข (๐ โ ๐ด โ On) & โข (๐ โ dom ๐ง โ ๐ด) & โข (๐ โ โ๐ โ ๐ซ (๐ 1โ๐ด)(๐ โ โ โ (๐ฆโ๐) โ ((๐ซ ๐ โฉ Fin) โ {โ }))) โ โข (๐ โ โ๐ โ ๐ซ (๐ 1โdom ๐ง)(๐ โ โ โ (๐ถโ๐) โ ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |