Metamath Proof Explorer

Theorem metakunt27

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024)

Ref Expression
Hypotheses metakunt27.1 
|- ( ph -> M e. NN )
metakunt27.2 
|- ( ph -> I e. NN )
metakunt27.3 
|- ( ph -> I <_ M )
metakunt27.4 
|- ( ph -> X e. ( 1 ... M ) )
metakunt27.5 
|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
metakunt27.6 
|- B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
metakunt27.7 
|- ( ph -> -. X = I )
metakunt27.8 
|- ( ph -> X < I )
Assertion metakunt27 
|- ( ph -> ( B ` ( A ` X ) ) = ( X + ( M - I ) ) )

Proof

Step Hyp Ref Expression
1 metakunt27.1 
 |-  ( ph -> M e. NN )
2 metakunt27.2 
 |-  ( ph -> I e. NN )
3 metakunt27.3 
 |-  ( ph -> I <_ M )
4 metakunt27.4 
 |-  ( ph -> X e. ( 1 ... M ) )
5 metakunt27.5 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
6 metakunt27.6 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
7 metakunt27.7 
 |-  ( ph -> -. X = I )
8 metakunt27.8 
 |-  ( ph -> X < I )
9 5 a1i 
 |-  ( ph -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
10 7 adantr 
 |-  ( ( ph /\ x = X ) -> -. X = I )
11 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
12 11 eqeq1d 
 |-  ( ( ph /\ x = X ) -> ( x = I <-> X = I ) )
13 12 notbid 
 |-  ( ( ph /\ x = X ) -> ( -. x = I <-> -. X = I ) )
14 10 13 mpbird 
 |-  ( ( ph /\ x = X ) -> -. x = I )
15 14 iffalsed 
 |-  ( ( ph /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( x < I , x , ( x - 1 ) ) )
16 8 adantr 
 |-  ( ( ph /\ x = X ) -> X < I )
17 11 breq1d 
 |-  ( ( ph /\ x = X ) -> ( x < I <-> X < I ) )
18 16 17 mpbird 
 |-  ( ( ph /\ x = X ) -> x < I )
19 18 iftrued 
 |-  ( ( ph /\ x = X ) -> if ( x < I , x , ( x - 1 ) ) = x )
20 19 11 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x < I , x , ( x - 1 ) ) = X )
21 15 20 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = X )
22 9 21 4 4 fvmptd 
 |-  ( ph -> ( A ` X ) = X )
23 22 fveq2d 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( B ` X ) )
24 6 a1i 
 |-  ( ph -> B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) ) )
25 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
26 4 25 syl 
 |-  ( ph -> X e. NN )
27 26 nnred 
 |-  ( ph -> X e. RR )
28 2 nnred 
 |-  ( ph -> I e. RR )
29 1 nnred 
 |-  ( ph -> M e. RR )
30 27 28 29 8 3 ltletrd 
 |-  ( ph -> X < M )
31 27 30 ltned 
 |-  ( ph -> X =/= M )
32 31 neneqd 
 |-  ( ph -> -. X = M )
33 32 adantr 
 |-  ( ( ph /\ z = X ) -> -. X = M )
34 simpr 
 |-  ( ( ph /\ z = X ) -> z = X )
35 34 eqeq1d 
 |-  ( ( ph /\ z = X ) -> ( z = M <-> X = M ) )
36 35 notbid 
 |-  ( ( ph /\ z = X ) -> ( -. z = M <-> -. X = M ) )
37 33 36 mpbird 
 |-  ( ( ph /\ z = X ) -> -. z = M )
38 37 iffalsed 
 |-  ( ( ph /\ z = X ) -> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) = if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) )
39 8 adantr 
 |-  ( ( ph /\ z = X ) -> X < I )
40 34 breq1d 
 |-  ( ( ph /\ z = X ) -> ( z < I <-> X < I ) )
41 39 40 mpbird 
 |-  ( ( ph /\ z = X ) -> z < I )
42 41 iftrued 
 |-  ( ( ph /\ z = X ) -> if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) = ( z + ( M - I ) ) )
43 34 oveq1d 
 |-  ( ( ph /\ z = X ) -> ( z + ( M - I ) ) = ( X + ( M - I ) ) )
44 42 43 eqtrd 
 |-  ( ( ph /\ z = X ) -> if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) = ( X + ( M - I ) ) )
45 38 44 eqtrd 
 |-  ( ( ph /\ z = X ) -> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) = ( X + ( M - I ) ) )
46 4 elfzelzd 
 |-  ( ph -> X e. ZZ )
47 1 nnzd 
 |-  ( ph -> M e. ZZ )
48 2 nnzd 
 |-  ( ph -> I e. ZZ )
49 47 48 zsubcld 
 |-  ( ph -> ( M - I ) e. ZZ )
50 46 49 zaddcld 
 |-  ( ph -> ( X + ( M - I ) ) e. ZZ )
51 24 45 4 50 fvmptd 
 |-  ( ph -> ( B ` X ) = ( X + ( M - I ) ) )
52 23 51 eqtrd 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( X + ( M - I ) ) )