Theorem List for Intuitionistic Logic Explorer - 8801-8900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | eluzp1l 8801 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) |
|
Theorem | eluzp1p1 8802 |
Membership in the next upper set of integers. (Contributed by NM,
5-Oct-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
|
Theorem | eluzaddi 8803 |
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
|
Theorem | eluzsubi 8804 |
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈
ℤ ⇒ ⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | eluzadd 8805 |
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
|
Theorem | eluzsub 8806 |
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | uzm1 8807 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
|
Theorem | uznn0sub 8808 |
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈
ℕ0) |
|
Theorem | uzin 8809 |
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24-Dec-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
|
Theorem | uzp1 8810 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈
(ℤ≥‘(𝑀 + 1)))) |
|
Theorem | nn0uz 8811 |
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
⊢ ℕ0 =
(ℤ≥‘0) |
|
Theorem | nnuz 8812 |
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2-Sep-2005.)
|
⊢ ℕ =
(ℤ≥‘1) |
|
Theorem | elnnuz 8813 |
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
|
Theorem | elnn0uz 8814 |
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈
(ℤ≥‘0)) |
|
Theorem | eluz2nn 8815 |
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3-Nov-2018.)
|
⊢ (𝐴 ∈ (ℤ≥‘2)
→ 𝐴 ∈
ℕ) |
|
Theorem | eluzge2nn0 8816 |
If an integer is greater than or equal to 2, then it is a nonnegative
integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV,
3-Nov-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ 𝑁 ∈
ℕ0) |
|
Theorem | uzuzle23 8817 |
An integer in the upper set of integers starting at 3 is element of the
upper set of integers starting at 2. (Contributed by Alexander van der
Vekens, 17-Sep-2018.)
|
⊢ (𝐴 ∈ (ℤ≥‘3)
→ 𝐴 ∈
(ℤ≥‘2)) |
|
Theorem | eluzge3nn 8818 |
If an integer is greater than 3, then it is a positive integer.
(Contributed by Alexander van der Vekens, 17-Sep-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘3)
→ 𝑁 ∈
ℕ) |
|
Theorem | uz3m2nn 8819 |
An integer greater than or equal to 3 decreased by 2 is a positive
integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|
⊢ (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2)
∈ ℕ) |
|
Theorem | 1eluzge0 8820 |
1 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8-Jun-2018.)
|
⊢ 1 ∈
(ℤ≥‘0) |
|
Theorem | 2eluzge0 8821 |
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|
⊢ 2 ∈
(ℤ≥‘0) |
|
Theorem | 2eluzge1 8822 |
2 is an integer greater than or equal to 1. (Contributed by Alexander van
der Vekens, 8-Jun-2018.)
|
⊢ 2 ∈
(ℤ≥‘1) |
|
Theorem | uznnssnn 8823 |
The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘𝑁) ⊆ ℕ) |
|
Theorem | raluz 8824* |
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈
(ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) |
|
Theorem | raluz2 8825* |
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) |
|
Theorem | rexuz 8826* |
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈
(ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) |
|
Theorem | rexuz2 8827* |
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) |
|
Theorem | 2rexuz 8828* |
Double existential quantification in an upper set of integers.
(Contributed by NM, 3-Nov-2005.)
|
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) |
|
Theorem | peano2uz 8829 |
Second Peano postulate for an upper set of integers. (Contributed by NM,
7-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
|
Theorem | peano2uzs 8830 |
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) |
|
Theorem | peano2uzr 8831 |
Reversed second Peano axiom for upper integers. (Contributed by NM,
2-Jan-2006.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzaddcl 8832 |
Addition closure law for an upper set of integers. (Contributed by NM,
4-Jun-2006.)
|
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | nn0pzuz 8833 |
The sum of a nonnegative integer and an integer is an integer greater than
or equal to that integer. (Contributed by Alexander van der Vekens,
3-Oct-2018.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ) → (𝑁 + 𝑍) ∈
(ℤ≥‘𝑍)) |
|
Theorem | uzind4 8834* |
Induction on the upper set of integers that starts at an integer 𝑀.
The first four hypotheses give us the substitution instances we need,
and the last two are the basis and the induction step. (Contributed by
NM, 7-Sep-2005.)
|
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) |
|
Theorem | uzind4ALT 8835* |
Induction on the upper set of integers that starts at an integer 𝑀.
The last four hypotheses give us the substitution instances we need; the
first two are the basis and the induction step. Either uzind4 8834 or
uzind4ALT 8835 may be used; see comment for nnind 8199. (Contributed by NM,
7-Sep-2005.) (New usage is discouraged.)
(Proof modification is discouraged.)
|
⊢ (𝑀 ∈ ℤ → 𝜓)
& ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) |
|
Theorem | uzind4s 8836* |
Induction on the upper set of integers that starts at an integer 𝑀,
using explicit substitution. The hypotheses are the basis and the
induction step. (Contributed by NM, 4-Nov-2005.)
|
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑘]𝜑)
& ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜑 → [(𝑘 + 1) / 𝑘]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑘]𝜑) |
|
Theorem | uzind4s2 8837* |
Induction on the upper set of integers that starts at an integer 𝑀,
using explicit substitution. The hypotheses are the basis and the
induction step. Use this instead of uzind4s 8836 when 𝑗 and 𝑘 must
be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM,
16-Nov-2005.)
|
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑)
& ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) |
|
Theorem | uzind4i 8838* |
Induction on the upper integers that start at 𝑀. The first
hypothesis specifies the lower bound, the next four give us the
substitution instances we need, and the last two are the basis and the
induction step. (Contributed by NM, 4-Sep-2005.)
|
⊢ 𝑀 ∈ ℤ & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) |
|
Theorem | indstr 8839* |
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17-Aug-2001.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) |
|
Theorem | infrenegsupex 8840* |
The infimum of a set of reals 𝐴 is the negative of the supremum of
the negatives of its elements. (Contributed by Jim Kingdon,
14-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ)
⇒ ⊢ (𝜑 → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) |
|
Theorem | supinfneg 8841* |
If a set of real numbers has a least upper bound, the set of the
negation of those numbers has a greatest lower bound. For a theorem
which is similar but only for the boundedness part, see ublbneg 8856.
(Contributed by Jim Kingdon, 15-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ)
⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |
|
Theorem | infsupneg 8842* |
If a set of real numbers has a greatest lower bound, the set of the
negation of those numbers has a least upper bound. To go in the other
direction see supinfneg 8841. (Contributed by Jim Kingdon,
15-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ)
⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))) |
|
Theorem | supminfex 8843* |
A supremum is the negation of the infimum of that set's image under
negation. (Contributed by Jim Kingdon, 14-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ)
⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) = -inf({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}, ℝ, < )) |
|
Theorem | eluznn0 8844 |
Membership in a nonnegative upper set of integers implies membership in
ℕ0. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈
ℕ0) |
|
Theorem | eluznn 8845 |
Membership in a positive upper set of integers implies membership in
ℕ. (Contributed by JJ, 1-Oct-2018.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) |
|
Theorem | eluz2b1 8846 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
↔ (𝑁 ∈ ℤ
∧ 1 < 𝑁)) |
|
Theorem | eluz2gt1 8847 |
An integer greater than or equal to 2 is greater than 1. (Contributed by
AV, 24-May-2020.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ 1 < 𝑁) |
|
Theorem | eluz2b2 8848 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
↔ (𝑁 ∈ ℕ
∧ 1 < 𝑁)) |
|
Theorem | eluz2b3 8849 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
↔ (𝑁 ∈ ℕ
∧ 𝑁 ≠
1)) |
|
Theorem | uz2m1nn 8850 |
One less than an integer greater than or equal to 2 is a positive integer.
(Contributed by Paul Chapman, 17-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ (𝑁 − 1)
∈ ℕ) |
|
Theorem | 1nuz2 8851 |
1 is not in (ℤ≥‘2).
(Contributed by Paul Chapman,
21-Nov-2012.)
|
⊢ ¬ 1 ∈
(ℤ≥‘2) |
|
Theorem | elnn1uz2 8852 |
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17-Nov-2012.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
|
Theorem | uz2mulcl 8853 |
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26-Oct-2012.)
|
⊢ ((𝑀 ∈ (ℤ≥‘2)
∧ 𝑁 ∈
(ℤ≥‘2)) → (𝑀 · 𝑁) ∈
(ℤ≥‘2)) |
|
Theorem | indstr2 8854* |
Strong Mathematical Induction for positive integers (inference schema).
The first two hypotheses give us the substitution instances we need; the
last two are the basis and the induction step. (Contributed by Paul
Chapman, 21-Nov-2012.)
|
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜒 & ⊢ (𝑥 ∈
(ℤ≥‘2) → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) |
|
Theorem | eluzdc 8855 |
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18-Apr-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑁
∈ (ℤ≥‘𝑀)) |
|
Theorem | ublbneg 8856* |
The image under negation of a bounded-above set of reals is bounded
below. For a theorem which is similar but also adds that the bounds
need to be the tightest possible, see supinfneg 8841. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) |
|
Theorem | eqreznegel 8857* |
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴}) |
|
Theorem | negm 8858* |
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10-Apr-2020.)
|
⊢ ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}) |
|
Theorem | lbzbi 8859* |
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
|
Theorem | nn01to3 8860 |
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13-Sep-2018.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 1 ≤
𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) |
|
Theorem | nn0ge2m1nnALT 8861 |
Alternate proof of nn0ge2m1nn 8492: If a nonnegative integer is greater
than or equal to two, the integer decreased by 1 is a positive integer.
This version is proved using eluz2 8783, a theorem for upper sets of
integers, which are defined later than the positive and nonnegative
integers. This proof is, however, much shorter than the proof of
nn0ge2m1nn 8492. (Contributed by Alexander van der Vekens,
1-Aug-2018.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤
𝑁) → (𝑁 − 1) ∈
ℕ) |
|
3.4.12 Rational numbers (as a subset of complex
numbers)
|
|
Syntax | cq 8862 |
Extend class notation to include the class of rationals.
|
class ℚ |
|
Definition | df-q 8863 |
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 8865
for the relation "is rational." (Contributed
by NM, 8-Jan-2002.)
|
⊢ ℚ = ( / “ (ℤ ×
ℕ)) |
|
Theorem | divfnzn 8864 |
Division restricted to ℤ × ℕ is a
function. Given excluded
middle, it would be easy to prove this for ℂ
× (ℂ ∖ {0}).
The key difference is that an element of ℕ
is apart from zero,
whereas being an element of ℂ ∖ {0}
implies being not equal to
zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|
⊢ ( / ↾ (ℤ × ℕ)) Fn
(ℤ × ℕ) |
|
Theorem | elq 8865* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
Theorem | qmulz 8866* |
If 𝐴 is rational, then some integer
multiple of it is an integer.
(Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro,
22-Jul-2014.)
|
⊢ (𝐴 ∈ ℚ → ∃𝑥 ∈ ℕ (𝐴 · 𝑥) ∈ ℤ) |
|
Theorem | znq 8867 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qre 8868 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) |
|
Theorem | zq 8869 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) |
|
Theorem | zssq 8870 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℤ ⊆ ℚ |
|
Theorem | nn0ssq 8871 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
⊢ ℕ0 ⊆
ℚ |
|
Theorem | nnssq 8872 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
⊢ ℕ ⊆ ℚ |
|
Theorem | qssre 8873 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℚ ⊆ ℝ |
|
Theorem | qsscn 8874 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℚ ⊆ ℂ |
|
Theorem | qex 8875 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℚ ∈ V |
|
Theorem | nnq 8876 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) |
|
Theorem | qcn 8877 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) |
|
Theorem | qaddcl 8878 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |
|
Theorem | qnegcl 8879 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ) |
|
Theorem | qmulcl 8880 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) |
|
Theorem | qsubcl 8881 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) |
|
Theorem | qapne 8882 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 # 𝐵 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | qltlen 8883 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7874 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) |
|
Theorem | qlttri2 8884 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | qreccl 8885 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) |
|
Theorem | qdivcl 8886 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qrevaddcl 8887 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) |
|
Theorem | nnrecq 8888 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈
ℚ) |
|
Theorem | irradd 8889 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ) →
(𝐴 + 𝐵) ∈ (ℝ ∖
ℚ)) |
|
Theorem | irrmul 8890 |
The product of a real which is not rational with a nonzero rational is not
rational. Note that by "not rational" we mean the negation of
"is
rational" (whereas "irrational" is often defined to mean
apart from any
rational number - given excluded middle these two definitions would be
equivalent). (Contributed by NM, 7-Nov-2008.)
|
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ ∧
𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖
ℚ)) |
|
3.4.13 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 8891* |
There is a natural one-to-one mapping from (ℝ ×
ℝ) to ℂ,
where we map 〈𝑥, 𝑦〉 to (𝑥 + (i · 𝑦)). In our
construction of the complex numbers, this is in fact our
definition of
ℂ (see df-c 7126), but in the axiomatic treatment we can only
show
that there is the expected mapping between these two sets. (Contributed
by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro,
17-Feb-2014.)
|
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→ℂ |
|
3.5 Order sets
|
|
3.5.1 Positive reals (as a subset of complex
numbers)
|
|
Syntax | crp 8892 |
Extend class notation to include the class of positive reals.
|
class ℝ+ |
|
Definition | df-rp 8893 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} |
|
Theorem | elrp 8894 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | elrpii 8895 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈
ℝ+ |
|
Theorem | 1rp 8896 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
⊢ 1 ∈
ℝ+ |
|
Theorem | 2rp 8897 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ 2 ∈
ℝ+ |
|
Theorem | rpre 8898 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ) |
|
Theorem | rpxr 8899 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ*) |
|
Theorem | rpcn 8900 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℂ) |