This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ico01fl0

Description: The floor of a real number in [ 0 , 1 ) is 0. Remark: may shorten the proof of modid or a version of it where the antecedent is membership in an interval. (Contributed by BJ, 29-Jun-2019)

Ref Expression
Assertion ico01fl0 ⊢ A ∈ 0 1 → A = 0

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 1xr ⊢ 1 ∈ ℝ *
3 icossre ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ * → 0 1 ⊆ ℝ
4 1 2 3 mp2an ⊢ 0 1 ⊆ ℝ
5 4 sseli ⊢ A ∈ 0 1 → A ∈ ℝ
6 0xr ⊢ 0 ∈ ℝ *
7 elico1 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ * → A ∈ 0 1 ↔ A ∈ ℝ * ∧ 0 ≤ A ∧ A < 1
8 6 2 7 mp2an ⊢ A ∈ 0 1 ↔ A ∈ ℝ * ∧ 0 ≤ A ∧ A < 1
9 8 simp2bi ⊢ A ∈ 0 1 → 0 ≤ A
10 8 simp3bi ⊢ A ∈ 0 1 → A < 1
11 recn ⊢ A ∈ ℝ → A ∈ ℂ
12 11 addlidd ⊢ A ∈ ℝ → 0 + A = A
13 12 fveqeq2d ⊢ A ∈ ℝ → 0 + A = 0 ↔ A = 0
14 0z ⊢ 0 ∈ ℤ
15 flbi2 ⊢ 0 ∈ ℤ ∧ A ∈ ℝ → 0 + A = 0 ↔ 0 ≤ A ∧ A < 1
16 14 15 mpan ⊢ A ∈ ℝ → 0 + A = 0 ↔ 0 ≤ A ∧ A < 1
17 13 16 bitr3d ⊢ A ∈ ℝ → A = 0 ↔ 0 ≤ A ∧ A < 1
18 17 biimpar ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A < 1 → A = 0
19 5 9 10 18 syl12anc ⊢ A ∈ 0 1 → A = 0