Metamath Proof Explorer

Theorem metakunt1

Description: A is an endomapping. (Contributed by metakunt, 23-May-2024)

Ref Expression
Hypotheses metakunt1.1 
|- ( ph -> M e. NN )
metakunt1.2 
|- ( ph -> I e. NN )
metakunt1.3 
|- ( ph -> I <_ M )
metakunt1.4 
|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
Assertion metakunt1 
|- ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )

Proof

Step Hyp Ref Expression
1 metakunt1.1 
 |-  ( ph -> M e. NN )
2 metakunt1.2 
 |-  ( ph -> I e. NN )
3 metakunt1.3 
 |-  ( ph -> I <_ M )
4 metakunt1.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 eleq1 
 |-  ( M = if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) -> ( M e. ( 1 ... M ) <-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) e. ( 1 ... M ) ) )
6 eleq1 
 |-  ( if ( x < I , x , ( x - 1 ) ) = if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) -> ( if ( x < I , x , ( x - 1 ) ) e. ( 1 ... M ) <-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) e. ( 1 ... M ) ) )
7 1zzd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> 1 e. ZZ )
8 1 nnzd 
 |-  ( ph -> M e. ZZ )
9 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> M e. ZZ )
10 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> M e. NN )
11 10 nnge1d 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> 1 <_ M )
12 1 nnred 
 |-  ( ph -> M e. RR )
13 12 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> M e. RR )
14 13 leidd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> M <_ M )
15 7 9 9 11 14 elfzd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = I ) -> M e. ( 1 ... M ) )
16 eleq1 
 |-  ( x = if ( x < I , x , ( x - 1 ) ) -> ( x e. ( 1 ... M ) <-> if ( x < I , x , ( x - 1 ) ) e. ( 1 ... M ) ) )
17 eleq1 
 |-  ( ( x - 1 ) = if ( x < I , x , ( x - 1 ) ) -> ( ( x - 1 ) e. ( 1 ... M ) <-> if ( x < I , x , ( x - 1 ) ) e. ( 1 ... M ) ) )
18 simpllr 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = I ) /\ x < I ) -> x e. ( 1 ... M ) )
19 pm4.56 
 |-  ( ( -. x = I /\ -. x < I ) <-> -. ( x = I \/ x < I ) )
20 19 anbi2i 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = I /\ -. x < I ) ) <-> ( ( ph /\ x e. ( 1 ... M ) ) /\ -. ( x = I \/ x < I ) ) )
21 2 nnred 
 |-  ( ph -> I e. RR )
22 21 adantr 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> I e. RR )
23 elfznn 
 |-  ( x e. ( 1 ... M ) -> x e. NN )
24 23 nnred 
 |-  ( x e. ( 1 ... M ) -> x e. RR )
25 24 adantl 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> x e. RR )
26 22 25 jca 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( I e. RR /\ x e. RR ) )
27 axlttri 
 |-  ( ( I e. RR /\ x e. RR ) -> ( I < x <-> -. ( I = x \/ x < I ) ) )
28 26 27 syl 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( I < x <-> -. ( I = x \/ x < I ) ) )
29 eqcom 
 |-  ( I = x <-> x = I )
30 29 orbi1i 
 |-  ( ( I = x \/ x < I ) <-> ( x = I \/ x < I ) )
31 30 notbii 
 |-  ( -. ( I = x \/ x < I ) <-> -. ( x = I \/ x < I ) )
32 28 31 bitrdi 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( I < x <-> -. ( x = I \/ x < I ) ) )
33 1zzd 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> 1 e. ZZ )
34 8 3ad2ant1 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> M e. ZZ )
35 simp2 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> x e. ( 1 ... M ) )
36 35 elfzelzd 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> x e. ZZ )
37 36 33 zsubcld 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> ( x - 1 ) e. ZZ )
38 1red 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> 1 e. RR )
39 22 3adant3 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> I e. RR )
40 35 24 syl 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> x e. RR )
41 2 nnge1d 
 |-  ( ph -> 1 <_ I )
42 41 3ad2ant1 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> 1 <_ I )
43 simp3 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> I < x )
44 38 39 40 42 43 lelttrd 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> 1 < x )
45 33 36 zltlem1d 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> ( 1 < x <-> 1 <_ ( x - 1 ) ) )
46 44 45 mpbid 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> 1 <_ ( x - 1 ) )
47 1red 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> 1 e. RR )
48 25 47 resubcld 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( x - 1 ) e. RR )
49 12 adantr 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> M e. RR )
50 0le1 
 |-  0 <_ 1
51 50 a1i 
 |-  ( x e. ( 1 ... M ) -> 0 <_ 1 )
52 1red 
 |-  ( x e. ( 1 ... M ) -> 1 e. RR )
53 24 52 subge02d 
 |-  ( x e. ( 1 ... M ) -> ( 0 <_ 1 <-> ( x - 1 ) <_ x ) )
54 51 53 mpbid 
 |-  ( x e. ( 1 ... M ) -> ( x - 1 ) <_ x )
55 54 adantl 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( x - 1 ) <_ x )
56 elfzle2 
 |-  ( x e. ( 1 ... M ) -> x <_ M )
57 56 adantl 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> x <_ M )
58 48 25 49 55 57 letrd 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( x - 1 ) <_ M )
59 58 3adant3 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> ( x - 1 ) <_ M )
60 33 34 37 46 59 elfzd 
 |-  ( ( ph /\ x e. ( 1 ... M ) /\ I < x ) -> ( x - 1 ) e. ( 1 ... M ) )
61 60 3expia 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( I < x -> ( x - 1 ) e. ( 1 ... M ) ) )
62 32 61 sylbird 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( -. ( x = I \/ x < I ) -> ( x - 1 ) e. ( 1 ... M ) ) )
63 62 imp 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. ( x = I \/ x < I ) ) -> ( x - 1 ) e. ( 1 ... M ) )
64 20 63 sylbi 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = I /\ -. x < I ) ) -> ( x - 1 ) e. ( 1 ... M ) )
65 64 anassrs 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = I ) /\ -. x < I ) -> ( x - 1 ) e. ( 1 ... M ) )
66 16 17 18 65 ifbothda 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = I ) -> if ( x < I , x , ( x - 1 ) ) e. ( 1 ... M ) )
67 5 6 15 66 ifbothda 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) e. ( 1 ... M ) )
68 67 4 fmptd 
 |-  ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )