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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) )

Proof

Step	Hyp	Ref	Expression
1		unidm	⊢ ( { 𝑁 } ∪ { 𝑁 } ) = { 𝑁 }
2	1	eqcomi	⊢ { 𝑁 } = ( { 𝑁 } ∪ { 𝑁 } )
3		oveq1	⊢ ( 𝑀 = 𝑁 → ( 𝑀 ... 𝑁 ) = ( 𝑁 ... 𝑁 ) )
4		fzsn	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
5	3 4	sylan9eqr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = 𝑁 ) → ( 𝑀 ... 𝑁 ) = { 𝑁 } )
6		sneq	⊢ ( 𝑀 = 𝑁 → { 𝑀 } = { 𝑁 } )
7		oveq1	⊢ ( 𝑀 = 𝑁 → ( 𝑀 + 1 ) = ( 𝑁 + 1 ) )
8	7	oveq1d	⊢ ( 𝑀 = 𝑁 → ( ( 𝑀 + 1 ) ..^ 𝑁 ) = ( ( 𝑁 + 1 ) ..^ 𝑁 ) )
9	6 8	uneq12d	⊢ ( 𝑀 = 𝑁 → ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ( { 𝑁 } ∪ ( ( 𝑁 + 1 ) ..^ 𝑁 ) ) )
10	9	uneq1d	⊢ ( 𝑀 = 𝑁 → ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) = ( ( { 𝑁 } ∪ ( ( 𝑁 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) )
11		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
12	11	lep1d	⊢ ( 𝑁 ∈ ℤ → 𝑁 ≤ ( 𝑁 + 1 ) )
13		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
14	13	zred	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℝ )
15	11 14	lenltd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ≤ ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) < 𝑁 ) )
16	12 15	mpbid	⊢ ( 𝑁 ∈ ℤ → ¬ ( 𝑁 + 1 ) < 𝑁 )
17		fzonlt0	⊢ ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑁 + 1 ) < 𝑁 ↔ ( ( 𝑁 + 1 ) ..^ 𝑁 ) = ∅ ) )
18	13 17	mpancom	⊢ ( 𝑁 ∈ ℤ → ( ¬ ( 𝑁 + 1 ) < 𝑁 ↔ ( ( 𝑁 + 1 ) ..^ 𝑁 ) = ∅ ) )
19	16 18	mpbid	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 + 1 ) ..^ 𝑁 ) = ∅ )
20	19	uneq2d	⊢ ( 𝑁 ∈ ℤ → ( { 𝑁 } ∪ ( ( 𝑁 + 1 ) ..^ 𝑁 ) ) = ( { 𝑁 } ∪ ∅ ) )
21		un0	⊢ ( { 𝑁 } ∪ ∅ ) = { 𝑁 }
22	20 21	eqtrdi	⊢ ( 𝑁 ∈ ℤ → ( { 𝑁 } ∪ ( ( 𝑁 + 1 ) ..^ 𝑁 ) ) = { 𝑁 } )
23	22	uneq1d	⊢ ( 𝑁 ∈ ℤ → ( ( { 𝑁 } ∪ ( ( 𝑁 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) = ( { 𝑁 } ∪ { 𝑁 } ) )
24	10 23	sylan9eqr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = 𝑁 ) → ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) = ( { 𝑁 } ∪ { 𝑁 } ) )
25	2 5 24	3eqtr4a	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = 𝑁 ) → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) )
26	25	ex	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 = 𝑁 → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) ) )
27		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
28	26 27	syl11	⊢ ( 𝑀 = 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) ) )
29		fzisfzounsn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) )
30	29	adantl	⊢ ( ( ¬ 𝑀 = 𝑁 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) )
31		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
32		simpl1	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ∧ ¬ 𝑀 = 𝑁 ) → 𝑀 ∈ ℤ )
33		simpl2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ∧ ¬ 𝑀 = 𝑁 ) → 𝑁 ∈ ℤ )
34		nesym	⊢ ( 𝑁 ≠ 𝑀 ↔ ¬ 𝑀 = 𝑁 )
35		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
36		ltlen	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀 ) ) )
37	35 11 36	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀 ) ) )
38	37	biimprd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀 ) → 𝑀 < 𝑁 ) )
39	38	exp4b	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝑁 → ( 𝑁 ≠ 𝑀 → 𝑀 < 𝑁 ) ) ) )
40	39	3imp	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 ≠ 𝑀 → 𝑀 < 𝑁 ) )
41	34 40	syl5bir	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( ¬ 𝑀 = 𝑁 → 𝑀 < 𝑁 ) )
42	41	imp	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ∧ ¬ 𝑀 = 𝑁 ) → 𝑀 < 𝑁 )
43	32 33 42	3jca	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ∧ ¬ 𝑀 = 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
44	43	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( ¬ 𝑀 = 𝑁 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ) )
45	31 44	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ¬ 𝑀 = 𝑁 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ) )
46	45	impcom	⊢ ( ( ¬ 𝑀 = 𝑁 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
47		fzopred	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑀 ..^ 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
48	46 47	syl	⊢ ( ( ¬ 𝑀 = 𝑁 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ..^ 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
49	48	uneq1d	⊢ ( ( ¬ 𝑀 = 𝑁 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) )
50	30 49	eqtrd	⊢ ( ( ¬ 𝑀 = 𝑁 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) )
51	50	ex	⊢ ( ¬ 𝑀 = 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) ) )
52	28 51	pm2.61i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∪ { 𝑁 } ) )