Metamath Proof Explorer

Theorem metakunt16

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

Ref Expression
Hypotheses metakunt16.1 ⊢φ→M∈ℕ
metakunt16.2 ⊢φ→I∈ℕ
metakunt16.3 ⊢φ→I≤M
metakunt16.4 ⊢F=x∈I…M−1⟼x+1-I
Assertion metakunt16 ⊢φ→F:I…M−1⟶1-1 onto1…M−I

Proof

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