Theorem List for Intuitionistic Logic Explorer - 9501-9600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rpdivcld 9501 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈
ℝ+) |
|
Theorem | ltrecd 9502 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) |
|
Theorem | lerecd 9503 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) |
|
Theorem | ltrec1d 9504 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (1 / 𝐴) < 𝐵) ⇒ ⊢ (𝜑 → (1 / 𝐵) < 𝐴) |
|
Theorem | lerec2d 9505 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≤ (1 / 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 ≤ (1 / 𝐴)) |
|
Theorem | lediv2ad 9506 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)) |
|
Theorem | ltdiv2d 9507 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) |
|
Theorem | lediv2d 9508 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) |
|
Theorem | ledivdivd 9509 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ (𝐶 / 𝐷)) ⇒ ⊢ (𝜑 → (𝐷 / 𝐶) ≤ (𝐵 / 𝐴)) |
|
Theorem | divge1 9510 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 1 ≤ (𝐵 / 𝐴)) |
|
Theorem | divlt1lt 9511 |
A real number divided by a positive real number is less than 1 iff the
real number is less than the positive real number. (Contributed by AV,
25-May-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < 𝐵)) |
|
Theorem | divle1le 9512 |
A real number divided by a positive real number is less than or equal to 1
iff the real number is less than or equal to the positive real number.
(Contributed by AV, 29-Jun-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) ≤ 1 ↔ 𝐴 ≤ 𝐵)) |
|
Theorem | ledivge1le 9513 |
If a number is less than or equal to another number, the number divided by
a positive number greater than or equal to one is less than or equal to
the other number. (Contributed by AV, 29-Jun-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+
∧ 1 ≤ 𝐶)) →
(𝐴 ≤ 𝐵 → (𝐴 / 𝐶) ≤ 𝐵)) |
|
Theorem | ge0p1rpd 9514 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 + 1) ∈
ℝ+) |
|
Theorem | rerpdivcld 9515 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) |
|
Theorem | ltsubrpd 9516 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) < 𝐴) |
|
Theorem | ltaddrpd 9517 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵)) |
|
Theorem | ltaddrp2d 9518 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐴)) |
|
Theorem | ltmulgt11d 9519 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴))) |
|
Theorem | ltmulgt12d 9520 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐴 · 𝐵))) |
|
Theorem | gt0divd 9521 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵))) |
|
Theorem | ge0divd 9522 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) |
|
Theorem | rpgecld 9523 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈
ℝ+) |
|
Theorem | divge0d 9524 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵)) |
|
Theorem | ltmul1d 9525 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) |
|
Theorem | ltmul2d 9526 |
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.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) |
|
Theorem | lemul1d 9527 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) |
|
Theorem | lemul2d 9528 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) |
|
Theorem | ltdiv1d 9529 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) |
|
Theorem | lediv1d 9530 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))) |
|
Theorem | ltmuldivd 9531 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | ltmuldiv2d 9532 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | lemuldivd 9533 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) |
|
Theorem | lemuldiv2d 9534 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) |
|
Theorem | ltdivmuld 9535 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) |
|
Theorem | ltdivmul2d 9536 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) |
|
Theorem | ledivmuld 9537 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵))) |
|
Theorem | ledivmul2d 9538 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶))) |
|
Theorem | ltmul1dd 9539 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶)) |
|
Theorem | ltmul2dd 9540 |
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.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · 𝐴) < (𝐶 · 𝐵)) |
|
Theorem | ltdiv1dd 9541 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶)) |
|
Theorem | lediv1dd 9542 |
Division of both sides of a less than or equal to relation by a
positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) ≤ (𝐵 / 𝐶)) |
|
Theorem | lediv12ad 9543 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) |
|
Theorem | ltdiv23d 9544 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵) |
|
Theorem | lediv23d 9545 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵) |
|
Theorem | mul2lt0rlt0 9546 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < 𝐴) |
|
Theorem | mul2lt0rgt0 9547 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0) |
|
Theorem | mul2lt0llt0 9548 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 𝐵) |
|
Theorem | mul2lt0lgt0 9549 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
2-Oct-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) < 0) ⇒ ⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐵 < 0) |
|
Theorem | mul2lt0np 9550 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) < 0) |
|
Theorem | mul2lt0pn 9551 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) < 0) |
|
Theorem | lt2mul2divd 9552 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈
ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) |
|
Theorem | nnledivrp 9553 |
Division of a positive integer by a positive number is less than or equal
to the integer iff the number is greater than or equal to 1. (Contributed
by AV, 19-Jun-2021.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → (1 ≤
𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐴)) |
|
Theorem | nn0ledivnn 9554 |
Division of a nonnegative integer by a positive integer is less than or
equal to the integer. (Contributed by AV, 19-Jun-2021.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≤ 𝐴) |
|
Theorem | addlelt 9555 |
If the sum of a real number and a positive real number is less than or
equal to a third real number, the first real number is less than the third
real number. (Contributed by AV, 1-Jul-2021.)
|
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁 → 𝑀 < 𝑁)) |
|
4.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 9556 |
Extend class notation to include the negative of an extended real.
|
class -𝑒𝐴 |
|
Syntax | cxad 9557 |
Extend class notation to include addition of extended reals.
|
class +𝑒 |
|
Syntax | cxmu 9558 |
Extend class notation to include multiplication of extended reals.
|
class ·e |
|
Definition | df-xneg 9559 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) |
|
Definition | df-xadd 9560* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if(𝑥 = +∞,
if(𝑦 = -∞, 0,
+∞), if(𝑥 =
-∞, if(𝑦 = +∞,
0, -∞), if(𝑦 =
+∞, +∞, if(𝑦 =
-∞, -∞, (𝑥 +
𝑦)))))) |
|
Definition | df-xmul 9561* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if((𝑥 = 0 ∨
𝑦 = 0), 0, if((((0 <
𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦))))) |
|
Theorem | ltxr 9562 |
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.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))))) |
|
Theorem | elxr 9563 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
|
Theorem | xrnemnf 9564 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
|
Theorem | xrnepnf 9565 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞)) |
|
Theorem | xrltnr 9566 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 < 𝐴) |
|
Theorem | ltpnf 9567 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
|
Theorem | 0ltpnf 9568 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 < +∞ |
|
Theorem | mnflt 9569 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) |
|
Theorem | mnflt0 9570 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ -∞ < 0 |
|
Theorem | mnfltpnf 9571 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
⊢ -∞ < +∞ |
|
Theorem | mnfltxr 9572 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴) |
|
Theorem | pnfnlt 9573 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
+∞ < 𝐴) |
|
Theorem | nltmnf 9574 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
⊢ (𝐴 ∈ ℝ* → ¬
𝐴 <
-∞) |
|
Theorem | pnfge 9575 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤
+∞) |
|
Theorem | 0lepnf 9576 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 0 ≤ +∞ |
|
Theorem | nn0pnfge0 9577 |
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 9578 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → -∞
≤ 𝐴) |
|
Theorem | xrltnsym 9579 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
|
Theorem | xrltnsym2 9580 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | xrlttr 9581 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltso 9582 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
⊢ < Or
ℝ* |
|
Theorem | xrlttri3 9583 |
Extended real version of lttri3 7844. (Contributed by NM, 9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | xrltle 9584 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
|
Theorem | xrltled 9585 |
'Less than' implies 'less than or equal to' for extended reals.
Deduction form of xrltle 9584. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | xrleid 9586 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) |
|
Theorem | xrleidd 9587 |
'Less than or equal to' is reflexive for extended reals. Deduction form
of xrleid 9586. (Contributed by Glauco Siliprandi,
26-Jun-2021.)
|
⊢ (𝜑 → 𝐴 ∈
ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) |
|
Theorem | xrletri3 9588 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | xrlelttr 9589 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrltletr 9590 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | xrletr 9591 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | xrlttrd 9592 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrlelttrd 9593 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrltletrd 9594 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | xrletrd 9595 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | xrltne 9596 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) |
|
Theorem | nltpnft 9597 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 <
+∞)) |
|
Theorem | npnflt 9598 |
An extended real is less than plus infinity iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 < +∞ ↔ 𝐴 ≠
+∞)) |
|
Theorem | xgepnf 9599 |
An extended real which is greater than plus infinity is plus infinity.
(Contributed by Thierry Arnoux, 18-Dec-2016.)
|
⊢ (𝐴 ∈ ℝ* →
(+∞ ≤ 𝐴 ↔
𝐴 =
+∞)) |
|
Theorem | ngtmnft 9600 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬
-∞ < 𝐴)) |