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 ⊢A∈ℤ∧B∈ℤ≥A+1→A..^B=A..^B−1∪B−1

Proof

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