Step |
Hyp |
Ref |
Expression |
1 |
|
flval |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) ) |
2 |
1
|
eqcomd |
⊢ ( 𝐴 ∈ ℝ → ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = ( ⌊ ‘ 𝐴 ) ) |
3 |
|
flcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
4 |
|
rebtwnz |
⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) |
5 |
|
breq1 |
⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥 ≤ 𝐴 ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) ) |
6 |
|
oveq1 |
⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥 + 1 ) = ( ( ⌊ ‘ 𝐴 ) + 1 ) ) |
7 |
6
|
breq2d |
⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝐴 < ( 𝑥 + 1 ) ↔ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) |
8 |
5 7
|
anbi12d |
⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ↔ ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ) |
9 |
8
|
riota2 |
⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = ( ⌊ ‘ 𝐴 ) ) ) |
10 |
3 4 9
|
syl2anc |
⊢ ( 𝐴 ∈ ℝ → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = ( ⌊ ‘ 𝐴 ) ) ) |
11 |
2 10
|
mpbird |
⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) |