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 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) )