Metamath Proof Explorer


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 ( 𝐴 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐴 < 𝑁 ) )