Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
The floor and ceiling functions
flval2
Next ⟩
flval3
Metamath Proof Explorer
Ascii
Unicode
Theorem
flval2
Description:
An alternate way to define the floor function.
(Contributed by
NM
, 16-Nov-2004)
Ref
Expression
Assertion
flval2
⊢
A
∈
ℝ
→
A
=
ι
x
∈
ℤ
|
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
Proof
Step
Hyp
Ref
Expression
1
flle
⊢
A
∈
ℝ
→
A
≤
A
2
flge
⊢
A
∈
ℝ
∧
y
∈
ℤ
→
y
≤
A
↔
y
≤
A
3
2
biimpd
⊢
A
∈
ℝ
∧
y
∈
ℤ
→
y
≤
A
→
y
≤
A
4
3
ralrimiva
⊢
A
∈
ℝ
→
∀
y
∈
ℤ
y
≤
A
→
y
≤
A
5
flcl
⊢
A
∈
ℝ
→
A
∈
ℤ
6
zmax
⊢
A
∈
ℝ
→
∃!
x
∈
ℤ
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
7
breq1
⊢
x
=
A
→
x
≤
A
↔
A
≤
A
8
breq2
⊢
x
=
A
→
y
≤
x
↔
y
≤
A
9
8
imbi2d
⊢
x
=
A
→
y
≤
A
→
y
≤
x
↔
y
≤
A
→
y
≤
A
10
9
ralbidv
⊢
x
=
A
→
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
↔
∀
y
∈
ℤ
y
≤
A
→
y
≤
A
11
7
10
anbi12d
⊢
x
=
A
→
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
↔
A
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
A
12
11
riota2
⊢
A
∈
ℤ
∧
∃!
x
∈
ℤ
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
→
A
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
A
↔
ι
x
∈
ℤ
|
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
=
A
13
5
6
12
syl2anc
⊢
A
∈
ℝ
→
A
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
A
↔
ι
x
∈
ℤ
|
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
=
A
14
1
4
13
mpbi2and
⊢
A
∈
ℝ
→
ι
x
∈
ℤ
|
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x
=
A
15
14
eqcomd
⊢
A
∈
ℝ
→
A
=
ι
x
∈
ℤ
|
x
≤
A
∧
∀
y
∈
ℤ
y
≤
A
→
y
≤
x