![]() |
Metamath
Proof Explorer Theorem List (p. 130 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfzlmr 12901 | A member of a finite interval of integers is either its lower bound or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁) ∨ 𝐾 = 𝑁)) | ||
Theorem | elfz0lmr 12902 | A member of a finite interval of nonnegative integers is either 0 or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 = 0 ∨ 𝐾 ∈ (1..^𝑁) ∨ 𝐾 = 𝑁)) | ||
Theorem | fzostep1 12903 | Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → ((𝐴 + 1) ∈ (𝐵..^𝐶) ∨ (𝐴 + 1) = 𝐶)) | ||
Theorem | fzoshftral 12904* | Shift the scanning order inside of a quantification over a half-open integer range, analogous to fzshftral 12746. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀..^𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)..^(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) | ||
Theorem | fzind2 12905* | Induction on the integers from 𝑀 to 𝑁 inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Version of fzind 11827 using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.) |
⊢ (𝑥 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏)) & ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜓) & ⊢ (𝑦 ∈ (𝑀..^𝑁) → (𝜒 → 𝜃)) ⇒ ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝜏) | ||
Theorem | fvinim0ffz 12906 | The function values for the borders of a finite interval of integers, which is the domain of the function, are not in the image of the interior of the interval iff the intersection of the images of the interior and the borders is empty. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.) |
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) | ||
Theorem | injresinjlem 12907 | Lemma for injresinj 12908. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Proof shortened by AV, 14-Feb-2021.) (Revised by Thierry Arnoux, 23-Dec-2021.) |
⊢ (¬ 𝑌 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹‘𝐾) → ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑋 ∈ (0...𝐾) ∧ 𝑌 ∈ (0...𝐾)) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌)))))) | ||
Theorem | injresinj 12908 | A function whose restriction is injective and the values of the remaining arguments are different from all other values is injective itself. (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
⊢ (𝐾 ∈ ℕ0 → ((𝐹:(0...𝐾)⟶𝑉 ∧ Fun ◡(𝐹 ↾ (1..^𝐾)) ∧ (𝐹‘0) ≠ (𝐹‘𝐾)) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → Fun ◡𝐹))) | ||
Theorem | subfzo0 12909 | The difference between two elements in a half-open range of nonnegative integers is greater than the negation of the upper bound and less than the upper bound of the range. (Contributed by AV, 20-Mar-2021.) |
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁)) | ||
Syntax | cfl 12910 | Extend class notation with floor (greatest integer) function. |
class ⌊ | ||
Syntax | cceil 12911 | Extend class notation to include the ceiling function. |
class ⌈ | ||
Definition | df-fl 12912* |
Define the floor (greatest integer less than or equal to) function. See
flval 12914 for its value, fllelt 12917 for its basic property, and flcl 12915
for
its closure. For example, (⌊‘(3 / 2)) =
1 while
(⌊‘-(3 / 2)) = -2 (ex-fl 27879).
The term "floor" was coined by Ken Iverson. He also invented a mathematical notation for floor, consisting of an L-shaped left bracket and its reflection as a right bracket. In APL, the left-bracket alone is used, and we borrow this idea. (Thanks to Paul Chapman for this information.) (Contributed by NM, 14-Nov-2004.) |
⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)))) | ||
Definition | df-ceil 12913 |
The ceiling (least integer greater than or equal to) function. Defined in
ISO 80000-2:2009(E) operation 2-9.18 and the "NIST Digital Library of
Mathematical Functions" , front introduction, "Common Notations
and
Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4.
See ceilval 12958 for its value, ceilge 12964 and ceilm1lt 12966 for its basic
properties, and ceilcl 12962 for its closure. For example,
(⌈‘(3 / 2)) = 2 while (⌈‘-(3 / 2)) = -1
(ex-ceil 27880).
The symbol ⌈ is inspired by the gamma shaped left bracket of the usual notation. (Contributed by David A. Wheeler, 19-May-2015.) |
⊢ ⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥)) | ||
Theorem | flval 12914* | Value of the floor (greatest integer) function. The floor of 𝐴 is the (unique) integer less than or equal to 𝐴 whose successor is strictly greater than 𝐴. (Contributed by NM, 14-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) | ||
Theorem | flcl 12915 | The floor (greatest integer) function is an integer (closure law). (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ) | ||
Theorem | reflcl 12916 | The floor (greatest integer) function is real. (Contributed by NM, 15-Jul-2008.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ) | ||
Theorem | fllelt 12917 | A basic property of the floor (greatest integer) function. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.) |
⊢ (𝐴 ∈ ℝ → ((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1))) | ||
Theorem | flcld 12918 | The floor (greatest integer) function is an integer (closure law). (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (⌊‘𝐴) ∈ ℤ) | ||
Theorem | flle 12919 | A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ 𝐴) | ||
Theorem | flltp1 12920 | A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < ((⌊‘𝐴) + 1)) | ||
Theorem | fllep1 12921 | A basic property of the floor (greatest integer) function. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) | ||
Theorem | fraclt1 12922 | The fractional part of a real number is less than one. (Contributed by NM, 15-Jul-2008.) |
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) < 1) | ||
Theorem | fracle1 12923 | The fractional part of a real number is less than or equal to one. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) ≤ 1) | ||
Theorem | fracge0 12924 | The fractional part of a real number is nonnegative. (Contributed by NM, 17-Jul-2008.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 − (⌊‘𝐴))) | ||
Theorem | flge 12925 | The floor function value is the greatest integer less than or equal to its argument. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Fan Zheng, 14-Jul-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ (⌊‘𝐴))) | ||
Theorem | fllt 12926 | The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (⌊‘𝐴) < 𝐵)) | ||
Theorem | flflp1 12927 | Move floor function between strict and non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) ≤ 𝐵 ↔ 𝐴 < ((⌊‘𝐵) + 1))) | ||
Theorem | flid 12928 | An integer is its own floor. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝐴 ∈ ℤ → (⌊‘𝐴) = 𝐴) | ||
Theorem | flidm 12929 | The floor function is idempotent. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ ℝ → (⌊‘(⌊‘𝐴)) = (⌊‘𝐴)) | ||
Theorem | flidz 12930 | A real number equals its floor iff it is an integer. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ → ((⌊‘𝐴) = 𝐴 ↔ 𝐴 ∈ ℤ)) | ||
Theorem | flltnz 12931 | If A is not an integer, then the floor of A is less than A. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ) → (⌊‘𝐴) < 𝐴) | ||
Theorem | flwordi 12932 | Ordering relationship for the greatest integer function. (Contributed by NM, 31-Dec-2005.) (Proof shortened by Fan Zheng, 14-Jul-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ (⌊‘𝐵)) | ||
Theorem | flword2 12933 | Ordering relationship for the greatest integer function. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐵) ∈ (ℤ≥‘(⌊‘𝐴))) | ||
Theorem | flval2 12934* | An alternate way to define the floor (greatest integer) function. (Contributed by NM, 16-Nov-2004.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) | ||
Theorem | flval3 12935* | An alternate way to define the floor (greatest integer) function, as the supremum of all integers less than or equal to its argument. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = sup({𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴}, ℝ, < )) | ||
Theorem | flbi 12936 | A condition equivalent to floor. (Contributed by NM, 11-Mar-2005.) (Revised by Mario Carneiro, 2-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → ((⌊‘𝐴) = 𝐵 ↔ (𝐵 ≤ 𝐴 ∧ 𝐴 < (𝐵 + 1)))) | ||
Theorem | flbi2 12937 | A condition equivalent to floor. (Contributed by NM, 15-Aug-2008.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐹 ∈ ℝ) → ((⌊‘(𝑁 + 𝐹)) = 𝑁 ↔ (0 ≤ 𝐹 ∧ 𝐹 < 1))) | ||
Theorem | adddivflid 12938 | The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ) → (𝐵 < 𝐶 ↔ (⌊‘(𝐴 + (𝐵 / 𝐶))) = 𝐴)) | ||
Theorem | ico01fl0 12939 | The floor of a real number in [0, 1) is 0. Remark: may shorten the proof of modid 13014 or a version of it where the antecedent is membership in an interval. (Contributed by BJ, 29-Jun-2019.) |
⊢ (𝐴 ∈ (0[,)1) → (⌊‘𝐴) = 0) | ||
Theorem | flge0nn0 12940 | The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0) | ||
Theorem | flge1nn 12941 | The floor of a number greater than or equal to 1 is a positive integer. (Contributed by NM, 26-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ) | ||
Theorem | fldivnn0 12942 | The floor function of a division of a nonnegative integer by a positive integer is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (⌊‘(𝐾 / 𝐿)) ∈ ℕ0) | ||
Theorem | refldivcl 12943 | The floor function of a division of a real number by a positive real number is a real number. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ+) → (⌊‘(𝐾 / 𝐿)) ∈ ℝ) | ||
Theorem | divfl0 12944 | The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (⌊‘(𝐴 / 𝐵)) = 0)) | ||
Theorem | fladdz 12945 | An integer can be moved in and out of the floor of a sum. (Contributed by NM, 27-Apr-2005.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 + 𝑁)) = ((⌊‘𝐴) + 𝑁)) | ||
Theorem | flzadd 12946 | An integer can be moved in and out of the floor of a sum. (Contributed by NM, 2-Jan-2009.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (⌊‘(𝑁 + 𝐴)) = (𝑁 + (⌊‘𝐴))) | ||
Theorem | flmulnn0 12947 | Move a nonnegative integer in and out of a floor. (Contributed by NM, 2-Jan-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) | ||
Theorem | btwnzge0 12948 | A real bounded between an integer and its successor is nonnegative iff the integer is nonnegative. Second half of Lemma 13-4.1 of [Gleason] p. 217. (For the first half see rebtwnz 12094.) (Contributed by NM, 12-Mar-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ≤ 𝐴 ∧ 𝐴 < (𝑁 + 1))) → (0 ≤ 𝐴 ↔ 0 ≤ 𝑁)) | ||
Theorem | 2tnp1ge0ge0 12949 | Two times an integer plus one is not negative iff the integer is not negative. (Contributed by AV, 19-Jun-2021.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ (𝑁 ∈ ℤ → (0 ≤ ((2 · 𝑁) + 1) ↔ 0 ≤ 𝑁)) | ||
Theorem | flhalf 12950 | Ordering relation for the floor of half of an integer. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (2 · (⌊‘((𝑁 + 1) / 2)))) | ||
Theorem | fldivle 12951 | The floor function of a division of a real number by a positive real number is less than or equal to the division. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ+) → (⌊‘(𝐾 / 𝐿)) ≤ (𝐾 / 𝐿)) | ||
Theorem | fldivnn0le 12952 | The floor function of a division of a nonnegative integer by a positive integer is less than or equal to the division. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (⌊‘(𝐾 / 𝐿)) ≤ (𝐾 / 𝐿)) | ||
Theorem | flltdivnn0lt 12953 | The floor function of a division of a nonnegative integer by a positive integer is less than the division of a greater dividend by the same positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (𝐾 < 𝑁 → (⌊‘(𝐾 / 𝐿)) < (𝑁 / 𝐿))) | ||
Theorem | ltdifltdiv 12954 | If the dividend of a division is less than the difference between a real number and the divisor, the floor function of the division plus 1 is less than the division of the real number by the divisor. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐶 − 𝐵) → ((⌊‘(𝐴 / 𝐵)) + 1) < (𝐶 / 𝐵))) | ||
Theorem | fldiv4p1lem1div2 12955 | The floor of an integer equal to 3 or greater than 4, increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) |
⊢ ((𝑁 = 3 ∨ 𝑁 ∈ (ℤ≥‘5)) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) / 2)) | ||
Theorem | fldiv4lem1div2uz2 12956 | The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2)) | ||
Theorem | fldiv4lem1div2 12957 | The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021.) |
⊢ (𝑁 ∈ ℕ → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2)) | ||
Theorem | ceilval 12958 | The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) |
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) = -(⌊‘-𝐴)) | ||
Theorem | dfceil2 12959* | Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.) |
⊢ ⌈ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑥 ≤ 𝑦 ∧ 𝑦 < (𝑥 + 1)))) | ||
Theorem | ceilval2 12960* | The value of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.) |
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) = (℩𝑦 ∈ ℤ (𝐴 ≤ 𝑦 ∧ 𝑦 < (𝐴 + 1)))) | ||
Theorem | ceicl 12961 | The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ (𝐴 ∈ ℝ → -(⌊‘-𝐴) ∈ ℤ) | ||
Theorem | ceilcl 12962 | Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) |
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) ∈ ℤ) | ||
Theorem | ceige 12963 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ -(⌊‘-𝐴)) | ||
Theorem | ceilge 12964 | The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (⌈‘𝐴)) | ||
Theorem | ceim1l 12965 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ (𝐴 ∈ ℝ → (-(⌊‘-𝐴) − 1) < 𝐴) | ||
Theorem | ceilm1lt 12966 | One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → ((⌈‘𝐴) − 1) < 𝐴) | ||
Theorem | ceile 12967 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → -(⌊‘-𝐴) ≤ 𝐵) | ||
Theorem | ceille 12968 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → (⌈‘𝐴) ≤ 𝐵) | ||
Theorem | ceilid 12969 | An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℤ → (⌈‘𝐴) = 𝐴) | ||
Theorem | ceilidz 12970 | A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴)) | ||
Theorem | flleceil 12971 | The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ (⌈‘𝐴)) | ||
Theorem | fleqceilz 12972 | A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴))) | ||
Theorem | quoremz 12973 | Quotient and remainder of an integer divided by a positive integer. TODO - is this really needed for anything? Should we use mod to simplify it? Remark (AV): This is a special case of divalg 15533. (Contributed by NM, 14-Aug-2008.) |
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) & ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) | ||
Theorem | quoremnn0 12974 | Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.) |
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) & ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) ⇒ ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) | ||
Theorem | quoremnn0ALT 12975 | Alternate proof of quoremnn0 12974 not using quoremz 12973. TODO - Keep either quoremnn0ALT 12975 (if we don't keep quoremz 12973) or quoremnn0 12974? (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) & ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) ⇒ ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) | ||
Theorem | intfrac2 12976 | Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 13004? (Contributed by NM, 16-Aug-2008.) |
⊢ 𝑍 = (⌊‘𝐴) & ⊢ 𝐹 = (𝐴 − 𝑍) ⇒ ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹))) | ||
Theorem | intfracq 12977 | Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 12976. (Contributed by NM, 16-Aug-2008.) |
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁)) & ⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) | ||
Theorem | fldiv 12978 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁))) | ||
Theorem | fldiv2 12979 | Cancellation of an embedded floor of a ratio. Generalization of Equation 2.4 in [CormenLeisersonRivest] p. 33 (where 𝐴 must be an integer). (Contributed by NM, 9-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘(𝐴 / 𝑀)) / 𝑁)) = (⌊‘(𝐴 / (𝑀 · 𝑁)))) | ||
Theorem | fznnfl 12980 | Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ (𝑁 ∈ ℝ → (𝐾 ∈ (1...(⌊‘𝑁)) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | uzsup 12981 | An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞) | ||
Theorem | ioopnfsup 12982 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴(,)+∞), ℝ*, < ) = +∞) | ||
Theorem | icopnfsup 12983 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴[,)+∞), ℝ*, < ) = +∞) | ||
Theorem | rpsup 12984 | The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ sup(ℝ+, ℝ*, < ) = +∞ | ||
Theorem | resup 12985 | The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ sup(ℝ, ℝ*, < ) = +∞ | ||
Theorem | xrsup 12986 | The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ sup(ℝ*, ℝ*, < ) = +∞ | ||
Syntax | cmo 12987 | Extend class notation with the modulo operation. |
class mod | ||
Definition | df-mod 12988* | Define the modulo (remainder) operation. See modval 12989 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 27881). (Contributed by NM, 10-Nov-2008.) |
⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) | ||
Theorem | modval 12989 | The value of the modulo operation. The modulo congruence notation of number theory, 𝐽≡𝐾 (modulo 𝑁), can be expressed in our notation as (𝐽 mod 𝑁) = (𝐾 mod 𝑁). Definition 1 in Knuth, The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive reals to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) (Contributed by NM, 10-Nov-2008.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | ||
Theorem | modvalr 12990 | The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵))) | ||
Theorem | modcl 12991 | Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ ℝ) | ||
Theorem | flpmodeq 12992 | Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴) | ||
Theorem | modcld 12993 | Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℝ) | ||
Theorem | mod0 12994 | 𝐴 mod 𝐵 is zero iff 𝐴 is evenly divisible by 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ (𝐴 / 𝐵) ∈ ℤ)) | ||
Theorem | mulmod0 12995 | The product of an integer and a positive real number is 0 modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) (Revised by AV, 5-Jul-2020.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → ((𝐴 · 𝑀) mod 𝑀) = 0) | ||
Theorem | negmod0 12996 | 𝐴 is divisible by 𝐵 iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ (-𝐴 mod 𝐵) = 0)) | ||
Theorem | modge0 12997 | The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵)) | ||
Theorem | modlt 12998 | The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵) | ||
Theorem | modelico 12999 | Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵)) | ||
Theorem | moddiffl 13000 | Value of the modulo operation rewritten to give two ways of expressing the quotient when "𝐴 is divided by 𝐵 using Euclidean division." Multiplying both sides by 𝐵, this implies that 𝐴 mod 𝐵 differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 6-Sep-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) = (⌊‘(𝐴 / 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |