Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | raluz2 9401* |
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) |
|
Theorem | rexuz 9402* |
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈
(ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) |
|
Theorem | rexuz2 9403* |
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) |
|
Theorem | 2rexuz 9404* |
Double existential quantification in an upper set of integers.
(Contributed by NM, 3-Nov-2005.)
|
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) |
|
Theorem | peano2uz 9405 |
Second Peano postulate for an upper set of integers. (Contributed by NM,
7-Sep-2005.)
|
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
|
Theorem | peano2uzs 9406 |
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26-Dec-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) |
|
Theorem | peano2uzr 9407 |
Reversed second Peano axiom for upper integers. (Contributed by NM,
2-Jan-2006.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) |
|
Theorem | uzaddcl 9408 |
Addition closure law for an upper set of integers. (Contributed by NM,
4-Jun-2006.)
|
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈
(ℤ≥‘𝑀)) |
|
Theorem | nn0pzuz 9409 |
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 9410* |
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 9411* |
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 9410 or
uzind4ALT 9411 may be used; see comment for nnind 8760. (Contributed by NM,
7-Sep-2005.) (New usage is discouraged.)
(Proof modification is discouraged.)
|
⊢ (𝑀 ∈ ℤ → 𝜓)
& ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) |
|
Theorem | uzind4s 9412* |
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 9413* |
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 9412 when 𝑗 and 𝑘 must
be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM,
16-Nov-2005.)
|
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑)
& ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) |
|
Theorem | uzind4i 9414* |
Induction on the upper integers that start at 𝑀. The first four
give us the substitution instances we need, and the last two are the
basis and the induction step. This is a stronger version of uzind4 9410
assuming that 𝜓 holds unconditionally. Notice that
𝑁
∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an
integer
(𝑀
∈ ℤ, see eluzel2 9355). (Contributed by NM, 4-Sep-2005.)
(Revised by AV, 13-Jul-2022.)
|
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) |
|
Theorem | indstr 9415* |
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17-Aug-2001.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) |
|
Theorem | infrenegsupex 9416* |
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 9417* |
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 9432.
(Contributed by Jim Kingdon, 15-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ)
⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |
|
Theorem | infsupneg 9418* |
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 9417. (Contributed by Jim Kingdon,
15-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ)
⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))) |
|
Theorem | supminfex 9419* |
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 9420 |
Membership in a nonnegative upper set of integers implies membership in
ℕ0. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈
ℕ0) |
|
Theorem | eluznn 9421 |
Membership in a positive upper set of integers implies membership in
ℕ. (Contributed by JJ, 1-Oct-2018.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) |
|
Theorem | eluz2b1 9422 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
↔ (𝑁 ∈ ℤ
∧ 1 < 𝑁)) |
|
Theorem | eluz2gt1 9423 |
An integer greater than or equal to 2 is greater than 1. (Contributed by
AV, 24-May-2020.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ 1 < 𝑁) |
|
Theorem | eluz2b2 9424 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
↔ (𝑁 ∈ ℕ
∧ 1 < 𝑁)) |
|
Theorem | eluz2b3 9425 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
↔ (𝑁 ∈ ℕ
∧ 𝑁 ≠
1)) |
|
Theorem | uz2m1nn 9426 |
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 9427 |
1 is not in (ℤ≥‘2).
(Contributed by Paul Chapman,
21-Nov-2012.)
|
⊢ ¬ 1 ∈
(ℤ≥‘2) |
|
Theorem | elnn1uz2 9428 |
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17-Nov-2012.)
|
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
|
Theorem | uz2mulcl 9429 |
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26-Oct-2012.)
|
⊢ ((𝑀 ∈ (ℤ≥‘2)
∧ 𝑁 ∈
(ℤ≥‘2)) → (𝑀 · 𝑁) ∈
(ℤ≥‘2)) |
|
Theorem | indstr2 9430* |
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 9431 |
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18-Apr-2020.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑁
∈ (ℤ≥‘𝑀)) |
|
Theorem | ublbneg 9432* |
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 9417. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) |
|
Theorem | eqreznegel 9433* |
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴}) |
|
Theorem | negm 9434* |
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10-Apr-2020.)
|
⊢ ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}) |
|
Theorem | lbzbi 9435* |
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
|
Theorem | nn01to3 9436 |
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 9437 |
Alternate proof of nn0ge2m1nn 9061: 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 9356, 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 9061. (Contributed by Alexander van der Vekens,
1-Aug-2018.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤
𝑁) → (𝑁 − 1) ∈
ℕ) |
|
4.4.12 Rational numbers (as a subset of complex
numbers)
|
|
Syntax | cq 9438 |
Extend class notation to include the class of rationals.
|
class ℚ |
|
Definition | df-q 9439 |
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 9441
for the relation "is rational." (Contributed
by NM, 8-Jan-2002.)
|
⊢ ℚ = ( / “ (ℤ ×
ℕ)) |
|
Theorem | divfnzn 9440 |
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 9441* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
Theorem | qmulz 9442* |
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 9443 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qre 9444 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) |
|
Theorem | zq 9445 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) |
|
Theorem | zssq 9446 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℤ ⊆ ℚ |
|
Theorem | nn0ssq 9447 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
⊢ ℕ0 ⊆
ℚ |
|
Theorem | nnssq 9448 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
⊢ ℕ ⊆ ℚ |
|
Theorem | qssre 9449 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℚ ⊆ ℝ |
|
Theorem | qsscn 9450 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℚ ⊆ ℂ |
|
Theorem | qex 9451 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℚ ∈ V |
|
Theorem | nnq 9452 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) |
|
Theorem | qcn 9453 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) |
|
Theorem | qaddcl 9454 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |
|
Theorem | qnegcl 9455 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ) |
|
Theorem | qmulcl 9456 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) |
|
Theorem | qsubcl 9457 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) |
|
Theorem | qapne 9458 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 # 𝐵 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | qltlen 9459 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8418 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) |
|
Theorem | qlttri2 9460 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | qreccl 9461 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) |
|
Theorem | qdivcl 9462 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qrevaddcl 9463 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) |
|
Theorem | nnrecq 9464 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈
ℚ) |
|
Theorem | irradd 9465 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ) →
(𝐴 + 𝐵) ∈ (ℝ ∖
ℚ)) |
|
Theorem | irrmul 9466 |
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) → (𝐴 · 𝐵) ∈ (ℝ ∖
ℚ)) |
|
Theorem | elpq 9467* |
A positive rational is the quotient of two positive integers.
(Contributed by AV, 29-Dec-2022.)
|
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
Theorem | elpqb 9468* |
A class is a positive rational iff it is the quotient of two positive
integers. (Contributed by AV, 30-Dec-2022.)
|
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
4.4.13 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 9469* |
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 7650), 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→ℂ |
|
4.5 Order sets
|
|
4.5.1 Positive reals (as a subset of complex
numbers)
|
|
Syntax | crp 9470 |
Extend class notation to include the class of positive reals.
|
class ℝ+ |
|
Definition | df-rp 9471 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} |
|
Theorem | elrp 9472 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | elrpii 9473 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈
ℝ+ |
|
Theorem | 1rp 9474 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
⊢ 1 ∈
ℝ+ |
|
Theorem | 2rp 9475 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ 2 ∈
ℝ+ |
|
Theorem | 3rp 9476 |
3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
⊢ 3 ∈
ℝ+ |
|
Theorem | rpre 9477 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ) |
|
Theorem | rpxr 9478 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ*) |
|
Theorem | rpcn 9479 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℂ) |
|
Theorem | nnrp 9480 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ+) |
|
Theorem | rpssre 9481 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
⊢ ℝ+ ⊆
ℝ |
|
Theorem | rpgt0 9482 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 0 <
𝐴) |
|
Theorem | rpge0 9483 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 0 ≤
𝐴) |
|
Theorem | rpregt0 9484 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | rprege0 9485 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
|
Theorem | rpne0 9486 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0) |
|
Theorem | rpap0 9487 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 # 0) |
|
Theorem | rprene0 9488 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpreap0 9489 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 # 0)) |
|
Theorem | rpcnne0 9490 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpcnap0 9491 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 # 0)) |
|
Theorem | ralrp 9492 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑)) |
|
Theorem | rexrp 9493 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑)) |
|
Theorem | rpaddcl 9494 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 + 𝐵) ∈
ℝ+) |
|
Theorem | rpmulcl 9495 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 · 𝐵) ∈
ℝ+) |
|
Theorem | rpdivcl 9496 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ+) |
|
Theorem | rpreccl 9497 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (1 /
𝐴) ∈
ℝ+) |
|
Theorem | rphalfcl 9498 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈
ℝ+) |
|
Theorem | rpgecl 9499 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ+) |
|
Theorem | rphalflt 9500 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴) |