Metamath Proof Explorer

Theorem metakunt7

Description: C is the left inverse for A. (Contributed by metakunt, 24-May-2024)

Ref Expression
Hypotheses metakunt7.1 
|- ( ph -> M e. NN )
metakunt7.2 
|- ( ph -> I e. NN )
metakunt7.3 
|- ( ph -> I <_ M )
metakunt7.4 
|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
metakunt7.5 
|- C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
metakunt7.6 
|- ( ph -> X e. ( 1 ... M ) )
Assertion metakunt7 
|- ( ( ph /\ I < X ) -> ( ( A ` X ) = ( X - 1 ) /\ -. ( A ` X ) = M /\ -. ( A ` X ) < I ) )

Proof

Step Hyp Ref Expression
1 metakunt7.1 
 |-  ( ph -> M e. NN )
2 metakunt7.2 
 |-  ( ph -> I e. NN )
3 metakunt7.3 
 |-  ( ph -> I <_ M )
4 metakunt7.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt7.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt7.6 
 |-  ( ph -> X e. ( 1 ... M ) )
7 4 a1i 
 |-  ( ( ph /\ I < X ) -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
8 eqeq1 
 |-  ( x = X -> ( x = I <-> X = I ) )
9 breq1 
 |-  ( x = X -> ( x < I <-> X < I ) )
10 id 
 |-  ( x = X -> x = X )
11 oveq1 
 |-  ( x = X -> ( x - 1 ) = ( X - 1 ) )
12 9 10 11 ifbieq12d 
 |-  ( x = X -> if ( x < I , x , ( x - 1 ) ) = if ( X < I , X , ( X - 1 ) ) )
13 8 12 ifbieq2d 
 |-  ( x = X -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) )
14 13 adantl 
 |-  ( ( ( ph /\ I < X ) /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) )
15 2 nnred 
 |-  ( ph -> I e. RR )
16 15 adantr 
 |-  ( ( ph /\ I < X ) -> I e. RR )
17 simpr 
 |-  ( ( ph /\ I < X ) -> I < X )
18 16 17 ltned 
 |-  ( ( ph /\ I < X ) -> I =/= X )
19 18 necomd 
 |-  ( ( ph /\ I < X ) -> X =/= I )
20 df-ne 
 |-  ( X =/= I <-> -. X = I )
21 19 20 sylib 
 |-  ( ( ph /\ I < X ) -> -. X = I )
22 iffalse 
 |-  ( -. X = I -> if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) = if ( X < I , X , ( X - 1 ) ) )
23 21 22 syl 
 |-  ( ( ph /\ I < X ) -> if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) = if ( X < I , X , ( X - 1 ) ) )
24 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
25 6 24 syl 
 |-  ( ph -> X e. NN )
26 25 nnred 
 |-  ( ph -> X e. RR )
27 26 adantr 
 |-  ( ( ph /\ I < X ) -> X e. RR )
28 16 27 17 ltled 
 |-  ( ( ph /\ I < X ) -> I <_ X )
29 16 27 lenltd 
 |-  ( ( ph /\ I < X ) -> ( I <_ X <-> -. X < I ) )
30 28 29 mpbid 
 |-  ( ( ph /\ I < X ) -> -. X < I )
31 iffalse 
 |-  ( -. X < I -> if ( X < I , X , ( X - 1 ) ) = ( X - 1 ) )
32 30 31 syl 
 |-  ( ( ph /\ I < X ) -> if ( X < I , X , ( X - 1 ) ) = ( X - 1 ) )
33 23 32 eqtrd 
 |-  ( ( ph /\ I < X ) -> if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) = ( X - 1 ) )
34 33 adantr 
 |-  ( ( ( ph /\ I < X ) /\ x = X ) -> if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) = ( X - 1 ) )
35 14 34 eqtrd 
 |-  ( ( ( ph /\ I < X ) /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = ( X - 1 ) )
36 6 adantr 
 |-  ( ( ph /\ I < X ) -> X e. ( 1 ... M ) )
37 36 elfzelzd 
 |-  ( ( ph /\ I < X ) -> X e. ZZ )
38 1zzd 
 |-  ( ( ph /\ I < X ) -> 1 e. ZZ )
39 37 38 zsubcld 
 |-  ( ( ph /\ I < X ) -> ( X - 1 ) e. ZZ )
40 7 35 36 39 fvmptd 
 |-  ( ( ph /\ I < X ) -> ( A ` X ) = ( X - 1 ) )
41 1red 
 |-  ( ph -> 1 e. RR )
42 26 41 resubcld 
 |-  ( ph -> ( X - 1 ) e. RR )
43 elfzle2 
 |-  ( X e. ( 1 ... M ) -> X <_ M )
44 6 43 syl 
 |-  ( ph -> X <_ M )
45 6 elfzelzd 
 |-  ( ph -> X e. ZZ )
46 1 nnzd 
 |-  ( ph -> M e. ZZ )
47 zlem1lt 
 |-  ( ( X e. ZZ /\ M e. ZZ ) -> ( X <_ M <-> ( X - 1 ) < M ) )
48 45 46 47 syl2anc 
 |-  ( ph -> ( X <_ M <-> ( X - 1 ) < M ) )
49 44 48 mpbid 
 |-  ( ph -> ( X - 1 ) < M )
50 42 49 ltned 
 |-  ( ph -> ( X - 1 ) =/= M )
51 50 adantr 
 |-  ( ( ph /\ I < X ) -> ( X - 1 ) =/= M )
52 40 51 eqnetrd 
 |-  ( ( ph /\ I < X ) -> ( A ` X ) =/= M )
53 52 neneqd 
 |-  ( ( ph /\ I < X ) -> -. ( A ` X ) = M )
54 2 nnzd 
 |-  ( ph -> I e. ZZ )
55 zltlem1 
 |-  ( ( I e. ZZ /\ X e. ZZ ) -> ( I < X <-> I <_ ( X - 1 ) ) )
56 55 biimpd 
 |-  ( ( I e. ZZ /\ X e. ZZ ) -> ( I < X -> I <_ ( X - 1 ) ) )
57 54 45 56 syl2anc 
 |-  ( ph -> ( I < X -> I <_ ( X - 1 ) ) )
58 57 imp 
 |-  ( ( ph /\ I < X ) -> I <_ ( X - 1 ) )
59 58 40 breqtrrd 
 |-  ( ( ph /\ I < X ) -> I <_ ( A ` X ) )
60 39 zred 
 |-  ( ( ph /\ I < X ) -> ( X - 1 ) e. RR )
61 40 60 eqeltrd 
 |-  ( ( ph /\ I < X ) -> ( A ` X ) e. RR )
62 16 61 lenltd 
 |-  ( ( ph /\ I < X ) -> ( I <_ ( A ` X ) <-> -. ( A ` X ) < I ) )
63 59 62 mpbid 
 |-  ( ( ph /\ I < X ) -> -. ( A ` X ) < I )
64 40 53 63 3jca 
 |-  ( ( ph /\ I < X ) -> ( ( A ` X ) = ( X - 1 ) /\ -. ( A ` X ) = M /\ -. ( A ` X ) < I ) )