Metamath Proof Explorer


Theorem metakunt15

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

Ref Expression
Hypotheses metakunt15.1 φ M
metakunt15.2 φ I
metakunt15.3 φ I M
metakunt15.4 F = x 1 I 1 x + M - I
Assertion metakunt15 φ F : 1 I 1 1-1 onto M - I + 1 M 1

Proof

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