Metamath Proof Explorer

Theorem metakunt2

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

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

Proof

Step Hyp Ref Expression
1 metakunt2.1 
 |-  ( ph -> M e. NN )
2 metakunt2.2 
 |-  ( ph -> I e. NN )
3 metakunt2.3 
 |-  ( ph -> I <_ M )
4 metakunt2.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) )
5 eleq1 
 |-  ( I = if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) -> ( I e. ( 1 ... M ) <-> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) e. ( 1 ... M ) ) )
6 eleq1 
 |-  ( if ( x < I , x , ( x + 1 ) ) = if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) -> ( if ( x < I , x , ( x + 1 ) ) e. ( 1 ... M ) <-> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) e. ( 1 ... M ) ) )
7 1zzd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> 1 e. ZZ )
8 1 nnzd 
 |-  ( ph -> M e. ZZ )
9 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> M e. ZZ )
10 2 nnzd 
 |-  ( ph -> I e. ZZ )
11 10 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> I e. ZZ )
12 2 nnge1d 
 |-  ( ph -> 1 <_ I )
13 12 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> 1 <_ I )
14 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> I <_ M )
15 7 9 11 13 14 elfzd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> I 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 = M ) /\ x < I ) -> x e. ( 1 ... M ) )
19 1zzd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> 1 e. ZZ )
20 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> M e. ZZ )
21 elfznn 
 |-  ( x e. ( 1 ... M ) -> x e. NN )
22 21 nnzd 
 |-  ( x e. ( 1 ... M ) -> x e. ZZ )
23 22 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> x e. ZZ )
24 23 peano2zd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> ( x + 1 ) e. ZZ )
25 0p1e1 
 |-  ( 0 + 1 ) = 1
26 0red 
 |-  ( x e. ( 1 ... M ) -> 0 e. RR )
27 21 nnred 
 |-  ( x e. ( 1 ... M ) -> x e. RR )
28 1red 
 |-  ( x e. ( 1 ... M ) -> 1 e. RR )
29 21 nnnn0d 
 |-  ( x e. ( 1 ... M ) -> x e. NN0 )
30 29 nn0ge0d 
 |-  ( x e. ( 1 ... M ) -> 0 <_ x )
31 26 27 28 30 leadd1dd 
 |-  ( x e. ( 1 ... M ) -> ( 0 + 1 ) <_ ( x + 1 ) )
32 25 31 eqbrtrrid 
 |-  ( x e. ( 1 ... M ) -> 1 <_ ( x + 1 ) )
33 32 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> 1 <_ ( x + 1 ) )
34 simplr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> x e. ( 1 ... M ) )
35 neqne 
 |-  ( -. x = M -> x =/= M )
36 35 adantl 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> x =/= M )
37 34 36 fzne2d 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> x < M )
38 37 adantrr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> x < M )
39 22 adantl 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> x e. ZZ )
40 8 adantr 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> M e. ZZ )
41 39 40 zltp1led 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> ( x < M <-> ( x + 1 ) <_ M ) )
42 41 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> ( x < M <-> ( x + 1 ) <_ M ) )
43 38 42 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> ( x + 1 ) <_ M )
44 19 20 24 33 43 elfzd 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ ( -. x = M /\ -. x < I ) ) -> ( x + 1 ) e. ( 1 ... M ) )
45 44 anassrs 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ -. x < I ) -> ( x + 1 ) e. ( 1 ... M ) )
46 16 17 18 45 ifbothda 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> if ( x < I , x , ( x + 1 ) ) e. ( 1 ... M ) )
47 5 6 15 46 ifbothda 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) e. ( 1 ... M ) )
48 47 4 fmptd 
 |-  ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )