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

Metamath Proof Explorer

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 ) = 𝐶 ) )