Database
REAL AND COMPLEX NUMBERS
Integer sets
Simple number properties
nominpos
Next ⟩
avglt1
Metamath Proof Explorer
Ascii
Unicode
Theorem
nominpos
Description:
There is no smallest positive real number.
(Contributed by
NM
, 28-Oct-2004)
Ref
Expression
Assertion
nominpos
⊢
¬
∃
x
∈
ℝ
0
<
x
∧
¬
∃
y
∈
ℝ
0
<
y
∧
y
<
x
Proof
Step
Hyp
Ref
Expression
1
rehalfcl
⊢
x
∈
ℝ
→
x
2
∈
ℝ
2
2re
⊢
2
∈
ℝ
3
2pos
⊢
0
<
2
4
divgt0
⊢
x
∈
ℝ
∧
0
<
x
∧
2
∈
ℝ
∧
0
<
2
→
0
<
x
2
5
2
3
4
mpanr12
⊢
x
∈
ℝ
∧
0
<
x
→
0
<
x
2
6
5
ex
⊢
x
∈
ℝ
→
0
<
x
→
0
<
x
2
7
halfpos
⊢
x
∈
ℝ
→
0
<
x
↔
x
2
<
x
8
7
biimpd
⊢
x
∈
ℝ
→
0
<
x
→
x
2
<
x
9
6
8
jcad
⊢
x
∈
ℝ
→
0
<
x
→
0
<
x
2
∧
x
2
<
x
10
breq2
⊢
y
=
x
2
→
0
<
y
↔
0
<
x
2
11
breq1
⊢
y
=
x
2
→
y
<
x
↔
x
2
<
x
12
10
11
anbi12d
⊢
y
=
x
2
→
0
<
y
∧
y
<
x
↔
0
<
x
2
∧
x
2
<
x
13
12
rspcev
⊢
x
2
∈
ℝ
∧
0
<
x
2
∧
x
2
<
x
→
∃
y
∈
ℝ
0
<
y
∧
y
<
x
14
1
9
13
syl6an
⊢
x
∈
ℝ
→
0
<
x
→
∃
y
∈
ℝ
0
<
y
∧
y
<
x
15
iman
⊢
0
<
x
→
∃
y
∈
ℝ
0
<
y
∧
y
<
x
↔
¬
0
<
x
∧
¬
∃
y
∈
ℝ
0
<
y
∧
y
<
x
16
14
15
sylib
⊢
x
∈
ℝ
→
¬
0
<
x
∧
¬
∃
y
∈
ℝ
0
<
y
∧
y
<
x
17
16
nrex
⊢
¬
∃
x
∈
ℝ
0
<
x
∧
¬
∃
y
∈
ℝ
0
<
y
∧
y
<
x