Metamath Proof Explorer

Theorem fzsuc2

Description: Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fzsuc2 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )

Proof

Step Hyp Ref Expression
1 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( 𝑁 = ( 𝑀 − 1 ) ∨ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) ) )
2 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
3 ax-1cn ⊢ 1 ∈ ℂ
4 npcan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
5 2 3 4 sylancl ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
6 5 oveq2d ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( ( 𝑀 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑀 ) )
7 uncom ⊢ ( ∅ ∪ { 𝑀 } ) = ( { 𝑀 } ∪ ∅ )
8 un0 ⊢ ( { 𝑀 } ∪ ∅ ) = { 𝑀 }
9 7 8 eqtri ⊢ ( ∅ ∪ { 𝑀 } ) = { 𝑀 }
10 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
11 10 ltm1d ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) < 𝑀 )
12 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
13 fzn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
14 12 13 mpdan ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
15 11 14 mpbid ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ )
16 5 sneqd ⊢ ( 𝑀 ∈ ℤ → { ( ( 𝑀 − 1 ) + 1 ) } = { 𝑀 } )
17 15 16 uneq12d ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ... ( 𝑀 − 1 ) ) ∪ { ( ( 𝑀 − 1 ) + 1 ) } ) = ( ∅ ∪ { 𝑀 } ) )
18 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
19 9 17 18 3eqtr4a ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ... ( 𝑀 − 1 ) ) ∪ { ( ( 𝑀 − 1 ) + 1 ) } ) = ( 𝑀 ... 𝑀 ) )
20 6 19 eqtr4d ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( ( 𝑀 − 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑀 − 1 ) ) ∪ { ( ( 𝑀 − 1 ) + 1 ) } ) )
21 oveq1 ⊢ ( 𝑁 = ( 𝑀 − 1 ) → ( 𝑁 + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
22 21 oveq2d ⊢ ( 𝑁 = ( 𝑀 − 1 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( 𝑀 ... ( ( 𝑀 − 1 ) + 1 ) ) )
23 oveq2 ⊢ ( 𝑁 = ( 𝑀 − 1 ) → ( 𝑀 ... 𝑁 ) = ( 𝑀 ... ( 𝑀 − 1 ) ) )
24 21 sneqd ⊢ ( 𝑁 = ( 𝑀 − 1 ) → { ( 𝑁 + 1 ) } = { ( ( 𝑀 − 1 ) + 1 ) } )
25 23 24 uneq12d ⊢ ( 𝑁 = ( 𝑀 − 1 ) → ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) = ( ( 𝑀 ... ( 𝑀 − 1 ) ) ∪ { ( ( 𝑀 − 1 ) + 1 ) } ) )
26 22 25 eqeq12d ⊢ ( 𝑁 = ( 𝑀 − 1 ) → ( ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ↔ ( 𝑀 ... ( ( 𝑀 − 1 ) + 1 ) ) = ( ( 𝑀 ... ( 𝑀 − 1 ) ) ∪ { ( ( 𝑀 − 1 ) + 1 ) } ) ) )
27 20 26 syl5ibrcom ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 = ( 𝑀 − 1 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ) )
28 27 imp ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 = ( 𝑀 − 1 ) ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
29 5 fveq2d ⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝑀 ) )
30 29 eleq2d ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
31 30 biimpa ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
32 fzsuc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
33 31 32 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
34 28 33 jaodan ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 = ( 𝑀 − 1 ) ∨ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑀 − 1 ) + 1 ) ) ) ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
35 1 34 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) → ( 𝑀 ... ( 𝑁 + 1 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )