Theorem elfzfzo

Description: Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elfzfzo	⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzofz	⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐴 ∈ ( 𝑀 ... 𝑁 ) )
2		elfzolt2	⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐴 < 𝑁 )
3	1 2	jca	⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) )
4		elfzuz	⊢ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) )
6		elfzel2	⊢ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝑁 ∈ ℤ )
8		simpr	⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝐴 < 𝑁 )
9		elfzo2	⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) )
10	5 7 8 9	syl3anbrc	⊢ ( ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) )
11	3 10	impbii	⊢ ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) )