Theorem List for Intuitionistic Logic Explorer - 8401-8500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mvllmulapd 8401 |
Move LHS left multiplication to RHS. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) & ⊢ (𝜑 → (𝐴 · 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 / 𝐴)) |
|
3.3.9 Ordering on reals (cont.)
|
|
Theorem | ltp1 8402 |
A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) |
|
Theorem | lep1 8403 |
A number is less than or equal to itself plus 1. (Contributed by NM,
5-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1)) |
|
Theorem | ltm1 8404 |
A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴) |
|
Theorem | lem1 8405 |
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 2-Oct-2015.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≤ 𝐴) |
|
Theorem | letrp1 8406 |
A transitive property of 'less than or equal' and plus 1. (Contributed by
NM, 5-Aug-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ (𝐵 + 1)) |
|
Theorem | p1le 8407 |
A transitive property of plus 1 and 'less than or equal'. (Contributed by
NM, 16-Aug-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + 1) ≤ 𝐵) → 𝐴 ≤ 𝐵) |
|
Theorem | recgt0 8408 |
The reciprocal of a positive number is positive. Exercise 4 of [Apostol]
p. 21. (Contributed by NM, 25-Aug-1999.) (Revised by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (1 / 𝐴)) |
|
Theorem | prodgt0gt0 8409 |
Infer that a multiplicand is positive from a positive multiplier and
positive product. See prodgt0 8410 for the same theorem with 0 < 𝐴
replaced by the weaker condition 0 ≤ 𝐴. (Contributed by Jim
Kingdon, 29-Feb-2020.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵) |
|
Theorem | prodgt0 8410 |
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 24-Apr-2005.) (Revised by Mario
Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵) |
|
Theorem | prodgt02 8411 |
Infer that a multiplier is positive from a nonnegative multiplicand and
positive product. (Contributed by NM, 24-Apr-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐵 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴) |
|
Theorem | prodge0 8412 |
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario
Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ (𝐴 · 𝐵))) → 0 ≤ 𝐵) |
|
Theorem | prodge02 8413 |
Infer that a multiplier is nonnegative from a positive multiplicand and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐵 ∧ 0 ≤ (𝐴 · 𝐵))) → 0 ≤ 𝐴) |
|
Theorem | ltmul2 8414 |
Multiplication of both sides of 'less than' by a positive number. Theorem
I.19 of [Apostol] p. 20. (Contributed by
NM, 13-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) |
|
Theorem | lemul2 8415 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 16-Mar-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) |
|
Theorem | lemul1a 8416 |
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 21-Feb-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) |
|
Theorem | lemul2a 8417 |
Multiplication of both sides of 'less than or equal to' by a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) |
|
Theorem | ltmul12a 8418 |
Comparison of product of two positive numbers. (Contributed by NM,
30-Dec-2005.)
|
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (𝐴 · 𝐶) < (𝐵 · 𝐷)) |
|
Theorem | lemul12b 8419 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) |
|
Theorem | lemul12a 8420 |
Comparison of product of two nonnegative numbers. (Contributed by NM,
22-Feb-2008.)
|
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ ((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) |
|
Theorem | mulgt1 8421 |
The product of two numbers greater than 1 is greater than 1. (Contributed
by NM, 13-Feb-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵)) |
|
Theorem | ltmulgt11 8422 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐴 · 𝐵))) |
|
Theorem | ltmulgt12 8423 |
Multiplication by a number greater than 1. (Contributed by NM,
24-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐵 · 𝐴))) |
|
Theorem | lemulge11 8424 |
Multiplication by a number greater than or equal to 1. (Contributed by
NM, 17-Dec-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐴 · 𝐵)) |
|
Theorem | lemulge12 8425 |
Multiplication by a number greater than or equal to 1. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐵 · 𝐴)) |
|
Theorem | ltdiv1 8426 |
Division of both sides of 'less than' by a positive number. (Contributed
by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) |
|
Theorem | lediv1 8427 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by NM, 18-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))) |
|
Theorem | gt0div 8428 |
Division of a positive number by a positive number. (Contributed by NM,
28-Sep-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵))) |
|
Theorem | ge0div 8429 |
Division of a nonnegative number by a positive number. (Contributed by
NM, 28-Sep-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) |
|
Theorem | divgt0 8430 |
The ratio of two positive numbers is positive. (Contributed by NM,
12-Oct-1999.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 / 𝐵)) |
|
Theorem | divge0 8431 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 27-Sep-1999.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
|
Theorem | ltmuldiv 8432 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | ltmuldiv2 8433 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | ltdivmul 8434 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 18-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) |
|
Theorem | ledivmul 8435 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵))) |
|
Theorem | ltdivmul2 8436 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 24-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) |
|
Theorem | lt2mul2div 8437 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 8-Jan-2006.)
|
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) |
|
Theorem | ledivmul2 8438 |
'Less than or equal to' relationship between division and multiplication.
(Contributed by NM, 9-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶))) |
|
Theorem | lemuldiv 8439 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) |
|
Theorem | lemuldiv2 8440 |
'Less than or equal' relationship between division and multiplication.
(Contributed by NM, 10-Mar-2006.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) |
|
Theorem | ltrec 8441 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) |
|
Theorem | lerec 8442 |
The reciprocal of both sides of 'less than or equal to'. (Contributed by
NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) |
|
Theorem | lt2msq1 8443 |
Lemma for lt2msq 8444. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴 · 𝐴) < (𝐵 · 𝐵)) |
|
Theorem | lt2msq 8444 |
Two nonnegative numbers compare the same as their squares. (Contributed
by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro,
27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵))) |
|
Theorem | ltdiv2 8445 |
Division of a positive number by both sides of 'less than'. (Contributed
by NM, 27-Apr-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) |
|
Theorem | ltrec1 8446 |
Reciprocal swap in a 'less than' relation. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((1 / 𝐴) < 𝐵 ↔ (1 / 𝐵) < 𝐴)) |
|
Theorem | lerec2 8447 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed by
NM, 24-Feb-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ (1 / 𝐵) ↔ 𝐵 ≤ (1 / 𝐴))) |
|
Theorem | ledivdiv 8448 |
Invert ratios of positive numbers and swap their ordering. (Contributed
by NM, 9-Jan-2006.)
|
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (𝐷 / 𝐶) ≤ (𝐵 / 𝐴))) |
|
Theorem | lediv2 8449 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by NM, 10-Jan-2006.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) |
|
Theorem | ltdiv23 8450 |
Swap denominator with other side of 'less than'. (Contributed by NM,
3-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) |
|
Theorem | lediv23 8451 |
Swap denominator with other side of 'less than or equal to'. (Contributed
by NM, 30-May-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ (𝐴 / 𝐶) ≤ 𝐵)) |
|
Theorem | lediv12a 8452 |
Comparison of ratio of two nonnegative numbers. (Contributed by NM,
31-Dec-2005.)
|
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) |
|
Theorem | lediv2a 8453 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Paul Chapman, 7-Sep-2007.)
|
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)) |
|
Theorem | reclt1 8454 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by NM, 23-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (𝐴 < 1 ↔ 1 < (1 / 𝐴))) |
|
Theorem | recgt1 8455 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by NM, 28-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐴 ↔ (1 / 𝐴) < 1)) |
|
Theorem | recgt1i 8456 |
The reciprocal of a number greater than 1 is positive and less than 1.
(Contributed by NM, 23-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (0 < (1 / 𝐴) ∧ (1 / 𝐴) < 1)) |
|
Theorem | recp1lt1 8457 |
Construct a number less than 1 from any nonnegative number. (Contributed
by NM, 30-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 / (1 + 𝐴)) < 1) |
|
Theorem | recreclt 8458 |
Given a positive number 𝐴, construct a new positive number
less than
both 𝐴 and 1. (Contributed by NM,
28-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ((1 / (1 + (1 / 𝐴))) < 1 ∧ (1 / (1 + (1 /
𝐴))) < 𝐴)) |
|
Theorem | le2msq 8459 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵))) |
|
Theorem | msq11 8460 |
The square of a nonnegative number is a one-to-one function. (Contributed
by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | ledivp1 8461 |
Less-than-or-equal-to and division relation. (Lemma for computing upper
bounds of products. The "+ 1" prevents division by zero.)
(Contributed
by NM, 28-Sep-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ 𝐴) |
|
Theorem | squeeze0 8462* |
If a nonnegative number is less than any positive number, it is zero.
(Contributed by NM, 11-Feb-2006.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0) |
|
Theorem | ltp1i 8463 |
A number is less than itself plus 1. (Contributed by NM,
20-Aug-2001.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ 𝐴 < (𝐴 + 1) |
|
Theorem | recgt0i 8464 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (0 < 𝐴 → 0 < (1 / 𝐴)) |
|
Theorem | recgt0ii 8465 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by NM,
15-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 0 < (1 / 𝐴) |
|
Theorem | prodgt0i 8466 |
Infer that a multiplicand is positive from a nonnegative multiplier and
positive product. (Contributed by NM, 15-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵)) → 0 < 𝐵) |
|
Theorem | prodge0i 8467 |
Infer that a multiplicand is nonnegative from a positive multiplier and
nonnegative product. (Contributed by NM, 2-Jul-2005.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 ≤ (𝐴 · 𝐵)) → 0 ≤ 𝐵) |
|
Theorem | divgt0i 8468 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 / 𝐵)) |
|
Theorem | divge0i 8469 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by NM, 12-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 ≤ (𝐴 / 𝐵)) |
|
Theorem | ltreci 8470 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) |
|
Theorem | lereci 8471 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by NM, 16-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) |
|
Theorem | lt2msqi 8472 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 3-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵))) |
|
Theorem | le2msqi 8473 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵))) |
|
Theorem | msq11i 8474 |
The square of a nonnegative number is a one-to-one function.
(Contributed by NM, 29-Jul-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | divgt0i2i 8475 |
The ratio of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐵 ⇒ ⊢ (0 < 𝐴 → 0 < (𝐴 / 𝐵)) |
|
Theorem | ltrecii 8476 |
The reciprocal of both sides of 'less than'. (Contributed by NM,
15-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)) |
|
Theorem | divgt0ii 8477 |
The ratio of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 / 𝐵) |
|
Theorem | ltmul1i 8478 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) |
|
Theorem | ltdiv1i 8479 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) |
|
Theorem | ltmuldivi 8480 |
'Less than' relationship between division and multiplication.
(Contributed by NM, 12-Oct-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) |
|
Theorem | ltmul2i 8481 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) |
|
Theorem | lemul1i 8482 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) |
|
Theorem | lemul2i 8483 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by NM, 1-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) |
|
Theorem | ltdiv23i 8484 |
Swap denominator with other side of 'less than'. (Contributed by NM,
26-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((0 < 𝐵 ∧ 0 < 𝐶) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) |
|
Theorem | ltdiv23ii 8485 |
Swap denominator with other side of 'less than'. (Contributed by NM,
26-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 0 < 𝐵 & ⊢ 0 < 𝐶 ⇒ ⊢ ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵) |
|
Theorem | ltmul1ii 8486 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by NM, 16-May-1999.)
(Proof shortened by Paul Chapman, 25-Jan-2008.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 0 < 𝐶 ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)) |
|
Theorem | ltdiv1ii 8487 |
Division of both sides of 'less than' by a positive number.
(Contributed by NM, 16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 0 < 𝐶 ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)) |
|
Theorem | ltp1d 8488 |
A number is less than itself plus 1. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 𝐴 < (𝐴 + 1)) |
|
Theorem | lep1d 8489 |
A number is less than or equal to itself plus 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1)) |
|
Theorem | ltm1d 8490 |
A number minus 1 is less than itself. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 − 1) < 𝐴) |
|
Theorem | lem1d 8491 |
A number minus 1 is less than or equal to itself. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 − 1) ≤ 𝐴) |
|
Theorem | recgt0d 8492 |
The reciprocal of a positive number is positive. Exercise 4 of
[Apostol] p. 21. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 0 < (1 / 𝐴)) |
|
Theorem | divgt0d 8493 |
The ratio of two positive numbers is positive. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 / 𝐵)) |
|
Theorem | mulgt1d 8494 |
The product of two numbers greater than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴)
& ⊢ (𝜑 → 1 < 𝐵) ⇒ ⊢ (𝜑 → 1 < (𝐴 · 𝐵)) |
|
Theorem | lemulge11d 8495 |
Multiplication by a number greater than or equal to 1. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 1 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 · 𝐵)) |
|
Theorem | lemulge12d 8496 |
Multiplication by a number greater than or equal to 1. (Contributed
by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 1 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐵 · 𝐴)) |
|
Theorem | lemul1ad 8497 |
Multiplication of both sides of 'less than or equal to' by a
nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) |
|
Theorem | lemul2ad 8498 |
Multiplication of both sides of 'less than or equal to' by a
nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) |
|
Theorem | ltmul12ad 8499 |
Comparison of product of two positive numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 0 ≤ 𝐶)
& ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐷)) |
|
Theorem | lemul12ad 8500 |
Comparison of product of two nonnegative numbers. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 ≤ 𝐶)
& ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)) |