ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fzen GIF version

Theorem fzen 10016
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.
StepHypRef Expression
1 fzf 9986 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
2 ffn 5360 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
31, 2ax-mp 5 . . . 4 ... Fn (ℤ × ℤ)
4 fnovex 5901 . . . 4 ((... Fn (ℤ × ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ V)
53, 4mp3an1 1324 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ V)
653adant3 1017 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ∈ V)
7 simp1 997 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑀 ∈ ℤ)
8 simp3 999 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈ ℤ)
97, 8zaddcld 9355 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
10 simp2 998 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℤ)
1110, 8zaddcld 9355 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
12 fnovex 5901 . . . 4 ((... Fn (ℤ × ℤ) ∧ (𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
133, 12mp3an1 1324 . . 3 (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
149, 11, 13syl2anc 411 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
15 elfz1 9987 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
1615biimpd 144 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
17163adant3 1017 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
18 zaddcl 9269 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ℤ)
1918expcom 116 . . . . . . . . . 10 (𝐾 ∈ ℤ → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ))
20193ad2ant3 1020 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ))
2120adantrd 279 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ∈ ℤ))
22 zre 9233 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
23 zre 9233 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
24 zre 9233 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℤ → 𝐾 ∈ ℝ)
25 leadd1 8364 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
2622, 23, 24, 25syl3an 1280 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
2726biimpd 144 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀𝑘 → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
2827adantrd 279 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
29283com23 1209 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
30293expia 1205 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀𝑘𝑘𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))))
3130impd 254 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
32313adant2 1016 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
33 zre 9233 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
34 leadd1 8364 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑘𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
3523, 33, 24, 34syl3an 1280 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
3635biimpd 144 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝑁 → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
3736adantld 278 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
38373coml 1210 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
39383expia 1205 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
4039impd 254 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
41403adant1 1015 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
4221, 32, 413jcad 1178 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
43 zaddcl 9269 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
44433adant2 1016 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
45 zaddcl 9269 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
46453adant1 1015 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
47 elfz1 9987 . . . . . . . . 9 (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
4844, 46, 47syl2anc 411 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
4948biimprd 158 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5042, 49syld 45 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5150com12 30 . . . . 5 ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
52513impb 1199 . . . 4 ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5352com12 30 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5417, 53syld 45 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
55 elfz1 9987 . . . . 5 (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))))
5644, 46, 55syl2anc 411 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))))
5756biimpd 144 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))))
58 zsubcl 9270 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ ℤ)
5958expcom 116 . . . . . . . . . 10 (𝐾 ∈ ℤ → (𝑚 ∈ ℤ → (𝑚𝐾) ∈ ℤ))
60593ad2ant3 1020 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (𝑚𝐾) ∈ ℤ))
6160adantrd 279 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ∈ ℤ))
62 zre 9233 . . . . . . . . . . . . . 14 (𝑚 ∈ ℤ → 𝑚 ∈ ℝ)
63 leaddsub 8372 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑀 + 𝐾) ≤ 𝑚𝑀 ≤ (𝑚𝐾)))
6422, 24, 62, 63syl3an 1280 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚𝑀 ≤ (𝑚𝐾)))
6564biimpd 144 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚𝑀 ≤ (𝑚𝐾)))
6665adantrd 279 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚𝐾)))
67663expia 1205 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚𝐾))))
6867impd 254 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚𝐾)))
69683adant2 1016 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚𝐾)))
70 lesubadd 8368 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑚𝐾) ≤ 𝑁𝑚 ≤ (𝑁 + 𝐾)))
7162, 24, 33, 70syl3an 1280 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚𝐾) ≤ 𝑁𝑚 ≤ (𝑁 + 𝐾)))
7271biimprd 158 . . . . . . . . . . . . . 14 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ≤ (𝑁 + 𝐾) → (𝑚𝐾) ≤ 𝑁))
7372adantld 278 . . . . . . . . . . . . 13 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ≤ 𝑁))
74733coml 1210 . . . . . . . . . . . 12 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ≤ 𝑁))
75743expia 1205 . . . . . . . . . . 11 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ≤ 𝑁)))
7675impd 254 . . . . . . . . . 10 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ≤ 𝑁))
7776ancoms 268 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ≤ 𝑁))
78773adant1 1015 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ≤ 𝑁))
7961, 69, 783jcad 1178 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → ((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁)))
80 elfz1 9987 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚𝐾) ∈ (𝑀...𝑁) ↔ ((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁)))
8180biimprd 158 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁) → (𝑚𝐾) ∈ (𝑀...𝑁)))
82813adant3 1017 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8379, 82syld 45 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8483com12 30 . . . . 5 ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ (𝑀...𝑁)))
85843impb 1199 . . . 4 ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8685com12 30 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8757, 86syld 45 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8817imp 124 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁))
8988simp1d 1009 . . . 4 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℤ)
9089ex 115 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ))
9157imp 124 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)))
9291simp1d 1009 . . . 4 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → 𝑚 ∈ ℤ)
9392ex 115 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑚 ∈ ℤ))
94 zcn 9234 . . . . . . 7 (𝑚 ∈ ℤ → 𝑚 ∈ ℂ)
95 zcn 9234 . . . . . . 7 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
96 zcn 9234 . . . . . . 7 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97 subadd 8137 . . . . . . . . 9 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚𝐾) = 𝑘 ↔ (𝐾 + 𝑘) = 𝑚))
98 eqcom 2179 . . . . . . . . 9 ((𝑚𝐾) = 𝑘𝑘 = (𝑚𝐾))
99 eqcom 2179 . . . . . . . . 9 ((𝐾 + 𝑘) = 𝑚𝑚 = (𝐾 + 𝑘))
10097, 98, 993bitr3g 222 . . . . . . . 8 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝐾 + 𝑘)))
101 addcom 8071 . . . . . . . . . 10 ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾))
1021013adant1 1015 . . . . . . . . 9 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾))
103102eqeq2d 2189 . . . . . . . 8 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 = (𝐾 + 𝑘) ↔ 𝑚 = (𝑘 + 𝐾)))
104100, 103bitrd 188 . . . . . . 7 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
10594, 95, 96, 104syl3an 1280 . . . . . 6 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
1061053coml 1210 . . . . 5 ((𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
1071063expib 1206 . . . 4 (𝐾 ∈ ℤ → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
1081073ad2ant3 1020 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
10990, 93, 108syl2and 295 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
1106, 14, 54, 87, 109en3d 6762 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wcel 2148  Vcvv 2737  𝒫 cpw 3574   class class class wbr 4000   × cxp 4620   Fn wfn 5206  wf 5207  (class class class)co 5868  cen 6731  cc 7787  cr 7788   + caddc 7792  cle 7970  cmin 8105  cz 9229  ...cfz 9982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205  ax-un 4429  ax-setind 4532  ax-cnex 7880  ax-resscn 7881  ax-1cn 7882  ax-1re 7883  ax-icn 7884  ax-addcl 7885  ax-addrcl 7886  ax-mulcl 7887  ax-addcom 7889  ax-addass 7891  ax-distr 7893  ax-i2m1 7894  ax-0lt1 7895  ax-0id 7897  ax-rnegex 7898  ax-cnre 7900  ax-pre-ltirr 7901  ax-pre-ltwlin 7902  ax-pre-lttrn 7903  ax-pre-ltadd 7905
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4289  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-res 4634  df-ima 4635  df-iota 5173  df-fun 5213  df-fn 5214  df-f 5215  df-f1 5216  df-fo 5217  df-f1o 5218  df-fv 5219  df-riota 5824  df-ov 5871  df-oprab 5872  df-mpo 5873  df-1st 6134  df-2nd 6135  df-en 6734  df-pnf 7971  df-mnf 7972  df-xr 7973  df-ltxr 7974  df-le 7975  df-sub 8107  df-neg 8108  df-inn 8896  df-n0 9153  df-z 9230  df-fz 9983
This theorem is referenced by:  fz01en  10026  frecfzen2  10400  hashfz  10772  mertenslemi1  11514  hashdvds  12191
  Copyright terms: Public domain W3C validator