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

Metamath Proof Explorer

Theorem fzosplitsn

Description: Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzosplitsn ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
2 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
3 uzid ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ( ℤ≥ ‘ 𝐵 ) )
4 peano2uz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐵 ) → ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐵 ) )
5 2 3 4 3syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐵 ) )
6 elfzuzb ⊢ ( 𝐵 ∈ ( 𝐴 ... ( 𝐵 + 1 ) ) ↔ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) )
7 1 5 6 sylanbrc ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ( 𝐴 ... ( 𝐵 + 1 ) ) )
8 fzosplit ⊢ ( 𝐵 ∈ ( 𝐴 ... ( 𝐵 + 1 ) ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( 𝐵 ..^ ( 𝐵 + 1 ) ) ) )
9 7 8 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( 𝐵 ..^ ( 𝐵 + 1 ) ) ) )
10 fzosn ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ..^ ( 𝐵 + 1 ) ) = { 𝐵 } )
11 2 10 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 ..^ ( 𝐵 + 1 ) ) = { 𝐵 } )
12 11 uneq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ..^ 𝐵 ) ∪ ( 𝐵 ..^ ( 𝐵 + 1 ) ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) )
13 9 12 eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) )