Metamath Proof Explorer

Theorem fzopredsuc

Description: Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if N = M (then ( M ... N ) = { M } = ( { M } u. (/) ) u. { M } ) . (Contributed by AV, 14-Jul-2020)

Ref Expression
Assertion fzopredsuc 
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) )

Proof

Step Hyp Ref Expression
1 unidm 
 |-  ( { N } u. { N } ) = { N }
2 1 eqcomi 
 |-  { N } = ( { N } u. { N } )
3 oveq1 
 |-  ( M = N -> ( M ... N ) = ( N ... N ) )
4 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
5 3 4 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = N ) -> ( M ... N ) = { N } )
6 sneq 
 |-  ( M = N -> { M } = { N } )
7 oveq1 
 |-  ( M = N -> ( M + 1 ) = ( N + 1 ) )
8 7 oveq1d 
 |-  ( M = N -> ( ( M + 1 ) ..^ N ) = ( ( N + 1 ) ..^ N ) )
9 6 8 uneq12d 
 |-  ( M = N -> ( { M } u. ( ( M + 1 ) ..^ N ) ) = ( { N } u. ( ( N + 1 ) ..^ N ) ) )
10 9 uneq1d 
 |-  ( M = N -> ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) = ( ( { N } u. ( ( N + 1 ) ..^ N ) ) u. { N } ) )
11 zre 
 |-  ( N e. ZZ -> N e. RR )
12 11 lep1d 
 |-  ( N e. ZZ -> N <_ ( N + 1 ) )
13 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
14 13 zred 
 |-  ( N e. ZZ -> ( N + 1 ) e. RR )
15 11 14 lenltd 
 |-  ( N e. ZZ -> ( N <_ ( N + 1 ) <-> -. ( N + 1 ) < N ) )
16 12 15 mpbid 
 |-  ( N e. ZZ -> -. ( N + 1 ) < N )
17 fzonlt0 
 |-  ( ( ( N + 1 ) e. ZZ /\ N e. ZZ ) -> ( -. ( N + 1 ) < N <-> ( ( N + 1 ) ..^ N ) = (/) ) )
18 13 17 mpancom 
 |-  ( N e. ZZ -> ( -. ( N + 1 ) < N <-> ( ( N + 1 ) ..^ N ) = (/) ) )
19 16 18 mpbid 
 |-  ( N e. ZZ -> ( ( N + 1 ) ..^ N ) = (/) )
20 19 uneq2d 
 |-  ( N e. ZZ -> ( { N } u. ( ( N + 1 ) ..^ N ) ) = ( { N } u. (/) ) )
21 un0 
 |-  ( { N } u. (/) ) = { N }
22 20 21 eqtrdi 
 |-  ( N e. ZZ -> ( { N } u. ( ( N + 1 ) ..^ N ) ) = { N } )
23 22 uneq1d 
 |-  ( N e. ZZ -> ( ( { N } u. ( ( N + 1 ) ..^ N ) ) u. { N } ) = ( { N } u. { N } ) )
24 10 23 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = N ) -> ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) = ( { N } u. { N } ) )
25 2 5 24 3eqtr4a 
 |-  ( ( N e. ZZ /\ M = N ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) )
26 25 ex 
 |-  ( N e. ZZ -> ( M = N -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) ) )
27 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
28 26 27 syl11 
 |-  ( M = N -> ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) ) )
29 fzisfzounsn 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ..^ N ) u. { N } ) )
30 29 adantl 
 |-  ( ( -. M = N /\ N e. ( ZZ>= ` M ) ) -> ( M ... N ) = ( ( M ..^ N ) u. { N } ) )
31 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
32 simpl1 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ -. M = N ) -> M e. ZZ )
33 simpl2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ -. M = N ) -> N e. ZZ )
34 nesym 
 |-  ( N =/= M <-> -. M = N )
35 zre 
 |-  ( M e. ZZ -> M e. RR )
36 ltlen 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N <-> ( M <_ N /\ N =/= M ) ) )
37 35 11 36 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M <_ N /\ N =/= M ) ) )
38 37 biimprd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M <_ N /\ N =/= M ) -> M < N ) )
39 38 exp4b 
 |-  ( M e. ZZ -> ( N e. ZZ -> ( M <_ N -> ( N =/= M -> M < N ) ) ) )
40 39 3imp 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( N =/= M -> M < N ) )
41 34 40 biimtrrid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( -. M = N -> M < N ) )
42 41 imp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ -. M = N ) -> M < N )
43 32 33 42 3jca 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) /\ -. M = N ) -> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
44 43 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( -. M = N -> ( M e. ZZ /\ N e. ZZ /\ M < N ) ) )
45 31 44 sylbi 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. M = N -> ( M e. ZZ /\ N e. ZZ /\ M < N ) ) )
46 45 impcom 
 |-  ( ( -. M = N /\ N e. ( ZZ>= ` M ) ) -> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
47 fzopred 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( M ..^ N ) = ( { M } u. ( ( M + 1 ) ..^ N ) ) )
48 46 47 syl 
 |-  ( ( -. M = N /\ N e. ( ZZ>= ` M ) ) -> ( M ..^ N ) = ( { M } u. ( ( M + 1 ) ..^ N ) ) )
49 48 uneq1d 
 |-  ( ( -. M = N /\ N e. ( ZZ>= ` M ) ) -> ( ( M ..^ N ) u. { N } ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) )
50 30 49 eqtrd 
 |-  ( ( -. M = N /\ N e. ( ZZ>= ` M ) ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) )
51 50 ex 
 |-  ( -. M = N -> ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) ) )
52 28 51 pm2.61i 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 ) ..^ N ) ) u. { N } ) )