Metamath Proof Explorer

Theorem metakunt16

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

Ref Expression
Hypotheses metakunt16.1 
|- ( ph -> M e. NN )
metakunt16.2 
|- ( ph -> I e. NN )
metakunt16.3 
|- ( ph -> I <_ M )
metakunt16.4 
|- F = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
Assertion metakunt16 
|- ( ph -> F : ( I ... ( M - 1 ) ) -1-1-onto-> ( 1 ... ( M - I ) ) )

Proof

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