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 |
⊢ ( 𝐴 ∈ ( 0 [,) 1 ) → 𝐴 ∈ ℝ ) |
6 |
|
0xr |
⊢ 0 ∈ ℝ* |
7 |
|
elico1 |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝐴 ∈ ( 0 [,) 1 ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < 1 ) ) ) |
8 |
6 2 7
|
mp2an |
⊢ ( 𝐴 ∈ ( 0 [,) 1 ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < 1 ) ) |
9 |
8
|
simp2bi |
⊢ ( 𝐴 ∈ ( 0 [,) 1 ) → 0 ≤ 𝐴 ) |
10 |
8
|
simp3bi |
⊢ ( 𝐴 ∈ ( 0 [,) 1 ) → 𝐴 < 1 ) |
11 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
12 |
11
|
addid2d |
⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 ) |
13 |
12
|
fveqeq2d |
⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 0 + 𝐴 ) ) = 0 ↔ ( ⌊ ‘ 𝐴 ) = 0 ) ) |
14 |
|
0z |
⊢ 0 ∈ ℤ |
15 |
|
flbi2 |
⊢ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( 0 + 𝐴 ) ) = 0 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < 1 ) ) ) |
16 |
14 15
|
mpan |
⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 0 + 𝐴 ) ) = 0 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < 1 ) ) ) |
17 |
13 16
|
bitr3d |
⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = 0 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < 1 ) ) ) |
18 |
17
|
biimpar |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 1 ) ) → ( ⌊ ‘ 𝐴 ) = 0 ) |
19 |
5 9 10 18
|
syl12anc |
⊢ ( 𝐴 ∈ ( 0 [,) 1 ) → ( ⌊ ‘ 𝐴 ) = 0 ) |