Theorem List for Intuitionistic Logic Explorer - 9001-9100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 8nn 9001 |
8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 8 ∈ ℕ |
|
Theorem | 9nn 9002 |
9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
|
⊢ 9 ∈ ℕ |
|
Theorem | 1lt2 9003 |
1 is less than 2. (Contributed by NM, 24-Feb-2005.)
|
⊢ 1 < 2 |
|
Theorem | 2lt3 9004 |
2 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
⊢ 2 < 3 |
|
Theorem | 1lt3 9005 |
1 is less than 3. (Contributed by NM, 26-Sep-2010.)
|
⊢ 1 < 3 |
|
Theorem | 3lt4 9006 |
3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 4 |
|
Theorem | 2lt4 9007 |
2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 4 |
|
Theorem | 1lt4 9008 |
1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 4 |
|
Theorem | 4lt5 9009 |
4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 5 |
|
Theorem | 3lt5 9010 |
3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 5 |
|
Theorem | 2lt5 9011 |
2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 5 |
|
Theorem | 1lt5 9012 |
1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 5 |
|
Theorem | 5lt6 9013 |
5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 6 |
|
Theorem | 4lt6 9014 |
4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 6 |
|
Theorem | 3lt6 9015 |
3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 6 |
|
Theorem | 2lt6 9016 |
2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 6 |
|
Theorem | 1lt6 9017 |
1 is less than 6. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 < 6 |
|
Theorem | 6lt7 9018 |
6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 < 7 |
|
Theorem | 5lt7 9019 |
5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 7 |
|
Theorem | 4lt7 9020 |
4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 7 |
|
Theorem | 3lt7 9021 |
3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 7 |
|
Theorem | 2lt7 9022 |
2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 7 |
|
Theorem | 1lt7 9023 |
1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 7 |
|
Theorem | 7lt8 9024 |
7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 7 < 8 |
|
Theorem | 6lt8 9025 |
6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 6 < 8 |
|
Theorem | 5lt8 9026 |
5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 5 < 8 |
|
Theorem | 4lt8 9027 |
4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 4 < 8 |
|
Theorem | 3lt8 9028 |
3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 3 < 8 |
|
Theorem | 2lt8 9029 |
2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 2 < 8 |
|
Theorem | 1lt8 9030 |
1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.)
|
⊢ 1 < 8 |
|
Theorem | 8lt9 9031 |
8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.)
|
⊢ 8 < 9 |
|
Theorem | 7lt9 9032 |
7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 7 < 9 |
|
Theorem | 6lt9 9033 |
6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 6 < 9 |
|
Theorem | 5lt9 9034 |
5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 5 < 9 |
|
Theorem | 4lt9 9035 |
4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 4 < 9 |
|
Theorem | 3lt9 9036 |
3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 3 < 9 |
|
Theorem | 2lt9 9037 |
2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.)
|
⊢ 2 < 9 |
|
Theorem | 1lt9 9038 |
1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
⊢ 1 < 9 |
|
Theorem | 0ne2 9039 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ≠ 2 |
|
Theorem | 1ne2 9040 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 ≠ 2 |
|
Theorem | 1ap2 9041 |
1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.)
|
⊢ 1 # 2 |
|
Theorem | 1le2 9042 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 1 ≤ 2 |
|
Theorem | 2cnne0 9043 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
⊢ (2 ∈ ℂ ∧ 2 ≠
0) |
|
Theorem | 2rene0 9044 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ (2 ∈ ℝ ∧ 2 ≠
0) |
|
Theorem | 1le3 9045 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ 1 ≤ 3 |
|
Theorem | neg1mulneg1e1 9046 |
-1 · -1 is 1 (common case). (Contributed by
David A. Wheeler,
8-Dec-2018.)
|
⊢ (-1 · -1) = 1 |
|
Theorem | halfre 9047 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 / 2) ∈ ℝ |
|
Theorem | halfcn 9048 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 / 2) ∈ ℂ |
|
Theorem | halfgt0 9049 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
⊢ 0 < (1 / 2) |
|
Theorem | halfge0 9050 |
One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|
⊢ 0 ≤ (1 / 2) |
|
Theorem | halflt1 9051 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
⊢ (1 / 2) < 1 |
|
Theorem | 1mhlfehlf 9052 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
⊢ (1 − (1 / 2)) = (1 /
2) |
|
Theorem | 8th4div3 9053 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
⊢ ((1 / 8) · (4 / 3)) = (1 /
6) |
|
Theorem | halfpm6th 9054 |
One half plus or minus one sixth. (Contributed by Paul Chapman,
17-Jan-2008.)
|
⊢ (((1 / 2) − (1 / 6)) = (1 / 3) ∧
((1 / 2) + (1 / 6)) = (2 / 3)) |
|
Theorem | it0e0 9055 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (i · 0) = 0 |
|
Theorem | 2mulicn 9056 |
(2 · i) ∈ ℂ (common case).
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (2 · i) ∈
ℂ |
|
Theorem | iap0 9057 |
The imaginary unit i is apart from zero. (Contributed
by Jim
Kingdon, 9-Mar-2020.)
|
⊢ i # 0 |
|
Theorem | 2muliap0 9058 |
2 · i is apart from zero. (Contributed by Jim
Kingdon,
9-Mar-2020.)
|
⊢ (2 · i) # 0 |
|
Theorem | 2muline0 9059 |
(2 · i) ≠ 0. See also 2muliap0 9058. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ (2 · i) ≠ 0 |
|
4.4.5 Simple number properties
|
|
Theorem | halfcl 9060 |
Closure of half of a number (common case). (Contributed by NM,
1-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈ ℂ) |
|
Theorem | rehalfcl 9061 |
Real closure of half. (Contributed by NM, 1-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ) |
|
Theorem | half0 9062 |
Half of a number is zero iff the number is zero. (Contributed by NM,
20-Apr-2006.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) = 0 ↔ 𝐴 = 0)) |
|
Theorem | 2halves 9063 |
Two halves make a whole. (Contributed by NM, 11-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) |
|
Theorem | halfpos2 9064 |
A number is positive iff its half is positive. (Contributed by NM,
10-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ 0 < (𝐴 / 2))) |
|
Theorem | halfpos 9065 |
A positive number is greater than its half. (Contributed by NM,
28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (𝐴 / 2) < 𝐴)) |
|
Theorem | halfnneg2 9066 |
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9-Dec-2005.)
|
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 2))) |
|
Theorem | halfaddsubcl 9067 |
Closure of half-sum and half-difference. (Contributed by Paul Chapman,
12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) / 2) ∈ ℂ ∧ ((𝐴 − 𝐵) / 2) ∈ ℂ)) |
|
Theorem | halfaddsub 9068 |
Sum and difference of half-sum and half-difference. (Contributed by Paul
Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2)) = 𝐴 ∧ (((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)) = 𝐵)) |
|
Theorem | lt2halves 9069 |
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13-Dec-2006.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < (𝐶 / 2) ∧ 𝐵 < (𝐶 / 2)) → (𝐴 + 𝐵) < 𝐶)) |
|
Theorem | addltmul 9070 |
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24-Sep-2010.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵)) |
|
Theorem | nominpos 9071* |
There is no smallest positive real number. (Contributed by NM,
28-Oct-2004.)
|
⊢ ¬ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ¬ ∃𝑦 ∈ ℝ (0 < 𝑦 ∧ 𝑦 < 𝑥)) |
|
Theorem | avglt1 9072 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) |
|
Theorem | avglt2 9073 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
|
Theorem | avgle1 9074 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ ((𝐴 + 𝐵) / 2))) |
|
Theorem | avgle2 9075 |
Ordering property for average. (Contributed by Jeff Hankins,
15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ((𝐴 + 𝐵) / 2) ≤ 𝐵)) |
|
Theorem | 2timesd 9076 |
Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴)) |
|
Theorem | times2d 9077 |
A number times 2. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · 2) = (𝐴 + 𝐴)) |
|
Theorem | halfcld 9078 |
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ) |
|
Theorem | 2halvesd 9079 |
Two halves make a whole. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) |
|
Theorem | rehalfcld 9080 |
Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ) |
|
Theorem | lt2halvesd 9081 |
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐶 / 2)) & ⊢ (𝜑 → 𝐵 < (𝐶 / 2)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < 𝐶) |
|
Theorem | rehalfcli 9082 |
Half a real number is real. Inference form. (Contributed by David
Moews, 28-Feb-2017.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴 / 2) ∈ ℝ |
|
Theorem | add1p1 9083 |
Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.)
|
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) + 1) = (𝑁 + 2)) |
|
Theorem | sub1m1 9084 |
Subtracting two times 1 from a number. (Contributed by AV,
23-Oct-2018.)
|
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
|
Theorem | cnm2m1cnm3 9085 |
Subtracting 2 and afterwards 1 from a number results in the difference
between the number and 3. (Contributed by Alexander van der Vekens,
16-Sep-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 − 2) − 1) = (𝐴 − 3)) |
|
Theorem | xp1d2m1eqxm1d2 9086 |
A complex number increased by 1, then divided by 2, then decreased by 1
equals the complex number decreased by 1 and then divided by 2.
(Contributed by AV, 24-May-2020.)
|
⊢ (𝑋 ∈ ℂ → (((𝑋 + 1) / 2) − 1) = ((𝑋 − 1) / 2)) |
|
Theorem | div4p1lem1div2 9087 |
An integer greater than 5, divided by 4 and increased by 1, is less than
or equal to the half of the integer minus 1. (Contributed by AV,
8-Jul-2021.)
|
⊢ ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → ((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2)) |
|
4.4.6 The Archimedean property
|
|
Theorem | arch 9088* |
Archimedean property of real numbers. For any real number, there is an
integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed
by NM, 21-Jan-1997.)
|
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ℕ 𝐴 < 𝑛) |
|
Theorem | nnrecl 9089* |
There exists a positive integer whose reciprocal is less than a given
positive real. Exercise 3 of [Apostol]
p. 28. (Contributed by NM,
8-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴) |
|
Theorem | bndndx 9090* |
A bounded real sequence 𝐴(𝑘) is less than or equal to at least
one of its indices. (Contributed by NM, 18-Jan-2008.)
|
⊢ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥) → ∃𝑘 ∈ ℕ 𝐴 ≤ 𝑘) |
|
4.4.7 Nonnegative integers (as a subset of
complex numbers)
|
|
Syntax | cn0 9091 |
Extend class notation to include the class of nonnegative integers.
|
class ℕ0 |
|
Definition | df-n0 9092 |
Define the set of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.)
|
⊢ ℕ0 = (ℕ ∪
{0}) |
|
Theorem | elnn0 9093 |
Nonnegative integers expressed in terms of naturals and zero.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
|
Theorem | nnssnn0 9094 |
Positive naturals are a subset of nonnegative integers. (Contributed by
Raph Levien, 10-Dec-2002.)
|
⊢ ℕ ⊆
ℕ0 |
|
Theorem | nn0ssre 9095 |
Nonnegative integers are a subset of the reals. (Contributed by Raph
Levien, 10-Dec-2002.)
|
⊢ ℕ0 ⊆
ℝ |
|
Theorem | nn0sscn 9096 |
Nonnegative integers are a subset of the complex numbers.) (Contributed
by NM, 9-May-2004.)
|
⊢ ℕ0 ⊆
ℂ |
|
Theorem | nn0ex 9097 |
The set of nonnegative integers exists. (Contributed by NM,
18-Jul-2004.)
|
⊢ ℕ0 ∈
V |
|
Theorem | nnnn0 9098 |
A positive integer is a nonnegative integer. (Contributed by NM,
9-May-2004.)
|
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
|
Theorem | nnnn0i 9099 |
A positive integer is a nonnegative integer. (Contributed by NM,
20-Jun-2005.)
|
⊢ 𝑁 ∈ ℕ
⇒ ⊢ 𝑁 ∈
ℕ0 |
|
Theorem | nn0re 9100 |
A nonnegative integer is a real number. (Contributed by NM,
9-May-2004.)
|
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈
ℝ) |