Metamath Proof Explorer

Theorem fzosplitprm1

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

Ref Expression
Assertion fzosplitprm1 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℤ )
2 peano2zm ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 − 1 ) ∈ ℤ )
3 2 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 1 ) ∈ ℤ )
4 zltlem1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ 𝐴 ≤ ( 𝐵 − 1 ) ) )
5 4 biimp3a ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ ( 𝐵 − 1 ) )
6 eluz2 ⊢ ( ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) ↔ ( 𝐴 ∈ ℤ ∧ ( 𝐵 − 1 ) ∈ ℤ ∧ 𝐴 ≤ ( 𝐵 − 1 ) ) )
7 1 3 5 6 syl3anbrc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
8 fzosplitpr ⊢ ( ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 2 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , ( ( 𝐵 − 1 ) + 1 ) } ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 2 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , ( ( 𝐵 − 1 ) + 1 ) } ) )
10 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
11 1cnd ⊢ ( 𝐵 ∈ ℤ → 1 ∈ ℂ )
12 2cnd ⊢ ( 𝐵 ∈ ℤ → 2 ∈ ℂ )
13 10 11 12 subadd23d ⊢ ( 𝐵 ∈ ℤ → ( ( 𝐵 − 1 ) + 2 ) = ( 𝐵 + ( 2 − 1 ) ) )
14 2m1e1 ⊢ ( 2 − 1 ) = 1
15 14 oveq2i ⊢ ( 𝐵 + ( 2 − 1 ) ) = ( 𝐵 + 1 )
16 13 15 eqtr2di ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 + 1 ) = ( ( 𝐵 − 1 ) + 2 ) )
17 16 oveq2d ⊢ ( 𝐵 ∈ ℤ → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 2 ) ) )
18 npcan1 ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
19 10 18 syl ⊢ ( 𝐵 ∈ ℤ → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
20 19 eqcomd ⊢ ( 𝐵 ∈ ℤ → 𝐵 = ( ( 𝐵 − 1 ) + 1 ) )
21 20 preq2d ⊢ ( 𝐵 ∈ ℤ → { ( 𝐵 − 1 ) , 𝐵 } = { ( 𝐵 − 1 ) , ( ( 𝐵 − 1 ) + 1 ) } )
22 21 uneq2d ⊢ ( 𝐵 ∈ ℤ → ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , 𝐵 } ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , ( ( 𝐵 − 1 ) + 1 ) } ) )
23 17 22 eqeq12d ⊢ ( 𝐵 ∈ ℤ → ( ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , 𝐵 } ) ↔ ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 2 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , ( ( 𝐵 − 1 ) + 1 ) } ) ) )
24 23 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , 𝐵 } ) ↔ ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 2 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , ( ( 𝐵 − 1 ) + 1 ) } ) ) )
25 9 24 mpbird ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) → ( 𝐴 ..^ ( 𝐵 + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) , 𝐵 } ) )