Type  Label  Description 
Statement 

Theorem  2rexuz 8301* 
Double existential quantification in an upper set of integers.
(Contributed by NM, 3Nov2005.)

⊢ (∃𝑚∃𝑛 ∈
(ℤ_{≥}‘𝑚)φ
↔ ∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
(𝑚 ≤ 𝑛 ∧ φ)) 

Theorem  peano2uz 8302 
Second Peano postulate for an upper set of integers. (Contributed by NM,
7Sep2005.)

⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → (𝑁 + 1) ∈
(ℤ_{≥}‘𝑀)) 

Theorem  peano2uzs 8303 
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26Dec2013.)

⊢ 𝑍 = (ℤ_{≥}‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈
𝑍) 

Theorem  peano2uzr 8304 
Reversed second Peano axiom for upper integers. (Contributed by NM,
2Jan2006.)

⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
(ℤ_{≥}‘(𝑀 + 1))) → 𝑁 ∈
(ℤ_{≥}‘𝑀)) 

Theorem  uzaddcl 8305 
Addition closure law for an upper set of integers. (Contributed by NM,
4Jun2006.)

⊢ ((𝑁 ∈
(ℤ_{≥}‘𝑀) ∧ 𝐾 ∈ ℕ_{0}) → (𝑁 + 𝐾) ∈
(ℤ_{≥}‘𝑀)) 

Theorem  nn0pzuz 8306 
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,
3Oct2018.)

⊢ ((𝑁 ∈
ℕ_{0} ∧ 𝑍 ∈
ℤ) → (𝑁 + 𝑍) ∈ (ℤ_{≥}‘𝑍)) 

Theorem  uzind4 8307* 
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, 7Sep2005.)

⊢ (𝑗 = 𝑀 → (φ ↔ ψ)) & ⊢ (𝑗 = 𝑘 → (φ ↔ χ)) & ⊢ (𝑗 = (𝑘 + 1) → (φ ↔ θ)) & ⊢ (𝑗 = 𝑁 → (φ ↔ τ)) & ⊢ (𝑀 ∈ ℤ → ψ)
& ⊢ (𝑘 ∈
(ℤ_{≥}‘𝑀) → (χ → θ)) ⇒ ⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → τ) 

Theorem  uzind4ALT 8308* 
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 8307 or uzind4ALT 8308 may be used; see comment for nnind 7711.
(Contributed by NM, 7Sep2005.) (New usage is discouraged.)
(Proof modification is discouraged.)

⊢ (𝑀 ∈
ℤ → ψ) & ⊢ (𝑘 ∈ (ℤ_{≥}‘𝑀) → (χ → θ)) & ⊢ (𝑗 = 𝑀 → (φ ↔ ψ)) & ⊢ (𝑗 = 𝑘 → (φ ↔ χ)) & ⊢ (𝑗 = (𝑘 + 1) → (φ ↔ θ)) & ⊢ (𝑗 = 𝑁 → (φ ↔ τ)) ⇒ ⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → τ) 

Theorem  uzind4s 8309* 
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, 4Nov2005.)

⊢ (𝑀 ∈
ℤ → [𝑀 /
𝑘]φ)
& ⊢ (𝑘 ∈
(ℤ_{≥}‘𝑀) → (φ → [(𝑘 + 1) / 𝑘]φ)) ⇒ ⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → [𝑁 / 𝑘]φ) 

Theorem  uzind4s2 8310* 
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 8309 when 𝑗 and 𝑘 must
be distinct in [(𝑘 + 1) / 𝑗]φ. (Contributed by NM,
16Nov2005.)

⊢ (𝑀 ∈
ℤ → [𝑀 /
𝑗]φ)
& ⊢ (𝑘 ∈
(ℤ_{≥}‘𝑀) → ([𝑘 / 𝑗]φ → [(𝑘 + 1) / 𝑗]φ)) ⇒ ⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → [𝑁 / 𝑗]φ) 

Theorem  uzind4i 8311* 
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, 4Sep2005.)

