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 onto 1 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 onto 1 M I