Metamath Proof Explorer

Theorem metakunt26

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

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

Proof

Step Hyp Ref Expression
1 metakunt26.1 
 |-  ( ph -> M e. NN )
2 metakunt26.2 
 |-  ( ph -> I e. NN )
3 metakunt26.3 
 |-  ( ph -> I <_ M )
4 metakunt26.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt26.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt26.6 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
7 metakunt26.7 
 |-  ( ph -> X = I )
8 4 a1i 
 |-  ( ph -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
9 7 eqeq2d 
 |-  ( ph -> ( x = X <-> x = I ) )
10 simpr 
 |-  ( ( ph /\ x = I ) -> x = I )
11 10 iftrued 
 |-  ( ( ph /\ x = I ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = M )
12 11 ex 
 |-  ( ph -> ( x = I -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = M ) )
13 9 12 sylbid 
 |-  ( ph -> ( x = X -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = M ) )
14 13 imp 
 |-  ( ( ph /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = M )
15 1zzd 
 |-  ( ph -> 1 e. ZZ )
16 nnz 
 |-  ( M e. NN -> M e. ZZ )
17 1 16 syl 
 |-  ( ph -> M e. ZZ )
18 2 nnzd 
 |-  ( ph -> I e. ZZ )
19 2 nnge1d 
 |-  ( ph -> 1 <_ I )
20 15 17 18 19 3 elfzd 
 |-  ( ph -> I e. ( 1 ... M ) )
21 7 eleq1d 
 |-  ( ph -> ( X e. ( 1 ... M ) <-> I e. ( 1 ... M ) ) )
22 20 21 mpbird 
 |-  ( ph -> X e. ( 1 ... M ) )
23 8 14 22 1 fvmptd 
 |-  ( ph -> ( A ` X ) = M )
24 23 fveq2d 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( B ` M ) )
25 6 a1i 
 |-  ( ph -> B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) ) )
26 simpr 
 |-  ( ( ph /\ z = M ) -> z = M )
27 26 iftrued 
 |-  ( ( ph /\ z = M ) -> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) = M )
28 1zzd 
 |-  ( M e. NN -> 1 e. ZZ )
29 nnge1 
 |-  ( M e. NN -> 1 <_ M )
30 nnre 
 |-  ( M e. NN -> M e. RR )
31 30 leidd 
 |-  ( M e. NN -> M <_ M )
32 28 16 16 29 31 elfzd 
 |-  ( M e. NN -> M e. ( 1 ... M ) )
33 1 32 syl 
 |-  ( ph -> M e. ( 1 ... M ) )
34 25 27 33 1 fvmptd 
 |-  ( ph -> ( B ` M ) = M )
35 24 34 eqtrd 
 |-  ( ph -> ( B ` ( A ` X ) ) = M )
36 35 fveq2d 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = ( C ` M ) )
37 5 a1i 
 |-  ( ph -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
38 simpr 
 |-  ( ( ph /\ y = M ) -> y = M )
39 38 iftrued 
 |-  ( ( ph /\ y = M ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = I )
40 37 39 33 2 fvmptd 
 |-  ( ph -> ( C ` M ) = I )
41 36 40 eqtrd 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = I )
42 7 eqcomd 
 |-  ( ph -> I = X )
43 41 42 eqtrd 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = X )