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	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M \dots N) \approx (M + K \dots N + K)$

Proof

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

Metamath Proof Explorer

Theorem fzen

Proof