Metamath Proof Explorer

Theorem metakunt31

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

Ref Expression
Hypotheses metakunt31.1 
|- ( ph -> M e. NN )
metakunt31.2 
|- ( ph -> I e. NN )
metakunt31.3 
|- ( ph -> I <_ M )
metakunt31.4 
|- ( ph -> X e. ( 1 ... M ) )
metakunt31.5 
|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
metakunt31.6 
|- B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
metakunt31.7 
|- C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
metakunt31.8 
|- G = if ( I <_ ( X + ( M - I ) ) , 1 , 0 )
metakunt31.9 
|- H = if ( I <_ ( X - I ) , 1 , 0 )
metakunt31.10 
|- R = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
Assertion metakunt31 
|- ( ph -> ( C ` ( B ` ( A ` X ) ) ) = R )

Proof

Step Hyp Ref Expression
1 metakunt31.1 
 |-  ( ph -> M e. NN )
2 metakunt31.2 
 |-  ( ph -> I e. NN )
3 metakunt31.3 
 |-  ( ph -> I <_ M )
4 metakunt31.4 
 |-  ( ph -> X e. ( 1 ... M ) )
5 metakunt31.5 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
6 metakunt31.6 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
7 metakunt31.7 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
8 metakunt31.8 
 |-  G = if ( I <_ ( X + ( M - I ) ) , 1 , 0 )
9 metakunt31.9 
 |-  H = if ( I <_ ( X - I ) , 1 , 0 )
10 metakunt31.10 
 |-  R = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
11 1 adantr 
 |-  ( ( ph /\ X = I ) -> M e. NN )
12 2 adantr 
 |-  ( ( ph /\ X = I ) -> I e. NN )
13 3 adantr 
 |-  ( ( ph /\ X = I ) -> I <_ M )
14 simpr 
 |-  ( ( ph /\ X = I ) -> X = I )
15 11 12 13 5 7 6 14 metakunt26 
 |-  ( ( ph /\ X = I ) -> ( C ` ( B ` ( A ` X ) ) ) = X )
16 14 iftrued 
 |-  ( ( ph /\ X = I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = X )
17 16 eqcomd 
 |-  ( ( ph /\ X = I ) -> X = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
18 15 17 eqtrd 
 |-  ( ( ph /\ X = I ) -> ( C ` ( B ` ( A ` X ) ) ) = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
19 10 eqcomi 
 |-  if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = R
20 19 a1i 
 |-  ( ( ph /\ X = I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = R )
21 18 20 eqtrd 
 |-  ( ( ph /\ X = I ) -> ( C ` ( B ` ( A ` X ) ) ) = R )
22 1 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> M e. NN )
23 2 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> I e. NN )
24 3 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> I <_ M )
25 4 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> X e. ( 1 ... M ) )
26 simp2 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> -. X = I )
27 simp3 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> X < I )
28 22 23 24 25 5 6 26 27 7 8 metakunt29 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = ( ( X + ( M - I ) ) + G ) )
29 26 iffalsed 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
30 27 iftrued 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) = ( ( X + ( M - I ) ) + G ) )
31 29 30 eqtrd 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = ( ( X + ( M - I ) ) + G ) )
32 31 eqcomd 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> ( ( X + ( M - I ) ) + G ) = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
33 28 32 eqtrd 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
34 19 a1i 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = R )
35 33 34 eqtrd 
 |-  ( ( ph /\ -. X = I /\ X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = R )
36 35 3expa 
 |-  ( ( ( ph /\ -. X = I ) /\ X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = R )
37 1 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> M e. NN )
38 2 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> I e. NN )
39 3 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> I <_ M )
40 4 3ad2ant1 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> X e. ( 1 ... M ) )
41 simp2 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> -. X = I )
42 simp3 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> -. X < I )
43 37 38 39 40 5 6 41 42 7 9 metakunt30 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = ( ( X - I ) + H ) )
44 41 iffalsed 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
45 42 iffalsed 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) = ( ( X - I ) + H ) )
46 44 45 eqtrd 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = ( ( X - I ) + H ) )
47 46 eqcomd 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> ( ( X - I ) + H ) = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
48 43 47 eqtrd 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
49 19 a1i 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = R )
50 48 49 eqtrd 
 |-  ( ( ph /\ -. X = I /\ -. X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = R )
51 50 3expa 
 |-  ( ( ( ph /\ -. X = I ) /\ -. X < I ) -> ( C ` ( B ` ( A ` X ) ) ) = R )
52 36 51 pm2.61dan 
 |-  ( ( ph /\ -. X = I ) -> ( C ` ( B ` ( A ` X ) ) ) = R )
53 21 52 pm2.61dan 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = R )