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 ) ∈ ( 𝐴 ..^ 𝐵 ) )