Metamath Proof Explorer

Theorem metakunt32

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

Ref Expression
Hypotheses metakunt32.1 
|- ( ph -> M e. NN )
metakunt32.2 
|- ( ph -> I e. NN )
metakunt32.3 
|- ( ph -> I <_ M )
metakunt32.4 
|- ( ph -> X e. ( 1 ... M ) )
metakunt32.5 
|- D = ( x e. ( 1 ... M ) |-> if ( x = I , x , if ( x < I , ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) , ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) ) ) )
metakunt32.6 
|- G = if ( I <_ ( X + ( M - I ) ) , 1 , 0 )
metakunt32.7 
|- H = if ( I <_ ( X - I ) , 1 , 0 )
metakunt32.8 
|- R = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
Assertion metakunt32 
|- ( ph -> ( D ` X ) = R )

Proof

Step Hyp Ref Expression
1 metakunt32.1 
 |-  ( ph -> M e. NN )
2 metakunt32.2 
 |-  ( ph -> I e. NN )
3 metakunt32.3 
 |-  ( ph -> I <_ M )
4 metakunt32.4 
 |-  ( ph -> X e. ( 1 ... M ) )
5 metakunt32.5 
 |-  D = ( x e. ( 1 ... M ) |-> if ( x = I , x , if ( x < I , ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) , ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) ) ) )
6 metakunt32.6 
 |-  G = if ( I <_ ( X + ( M - I ) ) , 1 , 0 )
7 metakunt32.7 
 |-  H = if ( I <_ ( X - I ) , 1 , 0 )
8 metakunt32.8 
 |-  R = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
9 5 a1i 
 |-  ( ph -> D = ( x e. ( 1 ... M ) |-> if ( x = I , x , if ( x < I , ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) , ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) ) ) ) )
10 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
11 10 eqeq1d 
 |-  ( ( ph /\ x = X ) -> ( x = I <-> X = I ) )
12 10 breq1d 
 |-  ( ( ph /\ x = X ) -> ( x < I <-> X < I ) )
13 oveq1 
 |-  ( x = X -> ( x + ( M - I ) ) = ( X + ( M - I ) ) )
14 13 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( M - I ) ) = ( X + ( M - I ) ) )
15 14 breq2d 
 |-  ( ( ph /\ x = X ) -> ( I <_ ( x + ( M - I ) ) <-> I <_ ( X + ( M - I ) ) ) )
16 15 ifbid 
 |-  ( ( ph /\ x = X ) -> if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
17 14 16 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) = ( ( X + ( M - I ) ) + if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) ) )
18 6 a1i 
 |-  ( ( ph /\ x = X ) -> G = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
19 18 eqcomd 
 |-  ( ( ph /\ x = X ) -> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) = G )
20 19 oveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( X + ( M - I ) ) + if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) ) = ( ( X + ( M - I ) ) + G ) )
21 17 20 eqtrd 
 |-  ( ( ph /\ x = X ) -> ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) = ( ( X + ( M - I ) ) + G ) )
22 10 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( x - I ) = ( X - I ) )
23 22 breq2d 
 |-  ( ( ph /\ x = X ) -> ( I <_ ( x - I ) <-> I <_ ( X - I ) ) )
24 23 ifbid 
 |-  ( ( ph /\ x = X ) -> if ( I <_ ( x - I ) , 1 , 0 ) = if ( I <_ ( X - I ) , 1 , 0 ) )
25 22 24 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) = ( ( X - I ) + if ( I <_ ( X - I ) , 1 , 0 ) ) )
26 7 a1i 
 |-  ( ( ph /\ x = X ) -> H = if ( I <_ ( X - I ) , 1 , 0 ) )
27 26 eqcomd 
 |-  ( ( ph /\ x = X ) -> if ( I <_ ( X - I ) , 1 , 0 ) = H )
28 27 oveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( X - I ) + if ( I <_ ( X - I ) , 1 , 0 ) ) = ( ( X - I ) + H ) )
29 25 28 eqtrd 
 |-  ( ( ph /\ x = X ) -> ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) = ( ( X - I ) + H ) )
30 12 21 29 ifbieq12d 
 |-  ( ( ph /\ x = X ) -> if ( x < I , ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) , ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) ) = if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) )
31 11 10 30 ifbieq12d 
 |-  ( ( ph /\ x = X ) -> if ( x = I , x , if ( x < I , ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) , ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) ) ) = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
32 8 a1i 
 |-  ( ( ph /\ x = X ) -> R = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
33 32 eqcomd 
 |-  ( ( ph /\ x = X ) -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) = R )
34 31 33 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x = I , x , if ( x < I , ( ( x + ( M - I ) ) + if ( I <_ ( x + ( M - I ) ) , 1 , 0 ) ) , ( ( x - I ) + if ( I <_ ( x - I ) , 1 , 0 ) ) ) ) = R )
35 4 elfzelzd 
 |-  ( ph -> X e. ZZ )
36 1 nnzd 
 |-  ( ph -> M e. ZZ )
37 2 nnzd 
 |-  ( ph -> I e. ZZ )
38 36 37 zsubcld 
 |-  ( ph -> ( M - I ) e. ZZ )
39 35 38 zaddcld 
 |-  ( ph -> ( X + ( M - I ) ) e. ZZ )
40 1zzd 
 |-  ( ph -> 1 e. ZZ )
41 0zd 
 |-  ( ph -> 0 e. ZZ )
42 40 41 ifcld 
 |-  ( ph -> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) e. ZZ )
43 6 a1i 
 |-  ( ph -> G = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
44 43 eleq1d 
 |-  ( ph -> ( G e. ZZ <-> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) e. ZZ ) )
45 42 44 mpbird 
 |-  ( ph -> G e. ZZ )
46 39 45 zaddcld 
 |-  ( ph -> ( ( X + ( M - I ) ) + G ) e. ZZ )
47 35 37 zsubcld 
 |-  ( ph -> ( X - I ) e. ZZ )
48 40 41 ifcld 
 |-  ( ph -> if ( I <_ ( X - I ) , 1 , 0 ) e. ZZ )
49 7 a1i 
 |-  ( ph -> H = if ( I <_ ( X - I ) , 1 , 0 ) )
50 49 eleq1d 
 |-  ( ph -> ( H e. ZZ <-> if ( I <_ ( X - I ) , 1 , 0 ) e. ZZ ) )
51 48 50 mpbird 
 |-  ( ph -> H e. ZZ )
52 47 51 zaddcld 
 |-  ( ph -> ( ( X - I ) + H ) e. ZZ )
53 46 52 ifcld 
 |-  ( ph -> if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) e. ZZ )
54 35 53 ifcld 
 |-  ( ph -> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) e. ZZ )
55 8 a1i 
 |-  ( ph -> R = if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) )
56 55 eleq1d 
 |-  ( ph -> ( R e. ZZ <-> if ( X = I , X , if ( X < I , ( ( X + ( M - I ) ) + G ) , ( ( X - I ) + H ) ) ) e. ZZ ) )
57 54 56 mpbird 
 |-  ( ph -> R e. ZZ )
58 9 34 4 57 fvmptd 
 |-  ( ph -> ( D ` X ) = R )