Theorem List for Intuitionistic Logic Explorer - 8401-8500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rpge0d 8401 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → 0 ≤ A) |
|
Theorem | rpne0d 8402 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → A ≠ 0) |
|
Theorem | rpregt0d 8403 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (A ∈ ℝ ∧ 0 < A)) |
|
Theorem | rprege0d 8404 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (A ∈ ℝ ∧ 0 ≤ A)) |
|
Theorem | rprene0d 8405 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (A ∈ ℝ ∧ A ≠
0)) |
|
Theorem | rpcnne0d 8406 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (A ∈ ℂ ∧ A ≠
0)) |
|
Theorem | rpreccld 8407 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (1 / A) ∈
ℝ+) |
|
Theorem | rprecred 8408 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (1 / A) ∈
ℝ) |
|
Theorem | rphalfcld 8409 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (A / 2) ∈
ℝ+) |
|
Theorem | reclt1d 8410 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (A < 1 ↔ 1 < (1 / A))) |
|
Theorem | recgt1d 8411 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+)
⇒ ⊢ (φ → (1 < A ↔ (1 / A) < 1)) |
|
Theorem | rpaddcld 8412 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A + B) ∈ ℝ+) |
|
Theorem | rpmulcld 8413 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A · B)
∈ ℝ+) |
|
Theorem | rpdivcld 8414 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A / B) ∈ ℝ+) |
|
Theorem | ltrecd 8415 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A < B ↔
(1 / B) < (1 / A))) |
|
Theorem | lerecd 8416 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A ≤ B ↔
(1 / B) ≤ (1 / A))) |
|
Theorem | ltrec1d 8417 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ (1 / A) < B) ⇒ ⊢ (φ → (1 / B) < A) |
|
Theorem | lerec2d 8418 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ A ≤ (1 / B)) ⇒ ⊢ (φ → B ≤ (1 / A)) |
|
Theorem | lediv2ad 8419 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ) & ⊢ (φ → 0 ≤ 𝐶)
& ⊢ (φ
→ A ≤ B) ⇒ ⊢ (φ → (𝐶 / B)
≤ (𝐶 / A)) |
|
Theorem | ltdiv2d 8420 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A < B ↔
(𝐶 / B) < (𝐶 / A))) |
|
Theorem | lediv2d 8421 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A ≤ B ↔
(𝐶 / B) ≤ (𝐶 / A))) |
|
Theorem | ledivdivd 8422 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ+) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → 𝐷 ∈
ℝ+)
& ⊢ (φ
→ (A / B) ≤ (𝐶 / 𝐷)) ⇒ ⊢ (φ → (𝐷 / 𝐶) ≤ (B / A)) |
|
Theorem | ge0p1rpd 8423 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → 0 ≤ A) ⇒ ⊢ (φ → (A + 1) ∈
ℝ+) |
|
Theorem | rerpdivcld 8424 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A / B) ∈ ℝ) |
|
Theorem | ltsubrpd 8425 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (A − B)
< A) |
|
Theorem | ltaddrpd 8426 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → A < (A +
B)) |
|
Theorem | ltaddrp2d 8427 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → A < (B +
A)) |
|
Theorem | ltmulgt11d 8428 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (1 < A ↔ B <
(B · A))) |
|
Theorem | ltmulgt12d 8429 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (1 < A ↔ B <
(A · B))) |
|
Theorem | gt0divd 8430 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (0 < A ↔ 0 < (A / B))) |
|
Theorem | ge0divd 8431 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+) ⇒ ⊢ (φ → (0 ≤ A ↔ 0 ≤ (A / B))) |
|
Theorem | rpgecld 8432 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ B ≤ A) ⇒ ⊢ (φ → A ∈
ℝ+) |
|
Theorem | divge0d 8433 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 0 ≤ A)
⇒ ⊢ (φ → 0 ≤ (A / B)) |
|
Theorem | ltmul1d 8434 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A < B ↔
(A · 𝐶) < (B · 𝐶))) |
|
Theorem | ltmul2d 8435 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A < B ↔
(𝐶 · A) < (𝐶 · B))) |
|
Theorem | lemul1d 8436 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A ≤ B ↔
(A · 𝐶) ≤ (B · 𝐶))) |
|
Theorem | lemul2d 8437 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A ≤ B ↔
(𝐶 · A) ≤ (𝐶 · B))) |
|
Theorem | ltdiv1d 8438 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A < B ↔
(A / 𝐶) < (B / 𝐶))) |
|
Theorem | lediv1d 8439 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → (A ≤ B ↔
(A / 𝐶) ≤ (B / 𝐶))) |
|
Theorem | ltmuldivd 8440 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((A · 𝐶) < B ↔ A <
(B / 𝐶))) |
|
Theorem | ltmuldiv2d 8441 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((𝐶 · A) < B
↔ A < (B / 𝐶))) |
|
Theorem | lemuldivd 8442 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((A · 𝐶) ≤ B ↔ A ≤
(B / 𝐶))) |
|
Theorem | lemuldiv2d 8443 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((𝐶 · A) ≤ B
↔ A ≤ (B / 𝐶))) |
|
Theorem | ltdivmuld 8444 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((A / 𝐶) < B ↔ A <
(𝐶 · B))) |
|
Theorem | ltdivmul2d 8445 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((A / 𝐶) < B ↔ A <
(B · 𝐶))) |
|
Theorem | ledivmuld 8446 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((A / 𝐶) ≤ B ↔ A ≤
(𝐶 · B))) |
|
Theorem | ledivmul2d 8447 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+)
⇒ ⊢ (φ → ((A / 𝐶) ≤ B ↔ A ≤
(B · 𝐶))) |
|
Theorem | ltmul1dd 8448 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → A < B) ⇒ ⊢ (φ → (A · 𝐶) < (B · 𝐶)) |
|
Theorem | ltmul2dd 8449 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
30-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → A < B) ⇒ ⊢ (φ → (𝐶 · A) < (𝐶 · B)) |
|
Theorem | ltdiv1dd 8450 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → A < B) ⇒ ⊢ (φ → (A / 𝐶) < (B / 𝐶)) |
|
Theorem | lediv1dd 8451 |
Division of both sides of a less than or equal to relation by a
positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → A ≤ B) ⇒ ⊢ (φ → (A / 𝐶) ≤ (B / 𝐶)) |
|
Theorem | lediv12ad 8452 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → 𝐷 ∈
ℝ)
& ⊢ (φ
→ 0 ≤ A) & ⊢ (φ → A ≤ B)
& ⊢ (φ
→ 𝐶 ≤ 𝐷)
⇒ ⊢ (φ → (A / 𝐷) ≤ (B / 𝐶)) |
|
Theorem | ltdiv23d 8453 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → (A / B) <
𝐶) ⇒ ⊢ (φ → (A / 𝐶) < B) |
|
Theorem | lediv23d 8454 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ+) & ⊢ (φ → (A / B) ≤
𝐶) ⇒ ⊢ (φ → (A / 𝐶) ≤ B) |
|
Theorem | lt2mul2divd 8455 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ+)
& ⊢ (φ
→ 𝐶 ∈ ℝ) & ⊢ (φ → 𝐷 ∈
ℝ+) ⇒ ⊢ (φ → ((A · B)
< (𝐶 · 𝐷) ↔ (A / 𝐷) < (𝐶 / B))) |
|
3.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 8456 |
Extend class notation to include the negative of an extended real.
|
class -𝑒A |
|
Syntax | cxad 8457 |
Extend class notation to include addition of extended reals.
|
class +𝑒 |
|
Syntax | cxmu 8458 |
Extend class notation to include multiplication of extended reals.
|
class ·e |
|
Definition | df-xneg 8459 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒A = if(A =
+∞, -∞, if(A = -∞,
+∞, -A)) |
|
Definition | df-xadd 8460* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ +𝑒 = (x ∈
ℝ*, y ∈ ℝ* ↦ if(x = +∞, if(y = -∞, 0, +∞), if(x = -∞, if(y = +∞, 0, -∞), if(y = +∞, +∞, if(y = -∞, -∞, (x + y)))))) |
|
Definition | df-xmul 8461* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ·e = (x ∈
ℝ*, y ∈ ℝ* ↦ if((x = 0 ∨ y = 0), 0, if((((0 < y ∧ x = +∞) ∨
(y < 0 ∧ x =
-∞)) ∨ ((0 < x ∧ y = +∞) ∨
(x < 0 ∧ y =
-∞))), +∞, if((((0 < y
∧ x =
-∞) ∨ (y < 0 ∧
x = +∞))
∨ ((0 < x ∧ y = -∞)
∨ (x <
0 ∧ y =
+∞))), -∞, (x ·
y))))) |
|
Theorem | pnfxr 8462 |
Plus infinity belongs to the set of extended reals. (Contributed by NM,
13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
|
⊢ +∞ ∈
ℝ* |
|
Theorem | pnfex 8463 |
Plus infinity exists (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ +∞ ∈
V |
|
Theorem | mnfxr 8464 |
Minus infinity belongs to the set of extended reals. (Contributed by NM,
13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof
shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ -∞ ∈
ℝ* |
|
Theorem | ltxr 8465 |
The 'less than' binary relation on the set of extended reals.
Definition 12-3.1 of [Gleason] p. 173.
(Contributed by NM,
14-Oct-2005.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔
((((A ∈
ℝ ∧ B ∈ ℝ)
∧ A
<ℝ B) ∨ (A = -∞
∧ B =
+∞)) ∨ ((A ∈ ℝ ∧ B = +∞)
∨ (A =
-∞ ∧ B ∈
ℝ))))) |
|
Theorem | elxr 8466 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
⊢ (A ∈ ℝ* ↔ (A ∈ ℝ ∨ A = +∞
∨ A =
-∞)) |
|
Theorem | pnfnemnf 8467 |
Plus and minus infinity are different elements of ℝ*. (Contributed
by NM, 14-Oct-2005.)
|
⊢ +∞ ≠ -∞ |
|
Theorem | mnfnepnf 8468 |
Minus and plus infinity are different (common case). (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
⊢ -∞ ≠ +∞ |
|
Theorem | xrnemnf 8469 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ A ≠
-∞) ↔ (A ∈ ℝ ∨
A = +∞)) |
|
Theorem | xrnepnf 8470 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((A ∈ ℝ* ∧ A ≠
+∞) ↔ (A ∈ ℝ ∨
A = -∞)) |
|
Theorem | xrltnr 8471 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
⊢ (A ∈ ℝ* → ¬ A < A) |
|
Theorem | ltpnf 8472 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ (A ∈ ℝ → A < +∞) |
|
Theorem | 0ltpnf 8473 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 < +∞ |
|
Theorem | mnflt 8474 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
⊢ (A ∈ ℝ → -∞ < A) |
|
Theorem | mnflt0 8475 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ -∞ < 0 |
|
Theorem | mnfltpnf 8476 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ -∞ < +∞ |
|
Theorem | mnfltxr 8477 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
⊢ ((A ∈ ℝ ∨
A = +∞) → -∞ <
A) |
|
Theorem | pnfnlt 8478 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (A ∈ ℝ* → ¬ +∞ <
A) |
|
Theorem | nltmnf 8479 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (A ∈ ℝ* → ¬ A < -∞) |
|
Theorem | pnfge 8480 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
⊢ (A ∈ ℝ* → A ≤ +∞) |
|
Theorem | 0lepnf 8481 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 ≤ +∞ |
|
Theorem | nn0pnfge0 8482 |
If a number is a nonnegative integer or positive infinity, it is greater
than or equal to 0. (Contributed by Alexander van der Vekens,
6-Jan-2018.)
|
⊢ ((𝑁 ∈
ℕ0 ∨ 𝑁 = +∞) → 0 ≤ 𝑁) |
|
Theorem | mnfle 8483 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
⊢ (A ∈ ℝ* → -∞ ≤
A) |
|
Theorem | xrltnsym 8484 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B →
¬ B < A)) |
|
Theorem | xrltnsym2 8485 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ (A < B ∧ B <
A)) |
|
Theorem | xrlttr 8486 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → ((A <
B ∧
B < 𝐶) → A < 𝐶)) |
|
Theorem | xrltso 8487 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
⊢ < Or ℝ* |
|
Theorem | xrlttri3 8488 |
Extended real version of lttri3 6895. (Contributed by NM, 9-Feb-2006.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔
(¬ A < B ∧ ¬ B < A))) |
|
Theorem | xrltle 8489 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B →
A ≤ B)) |
|
Theorem | xrleid 8490 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
⊢ (A ∈ ℝ* → A ≤ A) |
|
Theorem | xrletri3 8491 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔
(A ≤ B ∧ B ≤ A))) |
|
Theorem | xrlelttr 8492 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → ((A ≤
B ∧
B < 𝐶) → A < 𝐶)) |
|
Theorem | xrltletr 8493 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → ((A <
B ∧
B ≤ 𝐶) → A < 𝐶)) |
|
Theorem | xrletr 8494 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈
ℝ*) → ((A ≤
B ∧
B ≤ 𝐶) → A ≤ 𝐶)) |
|
Theorem | xrlttrd 8495 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (φ
→ A ∈ ℝ*) & ⊢ (φ → B ∈
ℝ*)
& ⊢ (φ
→ 𝐶 ∈ ℝ*) & ⊢ (φ → A < B)
& ⊢ (φ
→ B < 𝐶) ⇒ ⊢ (φ → A < 𝐶) |
|
Theorem | xrlelttrd 8496 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (φ
→ A ∈ ℝ*) & ⊢ (φ → B ∈
ℝ*)
& ⊢ (φ
→ 𝐶 ∈ ℝ*) & ⊢ (φ → A ≤ B)
& ⊢ (φ
→ B < 𝐶) ⇒ ⊢ (φ → A < 𝐶) |
|
Theorem | xrltletrd 8497 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (φ
→ A ∈ ℝ*) & ⊢ (φ → B ∈
ℝ*)
& ⊢ (φ
→ 𝐶 ∈ ℝ*) & ⊢ (φ → A < B)
& ⊢ (φ
→ B ≤ 𝐶) ⇒ ⊢ (φ → A < 𝐶) |
|
Theorem | xrletrd 8498 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (φ
→ A ∈ ℝ*) & ⊢ (φ → B ∈
ℝ*)
& ⊢ (φ
→ 𝐶 ∈ ℝ*) & ⊢ (φ → A ≤ B)
& ⊢ (φ
→ B ≤ 𝐶) ⇒ ⊢ (φ → A ≤ 𝐶) |
|
Theorem | xrltne 8499 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A <
B) → B ≠ A) |
|
Theorem | nltpnft 8500 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
⊢ (A ∈ ℝ* → (A = +∞ ↔ ¬ A < +∞)) |