This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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