Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
24-Oct-2021 | ax-ddkcomp 10114 | Axiom of Dedekind completeness for Dedekind real numbers: every nonempty upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then the axiom ax-ddkcomp 10114 should be used in place of construction specific results. In particular, axcaucvg 6974 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))) | ||
20-Oct-2021 | onunsnss 6355 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ⊆ 𝐴) | ||
19-Oct-2021 | snon0 6356 | An ordinal which is a singleton is {∅}. (Contributed by Jim Kingdon, 19-Oct-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ∈ On) → 𝐴 = ∅) | ||
18-Oct-2021 | qdencn 10124 | The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 9798 (and also would hold for ℝ × ℝ with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ 𝑄 = {𝑧 ∈ ℂ ∣ ((ℜ‘𝑧) ∈ ℚ ∧ (ℑ‘𝑧) ∈ ℚ)} ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ^{+}) → ∃𝑥 ∈ 𝑄 (abs‘(𝑥 − 𝐴)) < 𝐵) | ||
18-Oct-2021 | modqmulnn 9184 | Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℚ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀))) | ||
18-Oct-2021 | intqfrac 9181 | Break a number into its integer part and its fractional part. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1))) | ||
18-Oct-2021 | flqmod 9180 | The floor function expressed in terms of the modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1))) | ||
18-Oct-2021 | modqfrac 9179 | The fractional part of a number is the number modulo 1. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴))) | ||
18-Oct-2021 | modqdifz 9178 | The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ) | ||
18-Oct-2021 | modqdiffl 9177 | The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) = (⌊‘(𝐴 / 𝐵))) | ||
18-Oct-2021 | modqelico 9176 | Modular reduction produces a half-open interval. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) ∈ (0[,)𝐵)) | ||
18-Oct-2021 | modqlt 9175 | The modulo operation is less than its second argument. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) < 𝐵) | ||
18-Oct-2021 | modqge0 9174 | The modulo operation is nonnegative. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → 0 ≤ (𝐴 mod 𝐵)) | ||
18-Oct-2021 | negqmod0 9173 | 𝐴 is divisible by 𝐵 iff its negative is. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 mod 𝐵) = 0 ↔ (-𝐴 mod 𝐵) = 0)) | ||
18-Oct-2021 | mulqmod0 9172 | The product of an integer and a positive rational number is 0 modulo the positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℚ ∧ 0 < 𝑀) → ((𝐴 · 𝑀) mod 𝑀) = 0) | ||
18-Oct-2021 | flqdiv 9163 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁))) | ||
18-Oct-2021 | intqfrac2 9161 | Decompose a real into integer and fractional parts. (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ 𝑍 = (⌊‘𝐴) & ⊢ 𝐹 = (𝐴 − 𝑍) ⇒ ⊢ (𝐴 ∈ ℚ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹))) | ||
17-Oct-2021 | modq0 9171 | 𝐴 mod 𝐵 is zero iff 𝐴 is evenly divisible by 𝐵. (Contributed by Jim Kingdon, 17-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 mod 𝐵) = 0 ↔ (𝐴 / 𝐵) ∈ ℤ)) | ||
16-Oct-2021 | modqcld 9170 | Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℚ) | ||
16-Oct-2021 | flqpmodeq 9169 | Partition of a division into its integer part and the remainder. (Contributed by Jim Kingdon, 16-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴) | ||
16-Oct-2021 | modqcl 9168 | Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) ∈ ℚ) | ||
16-Oct-2021 | modqvalr 9167 | The value of the modulo operation (multiplication in reversed order). (Contributed by Jim Kingdon, 16-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵))) | ||
16-Oct-2021 | modqval 9166 | 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 numbers 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.) As with flqcl 9117 we only prove this for rationals although other particular kinds of real numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | ||
15-Oct-2021 | qdenre 9798 | The rational numbers are dense in ℝ: any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 9111. (Contributed by BJ, 15-Oct-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^{+}) → ∃𝑥 ∈ ℚ (abs‘(𝑥 − 𝐴)) < 𝐵) | ||
14-Oct-2021 | qbtwnrelemcalc 9110 | Lemma for qbtwnre 9111. Calculations involved in showing the constructed rational number is less than 𝐵. (Contributed by Jim Kingdon, 14-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < (𝐴 · (2 · 𝑁))) & ⊢ (𝜑 → (1 / 𝑁) < (𝐵 − 𝐴)) ⇒ ⊢ (𝜑 → ((𝑀 + 2) / (2 · 𝑁)) < 𝐵) | ||
13-Oct-2021 | rebtwn2z 9109 |
A real number can be bounded by integers above and below which are two
apart.
The proof starts by finding two integers which are less than and greater than the given real number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on weak linearity, and iterating until the range consists of integers which are two apart. (Contributed by Jim Kingdon, 13-Oct-2021.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) | ||
13-Oct-2021 | rebtwn2zlemshrink 9108 | Lemma for rebtwn2z 9109. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐽 ∈ (ℤ_{≥}‘2) ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) | ||
13-Oct-2021 | rebtwn2zlemstep 9107 | Lemma for rebtwn2z 9109. Induction step. (Contributed by Jim Kingdon, 13-Oct-2021.) |
⊢ ((𝐾 ∈ (ℤ_{≥}‘2) ∧ 𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐾))) | ||
11-Oct-2021 | flqeqceilz 9160 | A rational number is an integer iff its floor equals its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴))) | ||
11-Oct-2021 | flqleceil 9159 | The floor of a rational number is less than or equal to its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌊‘𝐴) ≤ (⌈‘𝐴)) | ||
11-Oct-2021 | ceilqidz 9158 | A rational number equals its ceiling iff it is an integer. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴)) | ||
11-Oct-2021 | ceilqle 9156 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → (⌈‘𝐴) ≤ 𝐵) | ||
11-Oct-2021 | ceiqle 9155 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → -(⌊‘-𝐴) ≤ 𝐵) | ||
11-Oct-2021 | ceilqm1lt 9154 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → ((⌈‘𝐴) − 1) < 𝐴) | ||
11-Oct-2021 | ceiqm1l 9153 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (-(⌊‘-𝐴) − 1) < 𝐴) | ||
11-Oct-2021 | ceilqge 9152 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ≤ (⌈‘𝐴)) | ||
11-Oct-2021 | ceiqge 9151 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ≤ -(⌊‘-𝐴)) | ||
11-Oct-2021 | ceilqcl 9150 | Closure of the ceiling function. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌈‘𝐴) ∈ ℤ) | ||
11-Oct-2021 | ceiqcl 9149 | The ceiling function returns an integer (closure law). (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → -(⌊‘-𝐴) ∈ ℤ) | ||
11-Oct-2021 | qdceq 9102 | Equality of rationals is decidable. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → DECID 𝐴 = 𝐵) | ||
11-Oct-2021 | qltlen 8575 | Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7621 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
10-Oct-2021 | ceilqval 9148 | The value of the ceiling function. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌈‘𝐴) = -(⌊‘-𝐴)) | ||
10-Oct-2021 | flqmulnn0 9141 | Move a nonnegative integer in and out of a floor. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ ((𝑁 ∈ ℕ_{0} ∧ 𝐴 ∈ ℚ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) | ||
10-Oct-2021 | flqzadd 9140 | An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℚ) → (⌊‘(𝑁 + 𝐴)) = (𝑁 + (⌊‘𝐴))) | ||
10-Oct-2021 | flqaddz 9139 | An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 + 𝑁)) = ((⌊‘𝐴) + 𝑁)) | ||
10-Oct-2021 | flqge1nn 9136 | The floor of a number greater than or equal to 1 is a positive integer. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ) | ||
10-Oct-2021 | flqge0nn0 9135 | The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ_{0}) | ||
10-Oct-2021 | 4ap0 8015 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ 4 # 0 | ||
10-Oct-2021 | 3ap0 8012 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ 3 # 0 | ||
9-Oct-2021 | flqbi2 9133 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐹 ∈ ℚ) → ((⌊‘(𝑁 + 𝐹)) = 𝑁 ↔ (0 ≤ 𝐹 ∧ 𝐹 < 1))) | ||
9-Oct-2021 | flqbi 9132 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ) → ((⌊‘𝐴) = 𝐵 ↔ (𝐵 ≤ 𝐴 ∧ 𝐴 < (𝐵 + 1)))) | ||
9-Oct-2021 | flqword2 9131 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐵) ∈ (ℤ_{≥}‘(⌊‘𝐴))) | ||
9-Oct-2021 | flqwordi 9130 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ (⌊‘𝐵)) | ||
9-Oct-2021 | flqltnz 9129 | If A is not an integer, then the floor of A is less than A. (Contributed by Jim Kingdon, 9-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ ¬ 𝐴 ∈ ℤ) → (⌊‘𝐴) < 𝐴) | ||
9-Oct-2021 | flqidz 9128 | A rational number equals its floor iff it is an integer. (Contributed by Jim Kingdon, 9-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → ((⌊‘𝐴) = 𝐴 ↔ 𝐴 ∈ ℤ)) | ||
8-Oct-2021 | flqidm 9127 | The floor function is idempotent. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌊‘(⌊‘𝐴)) = (⌊‘𝐴)) | ||
8-Oct-2021 | flqlt 9125 | The floor function value is less than the next integer. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (⌊‘𝐴) < 𝐵)) | ||
8-Oct-2021 | flqge 9124 | The floor function value is the greatest integer less than or equal to its argument. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ (⌊‘𝐴))) | ||
8-Oct-2021 | qfracge0 9123 | The fractional part of a rational number is nonnegative. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → 0 ≤ (𝐴 − (⌊‘𝐴))) | ||
8-Oct-2021 | qfraclt1 9122 | The fractional part of a rational number is less than one. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (𝐴 − (⌊‘𝐴)) < 1) | ||
8-Oct-2021 | flqltp1 9121 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → 𝐴 < ((⌊‘𝐴) + 1)) | ||
8-Oct-2021 | flqle 9120 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌊‘𝐴) ≤ 𝐴) | ||
8-Oct-2021 | flqcld 9119 | The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → (⌊‘𝐴) ∈ ℤ) | ||
8-Oct-2021 | flqlelt 9118 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → ((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1))) | ||
8-Oct-2021 | flqcl 9117 | The floor (greatest integer) function yields an integer when applied to a rational (closure law). It would presumably be possible to prove a similar result for some real numbers (for example, those apart from any integer), but not real numbers in general. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → (⌊‘𝐴) ∈ ℤ) | ||
8-Oct-2021 | qbtwnz 9106 | There is a unique greatest integer less than or equal to a rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) | ||
8-Oct-2021 | qbtwnzlemex 9105 |
Lemma for qbtwnz 9106. Existence of the integer.
The proof starts by finding two integers which are less than and greater than the given rational number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on rational number trichotomy, and iterating until the range consists of two consecutive integers. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ (𝐴 ∈ ℚ → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) | ||
8-Oct-2021 | qbtwnzlemshrink 9104 | Lemma for qbtwnz 9106. Shrinking the range around the given rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐽 ∈ ℕ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) | ||
8-Oct-2021 | qbtwnzlemstep 9103 | Lemma for qbtwnz 9106. Induction step. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐾))) | ||
8-Oct-2021 | qltnle 9101 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 8-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
7-Oct-2021 | qlelttric 9100 | Rational trichotomy. (Contributed by Jim Kingdon, 7-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) | ||
6-Oct-2021 | qletric 9099 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
6-Oct-2021 | qtri3or 9098 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) |
⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) | ||
3-Oct-2021 | reg3exmid 4304 | If any inhabited set satisfying df-wetr 4071 for E has a minimal element, excluded middle follows. (Contributed by Jim Kingdon, 3-Oct-2021.) |
⊢ (( E We 𝑧 ∧ ∃𝑤 𝑤 ∈ 𝑧) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 𝑥 ⊆ 𝑦) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
3-Oct-2021 | reg3exmidlemwe 4303 | Lemma for reg3exmid 4304. Our counterexample 𝐴 satisfies We. (Contributed by Jim Kingdon, 3-Oct-2021.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ (𝑥 = ∅ ∧ 𝜑))} ⇒ ⊢ E We 𝐴 | ||
2-Oct-2021 | reg2exmid 4261 | If any inhabited set has a minimal element (when expressed by ⊆), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.) |
⊢ ∀𝑧(∃𝑤 𝑤 ∈ 𝑧 → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 𝑥 ⊆ 𝑦) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
2-Oct-2021 | reg2exmidlema 4259 | Lemma for reg2exmid 4261. If 𝐴 has a minimal element (expressed by ⊆), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ (𝑥 = ∅ ∧ 𝜑))} ⇒ ⊢ (∃𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 𝑢 ⊆ 𝑣 → (𝜑 ∨ ¬ 𝜑)) | ||
30-Sep-2021 | fin0or 6343 | A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.) |
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ∃𝑥 𝑥 ∈ 𝐴)) | ||
30-Sep-2021 | wessep 4302 | A subset of a set well-ordered by set membership is well-ordered by set membership. (Contributed by Jim Kingdon, 30-Sep-2021.) |
⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴) → E We 𝐵) | ||
28-Sep-2021 | frind 4089 | Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑)) & ⊢ (𝜒 → 𝑅 Fr 𝐴) & ⊢ (𝜒 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑) | ||
26-Sep-2021 | wetriext 4301 | A trichotomous well-order is extensional. (Contributed by Jim Kingdon, 26-Sep-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 (𝑧𝑅𝐵 ↔ 𝑧𝑅𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
25-Sep-2021 | nnwetri 6354 | A natural number is well-ordered by E. More specifically, this order both satisfies We and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.) |
⊢ (𝐴 ∈ ω → ( E We 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | ||
23-Sep-2021 | wepo 4096 | A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.) |
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) | ||
23-Sep-2021 | df-wetr 4071 | Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals don't have that as seen at ordtriexmid 4247). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.) |
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
22-Sep-2021 | frforeq3 4084 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) | ||
22-Sep-2021 | frforeq2 4082 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) | ||
22-Sep-2021 | frforeq1 4080 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) | ||
22-Sep-2021 | df-frfor 4068 | Define the well-founded relation predicate where 𝐴 might be a proper class. By passing in 𝑆 we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.) |
⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)) | ||
21-Sep-2021 | frirrg 4087 | A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.) |
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
21-Sep-2021 | df-frind 4069 | Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because 𝑠 is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.) |
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) | ||
17-Sep-2021 | ontr2exmid 4250 | An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.) |
⊢ ∀𝑥 ∈ On ∀𝑦∀𝑧 ∈ On ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
16-Sep-2021 | nnsseleq 6079 | For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
15-Sep-2021 | fientri3 6353 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) | ||
15-Sep-2021 | nntri2or2 6076 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
14-Sep-2021 | findcard2sd 6349 | Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) | ||
13-Sep-2021 | php5fin 6339 | A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ (V ∖ 𝐴)) → ¬ 𝐴 ≈ (𝐴 ∪ {𝐵})) | ||
13-Sep-2021 | fiunsnnn 6338 | Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.) |
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ (V ∖ 𝐴)) ∧ (𝑁 ∈ ω ∧ 𝐴 ≈ 𝑁)) → (𝐴 ∪ {𝐵}) ≈ suc 𝑁) | ||
12-Sep-2021 | fisbth 6340 | Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.) |
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) | ||
11-Sep-2021 | diffisn 6350 | Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ∈ Fin) | ||
10-Sep-2021 | fin0 6342 | A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.) |
⊢ (𝐴 ∈ Fin → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
Copyright terms: Public domain | W3C HTML validation [external] |