Theorem List for Intuitionistic Logic Explorer - 7901-8000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 8lt10 7901 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.)
|
⊢ 8 < 10 |
|
Theorem | 7lt10 7902 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
⊢ 7 < 10 |
|
Theorem | 6lt10 7903 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
⊢ 6 < 10 |
|
Theorem | 5lt10 7904 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
⊢ 5 < 10 |
|
Theorem | 4lt10 7905 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
⊢ 4 < 10 |
|
Theorem | 3lt10 7906 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
⊢ 3 < 10 |
|
Theorem | 2lt10 7907 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
|
⊢ 2 < 10 |
|
Theorem | 1lt10 7908 |
1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.)
|
⊢ 1 < 10 |
|
Theorem | 0ne2 7909 |
0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ 0 ≠ 2 |
|
Theorem | 1ne2 7910 |
1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)
|
⊢ 1 ≠ 2 |
|
Theorem | 1le2 7911 |
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ 1 ≤ 2 |
|
Theorem | 2cnne0 7912 |
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
⊢ (2 ∈ ℂ
∧ 2 ≠ 0) |
|
Theorem | 2rene0 7913 |
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ (2 ∈ ℝ
∧ 2 ≠ 0) |
|
Theorem | 1le3 7914 |
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ 1 ≤ 3 |
|
Theorem | neg1mulneg1e1 7915 |
-1 · -1 is 1 (common case). (Contributed by
David A. Wheeler,
8-Dec-2018.)
|
⊢ (-1 · -1) = 1 |
|
Theorem | halfre 7916 |
One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 / 2) ∈
ℝ |
|
Theorem | halfcn 7917 |
One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
⊢ (1 / 2) ∈
ℂ |
|
Theorem | halfgt0 7918 |
One-half is greater than zero. (Contributed by NM, 24-Feb-2005.)
|
⊢ 0 < (1 / 2) |
|
Theorem | halflt1 7919 |
One-half is less than one. (Contributed by NM, 24-Feb-2005.)
|
⊢ (1 / 2) < 1 |
|
Theorem | 1mhlfehlf 7920 |
Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler,
4-Jan-2017.)
|
⊢ (1 − (1 / 2)) = (1 / 2) |
|
Theorem | 8th4div3 7921 |
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24-Nov-2007.)
|
⊢ ((1 / 8) · (4 / 3)) = (1 /
6) |
|
Theorem | halfpm6th 7922 |
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 7923 |
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (i · 0) = 0 |
|
Theorem | 2mulicn 7924 |
(2 · i) ∈
ℂ (common case). (Contributed by David A. Wheeler,
8-Dec-2018.)
|
⊢ (2 · i) ∈ ℂ |
|
Theorem | iap0 7925 |
The imaginary unit i is apart from zero. (Contributed
by Jim
Kingdon, 9-Mar-2020.)
|
⊢ i # 0 |
|
Theorem | 2muliap0 7926 |
2 · i is apart from zero. (Contributed by Jim
Kingdon,
9-Mar-2020.)
|
⊢ (2 · i) # 0 |
|
Theorem | 2muline0 7927 |
(2 · i) ≠ 0. See also 2muliap0 7926. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
⊢ (2 · i) ≠ 0 |
|
3.4.5 Simple number properties
|
|
Theorem | halfcl 7928 |
Closure of half of a number (common case). (Contributed by NM,
1-Jan-2006.)
|
⊢ (A ∈ ℂ → (A / 2) ∈
ℂ) |
|
Theorem | rehalfcl 7929 |
Real closure of half. (Contributed by NM, 1-Jan-2006.)
|
⊢ (A ∈ ℝ → (A / 2) ∈
ℝ) |
|
Theorem | half0 7930 |
Half of a number is zero iff the number is zero. (Contributed by NM,
20-Apr-2006.)
|
⊢ (A ∈ ℂ → ((A / 2) = 0 ↔ A = 0)) |
|
Theorem | 2halves 7931 |
Two halves make a whole. (Contributed by NM, 11-Apr-2005.)
|
⊢ (A ∈ ℂ → ((A / 2) + (A /
2)) = A) |
|
Theorem | halfpos2 7932 |
A number is positive iff its half is positive. (Contributed by NM,
10-Apr-2005.)
|
⊢ (A ∈ ℝ → (0 < A ↔ 0 < (A / 2))) |
|
Theorem | halfpos 7933 |
A positive number is greater than its half. (Contributed by NM,
28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (A ∈ ℝ → (0 < A ↔ (A /
2) < A)) |
|
Theorem | halfnneg2 7934 |
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9-Dec-2005.)
|
⊢ (A ∈ ℝ → (0 ≤ A ↔ 0 ≤ (A / 2))) |
|
Theorem | halfaddsubcl 7935 |
Closure of half-sum and half-difference. (Contributed by Paul Chapman,
12-Oct-2007.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B) / 2) ∈ ℂ
∧ ((A
− B) / 2) ∈ ℂ)) |
|
Theorem | halfaddsub 7936 |
Sum and difference of half-sum and half-difference. (Contributed by Paul
Chapman, 12-Oct-2007.)
|
⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → ((((A + B) / 2) + ((A
− B) / 2)) = A ∧ (((A + B) / 2)
− ((A − B) / 2)) = B)) |
|
Theorem | lt2halves 7937 |
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13-Dec-2006.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((A < (𝐶 / 2) ∧ B < (𝐶 / 2)) → (A + B) <
𝐶)) |
|
Theorem | addltmul 7938 |
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24-Sep-2010.)
|
⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (2 < A ∧ 2 <
B)) → (A + B) <
(A · B)) |
|
Theorem | nominpos 7939* |
There is no smallest positive real number. (Contributed by NM,
28-Oct-2004.)
|
⊢ ¬ ∃x ∈ ℝ (0 < x ∧ ¬ ∃y ∈ ℝ (0 < y ∧ y < x)) |
|
Theorem | avglt1 7940 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A < B ↔ A <
((A + B) / 2))) |
|
Theorem | avglt2 7941 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A < B ↔ ((A +
B) / 2) < B)) |
|
Theorem | avgle1 7942 |
Ordering property for average. (Contributed by Mario Carneiro,
28-May-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A ≤ B ↔ A ≤
((A + B) / 2))) |
|
Theorem | avgle2 7943 |
Ordering property for average. (Contributed by Jeff Hankins,
15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.)
|
⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A ≤ B ↔ ((A +
B) / 2) ≤ B)) |
|
Theorem | 2timesd 7944 |
Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (2 · A) = (A +
A)) |
|
Theorem | times2d 7945 |
A number times 2. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (A · 2) = (A + A)) |
|
Theorem | halfcld 7946 |
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → (A / 2) ∈
ℂ) |
|
Theorem | 2halvesd 7947 |
Two halves make a whole. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (φ
→ A ∈ ℂ) ⇒ ⊢ (φ → ((A / 2) + (A /
2)) = A) |
|
Theorem | rehalfcld 7948 |
Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) ⇒ ⊢ (φ → (A / 2) ∈
ℝ) |
|
Theorem | lt2halvesd 7949 |
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (φ
→ A ∈ ℝ) & ⊢ (φ → B ∈
ℝ)
& ⊢ (φ
→ 𝐶 ∈ ℝ) & ⊢ (φ → A < (𝐶 / 2)) & ⊢ (φ → B < (𝐶 / 2)) ⇒ ⊢ (φ → (A + B) <
𝐶) |
|
Theorem | rehalfcli 7950 |
Half a real number is real. Inference form. (Contributed by David
Moews, 28-Feb-2017.)
|
⊢ A ∈ ℝ ⇒ ⊢ (A / 2) ∈
ℝ |
|
Theorem | add1p1 7951 |
Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.)
|
⊢ (𝑁 ∈
ℂ → ((𝑁 + 1) +
1) = (𝑁 +
2)) |
|
Theorem | sub1m1 7952 |
Subtracting two times 1 from a number. (Contributed by AV,
23-Oct-2018.)
|
⊢ (𝑁 ∈
ℂ → ((𝑁 −
1) − 1) = (𝑁 −
2)) |
|
Theorem | cnm2m1cnm3 7953 |
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.)
|
⊢ (A ∈ ℂ → ((A − 2) − 1) = (A − 3)) |
|
3.4.6 The Archimedean property
|
|
Theorem | arch 7954* |
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.)
|
⊢ (A ∈ ℝ → ∃𝑛 ∈ ℕ
A < 𝑛) |
|
Theorem | nnrecl 7955* |
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.)
|
⊢ ((A ∈ ℝ ∧ 0
< A) → ∃𝑛 ∈ ℕ
(1 / 𝑛) < A) |
|
Theorem | bndndx 7956* |
A bounded real sequence A(𝑘) is less than or equal to at least
one of its indices. (Contributed by NM, 18-Jan-2008.)
|
⊢ (∃x ∈ ℝ ∀𝑘 ∈ ℕ
(A ∈
ℝ ∧ A ≤ x)
→ ∃𝑘 ∈ ℕ
A ≤ 𝑘) |
|
3.4.7 Nonnegative integers (as a subset of
complex numbers)
|
|
Syntax | cn0 7957 |
Extend class notation to include the class of nonnegative integers.
|
class ℕ0 |
|
Definition | df-n0 7958 |
Define the set of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.)
|
⊢ ℕ0 = (ℕ ∪
{0}) |
|
Theorem | elnn0 7959 |
Nonnegative integers expressed in terms of naturals and zero.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ (A ∈ ℕ0 ↔ (A ∈ ℕ ∨ A =
0)) |
|
Theorem | nnssnn0 7960 |
Positive naturals are a subset of nonnegative integers. (Contributed by
Raph Levien, 10-Dec-2002.)
|
⊢ ℕ ⊆
ℕ0 |
|
Theorem | nn0ssre 7961 |
Nonnegative integers are a subset of the reals. (Contributed by Raph
Levien, 10-Dec-2002.)
|
⊢ ℕ0 ⊆
ℝ |
|
Theorem | nn0sscn 7962 |
Nonnegative integers are a subset of the complex numbers.) (Contributed
by NM, 9-May-2004.)
|
⊢ ℕ0 ⊆
ℂ |
|
Theorem | nn0ex 7963 |
The set of nonnegative integers exists. (Contributed by NM,
18-Jul-2004.)
|
⊢ ℕ0 ∈ V |
|
Theorem | nnnn0 7964 |
A positive integer is a nonnegative integer. (Contributed by NM,
9-May-2004.)
|
⊢ (A ∈ ℕ → A ∈
ℕ0) |
|
Theorem | nnnn0i 7965 |
A positive integer is a nonnegative integer. (Contributed by NM,
20-Jun-2005.)
|
⊢ 𝑁 ∈
ℕ ⇒ ⊢ 𝑁 ∈
ℕ0 |
|
Theorem | nn0re 7966 |
A nonnegative integer is a real number. (Contributed by NM,
9-May-2004.)
|
⊢ (A ∈ ℕ0 → A ∈
ℝ) |
|
Theorem | nn0cn 7967 |
A nonnegative integer is a complex number. (Contributed by NM,
9-May-2004.)
|
⊢ (A ∈ ℕ0 → A ∈
ℂ) |
|
Theorem | nn0rei 7968 |
A nonnegative integer is a real number. (Contributed by NM,
14-May-2003.)
|
⊢ A ∈ ℕ0
⇒ ⊢ A ∈
ℝ |
|
Theorem | nn0cni 7969 |
A nonnegative integer is a complex number. (Contributed by NM,
14-May-2003.)
|
⊢ A ∈ ℕ0
⇒ ⊢ A ∈
ℂ |
|
Theorem | dfn2 7970 |
The set of positive integers defined in terms of nonnegative integers.
(Contributed by NM, 23-Sep-2007.) (Proof shortened by Mario Carneiro,
13-Feb-2013.)
|
⊢ ℕ = (ℕ0 ∖
{0}) |
|
Theorem | elnnne0 7971 |
The positive integer property expressed in terms of difference from zero.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
⊢ (𝑁 ∈
ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0)) |
|
Theorem | 0nn0 7972 |
0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 0 ∈
ℕ0 |
|
Theorem | 1nn0 7973 |
1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 1 ∈
ℕ0 |
|
Theorem | 2nn0 7974 |
2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 2 ∈
ℕ0 |
|
Theorem | 3nn0 7975 |
3 is a nonnegative integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 3 ∈
ℕ0 |
|
Theorem | 4nn0 7976 |
4 is a nonnegative integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 4 ∈
ℕ0 |
|
Theorem | 5nn0 7977 |
5 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 5 ∈
ℕ0 |
|
Theorem | 6nn0 7978 |
6 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 6 ∈
ℕ0 |
|
Theorem | 7nn0 7979 |
7 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 7 ∈
ℕ0 |
|
Theorem | 8nn0 7980 |
8 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 8 ∈
ℕ0 |
|
Theorem | 9nn0 7981 |
9 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 9 ∈
ℕ0 |
|
Theorem | 10nn0 7982 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
⊢ 10 ∈
ℕ0 |
|
Theorem | nn0ge0 7983 |
A nonnegative integer is greater than or equal to zero. (Contributed by
NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)
|
⊢ (𝑁 ∈
ℕ0 → 0 ≤ 𝑁) |
|
Theorem | nn0nlt0 7984 |
A nonnegative integer is not less than zero. (Contributed by NM,
9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (A ∈ ℕ0 → ¬ A < 0) |
|
Theorem | nn0ge0i 7985 |
Nonnegative integers are nonnegative. (Contributed by Raph Levien,
10-Dec-2002.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ 0 ≤ 𝑁 |
|
Theorem | nn0le0eq0 7986 |
A nonnegative integer is less than or equal to zero iff it is equal to
zero. (Contributed by NM, 9-Dec-2005.)
|
⊢ (𝑁 ∈
ℕ0 → (𝑁 ≤ 0 ↔ 𝑁 = 0)) |
|
Theorem | nn0p1gt0 7987 |
A nonnegative integer increased by 1 is greater than 0. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
⊢ (𝑁 ∈
ℕ0 → 0 < (𝑁 + 1)) |
|
Theorem | nnnn0addcl 7988 |
A positive integer plus a nonnegative integer is a positive integer.
(Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro,
16-May-2014.)
|
⊢ ((𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ0) → (𝑀 + 𝑁) ∈
ℕ) |
|
Theorem | nn0nnaddcl 7989 |
A nonnegative integer plus a positive integer is a positive integer.
(Contributed by NM, 22-Dec-2005.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
|
Theorem | 0mnnnnn0 7990 |
The result of subtracting a positive integer from 0 is not a nonnegative
integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
|
⊢ (𝑁 ∈
ℕ → (0 − 𝑁) ∉
ℕ0) |
|
Theorem | un0addcl 7991 |
If 𝑆 is closed under addition, then so is
𝑆 ∪
{0}.
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
⊢ (φ
→ 𝑆 ⊆
ℂ)
& ⊢ 𝑇 = (𝑆 ∪ {0}) & ⊢ ((φ ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 + 𝑁) ∈ 𝑆)
⇒ ⊢ ((φ ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 + 𝑁) ∈ 𝑇) |
|
Theorem | un0mulcl 7992 |
If 𝑆 is closed under multiplication, then
so is 𝑆
∪ {0}.
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
⊢ (φ
→ 𝑆 ⊆
ℂ)
& ⊢ 𝑇 = (𝑆 ∪ {0}) & ⊢ ((φ ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑆)
⇒ ⊢ ((φ ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 · 𝑁) ∈ 𝑇) |
|
Theorem | nn0addcl 7993 |
Closure of addition of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 + 𝑁) ∈
ℕ0) |
|
Theorem | nn0mulcl 7994 |
Closure of multiplication of nonnegative integers. (Contributed by NM,
22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|
⊢ ((𝑀 ∈
ℕ0 ∧ 𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0) |
|
Theorem | nn0addcli 7995 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 𝑀 ∈
ℕ0
& ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑀 + 𝑁) ∈
ℕ0 |
|
Theorem | nn0mulcli 7996 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
⊢ 𝑀 ∈
ℕ0
& ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑀 · 𝑁) ∈
ℕ0 |
|
Theorem | nn0p1nn 7997 |
A nonnegative integer plus 1 is a positive integer. (Contributed by Raph
Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
|
⊢ (𝑁 ∈
ℕ0 → (𝑁 + 1) ∈
ℕ) |
|
Theorem | peano2nn0 7998 |
Second Peano postulate for nonnegative integers. (Contributed by NM,
9-May-2004.)
|
⊢ (𝑁 ∈
ℕ0 → (𝑁 + 1) ∈
ℕ0) |
|
Theorem | nnm1nn0 7999 |
A positive integer minus 1 is a nonnegative integer. (Contributed by
Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro,
16-May-2014.)
|
⊢ (𝑁 ∈
ℕ → (𝑁 −
1) ∈ ℕ0) |
|
Theorem | elnn0nn 8000 |
The nonnegative integer property expressed in terms of positive integers.
(Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro,
16-May-2014.)
|
⊢ (𝑁 ∈
ℕ0 ↔ (𝑁 ∈
ℂ ∧ (𝑁 + 1) ∈
ℕ)) |