Metamath Proof Explorer

Theorem metakunt15

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

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

Proof

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