metakunt16

Description: Construction of another permutation. (Contributed by metakunt, 25-May-2024)

	Ref	Expression
Hypotheses	metakunt16.1	$⊢ φ \to M \in ℕ$
	metakunt16.2	$⊢ φ \to I \in ℕ$
	metakunt16.3	$⊢ φ \to I \leq M$
	metakunt16.4	$⊢ F = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
Assertion	metakunt16	$⊢ φ \to F : (I \dots M - 1) \underset{1-1 onto}{⟶} (1 \dots M - I)$

Proof

Step	Hyp	Ref	Expression
1		metakunt16.1	$⊢ φ \to M \in ℕ$
2		metakunt16.2	$⊢ φ \to I \in ℕ$
3		metakunt16.3	$⊢ φ \to I \leq M$
4		metakunt16.4	$⊢ F = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
5	2	nnzd	$⊢ φ \to I \in ℤ$
6	5	adantr	$⊢ (φ \land x \in (I \dots M - 1)) \to I \in ℤ$
7	1	nnzd	$⊢ φ \to M \in ℤ$
8	7	adantr	$⊢ (φ \land x \in (I \dots M - 1)) \to M \in ℤ$
9		1zzd	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 \in ℤ$
10	8 9	zsubcld	$⊢ (φ \land x \in (I \dots M - 1)) \to M - 1 \in ℤ$
11	9 6	zsubcld	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 - I \in ℤ$
12		simpr	$⊢ (φ \land x \in (I \dots M - 1)) \to x \in (I \dots M - 1)$
13		elfz3	$⊢ 1 - I \in ℤ \to 1 - I \in (1 - I \dots 1 - I)$
14	11 13	syl	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 - I \in (1 - I \dots 1 - I)$
15	6	zcnd	$⊢ (φ \land x \in (I \dots M - 1)) \to I \in ℂ$
16		1cnd	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 \in ℂ$
17	15 16	pncan3d	$⊢ (φ \land x \in (I \dots M - 1)) \to I + 1 - I = 1$
18	17	eqcomd	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 = I + 1 - I$
19	1	nncnd	$⊢ φ \to M \in ℂ$
20	19	adantr	$⊢ (φ \land x \in (I \dots M - 1)) \to M \in ℂ$
21	20 16 15	npncand	$⊢ (φ \land x \in (I \dots M - 1)) \to (M - 1) + 1 - I = M - I$
22	21	eqcomd	$⊢ (φ \land x \in (I \dots M - 1)) \to M - I = (M - 1) + 1 - I$
23	6 10 11 11 12 14 18 22	fzadd2d	$⊢ (φ \land x \in (I \dots M - 1)) \to x + 1 - I \in (1 \dots M - I)$
24	5	adantr	$⊢ (φ \land y \in (1 \dots M - I)) \to I \in ℤ$
25	7	adantr	$⊢ (φ \land y \in (1 \dots M - I)) \to M \in ℤ$
26		1zzd	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 \in ℤ$
27	25 26	zsubcld	$⊢ (φ \land y \in (1 \dots M - I)) \to M - 1 \in ℤ$
28		elfznn	$⊢ y \in (1 \dots M - I) \to y \in ℕ$
29	28	adantl	$⊢ (φ \land y \in (1 \dots M - I)) \to y \in ℕ$
30		nnz	$⊢ y \in ℕ \to y \in ℤ$
31	29 30	syl	$⊢ (φ \land y \in (1 \dots M - I)) \to y \in ℤ$
32	26 24	zsubcld	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 - I \in ℤ$
33	31 32	zsubcld	$⊢ (φ \land y \in (1 \dots M - I)) \to y - (1 - I) \in ℤ$
34	24	zred	$⊢ (φ \land y \in (1 \dots M - I)) \to I \in ℝ$
35	34	recnd	$⊢ (φ \land y \in (1 \dots M - I)) \to I \in ℂ$
36		1cnd	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 \in ℂ$
37	35 36	pncan3d	$⊢ (φ \land y \in (1 \dots M - I)) \to I + 1 - I = 1$
38	28	nnge1d	$⊢ y \in (1 \dots M - I) \to 1 \leq y$
39	38	adantl	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 \leq y$
40	37 39	eqbrtrd	$⊢ (φ \land y \in (1 \dots M - I)) \to I + 1 - I \leq y$
41		1red	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 \in ℝ$
42	41 34	resubcld	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 - I \in ℝ$
43	29	nnred	$⊢ (φ \land y \in (1 \dots M - I)) \to y \in ℝ$
44	34 42 43	3jca	$⊢ (φ \land y \in (1 \dots M - I)) \to (I \in ℝ \land 1 - I \in ℝ \land y \in ℝ)$
45		leaddsub	$⊢ (I \in ℝ \land 1 - I \in ℝ \land y \in ℝ) \to (I + 1 - I \leq y \leftrightarrow I \leq y - (1 - I))$
46	44 45	syl	$⊢ (φ \land y \in (1 \dots M - I)) \to (I + 1 - I \leq y \leftrightarrow I \leq y - (1 - I))$
47	40 46	mpbid	$⊢ (φ \land y \in (1 \dots M - I)) \to I \leq y - (1 - I)$
48		elfzle2	$⊢ y \in (1 \dots M - I) \to y \leq M - I$
49	48	adantl	$⊢ (φ \land y \in (1 \dots M - I)) \to y \leq M - I$
50	19	adantr	$⊢ (φ \land y \in (1 \dots M - I)) \to M \in ℂ$
51	24	zcnd	$⊢ (φ \land y \in (1 \dots M - I)) \to I \in ℂ$
52	50 36 51	npncand	$⊢ (φ \land y \in (1 \dots M - I)) \to (M - 1) + 1 - I = M - I$
53	49 52	breqtrrd	$⊢ (φ \land y \in (1 \dots M - I)) \to y \leq (M - 1) + 1 - I$
54	32	zred	$⊢ (φ \land y \in (1 \dots M - I)) \to 1 - I \in ℝ$
55	27	zred	$⊢ (φ \land y \in (1 \dots M - I)) \to M - 1 \in ℝ$
56	43 54 55	lesubaddd	$⊢ (φ \land y \in (1 \dots M - I)) \to (y - (1 - I) \leq M - 1 \leftrightarrow y \leq (M - 1) + 1 - I)$
57	53 56	mpbird	$⊢ (φ \land y \in (1 \dots M - I)) \to y - (1 - I) \leq M - 1$
58	24 27 33 47 57	elfzd	$⊢ (φ \land y \in (1 \dots M - I)) \to y - (1 - I) \in (I \dots M - 1)$
59		1cnd	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to 1 \in ℂ$
60	35	adantrl	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to I \in ℂ$
61	59 60	subcld	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to 1 - I \in ℂ$
62		elfzelz	$⊢ x \in (I \dots M - 1) \to x \in ℤ$
63	62	ad2antrl	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to x \in ℤ$
64		zcn	$⊢ x \in ℤ \to x \in ℂ$
65	63 64	syl	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to x \in ℂ$
66	29	adantrl	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to y \in ℕ$
67		nncn	$⊢ y \in ℕ \to y \in ℂ$
68	66 67	syl	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to y \in ℂ$
69	61 65 68	addrsub	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to (1 - I + x = y \leftrightarrow x = y - (1 - I))$
70	69	bicomd	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to (x = y - (1 - I) \leftrightarrow 1 - I + x = y)$
71	61 65	addcomd	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to 1 - I + x = x + 1 - I$
72	71	eqeq1d	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to (1 - I + x = y \leftrightarrow x + 1 - I = y)$
73		eqcom	$⊢ x + 1 - I = y \leftrightarrow y = x + 1 - I$
74	73	a1i	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to (x + 1 - I = y \leftrightarrow y = x + 1 - I)$
75	72 74	bitrd	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to (1 - I + x = y \leftrightarrow y = x + 1 - I)$
76	70 75	bitrd	$⊢ (φ \land (x \in (I \dots M - 1) \land y \in (1 \dots M - I))) \to (x = y - (1 - I) \leftrightarrow y = x + 1 - I)$
77	4 23 58 76	f1o2d	$⊢ φ \to F : (I \dots M - 1) \underset{1-1 onto}{⟶} (1 \dots M - I)$

Metamath Proof Explorer

Theorem metakunt16

Proof