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

Metamath Proof Explorer

Theorem fzen

Description: A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009)

Ref Expression
Assertion fzen ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ≈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 ovexd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ∈ V )
2 ovexd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∈ V )
3 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
4 3 biimpd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
5 4 3adant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
6 zaddcl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 + 𝐾 ) ∈ ℤ )
7 6 expcom ⊢ ( 𝐾 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑘 + 𝐾 ) ∈ ℤ ) )
8 7 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ℤ → ( 𝑘 + 𝐾 ) ∈ ℤ ) )
9 8 adantrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( 𝑘 + 𝐾 ) ∈ ℤ ) )
10 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
11 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
12 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
13 leadd1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ 𝑘 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
14 10 11 12 13 syl3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝑘 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
15 14 biimpd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝑘 → ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
16 15 adantrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
17 16 3com23 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
18 17 3expia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ℤ → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) ) )
19 18 impd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
20 19 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ) )
21 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
22 leadd1 ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑘 ≤ 𝑁 ↔ ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
23 11 21 12 22 syl3an ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ≤ 𝑁 ↔ ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
24 23 biimpd ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ≤ 𝑁 → ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
25 24 adantld ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
26 25 3coml ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
27 26 3expia ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ℤ → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
28 27 impd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
29 28 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
30 9 20 29 3jcad ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( ( 𝑘 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ∧ ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
31 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
32 31 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
33 zaddcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
34 33 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
35 elfz1 ⊢ ( ( ( 𝑀 + 𝐾 ) ∈ ℤ ∧ ( 𝑁 + 𝐾 ) ∈ ℤ ) → ( ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝑘 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ∧ ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
36 32 34 35 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝑘 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ∧ ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
37 36 biimprd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑘 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑘 + 𝐾 ) ∧ ( 𝑘 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
38 30 37 syldc ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
39 38 3impb ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
40 39 com12 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
41 5 40 syld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
42 elfz1 ⊢ ( ( ( 𝑀 + 𝐾 ) ∈ ℤ ∧ ( 𝑁 + 𝐾 ) ∈ ℤ ) → ( 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( 𝑚 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) )
43 32 34 42 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( 𝑚 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) )
44 43 biimpd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → ( 𝑚 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) )
45 zsubcl ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 − 𝐾 ) ∈ ℤ )
46 45 expcom ⊢ ( 𝐾 ∈ ℤ → ( 𝑚 ∈ ℤ → ( 𝑚 − 𝐾 ) ∈ ℤ ) )
47 46 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ℤ → ( 𝑚 − 𝐾 ) ∈ ℤ ) )
48 47 adantrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → ( 𝑚 − 𝐾 ) ∈ ℤ ) )
49 zre ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℝ )
50 leaddsub ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ↔ 𝑀 ≤ ( 𝑚 − 𝐾 ) ) )
51 10 12 49 50 syl3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ↔ 𝑀 ≤ ( 𝑚 − 𝐾 ) ) )
52 51 biimpd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑚 → 𝑀 ≤ ( 𝑚 − 𝐾 ) ) )
53 52 adantrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → 𝑀 ≤ ( 𝑚 − 𝐾 ) ) )
54 53 3expia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ℤ → ( ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → 𝑀 ≤ ( 𝑚 − 𝐾 ) ) ) )
55 54 impd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → 𝑀 ≤ ( 𝑚 − 𝐾 ) ) )
56 55 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → 𝑀 ≤ ( 𝑚 − 𝐾 ) ) )
57 lesubadd ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑚 − 𝐾 ) ≤ 𝑁 ↔ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) )
58 49 12 21 57 syl3an ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑚 − 𝐾 ) ≤ 𝑁 ↔ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) )
59 58 biimprd ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑚 ≤ ( 𝑁 + 𝐾 ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) )
60 59 adantld ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) )
61 60 3coml ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) )
62 61 3expia ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑚 ∈ ℤ → ( ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) ) )
63 62 impd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) )
64 63 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) )
65 64 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → ( 𝑚 − 𝐾 ) ≤ 𝑁 ) )
66 48 56 65 3jcad ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑚 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑚 − 𝐾 ) ∧ ( 𝑚 − 𝐾 ) ≤ 𝑁 ) ) )
67 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑚 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑚 − 𝐾 ) ∧ ( 𝑚 − 𝐾 ) ≤ 𝑁 ) ) )
68 67 biimprd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑚 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑚 − 𝐾 ) ∧ ( 𝑚 − 𝐾 ) ≤ 𝑁 ) → ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
69 68 3adant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑚 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑚 − 𝐾 ) ∧ ( 𝑚 − 𝐾 ) ≤ 𝑁 ) → ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
70 66 69 syldc ⊢ ( ( 𝑚 ∈ ℤ ∧ ( ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
71 70 3impb ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
72 71 com12 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) → ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
73 44 72 syld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → ( 𝑚 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
74 5 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) )
75 74 simp1d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
76 75 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ ) )
77 44 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( 𝑚 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑚 ∧ 𝑚 ≤ ( 𝑁 + 𝐾 ) ) )
78 77 simp1d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → 𝑚 ∈ ℤ )
79 78 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → 𝑚 ∈ ℤ ) )
80 zcn ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
81 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
82 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
83 subadd ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑚 − 𝐾 ) = 𝑘 ↔ ( 𝐾 + 𝑘 ) = 𝑚 ) )
84 eqcom ⊢ ( ( 𝑚 − 𝐾 ) = 𝑘 ↔ 𝑘 = ( 𝑚 − 𝐾 ) )
85 eqcom ⊢ ( ( 𝐾 + 𝑘 ) = 𝑚 ↔ 𝑚 = ( 𝐾 + 𝑘 ) )
86 83 84 85 3bitr3g ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝐾 + 𝑘 ) ) )
87 addcom ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐾 + 𝑘 ) = ( 𝑘 + 𝐾 ) )
88 87 3adant1 ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐾 + 𝑘 ) = ( 𝑘 + 𝐾 ) )
89 88 eqeq2d ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑚 = ( 𝐾 + 𝑘 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) )
90 86 89 bitrd ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) )
91 80 81 82 90 syl3an ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) )
92 91 3coml ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) )
93 92 3expib ⊢ ( 𝐾 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) ) )
94 93 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) ) )
95 76 79 94 syl2and ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑚 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( 𝑘 = ( 𝑚 − 𝐾 ) ↔ 𝑚 = ( 𝑘 + 𝐾 ) ) ) )
96 1 2 41 73 95 en3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ≈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )