Theorem List for Intuitionistic Logic Explorer - 8001-8100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lelttrdi 8001 |
If a number is less than another number, and the other number is less
than or equal to a third number, the first number is less than the third
number. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
|
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) |
|
Theorem | gt0ne0 8002 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0) |
|
Theorem | lt0ne0 8003 |
A number which is less than zero is not zero. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0) |
|
Theorem | ltadd1 8004 |
Addition to both sides of 'less than'. Part of definition 11.2.7(vi) of
[HoTT], p. (varies). (Contributed by NM,
12-Nov-1999.) (Proof shortened
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))) |
|
Theorem | leadd1 8005 |
Addition to both sides of 'less than or equal to'. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 18-Oct-1999.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))) |
|
Theorem | leadd2 8006 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))) |
|
Theorem | ltsubadd 8007 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) |
|
Theorem | ltsubadd2 8008 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) |
|
Theorem | lesubadd 8009 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵))) |
|
Theorem | lesubadd2 8010 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) |
|
Theorem | ltaddsub 8011 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
|
Theorem | ltaddsub2 8012 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) |
|
Theorem | leaddsub 8013 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵))) |
|
Theorem | leaddsub2 8014 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) |
|
Theorem | suble 8015 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵)) |
|
Theorem | lesub 8016 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴))) |
|
Theorem | ltsub23 8017 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵)) |
|
Theorem | ltsub13 8018 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴))) |
|
Theorem | le2add 8019 |
Adding both sides of two 'less than or equal to' relations. (Contributed
by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) |
|
Theorem | lt2add 8020 |
Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol]
p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | ltleadd 8021 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | leltadd 8022 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | addgt0 8023 |
The sum of 2 positive numbers is positive. (Contributed by NM,
1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addgegt0 8024 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addgtge0 8025 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ 𝐵)) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addge0 8026 |
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) |
|
Theorem | ltaddpos 8027 |
Adding a positive number to another number increases it. (Contributed by
NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) |
|
Theorem | ltaddpos2 8028 |
Adding a positive number to another number increases it. (Contributed by
NM, 8-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵))) |
|
Theorem | ltsubpos 8029 |
Subtracting a positive number from another number decreases it.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵)) |
|
Theorem | posdif 8030 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
|
Theorem | lesub1 8031 |
Subtraction from both sides of 'less than or equal to'. (Contributed by
NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝐶) ≤ (𝐵 − 𝐶))) |
|
Theorem | lesub2 8032 |
Subtraction of both sides of 'less than or equal to'. (Contributed by NM,
29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴))) |
|
Theorem | ltsub1 8033 |
Subtraction from both sides of 'less than'. (Contributed by FL,
3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶))) |
|
Theorem | ltsub2 8034 |
Subtraction of both sides of 'less than'. (Contributed by NM,
29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴))) |
|
Theorem | lt2sub 8035 |
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14-Apr-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷))) |
|
Theorem | le2sub 8036 |
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14-Apr-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷))) |
|
Theorem | ltneg 8037 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) |
|
Theorem | ltnegcon1 8038 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)) |
|
Theorem | ltnegcon2 8039 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)) |
|
Theorem | leneg 8040 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)) |
|
Theorem | lenegcon1 8041 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) |
|
Theorem | lenegcon2 8042 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) |
|
Theorem | lt0neg1 8043 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < -𝐴)) |
|
Theorem | lt0neg2 8044 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0)) |
|
Theorem | le0neg1 8045 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
|
Theorem | le0neg2 8046 |
Comparison of a number and its negative to zero. (Contributed by NM,
24-Aug-1999.)
|
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0)) |
|
Theorem | addge01 8047 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵))) |
|
Theorem | addge02 8048 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27-Jul-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴))) |
|
Theorem | add20 8049 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
|
Theorem | subge0 8050 |
Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) |
|
Theorem | suble0 8051 |
Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵)) |
|
Theorem | leaddle0 8052 |
The sum of a real number and a second real number is less then the real
number iff the second real number is negative. (Contributed by Alexander
van der Vekens, 30-May-2018.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐴 ↔ 𝐵 ≤ 0)) |
|
Theorem | subge02 8053 |
Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴)) |
|
Theorem | lesub0 8054 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0)) |
|
Theorem | mullt0 8055 |
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8-Jun-2009.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 𝐵 < 0)) → 0 < (𝐴 · 𝐵)) |
|
Theorem | 0le1 8056 |
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29-Apr-2015.)
|
⊢ 0 ≤ 1 |
|
Theorem | ltordlem 8057* |
Lemma for eqord1 8058. (Contributed by Mario Carneiro,
14-Jun-2014.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)
& ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)
& ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 → 𝑀 < 𝑁)) |
|
Theorem | eqord1 8058* |
A strictly increasing real function on a subset of ℝ is
one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised
by Jim Kingdon, 20-Dec-2022.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)
& ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)
& ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁)) |
|
Theorem | eqord2 8059* |
A strictly decreasing real function on a subset of ℝ is one-to-one.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀)
& ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁)
& ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁)) |
|
Theorem | leidi 8060 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ 𝐴 ≤ 𝐴 |
|
Theorem | gt0ne0i 8061 |
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (0 < 𝐴 → 𝐴 ≠ 0) |
|
Theorem | gt0ne0ii 8062 |
Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ≠ 0 |
|
Theorem | addgt0i 8063 |
Addition of 2 positive numbers is positive. (Contributed by NM,
16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addge0i 8064 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 + 𝐵)) |
|
Theorem | addgegt0i 8065 |
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addgt0ii 8066 |
Addition of 2 positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 + 𝐵) |
|
Theorem | add20i 8067 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
|
Theorem | ltnegi 8068 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ -𝐵 < -𝐴) |
|
Theorem | lenegi 8069 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴) |
|
Theorem | ltnegcon2i 8070 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < -𝐵 ↔ 𝐵 < -𝐴) |
|
Theorem | lesub0i 8071 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0) |
|
Theorem | ltaddposi 8072 |
Adding a positive number to another number increases it. (Contributed
by NM, 25-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)) |
|
Theorem | posdifi 8073 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19-Aug-2001.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)) |
|
Theorem | ltnegcon1i 8074 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴) |
|
Theorem | lenegcon1i 8075 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 6-Apr-2005.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴) |
|
Theorem | subge0i 8076 |
Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴) |
|
Theorem | ltadd1i 8077 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)) |
|
Theorem | leadd1i 8078 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)) |
|
Theorem | leadd2i 8079 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)) |
|
Theorem | ltsubaddi 8080 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵)) |
|
Theorem | lesubaddi 8081 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵)) |
|
Theorem | ltsubadd2i 8082 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)) |
|
Theorem | lesubadd2i 8083 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶)) |
|
Theorem | ltaddsubi 8084 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵)) |
|
Theorem | lt2addi 8085 |
Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)) |
|
Theorem | le2addi 8086 |
Adding both side of two inequalities. (Contributed by NM,
16-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) |
|
Theorem | gt0ne0d 8087 |
Positive implies nonzero. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) |
|
Theorem | lt0ne0d 8088 |
Something less than zero is not zero. Deduction form. (Contributed by
David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) |
|
Theorem | leidd 8089 |
'Less than or equal to' is reflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) |
|
Theorem | lt0neg1d 8090 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 < 0 ↔ 0 < -𝐴)) |
|
Theorem | lt0neg2d 8091 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ -𝐴 < 0)) |
|
Theorem | le0neg1d 8092 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
|
Theorem | le0neg2d 8093 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0)) |
|
Theorem | addgegt0d 8094 |
Addition of nonnegative and positive numbers is positive.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) |
|
Theorem | addgt0d 8095 |
Addition of 2 positive numbers is positive. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) |
|
Theorem | addge0d 8096 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 + 𝐵)) |
|
Theorem | ltnegd 8097 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) |
|
Theorem | lenegd 8098 |
Negative of both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)) |
|
Theorem | ltnegcon1d 8099 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → -𝐴 < 𝐵) ⇒ ⊢ (𝜑 → -𝐵 < 𝐴) |
|
Theorem | ltnegcon2d 8100 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < -𝐵) ⇒ ⊢ (𝜑 → 𝐵 < -𝐴) |