Theorem List for Intuitionistic Logic Explorer - 9601-9700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elnndc 9601 |
Membership of an integer in ℕ is decidable.
(Contributed by Jim
Kingdon, 17-Oct-2024.)
|
⊢ (𝑁 ∈ ℤ → DECID
𝑁 ∈
ℕ) |
|
Theorem | ublbneg 9602* |
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 9584. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) |
|
Theorem | eqreznegel 9603* |
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴}) |
|
Theorem | negm 9604* |
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10-Apr-2020.)
|
⊢ ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}) |
|
Theorem | lbzbi 9605* |
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
|
Theorem | nn01to3 9606 |
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 9607 |
Alternate proof of nn0ge2m1nn 9225: 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 9523, 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 9225. (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 9608 |
Extend class notation to include the class of rationals.
|
class ℚ |
|
Definition | df-q 9609 |
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 9611
for the relation "is rational". (Contributed
by NM, 8-Jan-2002.)
|
⊢ ℚ = ( / “ (ℤ ×
ℕ)) |
|
Theorem | divfnzn 9610 |
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 9611* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
Theorem | qmulz 9612* |
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 9613 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qre 9614 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) |
|
Theorem | zq 9615 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) |
|
Theorem | zssq 9616 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℤ ⊆ ℚ |
|
Theorem | nn0ssq 9617 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
⊢ ℕ0 ⊆
ℚ |
|
Theorem | nnssq 9618 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
⊢ ℕ ⊆ ℚ |
|
Theorem | qssre 9619 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℚ ⊆ ℝ |
|
Theorem | qsscn 9620 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℚ ⊆ ℂ |
|
Theorem | qex 9621 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℚ ∈ V |
|
Theorem | nnq 9622 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) |
|
Theorem | qcn 9623 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) |
|
Theorem | qaddcl 9624 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |
|
Theorem | qnegcl 9625 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ) |
|
Theorem | qmulcl 9626 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) |
|
Theorem | qsubcl 9627 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) |
|
Theorem | qapne 9628 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 # 𝐵 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | qltlen 9629 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8579 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) |
|
Theorem | qlttri2 9630 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | qreccl 9631 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) |
|
Theorem | qdivcl 9632 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qrevaddcl 9633 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) |
|
Theorem | nnrecq 9634 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈
ℚ) |
|
Theorem | irradd 9635 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ) →
(𝐴 + 𝐵) ∈ (ℝ ∖
ℚ)) |
|
Theorem | irrmul 9636 |
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 9637* |
A positive rational is the quotient of two positive integers.
(Contributed by AV, 29-Dec-2022.)
|
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
Theorem | elpqb 9638* |
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 9639* |
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 7808), 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 9640 |
Extend class notation to include the class of positive reals.
|
class ℝ+ |
|
Definition | df-rp 9641 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} |
|
Theorem | elrp 9642 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | elrpii 9643 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈
ℝ+ |
|
Theorem | 1rp 9644 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
⊢ 1 ∈
ℝ+ |
|
Theorem | 2rp 9645 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ 2 ∈
ℝ+ |
|
Theorem | 3rp 9646 |
3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
⊢ 3 ∈
ℝ+ |
|
Theorem | rpre 9647 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ) |
|
Theorem | rpxr 9648 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ*) |
|
Theorem | rpcn 9649 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℂ) |
|
Theorem | nnrp 9650 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ+) |
|
Theorem | rpssre 9651 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
⊢ ℝ+ ⊆
ℝ |
|
Theorem | rpgt0 9652 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 0 <
𝐴) |
|
Theorem | rpge0 9653 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 0 ≤
𝐴) |
|
Theorem | rpregt0 9654 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | rprege0 9655 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
|
Theorem | rpne0 9656 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0) |
|
Theorem | rpap0 9657 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 # 0) |
|
Theorem | rprene0 9658 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpreap0 9659 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 # 0)) |
|
Theorem | rpcnne0 9660 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpcnap0 9661 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 # 0)) |
|
Theorem | ralrp 9662 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑)) |
|
Theorem | rexrp 9663 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑)) |
|
Theorem | rpaddcl 9664 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 + 𝐵) ∈
ℝ+) |
|
Theorem | rpmulcl 9665 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 · 𝐵) ∈
ℝ+) |
|
Theorem | rpdivcl 9666 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ+) |
|
Theorem | rpreccl 9667 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (1 /
𝐴) ∈
ℝ+) |
|
Theorem | rphalfcl 9668 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈
ℝ+) |
|
Theorem | rpgecl 9669 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ+) |
|
Theorem | rphalflt 9670 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴) |
|
Theorem | rerpdivcl 9671 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ) |
|
Theorem | ge0p1rp 9672 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈
ℝ+) |
|
Theorem | rpnegap 9673 |
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (𝐴 ∈ ℝ+ ⊻ -𝐴 ∈
ℝ+)) |
|
Theorem | negelrp 9674 |
Elementhood of a negation in the positive real numbers. (Contributed by
Thierry Arnoux, 19-Sep-2018.)
|
⊢ (𝐴 ∈ ℝ → (-𝐴 ∈ ℝ+ ↔ 𝐴 < 0)) |
|
Theorem | negelrpd 9675 |
The negation of a negative number is in the positive real numbers.
(Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → -𝐴 ∈
ℝ+) |
|
Theorem | 0nrp 9676 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
⊢ ¬ 0 ∈
ℝ+ |
|
Theorem | ltsubrp 9677 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 − 𝐵) < 𝐴) |
|
Theorem | ltaddrp 9678 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵)) |
|
Theorem | difrp 9679 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈
ℝ+)) |
|
Theorem | elrpd 9680 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ+) |
|
Theorem | nnrpd 9681 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ)
⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ+) |
|
Theorem | zgt1rpn0n1 9682 |
An integer greater than 1 is a positive real number not equal to 0 or 1.
Useful for working with integer logarithm bases (which is a common case,
e.g., base 2, base 3, or base 10). (Contributed by Thierry Arnoux,
26-Sep-2017.) (Proof shortened by AV, 9-Jul-2022.)
|
⊢ (𝐵 ∈ (ℤ≥‘2)
→ (𝐵 ∈
ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1)) |
|
Theorem | rpred 9683 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | rpxrd 9684 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ*) |
|
Theorem | rpcnd 9685 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) |
|
Theorem | rpgt0d 9686 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 0 < 𝐴) |
|
Theorem | rpge0d 9687 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) |
|
Theorem | rpne0d 9688 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) |
|
Theorem | rpap0d 9689 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 # 0) |
|
Theorem | rpregt0d 9690 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
|
Theorem | rprege0d 9691 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
|
Theorem | rprene0d 9692 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpcnne0d 9693 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpreccld 9694 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈
ℝ+) |
|
Theorem | rprecred 9695 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) |
|
Theorem | rphalfcld 9696 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈
ℝ+) |
|
Theorem | reclt1d 9697 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 1 ↔ 1 < (1 / 𝐴))) |
|
Theorem | recgt1d 9698 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ (1 / 𝐴) < 1)) |
|
Theorem | rpaddcld 9699 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈
ℝ+) |
|
Theorem | rpmulcld 9700 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈
ℝ+) |