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

Metamath Proof Explorer

Theorem fzosplitsnm1

Description: Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) → 𝐵 ∈ ℤ )
2 1 zcnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) → 𝐵 ∈ ℂ )
3 2 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → 𝐵 ∈ ℂ )
4 ax-1cn ⊢ 1 ∈ ℂ
5 npcan ⊢ ( ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
6 5 eqcomd ⊢ ( ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) → 𝐵 = ( ( 𝐵 − 1 ) + 1 ) )
7 3 4 6 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → 𝐵 = ( ( 𝐵 − 1 ) + 1 ) )
8 7 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( 𝐴 ..^ 𝐵 ) = ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 1 ) ) )
9 eluzp1m1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
10 1 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → 𝐵 ∈ ℤ )
11 peano2zm ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 − 1 ) ∈ ℤ )
12 uzid ⊢ ( ( 𝐵 − 1 ) ∈ ℤ → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐵 − 1 ) ) )
13 peano2uz ⊢ ( ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐵 − 1 ) ) → ( ( 𝐵 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝐵 − 1 ) ) )
14 10 11 12 13 4syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( ( 𝐵 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝐵 − 1 ) ) )
15 elfzuzb ⊢ ( ( 𝐵 − 1 ) ∈ ( 𝐴 ... ( ( 𝐵 − 1 ) + 1 ) ) ↔ ( ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( ( 𝐵 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝐵 − 1 ) ) ) )
16 9 14 15 sylanbrc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( 𝐵 − 1 ) ∈ ( 𝐴 ... ( ( 𝐵 − 1 ) + 1 ) ) )
17 fzosplit ⊢ ( ( 𝐵 − 1 ) ∈ ( 𝐴 ... ( ( 𝐵 − 1 ) + 1 ) ) → ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ ( ( 𝐵 − 1 ) ..^ ( ( 𝐵 − 1 ) + 1 ) ) ) )
18 16 17 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( 𝐴 ..^ ( ( 𝐵 − 1 ) + 1 ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ ( ( 𝐵 − 1 ) ..^ ( ( 𝐵 − 1 ) + 1 ) ) ) )
19 1 11 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) → ( 𝐵 − 1 ) ∈ ℤ )
20 19 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( 𝐵 − 1 ) ∈ ℤ )
21 fzosn ⊢ ( ( 𝐵 − 1 ) ∈ ℤ → ( ( 𝐵 − 1 ) ..^ ( ( 𝐵 − 1 ) + 1 ) ) = { ( 𝐵 − 1 ) } )
22 20 21 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( ( 𝐵 − 1 ) ..^ ( ( 𝐵 − 1 ) + 1 ) ) = { ( 𝐵 − 1 ) } )
23 22 uneq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ ( ( 𝐵 − 1 ) ..^ ( ( 𝐵 − 1 ) + 1 ) ) ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) )
24 8 18 23 3eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( 𝐴 ..^ 𝐵 ) = ( ( 𝐴 ..^ ( 𝐵 − 1 ) ) ∪ { ( 𝐵 − 1 ) } ) )