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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ≈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )