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 ) } ) )