⊢ 𝑀 ∈
ℤ
& ⊢ (𝑗 = 𝑀 → (φ ↔ ψ)) & ⊢ (𝑗 = 𝑘 → (φ ↔ χ)) & ⊢ (𝑗 = (𝑘 + 1) → (φ ↔ θ)) & ⊢ (𝑗 = 𝑁 → (φ ↔ τ)) & ⊢ ψ
& ⊢ (𝑘 ∈
(ℤ_{≥}‘𝑀) → (χ → θ)) ⇒ ⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → τ) 

Theorem  indstr 8312* 
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17Aug2001.)

⊢ (x =
y → (φ ↔ ψ)) & ⊢ (x ∈ ℕ
→ (∀y ∈ ℕ
(y < x → ψ)
→ φ))
⇒ ⊢ (x ∈ ℕ
→ φ) 

Theorem  eluznn0 8313 
Membership in a nonnegative upper set of integers implies membership in
ℕ_{0}. (Contributed by Paul
Chapman, 22Jun2011.)

⊢ ((𝑁 ∈
ℕ_{0} ∧ 𝑀 ∈
(ℤ_{≥}‘𝑁)) → 𝑀 ∈
ℕ_{0}) 

Theorem  eluznn 8314 
Membership in a positive upper set of integers implies membership in
ℕ. (Contributed by JJ, 1Oct2018.)

⊢ ((𝑁 ∈
ℕ ∧ 𝑀 ∈
(ℤ_{≥}‘𝑁)) → 𝑀 ∈
ℕ) 

Theorem  eluz2b1 8315 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)

⊢ (𝑁 ∈
(ℤ_{≥}‘2) ↔ (𝑁 ∈
ℤ ∧ 1 < 𝑁)) 

Theorem  eluz2b2 8316 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)

⊢ (𝑁 ∈
(ℤ_{≥}‘2) ↔ (𝑁 ∈
ℕ ∧ 1 < 𝑁)) 

Theorem  eluz2b3 8317 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)

⊢ (𝑁 ∈
(ℤ_{≥}‘2) ↔ (𝑁 ∈
ℕ ∧ 𝑁 ≠ 1)) 

Theorem  uz2m1nn 8318 
One less than an integer greater than or equal to 2 is a positive
integer. (Contributed by Paul Chapman, 17Nov2012.)

⊢ (𝑁 ∈
(ℤ_{≥}‘2) → (𝑁 − 1) ∈ ℕ) 

Theorem  1nuz2 8319 
1 is not in (ℤ_{≥}‘2).
(Contributed by Paul Chapman,
21Nov2012.)

⊢ ¬ 1 ∈
(ℤ_{≥}‘2) 

Theorem  elnn1uz2 8320 
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17Nov2012.)

⊢ (𝑁 ∈
ℕ ↔ (𝑁 = 1
∨ 𝑁 ∈
(ℤ_{≥}‘2))) 

Theorem  uz2mulcl 8321 
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26Oct2012.)

⊢ ((𝑀 ∈
(ℤ_{≥}‘2) ∧ 𝑁 ∈ (ℤ_{≥}‘2)) → (𝑀 · 𝑁) ∈
(ℤ_{≥}‘2)) 

Theorem  indstr2 8322* 
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, 21Nov2012.)

⊢ (x = 1
→ (φ ↔ χ)) & ⊢ (x = y →
(φ ↔ ψ)) & ⊢ χ
& ⊢ (x ∈ (ℤ_{≥}‘2) → (∀y ∈ ℕ (y
< x → ψ) → φ)) ⇒ ⊢ (x ∈ ℕ
→ φ) 

Theorem  eluzdc 8323 
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18Apr2020.)

⊢ ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → DECID 𝑁 ∈
(ℤ_{≥}‘𝑀)) 

Theorem  ublbneg 8324* 
The image under negation of a boundedabove set of reals is bounded
below. (Contributed by Paul Chapman, 21Mar2011.)

⊢ (∃x ∈ ℝ ∀y ∈ A y ≤ x →
∃x
∈ ℝ ∀y ∈ {z ∈ ℝ ∣ z ∈ A}x ≤
y) 

Theorem  eqreznegel 8325* 
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21Mar2011.)

⊢ (A ⊆
ℤ → {z ∈ ℝ ∣ z ∈ A} = {z ∈ ℤ ∣ z ∈ A}) 

Theorem  negm 8326* 
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10Apr2020.)

⊢ ((A ⊆
ℝ ∧ ∃x x ∈ A) → ∃y y ∈ {z ∈ ℝ
∣ z ∈ A}) 

Theorem  lbzbi 8327* 
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21Mar2011.)

⊢ (A ⊆
ℝ → (∃x ∈ ℝ ∀y ∈ A x ≤ y ↔
∃x
∈ ℤ ∀y ∈ A x ≤ y)) 

Theorem  nn01to3 8328 
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13Sep2018.)

⊢ ((𝑁 ∈
ℕ_{0} ∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨
𝑁 = 2 ∨ 𝑁 = 3)) 

Theorem  nn0ge2m1nnALT 8329 
Alternate proof of nn0ge2m1nn 8018: 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 8255, 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 8018. (Contributed by Alexander van der Vekens,
1Aug2018.)
(New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝑁 ∈
ℕ_{0} ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ) 

3.4.11 Rational numbers (as a subset of complex
numbers)


Syntax  cq 8330 
Extend class notation to include the class of rationals.

class ℚ 

Definition  dfq 8331 
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 8333
for the relation "is rational." (Contributed
by NM, 8Jan2002.)

⊢ ℚ = ( / “ (ℤ ×
ℕ)) 

Theorem  divfnzn 8332 
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, 19Mar2020.)

⊢ ( / ↾ (ℤ × ℕ)) Fn
(ℤ × ℕ) 

Theorem  elq 8333* 
Membership in the set of rationals. (Contributed by NM, 8Jan2002.)
(Revised by Mario Carneiro, 28Jan2014.)

⊢ (A ∈ ℚ ↔ ∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)) 

Theorem  qmulz 8334* 
If A is rational,
then some integer multiple of it is an integer.
(Contributed by NM, 7Nov2008.) (Revised by Mario Carneiro,
22Jul2014.)

⊢ (A ∈ ℚ → ∃x ∈ ℕ (A
· x) ∈ ℤ) 

Theorem  znq 8335 
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12Jan2002.)

⊢ ((A ∈ ℤ ∧
B ∈
ℕ) → (A / B) ∈
ℚ) 

Theorem  qre 8336 
A rational number is a real number. (Contributed by NM,
14Nov2002.)

⊢ (A ∈ ℚ → A ∈
ℝ) 

Theorem  zq 8337 
An integer is a rational number. (Contributed by NM, 9Jan2002.)

⊢ (A ∈ ℤ → A ∈
ℚ) 

Theorem  zssq 8338 
The integers are a subset of the rationals. (Contributed by NM,
9Jan2002.)

⊢ ℤ ⊆ ℚ 

Theorem  nn0ssq 8339 
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31Jul2004.)

⊢ ℕ_{0} ⊆
ℚ 

Theorem  nnssq 8340 
The positive integers are a subset of the rationals. (Contributed by NM,
31Jul2004.)

⊢ ℕ ⊆ ℚ 

Theorem  qssre 8341 
The rationals are a subset of the reals. (Contributed by NM,
9Jan2002.)

⊢ ℚ ⊆ ℝ 

Theorem  qsscn 8342 
The rationals are a subset of the complex numbers. (Contributed by NM,
2Aug2004.)

⊢ ℚ ⊆ ℂ 

Theorem  qex 8343 
The set of rational numbers exists. (Contributed by NM, 30Jul2004.)
(Revised by Mario Carneiro, 17Nov2014.)

⊢ ℚ ∈
V 

Theorem  nnq 8344 
A positive integer is rational. (Contributed by NM, 17Nov2004.)

⊢ (A ∈ ℕ → A ∈
ℚ) 

