Theorem fzolb

Description: The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with M < N . This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate M e. ( ZZ>=N ) . (Contributed by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	fzolb	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo2	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
2		eluzel2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
3		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
4	2 3	impbii	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ∈ ℤ )
5	4	3anbi1i	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
6	1 5	bitri	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )