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

Theorem fzen 9853
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 9824 . . . . 5 ...:(ℤ × ℤ)⟶𝒫 ℤ
2 ffn 5279 . . . . 5 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
31, 2ax-mp 5 . . . 4 ... Fn (ℤ × ℤ)
4 fnovex 5811 . . . 4 ((... Fn (ℤ × ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ V)
53, 4mp3an1 1303 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ V)
653adant3 1002 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ∈ V)
7 simp1 982 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑀 ∈ ℤ)
8 simp3 984 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈ ℤ)
97, 8zaddcld 9200 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
10 simp2 983 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℤ)
1110, 8zaddcld 9200 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
12 fnovex 5811 . . . 4 ((... Fn (ℤ × ℤ) ∧ (𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
133, 12mp3an1 1303 . . 3 (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
149, 11, 13syl2anc 409 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V)
15 elfz1 9825 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
1615biimpd 143 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
17163adant3 1002 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
18 zaddcl 9117 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ℤ)
1918expcom 115 . . . . . . . . . 10 (𝐾 ∈ ℤ → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ))
20193ad2ant3 1005 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ))
2120adantrd 277 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ∈ ℤ))
22 zre 9081 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
23 zre 9081 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
24 zre 9081 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℤ → 𝐾 ∈ ℝ)
25 leadd1 8215 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
2622, 23, 24, 25syl3an 1259 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
2726biimpd 143 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀𝑘 → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
2827adantrd 277 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
29283com23 1188 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
30293expia 1184 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀𝑘𝑘𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))))
3130impd 252 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
32313adant2 1001 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))
33 zre 9081 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
34 leadd1 8215 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑘𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
3523, 33, 24, 34syl3an 1259 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
3635biimpd 143 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝑁 → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
3736adantld 276 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
38373coml 1189 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
39383expia 1184 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
4039impd 252 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
41403adant1 1000 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))
4221, 32, 413jcad 1163 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
43 zaddcl 9117 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
44433adant2 1001 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ)
45 zaddcl 9117 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
46453adant1 1000 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ)
47 elfz1 9825 . . . . . . . . 9 (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
4844, 46, 47syl2anc 409 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))))
4948biimprd 157 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5042, 49syld 45 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5150com12 30 . . . . 5 ((𝑘 ∈ ℤ ∧ (𝑀𝑘𝑘𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
52513impb 1178 . . . 4 ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5352com12 30 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
5417, 53syld 45 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
55 elfz1 9825 . . . . 5 (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))))
5644, 46, 55syl2anc 409 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))))
5756biimpd 143 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))))
58 zsubcl 9118 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ ℤ)
5958expcom 115 . . . . . . . . . 10 (𝐾 ∈ ℤ → (𝑚 ∈ ℤ → (𝑚𝐾) ∈ ℤ))
60593ad2ant3 1005 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (𝑚𝐾) ∈ ℤ))
6160adantrd 277 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ∈ ℤ))
62 zre 9081 . . . . . . . . . . . . . 14 (𝑚 ∈ ℤ → 𝑚 ∈ ℝ)
63 leaddsub 8223 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑀 + 𝐾) ≤ 𝑚𝑀 ≤ (𝑚𝐾)))
6422, 24, 62, 63syl3an 1259 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚𝑀 ≤ (𝑚𝐾)))
6564biimpd 143 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚𝑀 ≤ (𝑚𝐾)))
6665adantrd 277 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚𝐾)))
67663expia 1184 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚𝐾))))
6867impd 252 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚𝐾)))
69683adant2 1001 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚𝐾)))
70 lesubadd 8219 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑚𝐾) ≤ 𝑁𝑚 ≤ (𝑁 + 𝐾)))
7162, 24, 33, 70syl3an 1259 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚𝐾) ≤ 𝑁𝑚 ≤ (𝑁 + 𝐾)))
7271biimprd 157 . . . . . . . . . . . . . 14 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ≤ (𝑁 + 𝐾) → (𝑚𝐾) ≤ 𝑁))
7372adantld 276 . . . . . . . . . . . . 13 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ≤ 𝑁))
74733coml 1189 . . . . . . . . . . . 12 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ≤ 𝑁))
75743expia 1184 . . . . . . . . . . 11 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ≤ 𝑁)))
7675impd 252 . . . . . . . . . 10 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ≤ 𝑁))
7776ancoms 266 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ≤ 𝑁))
78773adant1 1000 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ≤ 𝑁))
7961, 69, 783jcad 1163 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → ((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁)))
80 elfz1 9825 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚𝐾) ∈ (𝑀...𝑁) ↔ ((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁)))
8180biimprd 157 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁) → (𝑚𝐾) ∈ (𝑀...𝑁)))
82813adant3 1002 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑚𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚𝐾) ∧ (𝑚𝐾) ≤ 𝑁) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8379, 82syld 45 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8483com12 30 . . . . 5 ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ (𝑀...𝑁)))
85843impb 1178 . . . 4 ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8685com12 30 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8757, 86syld 45 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚𝐾) ∈ (𝑀...𝑁)))
8817imp 123 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁))
8988simp1d 994 . . . 4 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℤ)
9089ex 114 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ))
9157imp 123 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚𝑚 ≤ (𝑁 + 𝐾)))
9291simp1d 994 . . . 4 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → 𝑚 ∈ ℤ)
9392ex 114 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑚 ∈ ℤ))
94 zcn 9082 . . . . . . 7 (𝑚 ∈ ℤ → 𝑚 ∈ ℂ)
95 zcn 9082 . . . . . . 7 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
96 zcn 9082 . . . . . . 7 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97 subadd 7988 . . . . . . . . 9 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚𝐾) = 𝑘 ↔ (𝐾 + 𝑘) = 𝑚))
98 eqcom 2142 . . . . . . . . 9 ((𝑚𝐾) = 𝑘𝑘 = (𝑚𝐾))
99 eqcom 2142 . . . . . . . . 9 ((𝐾 + 𝑘) = 𝑚𝑚 = (𝐾 + 𝑘))
10097, 98, 993bitr3g 221 . . . . . . . 8 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝐾 + 𝑘)))
101 addcom 7922 . . . . . . . . . 10 ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾))
1021013adant1 1000 . . . . . . . . 9 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾))
103102eqeq2d 2152 . . . . . . . 8 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 = (𝐾 + 𝑘) ↔ 𝑚 = (𝑘 + 𝐾)))
104100, 103bitrd 187 . . . . . . 7 ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
10594, 95, 96, 104syl3an 1259 . . . . . 6 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
1061053coml 1189 . . . . 5 ((𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))
1071063expib 1185 . . . 4 (𝐾 ∈ ℤ → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
1081073ad2ant3 1005 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
10990, 93, 108syl2and 293 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑘 = (𝑚𝐾) ↔ 𝑚 = (𝑘 + 𝐾))))
1106, 14, 54, 87, 109en3d 6670 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 963   = wceq 1332  wcel 1481  Vcvv 2689  𝒫 cpw 3514   class class class wbr 3936   × cxp 4544   Fn wfn 5125  wf 5126  (class class class)co 5781  cen 6639  cc 7641  cr 7642   + caddc 7646  cle 7824  cmin 7956  cz 9077  ...cfz 9820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-addcom 7743  ax-addass 7745  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-0id 7751  ax-rnegex 7752  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-ltadd 7759
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-id 4222  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-en 6642  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-inn 8744  df-n0 9001  df-z 9078  df-fz 9821
This theorem is referenced by:  fz01en  9863  frecfzen2  10230  hashfz  10598  mertenslemi1  11335  hashdvds  11931
  Copyright terms: Public domain W3C validator