Theorem  qcn 8345 
A rational number is a complex number. (Contributed by NM,
2Aug2004.)

⊢ (A ∈ ℚ → A ∈
ℂ) 

Theorem  qaddcl 8346 
Closure of addition of rationals. (Contributed by NM, 1Aug2004.)

⊢ ((A ∈ ℚ ∧
B ∈
ℚ) → (A + B) ∈
ℚ) 

Theorem  qnegcl 8347 
Closure law for the negative of a rational. (Contributed by NM,
2Aug2004.) (Revised by Mario Carneiro, 15Sep2014.)

⊢ (A ∈ ℚ → A ∈
ℚ) 

Theorem  qmulcl 8348 
Closure of multiplication of rationals. (Contributed by NM,
1Aug2004.)

⊢ ((A ∈ ℚ ∧
B ∈
ℚ) → (A · B) ∈
ℚ) 

Theorem  qsubcl 8349 
Closure of subtraction of rationals. (Contributed by NM, 2Aug2004.)

⊢ ((A ∈ ℚ ∧
B ∈
ℚ) → (A − B) ∈
ℚ) 

Theorem  qapne 8350 
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20Mar2020.)

⊢ ((A ∈ ℚ ∧
B ∈
ℚ) → (A # B ↔ A ≠
B)) 

Theorem  qreccl 8351 
Closure of reciprocal of rationals. (Contributed by NM, 3Aug2004.)

⊢ ((A ∈ ℚ ∧
A ≠ 0) → (1 / A) ∈
ℚ) 

Theorem  qdivcl 8352 
Closure of division of rationals. (Contributed by NM, 3Aug2004.)

⊢ ((A ∈ ℚ ∧
B ∈
ℚ ∧ B ≠ 0) → (A / B) ∈ ℚ) 

Theorem  qrevaddcl 8353 
Reverse closure law for addition of rationals. (Contributed by NM,
2Aug2004.)

⊢ (B ∈ ℚ → ((A ∈ ℂ ∧ (A + B) ∈ ℚ)
↔ A ∈ ℚ)) 

Theorem  nnrecq 8354 
The reciprocal of a positive integer is rational. (Contributed by NM,
17Nov2004.)

⊢ (A ∈ ℕ → (1 / A) ∈
ℚ) 

Theorem  irradd 8355 
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7Nov2008.)

⊢ ((A ∈ (ℝ ∖ ℚ) ∧ B ∈ ℚ) → (A + B) ∈ (ℝ ∖ ℚ)) 

Theorem  irrmul 8356 
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, 7Nov2008.)

⊢ ((A ∈ (ℝ ∖ ℚ) ∧ B ∈ ℚ ∧
B ≠ 0) → (A · B)
∈ (ℝ ∖
ℚ)) 

3.4.12 Complex numbers as pairs of
reals


Theorem  cnref1o 8357* 
There is a natural onetoone mapping from (ℝ ×
ℝ) to ℂ,
where we map ⟨x, y⟩ to (x + (i · y)). In our
construction of the complex numbers, this is in fact our
definition of
ℂ (see dfc 6717), but in the axiomatic treatment we can only
show
that there is the expected mapping between these two sets. (Contributed
by Mario Carneiro, 16Jun2013.) (Revised by Mario Carneiro,
17Feb2014.)

⊢ 𝐹 = (x
∈ ℝ, y ∈ ℝ
↦ (x + (i · y))) ⇒ ⊢ 𝐹:(ℝ × ℝ)–11onto→ℂ 

3.5 Order sets


3.5.1 Positive reals (as a subset of complex
numbers)


Syntax  crp 8358 
Extend class notation to include the class of positive reals.

class ℝ^{+} 

Definition  dfrp 8359 
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27Oct2007.)

⊢ ℝ^{+} = {x ∈ ℝ
∣ 0 < x} 

Theorem  elrp 8360 
Membership in the set of positive reals. (Contributed by NM,
27Oct2007.)

⊢ (A ∈ ℝ^{+} ↔ (A ∈ ℝ ∧ 0 < A)) 

