Metamath Proof Explorer

Theorem fzosplitpr

Description: Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 df-2 ⊢ 2 = ( 1 + 1 )
2 1 a1i ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 2 = ( 1 + 1 ) )
3 2 oveq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + 2 ) = ( 𝐵 + ( 1 + 1 ) ) )
4 eluzelcn ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℂ )
5 1cnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 1 ∈ ℂ )
6 add32r ⊢ ( ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐵 + ( 1 + 1 ) ) = ( ( 𝐵 + 1 ) + 1 ) )
7 4 5 5 6 syl3anc ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + ( 1 + 1 ) ) = ( ( 𝐵 + 1 ) + 1 ) )
8 3 7 eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + 2 ) = ( ( 𝐵 + 1 ) + 1 ) )
9 8 oveq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 2 ) ) = ( 𝐴 ..^ ( ( 𝐵 + 1 ) + 1 ) ) )
10 peano2uz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
11 fzosplitsn ⊢ ( ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( ( 𝐵 + 1 ) + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 + 1 ) ) ∪ { ( 𝐵 + 1 ) } ) )
12 10 11 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( ( 𝐵 + 1 ) + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 + 1 ) ) ∪ { ( 𝐵 + 1 ) } ) )
13 fzosplitsn ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) )
14 13 uneq1d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ..^ ( 𝐵 + 1 ) ) ∪ { ( 𝐵 + 1 ) } ) = ( ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) ∪ { ( 𝐵 + 1 ) } ) )
15 unass ⊢ ( ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) ∪ { ( 𝐵 + 1 ) } ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( { 𝐵 } ∪ { ( 𝐵 + 1 ) } ) )
16 15 a1i ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 } ) ∪ { ( 𝐵 + 1 ) } ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( { 𝐵 } ∪ { ( 𝐵 + 1 ) } ) ) )
17 df-pr ⊢ { 𝐵 , ( 𝐵 + 1 ) } = ( { 𝐵 } ∪ { ( 𝐵 + 1 ) } )
18 17 eqcomi ⊢ ( { 𝐵 } ∪ { ( 𝐵 + 1 ) } ) = { 𝐵 , ( 𝐵 + 1 ) }
19 18 a1i ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( { 𝐵 } ∪ { ( 𝐵 + 1 ) } ) = { 𝐵 , ( 𝐵 + 1 ) } )
20 19 uneq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ..^ 𝐵 ) ∪ ( { 𝐵 } ∪ { ( 𝐵 + 1 ) } ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 , ( 𝐵 + 1 ) } ) )
21 14 16 20 3eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ..^ ( 𝐵 + 1 ) ) ∪ { ( 𝐵 + 1 ) } ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 , ( 𝐵 + 1 ) } ) )
22 9 12 21 3eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( 𝐵 + 2 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ { 𝐵 , ( 𝐵 + 1 ) } ) )