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

Metamath Proof Explorer

Theorem flval2

Description: An alternate way to define the floor function. (Contributed by NM, 16-Nov-2004)

Ref Expression
Assertion flval2 ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 flle ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
2 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( 𝑦 ≤ 𝐴 ↔ 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) )
3 2 biimpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) )
4 3 ralrimiva ⊢ ( 𝐴 ∈ ℝ → ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) )
5 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
6 zmax ⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) )
7 breq1 ⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥 ≤ 𝐴 ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) )
8 breq2 ⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ↔ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) ) )
10 9 ralbidv ⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ↔ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) ) )
11 7 10 anbi12d ⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ↔ ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) ) ) )
12 11 riota2 ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) = ( ⌊ ‘ 𝐴 ) ) )
13 5 6 12 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) = ( ⌊ ‘ 𝐴 ) ) )
14 1 4 13 mpbi2and ⊢ ( 𝐴 ∈ ℝ → ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) = ( ⌊ ‘ 𝐴 ) )
15 14 eqcomd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) )