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

Metamath Proof Explorer

Theorem fzoend

Description: The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzoend ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝐵 − 1 ) ∈ ( 𝐴 ..^ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) )
2 elfzoel2 ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℤ )
3 fzoval ⊢ ( 𝐵 ∈ ℤ → ( 𝐴 ..^ 𝐵 ) = ( 𝐴 ... ( 𝐵 − 1 ) ) )
4 2 3 syl ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝐴 ..^ 𝐵 ) = ( 𝐴 ... ( 𝐵 − 1 ) ) )
5 1 4 eleqtrd ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐴 ∈ ( 𝐴 ... ( 𝐵 − 1 ) ) )
6 elfzuz3 ⊢ ( 𝐴 ∈ ( 𝐴 ... ( 𝐵 − 1 ) ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
7 5 6 syl ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
8 eluzfz2 ⊢ ( ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 − 1 ) ∈ ( 𝐴 ... ( 𝐵 − 1 ) ) )
9 7 8 syl ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝐵 − 1 ) ∈ ( 𝐴 ... ( 𝐵 − 1 ) ) )
10 9 4 eleqtrrd ⊢ ( 𝐴 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝐵 − 1 ) ∈ ( 𝐴 ..^ 𝐵 ) )