Theorem  elrpii 8361 
Membership in the set of positive reals. (Contributed by NM,
23Feb2008.)

⊢ A ∈ ℝ & ⊢ 0 <
A ⇒ ⊢ A ∈
ℝ^{+} 

Theorem  1rp 8362 
1 is a positive real. (Contributed by Jeff Hankins, 23Nov2008.)

⊢ 1 ∈
ℝ^{+} 

Theorem  2rp 8363 
2 is a positive real. (Contributed by Mario Carneiro, 28May2016.)

⊢ 2 ∈
ℝ^{+} 

Theorem  rpre 8364 
A positive real is a real. (Contributed by NM, 27Oct2007.)

⊢ (A ∈ ℝ^{+} → A ∈
ℝ) 

Theorem  rpxr 8365 
A positive real is an extended real. (Contributed by Mario Carneiro,
21Aug2015.)

⊢ (A ∈ ℝ^{+} → A ∈
ℝ^{*}) 

Theorem  rpcn 8366 
A positive real is a complex number. (Contributed by NM, 11Nov2008.)

⊢ (A ∈ ℝ^{+} → A ∈
ℂ) 

Theorem  nnrp 8367 
A positive integer is a positive real. (Contributed by NM,
28Nov2008.)

⊢ (A ∈ ℕ → A ∈
ℝ^{+}) 

Theorem  rpssre 8368 
The positive reals are a subset of the reals. (Contributed by NM,
24Feb2008.)

⊢ ℝ^{+} ⊆
ℝ 

Theorem  rpgt0 8369 
A positive real is greater than zero. (Contributed by FL,
27Dec2007.)

⊢ (A ∈ ℝ^{+} → 0 < A) 

Theorem  rpge0 8370 
A positive real is greater than or equal to zero. (Contributed by NM,
22Feb2008.)

⊢ (A ∈ ℝ^{+} → 0 ≤ A) 

Theorem  rpregt0 8371 
A positive real is a positive real number. (Contributed by NM,
11Nov2008.) (Revised by Mario Carneiro, 31Jan2014.)

⊢ (A ∈ ℝ^{+} → (A ∈ ℝ ∧ 0 < A)) 

Theorem  rprege0 8372 
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31Jan2014.)

⊢ (A ∈ ℝ^{+} → (A ∈ ℝ ∧ 0 ≤ A)) 

Theorem  rpne0 8373 
A positive real is nonzero. (Contributed by NM, 18Jul2008.)

⊢ (A ∈ ℝ^{+} → A ≠ 0) 

Theorem  rpap0 8374 
A positive real is apart from zero. (Contributed by Jim Kingdon,
22Mar2020.)

⊢ (A ∈ ℝ^{+} → A # 0) 

Theorem  rprene0 8375 
A positive real is a nonzero real number. (Contributed by NM,
11Nov2008.)

⊢ (A ∈ ℝ^{+} → (A ∈ ℝ ∧ A ≠
0)) 

Theorem  rpreap0 8376 
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22Mar2020.)

⊢ (A ∈ ℝ^{+} → (A ∈ ℝ ∧ A #
0)) 

Theorem  rpcnne0 8377 
A positive real is a nonzero complex number. (Contributed by NM,
11Nov2008.)

⊢ (A ∈ ℝ^{+} → (A ∈ ℂ ∧ A ≠
0)) 

Theorem  rpcnap0 8378 
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22Mar2020.)

⊢ (A ∈ ℝ^{+} → (A ∈ ℂ ∧ A #
0)) 

Theorem  ralrp 8379 
Quantification over positive reals. (Contributed by NM, 12Feb2008.)

⊢ (∀x ∈
ℝ^{+} φ ↔ ∀x ∈ ℝ (0 < x → φ)) 

Theorem  rexrp 8380 
Quantification over positive reals. (Contributed by Mario Carneiro,
21May2014.)

⊢ (∃x ∈
ℝ^{+} φ ↔ ∃x ∈ ℝ (0 < x ∧ φ)) 

Theorem  rpaddcl 8381 
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27Oct2007.)

