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

Metamath Proof Explorer

Theorem fzofzp1b

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion fzofzp1b ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ↔ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fzofzp1 ⊢ ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) → ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) )
2 simpl ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) )
3 eluzelz ⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐶 ∈ ℤ )
4 elfzuz3 ⊢ ( ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) )
5 eluzp1m1 ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
6 3 4 5 syl2an ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
7 elfzuzb ⊢ ( 𝐶 ∈ ( 𝐴 ... ( 𝐵 − 1 ) ) ↔ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
8 2 6 7 sylanbrc ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) → 𝐶 ∈ ( 𝐴 ... ( 𝐵 − 1 ) ) )
9 elfzel2 ⊢ ( ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) → 𝐵 ∈ ℤ )
10 9 adantl ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) → 𝐵 ∈ ℤ )
11 fzoval ⊢ ( 𝐵 ∈ ℤ → ( 𝐴 ..^ 𝐵 ) = ( 𝐴 ... ( 𝐵 − 1 ) ) )
12 10 11 syl ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) → ( 𝐴 ..^ 𝐵 ) = ( 𝐴 ... ( 𝐵 − 1 ) ) )
13 8 12 eleqtrrd ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) → 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) )
14 13 ex ⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) → 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ) )
15 1 14 impbid2 ⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ↔ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) )