Theorem fzostep1

Description: Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Assertion	fzostep1	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ 𝐶 ) ∨ ( 𝐴 + 1 ) = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoel1	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 ∈ ℤ )
2		uzid	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ( ℤ≥ ‘ 𝐵 ) )
3		peano2uz	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐵 ) → ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐵 ) )
4		fzoss1	⊢ ( ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐵 ) → ( ( 𝐵 + 1 ) ..^ ( 𝐶 + 1 ) ) ⊆ ( 𝐵 ..^ ( 𝐶 + 1 ) ) )
5	1 2 3 4	4syl	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( ( 𝐵 + 1 ) ..^ ( 𝐶 + 1 ) ) ⊆ ( 𝐵 ..^ ( 𝐶 + 1 ) ) )
6		1z	⊢ 1 ∈ ℤ
7		fzoaddel	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 1 ∈ ℤ ) → ( 𝐴 + 1 ) ∈ ( ( 𝐵 + 1 ) ..^ ( 𝐶 + 1 ) ) )
8	6 7	mpan2	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐴 + 1 ) ∈ ( ( 𝐵 + 1 ) ..^ ( 𝐶 + 1 ) ) )
9	5 8	sseldd	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ ( 𝐶 + 1 ) ) )
10		elfzoel2	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ )
11		elfzolt3	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 < 𝐶 )
12		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
13		zre	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℝ )
14		ltle	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 → 𝐵 ≤ 𝐶 ) )
15	12 13 14	syl2an	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 < 𝐶 → 𝐵 ≤ 𝐶 ) )
16	1 10 15	syl2anc	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐵 < 𝐶 → 𝐵 ≤ 𝐶 ) )
17	11 16	mpd	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 ≤ 𝐶 )
18		eluz2	⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ↔ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ≤ 𝐶 ) )
19	1 10 17 18	syl3anbrc	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) )
20		fzosplitsni	⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) → ( ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ ( 𝐶 + 1 ) ) ↔ ( ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ 𝐶 ) ∨ ( 𝐴 + 1 ) = 𝐶 ) ) )
21	19 20	syl	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ ( 𝐶 + 1 ) ) ↔ ( ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ 𝐶 ) ∨ ( 𝐴 + 1 ) = 𝐶 ) ) )
22	9 21	mpbid	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( ( 𝐴 + 1 ) ∈ ( 𝐵 ..^ 𝐶 ) ∨ ( 𝐴 + 1 ) = 𝐶 ) )