⊢ ((A ∈ ℝ^{+} ∧ B ∈ ℝ^{+}) → (A + B) ∈ ℝ^{+}) 

Theorem  rpmulcl 8382 
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27Oct2007.)

⊢ ((A ∈ ℝ^{+} ∧ B ∈ ℝ^{+}) → (A · B)
∈ ℝ^{+}) 

Theorem  rpdivcl 8383 
Closure law for division of positive reals. (Contributed by FL,
27Dec2007.)

⊢ ((A ∈ ℝ^{+} ∧ B ∈ ℝ^{+}) → (A / B) ∈ ℝ^{+}) 

Theorem  rpreccl 8384 
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23Nov2008.)

⊢ (A ∈ ℝ^{+} → (1 / A) ∈
ℝ^{+}) 

Theorem  rphalfcl 8385 
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31Jan2014.)

⊢ (A ∈ ℝ^{+} → (A / 2) ∈
ℝ^{+}) 

Theorem  rpgecl 8386 
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28May2016.)

⊢ ((A ∈ ℝ^{+} ∧ B ∈ ℝ ∧
A ≤ B) → B
∈ ℝ^{+}) 

Theorem  rphalflt 8387 
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21May2014.)

⊢ (A ∈ ℝ^{+} → (A / 2) < A) 

Theorem  rerpdivcl 8388 
Closure law for division of a real by a positive real. (Contributed by
NM, 10Nov2008.)

⊢ ((A ∈ ℝ ∧
B ∈
ℝ^{+}) → (A / B) ∈
ℝ) 

Theorem  ge0p1rp 8389 
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5Oct2015.)

⊢ ((A ∈ ℝ ∧ 0
≤ A) → (A + 1) ∈
ℝ^{+}) 

Theorem  rpnegap 8390 
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23Mar2020.)

⊢ ((A ∈ ℝ ∧
A # 0) → (A ∈
ℝ^{+} ⊻ A ∈ ℝ^{+})) 

Theorem  0nrp 8391 
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27Oct2007.)

⊢ ¬ 0 ∈
ℝ^{+} 

Theorem  ltsubrp 8392 
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27Dec2007.)

⊢ ((A ∈ ℝ ∧
B ∈
ℝ^{+}) → (A −
B) < A) 

Theorem  ltaddrp 8393 
Adding a positive number to another number increases it. (Contributed by
FL, 27Dec2007.)

⊢ ((A ∈ ℝ ∧
B ∈
ℝ^{+}) → A <
(A + B)) 

Theorem  difrp 8394 
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21May2014.)

⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A < B ↔ (B
− A) ∈ ℝ^{+})) 

Theorem  elrpd 8395 
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28May2016.)

⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → 0 < A) ⇒ ⊢ (φ → A ∈
ℝ^{+}) 

Theorem  nnrpd 8396 
A positive integer is a positive real. (Contributed by Mario Carneiro,
28May2016.)

⊢ (φ
→ A ∈ ℕ) ⇒ ⊢ (φ → A ∈
ℝ^{+}) 

Theorem  rpred 8397 
A positive real is a real. (Contributed by Mario Carneiro,
28May2016.)

⊢ (φ
→ A ∈ ℝ^{+})
⇒ ⊢ (φ → A ∈
ℝ) 

Theorem  rpxrd 8398 
A positive real is an extended real. (Contributed by Mario Carneiro,
28May2016.)

⊢ (φ
→ A ∈ ℝ^{+})
⇒ ⊢ (φ → A ∈
ℝ^{*}) 

Theorem  rpcnd 8399 
A positive real is a complex number. (Contributed by Mario Carneiro,
28May2016.)

⊢ (φ
→ A ∈ ℝ^{+})
⇒ ⊢ (φ → A ∈
ℂ) 

Theorem  rpgt0d 8400 
A positive real is greater than zero. (Contributed by Mario Carneiro,
28May2016.)

⊢ (φ
→ A ∈ ℝ^{+})
⇒ ⊢ (φ → 0 < A) 