metakunt15

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

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

Proof

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

Metamath Proof Explorer

Theorem metakunt15

Proof