Theorem fzen 9062

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

Assertion

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

Proof of Theorem fzen

Dummy variables 𝑘 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzf 9033	. . . . 5 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
2		ffn 5066	. . . . 5 ⊢ (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
3	1, 2	ax-mp 7	. . . 4 ⊢ ... Fn (ℤ × ℤ)
4		fnovex 5558	. . . 4 ⊢ ((... Fn (ℤ × ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ V)
5	3, 4	mp3an1 1255	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ V)
6	5	3adant3 958	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ∈ V)
7		simp1 938	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑀 ∈ ℤ)
8		simp3 940	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈ ℤ)
9	7, 8	zaddcld 8473	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
10		simp2 939	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℤ)
11	10, 8	zaddcld 8473	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
12		fnovex 5558	. . . 4 ⊢ ((... Fn (ℤ × ℤ) ∧ (𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
13	3, 12	mp3an1 1255	. . 3 ⊢ (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
14	9, 11, 13	syl2anc 403	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
15		elfz1 9034	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
16	15	biimpd 142	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
17	16	3adant3 958	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
18		zaddcl 8391	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ℤ)
19	18	expcom 114	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ))
20	19	3ad2ant3 961	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ))
21	20	adantrd 273	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ∈ ℤ))
22		zre 8355	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
23		zre 8355	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
24		zre 8355	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℝ)
25		leadd1 7534	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 ≤ 𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
26	22, 23, 24, 25	syl3an 1211	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
27	26	biimpd 142	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝑘 → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
28	27	adantrd 273	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
29	28	3com23 1144	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
30	29	3expia 1140	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))))
31	30	impd 251	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
32	31	3adant2 957	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
33		zre 8355	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
34		leadd1 7534	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑘 ≤ 𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
35	23, 33, 24, 34	syl3an 1211	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
36	35	biimpd 142	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ≤ 𝑁 → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
37	36	adantld 272	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
38	37	3coml 1145	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
39	38	3expia 1140	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
40	39	impd 251	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
41	40	3adant1 956	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
42	21, 32, 41	3jcad 1119	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
43		zaddcl 8391	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
44	43	3adant2 957	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
45		zaddcl 8391	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
46	45	3adant1 956	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
47		elfz1 9034	. . . . . . . . 9 ⊢ (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
48	44, 46, 47	syl2anc 403	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
49	48	biimprd 156	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
50	42, 49	syld 44	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
51	50	com12 30	. . . . 5 ⊢ ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
52	51	3impb 1134	. . . 4 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
53	52	com12 30	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
54	17, 53	syld 44	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
55		elfz1 9034	. . . . 5 ⊢ (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))))
56	44, 46, 55	syl2anc 403	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))))
57	56	biimpd 142	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))))
58		zsubcl 8392	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ ℤ)
59	58	expcom 114	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → (𝑚 ∈ ℤ → (𝑚 − 𝐾) ∈ ℤ))
60	59	3ad2ant3 961	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (𝑚 − 𝐾) ∈ ℤ))
61	60	adantrd 273	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ∈ ℤ))
62		zre 8355	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℤ → 𝑚 ∈ ℝ)
63		leaddsub 7542	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑀 + 𝐾) ≤ 𝑚 ↔ 𝑀 ≤ (𝑚 − 𝐾)))
64	22, 24, 62, 63	syl3an 1211	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚 ↔ 𝑀 ≤ (𝑚 − 𝐾)))
65	64	biimpd 142	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚 → 𝑀 ≤ (𝑚 − 𝐾)))
66	65	adantrd 273	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚 − 𝐾)))
67	66	3expia 1140	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚 − 𝐾))))
68	67	impd 251	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚 − 𝐾)))
69	68	3adant2 957	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚 − 𝐾)))
70		lesubadd 7538	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑚 − 𝐾) ≤ 𝑁 ↔ 𝑚 ≤ (𝑁 + 𝐾)))
71	62, 24, 33, 70	syl3an 1211	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 − 𝐾) ≤ 𝑁 ↔ 𝑚 ≤ (𝑁 + 𝐾)))
72	71	biimprd 156	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ≤ (𝑁 + 𝐾) → (𝑚 − 𝐾) ≤ 𝑁))
73	72	adantld 272	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ≤ 𝑁))
74	73	3coml 1145	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ≤ 𝑁))
75	74	3expia 1140	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ≤ 𝑁)))
76	75	impd 251	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ≤ 𝑁))
77	76	ancoms 264	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ≤ 𝑁))
78	77	3adant1 956	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ≤ 𝑁))
79	61, 69, 78	3jcad 1119	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → ((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁)))
80		elfz1 9034	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 − 𝐾) ∈ (𝑀...𝑁) ↔ ((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁)))
81	80	biimprd 156	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
82	81	3adant3 958	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
83	79, 82	syld 44	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
84	83	com12 30	. . . . 5 ⊢ ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
85	84	3impb 1134	. . . 4 ⊢ ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
86	85	com12 30	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
87	57, 86	syld 44	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚 − 𝐾) ∈ (𝑀...𝑁)))
88	17	imp 122	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))
89	88	simp1d 950	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℤ)
90	89	ex 113	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ))
91	57	imp 122	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)))
92	91	simp1d 950	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → 𝑚 ∈ ℤ)
93	92	ex 113	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑚 ∈ ℤ))
94		zcn 8356	. . . . . . 7 ⊢ (𝑚 ∈ ℤ → 𝑚 ∈ ℂ)
95		zcn 8356	. . . . . . 7 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
96		zcn 8356	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97		subadd 7311	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚 − 𝐾) = 𝑘 ↔ (𝐾 + 𝑘) = 𝑚))
98		eqcom 2083	. . . . . . . . 9 ⊢ ((𝑚 − 𝐾) = 𝑘 ↔ 𝑘 = (𝑚 − 𝐾))
99		eqcom 2083	. . . . . . . . 9 ⊢ ((𝐾 + 𝑘) = 𝑚 ↔ 𝑚 = (𝐾 + 𝑘))
100	97, 98, 99	3bitr3g 220	. . . . . . . 8 ⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝐾 + 𝑘)))
101		addcom 7245	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾))
102	101	3adant1 956	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾))
103	102	eqeq2d 2092	. . . . . . . 8 ⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 = (𝐾 + 𝑘) ↔ 𝑚 = (𝑘 + 𝐾)))
104	100, 103	bitrd 186	. . . . . . 7 ⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
105	94, 95, 96, 104	syl3an 1211	. . . . . 6 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
106	105	3coml 1145	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
107	106	3expib 1141	. . . 4 ⊢ (𝐾 ∈ ℤ → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
108	107	3ad2ant3 961	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
109	90, 93, 108	syl2and 289	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
110	6, 14, 54, 87, 109	en3d 6272	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∧ w3a 919   = wceq 1284   ∈ wcel 1433  Vcvv 2601  𝒫 cpw 3382   class class class wbr 3785   × cxp 4361   Fn wfn 4917  ⟶wf 4918  (class class class)co 5532   ≈ cen 6242  ℂcc 6979  ℝcr 6980   + caddc 6984   ≤ cle 7154   − cmin 7279  ℤcz 8351  ...cfz 9029

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-cnex 7067  ax-resscn 7068  ax-1cn 7069  ax-1re 7070  ax-icn 7071  ax-addcl 7072  ax-addrcl 7073  ax-mulcl 7074  ax-addcom 7076  ax-addass 7078  ax-distr 7080  ax-i2m1 7081  ax-0lt1 7082  ax-0id 7084  ax-rnegex 7085  ax-cnre 7087  ax-pre-ltirr 7088  ax-pre-ltwlin 7089  ax-pre-lttrn 7090  ax-pre-ltadd 7092

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-nel 2340  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-en 6245  df-pnf 7155  df-mnf 7156  df-xr 7157  df-ltxr 7158  df-le 7159  df-sub 7281  df-neg 7282  df-inn 8040  df-n0 8289  df-z 8352  df-fz 9030

This theorem is referenced by:  fz01en  9072  frecfzen2  9420