Home | Intuitionistic Logic Explorer Theorem List (p. 103 of 106) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||
Theorem | evend2 10201 | An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo 8402 and zeo2 8403. (Contributed by AV, 22-Jun-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ)) | ||||||||||||||
Theorem | oddp1d2 10202 | An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo 8402 and zeo2 8403. (Contributed by AV, 22-Jun-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℤ)) | ||||||||||||||
Theorem | zob 10203 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) | ||||||||||||
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈ ℤ)) | ||||||||||||||
Theorem | oddm1d2 10204 | An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℤ)) | ||||||||||||||
Theorem | ltoddhalfle 10205 | An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) | ||||||||||||||
Theorem | halfleoddlt 10206 | An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) | ||||||||||||||
Theorem | opoe 10207 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) | ||||||||||||
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵)) | ||||||||||||||
Theorem | omoe 10208 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) | ||||||||||||
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 − 𝐵)) | ||||||||||||||
Theorem | opeo 10209 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) | ||||||||||||
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 + 𝐵)) | ||||||||||||||
Theorem | omeo 10210 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) | ||||||||||||
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 − 𝐵)) | ||||||||||||||
Theorem | m1expe 10211 | Exponentiation of -1 by an even power. Variant of m1expeven 9467. (Contributed by AV, 25-Jun-2021.) | ||||||||||||
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1) | ||||||||||||||
Theorem | m1expo 10212 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1) | ||||||||||||||
Theorem | m1exp1 10213 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁)) | ||||||||||||||
Theorem | nn0enne 10214 | A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.) | ||||||||||||
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ_{0} ↔ (𝑁 / 2) ∈ ℕ)) | ||||||||||||||
Theorem | nn0ehalf 10215 | The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℕ_{0} ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ_{0}) | ||||||||||||||
Theorem | nnehalf 10216 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) | ||||||||||||||
Theorem | nn0o1gt2 10217 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) | ||||||||||||
⊢ ((𝑁 ∈ ℕ_{0} ∧ ((𝑁 + 1) / 2) ∈ ℕ_{0}) → (𝑁 = 1 ∨ 2 < 𝑁)) | ||||||||||||||
Theorem | nno 10218 | An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) | ||||||||||||
⊢ ((𝑁 ∈ (ℤ_{≥}‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ_{0}) → ((𝑁 − 1) / 2) ∈ ℕ) | ||||||||||||||
Theorem | nn0o 10219 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.) | ||||||||||||
⊢ ((𝑁 ∈ ℕ_{0} ∧ ((𝑁 + 1) / 2) ∈ ℕ_{0}) → ((𝑁 − 1) / 2) ∈ ℕ_{0}) | ||||||||||||||
Theorem | nn0ob 10220 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) | ||||||||||||
⊢ (𝑁 ∈ ℕ_{0} → (((𝑁 + 1) / 2) ∈ ℕ_{0} ↔ ((𝑁 − 1) / 2) ∈ ℕ_{0})) | ||||||||||||||
Theorem | nn0oddm1d2 10221 | A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℕ_{0} → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℕ_{0})) | ||||||||||||||
Theorem | nnoddm1d2 10222 | A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℕ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℕ)) | ||||||||||||||
Theorem | z0even 10223 | 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) | ||||||||||||
⊢ 2 ∥ 0 | ||||||||||||||
Theorem | n2dvds1 10224 | 2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) | ||||||||||||
⊢ ¬ 2 ∥ 1 | ||||||||||||||
Theorem | n2dvdsm1 10225 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) | ||||||||||||
⊢ ¬ 2 ∥ -1 | ||||||||||||||
Theorem | z2even 10226 | 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) | ||||||||||||
⊢ 2 ∥ 2 | ||||||||||||||
Theorem | n2dvds3 10227 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) | ||||||||||||
⊢ ¬ 2 ∥ 3 | ||||||||||||||
Theorem | z4even 10228 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) | ||||||||||||
⊢ 2 ∥ 4 | ||||||||||||||
Theorem | 4dvdseven 10229 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) | ||||||||||||
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁) | ||||||||||||||
Theorem | divalglemnn 10230* | Lemma for divalg 10236. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||||||||||||||
Theorem | divalglemqt 10231 | Lemma for divalg 10236. The 𝑄 = 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.) | ||||||||||||
⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 𝑄 = 𝑇) & ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → 𝑅 = 𝑆) | ||||||||||||||
Theorem | divalglemnqt 10232 | Lemma for divalg 10236. The 𝑄 < 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.) | ||||||||||||
⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 0 ≤ 𝑆) & ⊢ (𝜑 → 𝑅 < 𝐷) & ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → ¬ 𝑄 < 𝑇) | ||||||||||||||
Theorem | divalglemeunn 10233* | Lemma for divalg 10236. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||||||||||||||
Theorem | divalglemex 10234* | Lemma for divalg 10236. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||||||||||||||
Theorem | divalglemeuneg 10235* | Lemma for divalg 10236. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||||||||||||||
Theorem | divalg 10236* | The division algorithm (theorem). Dividing an integer 𝑁 by a nonzero integer 𝐷 produces a (unique) quotient 𝑞 and a unique remainder 0 ≤ 𝑟 < (abs‘𝐷). Theorem 1.14 in [ApostolNT] p. 19. (Contributed by Paul Chapman, 21-Mar-2011.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||||||||||||||
Theorem | divalgb 10237* | Express the division algorithm as stated in divalg 10236 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ_{0} (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) | ||||||||||||||
Theorem | divalg2 10238* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ_{0} (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) | ||||||||||||||
Theorem | divalgmod 10239 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 10238 and divalgb 10237). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ_{0} ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))) | ||||||||||||||
Theorem | divalgmodcl 10240 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 10239. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ_{0}) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | ||||||||||||||
Theorem | modremain 10241* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ_{0} ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) | ||||||||||||||
Theorem | ndvdssub 10242 | Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 − 1, 𝑁 − 2... 𝑁 − (𝐷 − 1). (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾))) | ||||||||||||||
Theorem | ndvdsadd 10243 | Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 + 1, 𝑁 + 2... 𝑁 + (𝐷 − 1). (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 𝐾))) | ||||||||||||||
Theorem | ndvdsp1 10244 | Special case of ndvdsadd 10243. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) | ||||||||||||||
Theorem | ndvdsi 10245 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) | ||||||||||||
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈ ℕ_{0} & ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵 & ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 | ||||||||||||||
Theorem | flodddiv4 10246 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) | ||||||||||||
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2))) | ||||||||||||||
Theorem | fldivndvdslt 10247 | The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.) | ||||||||||||
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐿 ≠ 0) ∧ ¬ 𝐿 ∥ 𝐾) → (⌊‘(𝐾 / 𝐿)) < (𝐾 / 𝐿)) | ||||||||||||||
Theorem | flodddiv4lt 10248 | The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (⌊‘(𝑁 / 4)) < (𝑁 / 4)) | ||||||||||||||
Theorem | flodddiv4t2lthalf 10249 | The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → ((⌊‘(𝑁 / 4)) · 2) < (𝑁 / 2)) | ||||||||||||||
Theorem | sqr2irrlem 10250 | Lemma concerning rationality of square root of 2. The core of the proof - if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) | ||||||||||||
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → (√‘2) = (𝐴 / 𝐵)) ⇒ ⊢ (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ)) | ||||||||||||||
Theorem | sqrt2irr 10251 |
The square root of 2 is not rational. That is, for any rational number,
(√‘2) does not equal it. However,
if we were to say "the
square root of 2 is irrational" that would mean something stronger:
"for any rational number, (√‘2)
is apart from it" (the two
statements are equivalent given excluded middle). We do not prove
irrationality in this stronger sense here.
The proof's core is proven in sqr2irrlem 10250, which shows that if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) | ||||||||||||
⊢ (√‘2) ∉ ℚ | ||||||||||||||
Theorem | sqrt2re 10252 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) | ||||||||||||
⊢ (√‘2) ∈ ℝ | ||||||||||||||
Theorem | pw2dvdslemn 10253* | Lemma for pw2dvds 10254. If a natural number has some power of two which does not divide it, there is a highest power of two which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.) | ||||||||||||
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ ¬ (2↑𝐴) ∥ 𝑁) → ∃𝑚 ∈ ℕ_{0} ((2↑𝑚) ∥ 𝑁 ∧ ¬ (2↑(𝑚 + 1)) ∥ 𝑁)) | ||||||||||||||
Theorem | pw2dvds 10254* | A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℕ → ∃𝑚 ∈ ℕ_{0} ((2↑𝑚) ∥ 𝑁 ∧ ¬ (2↑(𝑚 + 1)) ∥ 𝑁)) | ||||||||||||||
Theorem | pw2dvdseulemle 10255 | Lemma for pw2dvdseu 10256. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) | ||||||||||||
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℕ_{0}) & ⊢ (𝜑 → 𝐵 ∈ ℕ_{0}) & ⊢ (𝜑 → (2↑𝐴) ∥ 𝑁) & ⊢ (𝜑 → ¬ (2↑(𝐵 + 1)) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||||||||||||||
Theorem | pw2dvdseu 10256* | A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) | ||||||||||||
⊢ (𝑁 ∈ ℕ → ∃!𝑚 ∈ ℕ_{0} ((2↑𝑚) ∥ 𝑁 ∧ ¬ (2↑(𝑚 + 1)) ∥ 𝑁)) | ||||||||||||||
Theorem | oddpwdclemxy 10257* | Lemma for oddpwdc 10262. Another way of stating that decomposing a natural number into a power of two and an odd number is unique. (Contributed by Jim Kingdon, 16-Nov-2021.) | ||||||||||||
⊢ ((((𝑋 ∈ ℕ ∧ ¬ 2 ∥ 𝑋) ∧ 𝑌 ∈ ℕ_{0}) ∧ 𝐴 = ((2↑𝑌) · 𝑋)) → (𝑋 = (𝐴 / (2↑(℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∧ 𝑌 = (℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) | ||||||||||||||
Theorem | oddpwdclemdvds 10258* | Lemma for oddpwdc 10262. A natural number is divisible by the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) | ||||||||||||
⊢ (𝐴 ∈ ℕ → (2↑(℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∥ 𝐴) | ||||||||||||||
Theorem | oddpwdclemndvds 10259* | Lemma for oddpwdc 10262. A natural number is not divisible by one more than the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) | ||||||||||||
⊢ (𝐴 ∈ ℕ → ¬ (2↑((℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) + 1)) ∥ 𝐴) | ||||||||||||||
Theorem | oddpwdclemodd 10260* | Lemma for oddpwdc 10262. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.) | ||||||||||||
⊢ (𝐴 ∈ ℕ → ¬ 2 ∥ (𝐴 / (2↑(℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))) | ||||||||||||||
Theorem | oddpwdclemdc 10261* | Lemma for oddpwdc 10262. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.) | ||||||||||||
⊢ ((((𝑋 ∈ ℕ ∧ ¬ 2 ∥ 𝑋) ∧ 𝑌 ∈ ℕ_{0}) ∧ 𝐴 = ((2↑𝑌) · 𝑋)) ↔ (𝐴 ∈ ℕ ∧ (𝑋 = (𝐴 / (2↑(℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∧ 𝑌 = (℩𝑧 ∈ ℕ_{0} ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))) | ||||||||||||||
Theorem | oddpwdc 10262* | The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) | ||||||||||||
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ_{0} ↦ ((2↑𝑦) · 𝑥)) ⇒ ⊢ 𝐹:(𝐽 × ℕ_{0})–1-1-onto→ℕ | ||||||||||||||
Theorem | nn0seqcvgd 10263* | A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ (𝜑 → 𝐹:ℕ_{0}⟶ℕ_{0}) & ⊢ (𝜑 → 𝑁 = (𝐹‘0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ_{0}) → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) = 0) | ||||||||||||||
Theorem | ialgrlem1st 10264 | Lemma for ialgr0 10266. Expressing algrflemg 5879 in a form suitable for theorems such as iseq1 9386 or iseqfn 9385. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
⊢ (𝜑 → 𝐹:𝑆⟶𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝐹 ∘ 1^{st} )𝑦) ∈ 𝑆) | ||||||||||||||
Theorem | ialgrlemconst 10265 | Lemma for ialgr0 10266. Closure of a constant function, in a form suitable for theorems such as iseq1 9386 or iseqfn 9385. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
⊢ 𝑍 = (ℤ_{≥}‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_{≥}‘𝑀)) → ((𝑍 × {𝐴})‘𝑥) ∈ 𝑆) | ||||||||||||||
Theorem | ialgr0 10266 | The value of the algorithm iterator 𝑅 at 0 is the initial state 𝐴. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) | ||||||||||||
⊢ 𝑍 = (ℤ_{≥}‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1^{st} ), (𝑍 × {𝐴}), 𝑆) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆⟶𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑅‘𝑀) = 𝐴) | ||||||||||||||
Theorem | ialgrf 10267 |
An algorithm is a step function 𝐹:𝑆⟶𝑆 on a state space 𝑆.
An algorithm acts on an initial state 𝐴 ∈ 𝑆 by iteratively applying
𝐹 to give 𝐴, (𝐹‘𝐴), (𝐹‘(𝐹‘𝐴)) and so
on. An algorithm is said to halt if a fixed point of 𝐹 is
reached
after a finite number of iterations.
The algorithm iterator 𝑅:ℕ_{0}⟶𝑆 "runs" the algorithm 𝐹 so that (𝑅‘𝑘) is the state after 𝑘 iterations of 𝐹 on the initial state 𝐴. Domain and codomain of the algorithm iterator 𝑅. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) | ||||||||||||
⊢ 𝑍 = (ℤ_{≥}‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1^{st} ), (𝑍 × {𝐴}), 𝑆) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆⟶𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑅:𝑍⟶𝑆) | ||||||||||||||
Theorem | ialgrp1 10268 | The value of the algorithm iterator 𝑅 at (𝐾 + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) | ||||||||||||
⊢ 𝑍 = (ℤ_{≥}‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1^{st} ), (𝑍 × {𝐴}), 𝑆) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆⟶𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝑅‘(𝐾 + 1)) = (𝐹‘(𝑅‘𝐾))) | ||||||||||||||
Theorem | ialginv 10269* | If 𝐼 is an invariant of 𝐹, its value is unchanged after any number of iterations of 𝐹. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ 𝑅 = seq0((𝐹 ∘ 1^{st} ), (ℕ_{0} × {𝐴}), 𝑆) & ⊢ 𝐹:𝑆⟶𝑆 & ⊢ 𝐼 Fn 𝑆 & ⊢ (𝑥 ∈ 𝑆 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥)) & ⊢ 𝑆 ∈ 𝑉 ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ_{0}) → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0))) | ||||||||||||||
Theorem | ialgcvg 10270* |
One way to prove that an algorithm halts is to construct a countdown
function 𝐶:𝑆⟶ℕ_{0} whose
value is guaranteed to decrease for
each iteration of 𝐹 until it reaches 0. That is, if 𝑋 ∈ 𝑆
is not a fixed point of 𝐹, then
(𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋).
If 𝐶 is a countdown function for algorithm 𝐹, the sequence (𝐶‘(𝑅‘𝑘)) reaches 0 after at most 𝑁 steps, where 𝑁 is the value of 𝐶 for the initial state 𝐴. (Contributed by Paul Chapman, 22-Jun-2011.) | ||||||||||||
⊢ 𝐹:𝑆⟶𝑆 & ⊢ 𝑅 = seq0((𝐹 ∘ 1^{st} ), (ℕ_{0} × {𝐴}), 𝑆) & ⊢ 𝐶:𝑆⟶ℕ_{0} & ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) & ⊢ 𝑁 = (𝐶‘𝐴) & ⊢ 𝑆 ∈ 𝑉 ⇒ ⊢ (𝐴 ∈ 𝑆 → (𝐶‘(𝑅‘𝑁)) = 0) | ||||||||||||||
Theorem | algcvgblem 10271 | Lemma for algcvgb 10272. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ ((𝑀 ∈ ℕ_{0} ∧ 𝑁 ∈ ℕ_{0}) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0)))) | ||||||||||||||
Theorem | algcvgb 10272 | Two ways of expressing that 𝐶 is a countdown function for algorithm 𝐹. The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
⊢ 𝐹:𝑆⟶𝑆 & ⊢ 𝐶:𝑆⟶ℕ_{0} ⇒ ⊢ (𝑋 ∈ 𝑆 → (((𝐶‘(𝐹‘𝑋)) ≠ 0 → (𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋)) ↔ (((𝐶‘𝑋) ≠ 0 → (𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋)) ∧ ((𝐶‘𝑋) = 0 → (𝐶‘(𝐹‘𝑋)) = 0)))) | ||||||||||||||
Theorem | ialgcvga 10273* | The countdown function 𝐶 remains 0 after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.) | ||||||||||||
⊢ 𝐹:𝑆⟶𝑆 & ⊢ 𝑅 = seq0((𝐹 ∘ 1^{st} ), (ℕ_{0} × {𝐴}), 𝑆) & ⊢ 𝐶:𝑆⟶ℕ_{0} & ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) & ⊢ 𝑁 = (𝐶‘𝐴) & ⊢ 𝑆 ∈ 𝑉 ⇒ ⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ_{≥}‘𝑁) → (𝐶‘(𝑅‘𝐾)) = 0)) | ||||||||||||||
Theorem | ialgfx 10274* | If 𝐹 reaches a fixed point when the countdown function 𝐶 reaches 0, 𝐹 remains fixed after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.) | ||||||||||||
⊢ 𝐹:𝑆⟶𝑆 & ⊢ 𝑅 = seq0((𝐹 ∘ 1^{st} ), (ℕ_{0} × {𝐴}), 𝑆) & ⊢ 𝐶:𝑆⟶ℕ_{0} & ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧))) & ⊢ 𝑁 = (𝐶‘𝐴) & ⊢ 𝑆 ∈ 𝑉 & ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧)) ⇒ ⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ_{≥}‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁))) | ||||||||||||||
This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:
| ||||||||||||||
Theorem | conventions 10275 |
Unless there is a reason to diverge, we follow the conventions of
the Metamath Proof Explorer (aka "set.mm"). This list of
conventions is intended to be read in conjunction with the
corresponding conventions in the Metamath Proof Explorer, and
only the differences are described below.
Label naming conventions Here are a few of the label naming conventions:
The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.
(Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||||||||||||||
Theorem | ex-or 10276 | Example for ax-io 640. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||
⊢ (2 = 3 ∨ 4 = 4) | ||||||||||||||
Theorem | ex-an 10277 | Example for ax-ia1 103. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||
⊢ (2 = 2 ∧ 3 = 3) | ||||||||||||||
Theorem | 1kp2ke3k 10278 |
Example for df-dec 8428, 1000 + 2000 = 3000.
This proof disproves (by counterexample) the assertion of Hao Wang, who stated, "There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula would be forbiddingly long... even if (one) knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result." (Hao Wang, "Theory and practice in mathematics" , In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.) This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision." The proof here starts with (2 + 1) = 3, commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 8428 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.) | ||||||||||||
⊢ (;;;1000 + ;;;2000) = ;;;3000 | ||||||||||||||
Theorem | ex-fl 10279 | Example for df-fl 9222. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||
⊢ ((⌊‘(3 / 2)) = 1 ∧ (⌊‘-(3 / 2)) = -2) | ||||||||||||||
Theorem | ex-ceil 10280 | Example for df-ceil 9223. (Contributed by AV, 4-Sep-2021.) | ||||||||||||
⊢ ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1) | ||||||||||||||
Theorem | ex-fac 10281 | Example for df-fac 9594. (Contributed by AV, 4-Sep-2021.) | ||||||||||||
⊢ (!‘5) = ;;120 | ||||||||||||||
Theorem | ex-bc 10282 | Example for df-bc 9616. (Contributed by AV, 4-Sep-2021.) | ||||||||||||
⊢ (5C3) = ;10 | ||||||||||||||
Theorem | ex-dvds 10283 | Example for df-dvds 10109: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||
⊢ 3 ∥ 6 | ||||||||||||||
Theorem | mathbox 10284 |
(This theorem is a dummy placeholder for these guidelines. The name of
this theorem, "mathbox", is hard-coded into the Metamath
program to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it. Guidelines: 1. If at all possible, please use only 0-ary class constants for new definitions. 2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm. 4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed. Notes: 1. We may decide to move some theorems to the main part of set.mm for general use. 2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on. 3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.) | ||||||||||||
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||||||||||||||
Theorem | ax1hfs 10285 | Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.) | ||||||||||||
⊢ (𝜑 → (𝜑 ∧ 𝜑)) | ||||||||||||||
Theorem | nnexmid 10286 | Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
⊢ ¬ ¬ (𝜑 ∨ ¬ 𝜑) | ||||||||||||||
Theorem | nndc 10287 | Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
⊢ ¬ ¬ DECID 𝜑 | ||||||||||||||
Theorem | dcdc 10288 | Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
⊢ (DECID DECID 𝜑 ↔ DECID 𝜑) | ||||||||||||||
Theorem | bj-ex 10289* | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1505 and 19.9ht 1548 or 19.23ht 1402). (Proof modification is discouraged.) | ||||||||||||
⊢ (∃𝑥𝜑 → 𝜑) | ||||||||||||||
Theorem | bj-hbalt 10290 | Closed form of hbal 1382 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||||||||||||||
Theorem | bj-nfalt 10291 | Closed form of nfal 1484 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑) | ||||||||||||||
Theorem | spimd 10292 | Deduction form of spim 1642. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||||||||||||||
Theorem | 2spim 10293* | Double substitution, as in spim 1642. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑧𝜒 & ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑧∀𝑥𝜓 → 𝜒) | ||||||||||||||
Theorem | ch2var 10294* | Implicit substitution of 𝑦 for 𝑥 and 𝑡 for 𝑧 into a theorem. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑧𝜓 & ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||||||||||||||
Theorem | ch2varv 10295* | Version of ch2var 10294 with non-freeness hypotheses replaced by DV conditions. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||||||||||||||
Theorem | bj-exlimmp 10296 | Lemma for bj-vtoclgf 10302. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜒 → 𝜓)) | ||||||||||||||
Theorem | bj-exlimmpi 10297 | Lemma for bj-vtoclgf 10302. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → 𝜑) & ⊢ (𝜒 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||||||||||||||
Theorem | bj-sbimedh 10298 | A strengthening of sbiedh 1686 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → 𝜒)) | ||||||||||||||
Theorem | bj-sbimeh 10299 | A strengthening of sbieh 1689 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓) | ||||||||||||||
Theorem | bj-sbime 10300 | A strengthening of sbie 1690 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |