Theorem flval2

Description: An alternate way to define the floor (greatest integer) 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	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) ) )