Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lbzbi 9401* |
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
|
Theorem | nn01to3 9402 |
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 9403 |
Alternate proof of nn0ge2m1nn 9030: 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 9325, 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 9030. (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 9404 |
Extend class notation to include the class of rationals.
|
class ℚ |
|
Definition | df-q 9405 |
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 9407
for the relation "is rational." (Contributed
by NM, 8-Jan-2002.)
|
⊢ ℚ = ( / “ (ℤ ×
ℕ)) |
|
Theorem | divfnzn 9406 |
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 9407* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
|
Theorem | qmulz 9408* |
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 9409 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qre 9410 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) |
|
Theorem | zq 9411 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) |
|
Theorem | zssq 9412 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℤ ⊆ ℚ |
|
Theorem | nn0ssq 9413 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
⊢ ℕ0 ⊆
ℚ |
|
Theorem | nnssq 9414 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
⊢ ℕ ⊆ ℚ |
|
Theorem | qssre 9415 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
⊢ ℚ ⊆ ℝ |
|
Theorem | qsscn 9416 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
⊢ ℚ ⊆ ℂ |
|
Theorem | qex 9417 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ ℚ ∈ V |
|
Theorem | nnq 9418 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) |
|
Theorem | qcn 9419 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) |
|
Theorem | qaddcl 9420 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |
|
Theorem | qnegcl 9421 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ) |
|
Theorem | qmulcl 9422 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) |
|
Theorem | qsubcl 9423 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) |
|
Theorem | qapne 9424 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 # 𝐵 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | qltlen 9425 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8387 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) |
|
Theorem | qlttri2 9426 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | qreccl 9427 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) |
|
Theorem | qdivcl 9428 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
|
Theorem | qrevaddcl 9429 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) |
|
Theorem | nnrecq 9430 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈
ℚ) |
|
Theorem | irradd 9431 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧
𝐵 ∈ ℚ) →
(𝐴 + 𝐵) ∈ (ℝ ∖
ℚ)) |
|
Theorem | irrmul 9432 |
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) → (𝐴 · 𝐵) ∈ (ℝ ∖
ℚ)) |
|
4.4.13 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 9433* |
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 7619), 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 9434 |
Extend class notation to include the class of positive reals.
|
class ℝ+ |
|
Definition | df-rp 9435 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} |
|
Theorem | elrp 9436 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | elrpii 9437 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈
ℝ+ |
|
Theorem | 1rp 9438 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
⊢ 1 ∈
ℝ+ |
|
Theorem | 2rp 9439 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ 2 ∈
ℝ+ |
|
Theorem | 3rp 9440 |
3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
⊢ 3 ∈
ℝ+ |
|
Theorem | rpre 9441 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ) |
|
Theorem | rpxr 9442 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℝ*) |
|
Theorem | rpcn 9443 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈
ℂ) |
|
Theorem | nnrp 9444 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ+) |
|
Theorem | rpssre 9445 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
⊢ ℝ+ ⊆
ℝ |
|
Theorem | rpgt0 9446 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|
⊢ (𝐴 ∈ ℝ+ → 0 <
𝐴) |
|
Theorem | rpge0 9447 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 0 ≤
𝐴) |
|
Theorem | rpregt0 9448 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 <
𝐴)) |
|
Theorem | rprege0 9449 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
|
Theorem | rpne0 9450 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0) |
|
Theorem | rpap0 9451 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → 𝐴 # 0) |
|
Theorem | rprene0 9452 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpreap0 9453 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 # 0)) |
|
Theorem | rpcnne0 9454 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpcnap0 9455 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 # 0)) |
|
Theorem | ralrp 9456 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑)) |
|
Theorem | rexrp 9457 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑)) |
|
Theorem | rpaddcl 9458 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 + 𝐵) ∈
ℝ+) |
|
Theorem | rpmulcl 9459 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 · 𝐵) ∈
ℝ+) |
|
Theorem | rpdivcl 9460 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ+) |
|
Theorem | rpreccl 9461 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
⊢ (𝐴 ∈ ℝ+ → (1 /
𝐴) ∈
ℝ+) |
|
Theorem | rphalfcl 9462 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈
ℝ+) |
|
Theorem | rpgecl 9463 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ+) |
|
Theorem | rphalflt 9464 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴) |
|
Theorem | rerpdivcl 9465 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ) |
|
Theorem | ge0p1rp 9466 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈
ℝ+) |
|
Theorem | rpnegap 9467 |
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 9468 |
Elementhood of a negation in the positive real numbers. (Contributed by
Thierry Arnoux, 19-Sep-2018.)
|
⊢ (𝐴 ∈ ℝ → (-𝐴 ∈ ℝ+ ↔ 𝐴 < 0)) |
|
Theorem | negelrpd 9469 |
The negation of a negative number is in the positive real numbers.
(Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → -𝐴 ∈
ℝ+) |
|
Theorem | 0nrp 9470 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
⊢ ¬ 0 ∈
ℝ+ |
|
Theorem | ltsubrp 9471 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 − 𝐵) < 𝐴) |
|
Theorem | ltaddrp 9472 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵)) |
|
Theorem | difrp 9473 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈
ℝ+)) |
|
Theorem | elrpd 9474 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ+) |
|
Theorem | nnrpd 9475 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ)
⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ+) |
|
Theorem | rpred 9476 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | rpxrd 9477 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ*) |
|
Theorem | rpcnd 9478 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) |
|
Theorem | rpgt0d 9479 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 0 < 𝐴) |
|
Theorem | rpge0d 9480 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) |
|
Theorem | rpne0d 9481 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) |
|
Theorem | rpap0d 9482 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 # 0) |
|
Theorem | rpregt0d 9483 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
|
Theorem | rprege0d 9484 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
|
Theorem | rprene0d 9485 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpcnne0d 9486 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
|
Theorem | rpreccld 9487 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈
ℝ+) |
|
Theorem | rprecred 9488 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) |
|
Theorem | rphalfcld 9489 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈
ℝ+) |
|
Theorem | reclt1d 9490 |
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 9491 |
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 9492 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈
ℝ+) |
|
Theorem | rpmulcld 9493 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈
ℝ+) |
|
Theorem | rpdivcld 9494 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈
ℝ+) |
|
Theorem | ltrecd 9495 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) |
|
Theorem | lerecd 9496 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) |
|
Theorem | ltrec1d 9497 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (1 / 𝐴) < 𝐵) ⇒ ⊢ (𝜑 → (1 / 𝐵) < 𝐴) |
|
Theorem | lerec2d 9498 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≤ (1 / 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 ≤ (1 / 𝐴)) |
|
Theorem | lediv2ad 9499 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)) |
|
Theorem | ltdiv2d 9500 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) |