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

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