Metamath Proof Explorer

Theorem metakunt29

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

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

Proof

Step Hyp Ref Expression
1 metakunt29.1 
 |-  ( ph -> M e. NN )
2 metakunt29.2 
 |-  ( ph -> I e. NN )
3 metakunt29.3 
 |-  ( ph -> I <_ M )
4 metakunt29.4 
 |-  ( ph -> X e. ( 1 ... M ) )
5 metakunt29.5 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
6 metakunt29.6 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
7 metakunt29.7 
 |-  ( ph -> -. X = I )
8 metakunt29.8 
 |-  ( ph -> X < I )
9 metakunt29.9 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
10 metakunt29.10 
 |-  H = if ( I <_ ( X + ( M - I ) ) , 1 , 0 )
11 1 2 3 4 5 6 7 8 metakunt27 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( X + ( M - I ) ) )
12 11 fveq2d 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = ( C ` ( X + ( M - I ) ) ) )
13 9 a1i 
 |-  ( ph -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
14 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
15 4 14 syl 
 |-  ( ph -> X e. NN )
16 nnre 
 |-  ( X e. NN -> X e. RR )
17 15 16 syl 
 |-  ( ph -> X e. RR )
18 1 nnred 
 |-  ( ph -> M e. RR )
19 2 nnred 
 |-  ( ph -> I e. RR )
20 18 19 resubcld 
 |-  ( ph -> ( M - I ) e. RR )
21 17 20 readdcld 
 |-  ( ph -> ( X + ( M - I ) ) e. RR )
22 17 recnd 
 |-  ( ph -> X e. CC )
23 18 recnd 
 |-  ( ph -> M e. CC )
24 19 recnd 
 |-  ( ph -> I e. CC )
25 22 23 24 addsub12d 
 |-  ( ph -> ( X + ( M - I ) ) = ( M + ( X - I ) ) )
26 23 24 22 subsub2d 
 |-  ( ph -> ( M - ( I - X ) ) = ( M + ( X - I ) ) )
27 19 17 resubcld 
 |-  ( ph -> ( I - X ) e. RR )
28 17 19 posdifd 
 |-  ( ph -> ( X < I <-> 0 < ( I - X ) ) )
29 8 28 mpbid 
 |-  ( ph -> 0 < ( I - X ) )
30 27 29 elrpd 
 |-  ( ph -> ( I - X ) e. RR+ )
31 18 30 ltsubrpd 
 |-  ( ph -> ( M - ( I - X ) ) < M )
32 26 31 eqbrtrrd 
 |-  ( ph -> ( M + ( X - I ) ) < M )
33 25 32 eqbrtrd 
 |-  ( ph -> ( X + ( M - I ) ) < M )
34 21 33 ltned 
 |-  ( ph -> ( X + ( M - I ) ) =/= M )
35 34 adantr 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> ( X + ( M - I ) ) =/= M )
36 simpr 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> y = ( X + ( M - I ) ) )
37 36 neeq1d 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> ( y =/= M <-> ( X + ( M - I ) ) =/= M ) )
38 35 37 mpbird 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> y =/= M )
39 38 neneqd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> -. y = M )
40 39 iffalsed 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( y < I , y , ( y + 1 ) ) )
41 simpr 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> I <_ ( X + ( M - I ) ) )
42 19 adantr 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> I e. RR )
43 17 adantr 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> X e. RR )
44 18 adantr 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> M e. RR )
45 44 42 resubcld 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> ( M - I ) e. RR )
46 43 45 readdcld 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> ( X + ( M - I ) ) e. RR )
47 42 46 lenltd 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> ( I <_ ( X + ( M - I ) ) <-> -. ( X + ( M - I ) ) < I ) )
48 41 47 mpbid 
 |-  ( ( ph /\ I <_ ( X + ( M - I ) ) ) -> -. ( X + ( M - I ) ) < I )
49 48 3adant2 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> -. ( X + ( M - I ) ) < I )
50 simp2 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> y = ( X + ( M - I ) ) )
51 50 breq1d 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> ( y < I <-> ( X + ( M - I ) ) < I ) )
52 51 notbid 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> ( -. y < I <-> -. ( X + ( M - I ) ) < I ) )
53 49 52 mpbird 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> -. y < I )
54 53 iffalsed 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( y + 1 ) )
55 50 oveq1d 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> ( y + 1 ) = ( ( X + ( M - I ) ) + 1 ) )
56 54 55 eqtrd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X + ( M - I ) ) + 1 ) )
57 simp3 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> I <_ ( X + ( M - I ) ) )
58 57 iftrued 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) = 1 )
59 58 eqcomd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> 1 = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
60 59 10 eqtr4di 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> 1 = H )
61 60 oveq2d 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> ( ( X + ( M - I ) ) + 1 ) = ( ( X + ( M - I ) ) + H ) )
62 56 61 eqtrd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X + ( M - I ) ) + H ) )
63 62 3expa 
 |-  ( ( ( ph /\ y = ( X + ( M - I ) ) ) /\ I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X + ( M - I ) ) + H ) )
64 21 19 ltnled 
 |-  ( ph -> ( ( X + ( M - I ) ) < I <-> -. I <_ ( X + ( M - I ) ) ) )
65 64 biimprd 
 |-  ( ph -> ( -. I <_ ( X + ( M - I ) ) -> ( X + ( M - I ) ) < I ) )
66 65 imp 
 |-  ( ( ph /\ -. I <_ ( X + ( M - I ) ) ) -> ( X + ( M - I ) ) < I )
67 66 3adant2 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> ( X + ( M - I ) ) < I )
68 simp2 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> y = ( X + ( M - I ) ) )
69 68 breq1d 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> ( y < I <-> ( X + ( M - I ) ) < I ) )
70 67 69 mpbird 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> y < I )
71 70 iftrued 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = y )
72 22 adantr 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> X e. CC )
73 23 adantr 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> M e. CC )
74 24 adantr 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> I e. CC )
75 73 74 subcld 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> ( M - I ) e. CC )
76 72 75 addcld 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> ( X + ( M - I ) ) e. CC )
77 76 addridd 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> ( ( X + ( M - I ) ) + 0 ) = ( X + ( M - I ) ) )
78 77 eqcomd 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> ( X + ( M - I ) ) = ( ( X + ( M - I ) ) + 0 ) )
79 64 biimpa 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> -. I <_ ( X + ( M - I ) ) )
80 79 iffalsed 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) = 0 )
81 80 eqcomd 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> 0 = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
82 10 a1i 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> H = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
83 82 eqcomd 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) = H )
84 81 83 eqtrd 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> 0 = H )
85 84 oveq2d 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> ( ( X + ( M - I ) ) + 0 ) = ( ( X + ( M - I ) ) + H ) )
86 78 85 eqtrd 
 |-  ( ( ph /\ ( X + ( M - I ) ) < I ) -> ( X + ( M - I ) ) = ( ( X + ( M - I ) ) + H ) )
87 86 ex 
 |-  ( ph -> ( ( X + ( M - I ) ) < I -> ( X + ( M - I ) ) = ( ( X + ( M - I ) ) + H ) ) )
88 65 87 syld 
 |-  ( ph -> ( -. I <_ ( X + ( M - I ) ) -> ( X + ( M - I ) ) = ( ( X + ( M - I ) ) + H ) ) )
89 88 imp 
 |-  ( ( ph /\ -. I <_ ( X + ( M - I ) ) ) -> ( X + ( M - I ) ) = ( ( X + ( M - I ) ) + H ) )
90 89 3adant2 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> ( X + ( M - I ) ) = ( ( X + ( M - I ) ) + H ) )
91 68 90 eqtrd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> y = ( ( X + ( M - I ) ) + H ) )
92 71 91 eqtrd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X + ( M - I ) ) + H ) )
93 92 3expa 
 |-  ( ( ( ph /\ y = ( X + ( M - I ) ) ) /\ -. I <_ ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X + ( M - I ) ) + H ) )
94 63 93 pm2.61dan 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X + ( M - I ) ) + H ) )
95 40 94 eqtrd 
 |-  ( ( ph /\ y = ( X + ( M - I ) ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = ( ( X + ( M - I ) ) + H ) )
96 1zzd 
 |-  ( ph -> 1 e. ZZ )
97 1 nnzd 
 |-  ( ph -> M e. ZZ )
98 15 nnzd 
 |-  ( ph -> X e. ZZ )
99 2 nnzd 
 |-  ( ph -> I e. ZZ )
100 97 99 zsubcld 
 |-  ( ph -> ( M - I ) e. ZZ )
101 98 100 zaddcld 
 |-  ( ph -> ( X + ( M - I ) ) e. ZZ )
102 1p0e1 
 |-  ( 1 + 0 ) = 1
103 1red 
 |-  ( ph -> 1 e. RR )
104 0red 
 |-  ( ph -> 0 e. RR )
105 15 nnge1d 
 |-  ( ph -> 1 <_ X )
106 18 19 subge0d 
 |-  ( ph -> ( 0 <_ ( M - I ) <-> I <_ M ) )
107 3 106 mpbird 
 |-  ( ph -> 0 <_ ( M - I ) )
108 103 104 17 20 105 107 le2addd 
 |-  ( ph -> ( 1 + 0 ) <_ ( X + ( M - I ) ) )
109 102 108 eqbrtrrid 
 |-  ( ph -> 1 <_ ( X + ( M - I ) ) )
110 21 18 33 ltled 
 |-  ( ph -> ( X + ( M - I ) ) <_ M )
111 96 97 101 109 110 elfzd 
 |-  ( ph -> ( X + ( M - I ) ) e. ( 1 ... M ) )
112 111 elfzelzd 
 |-  ( ph -> ( X + ( M - I ) ) e. ZZ )
113 0zd 
 |-  ( ph -> 0 e. ZZ )
114 96 113 ifcld 
 |-  ( ph -> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) e. ZZ )
115 10 a1i 
 |-  ( ph -> H = if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) )
116 115 eleq1d 
 |-  ( ph -> ( H e. ZZ <-> if ( I <_ ( X + ( M - I ) ) , 1 , 0 ) e. ZZ ) )
117 114 116 mpbird 
 |-  ( ph -> H e. ZZ )
118 112 117 zaddcld 
 |-  ( ph -> ( ( X + ( M - I ) ) + H ) e. ZZ )
119 13 95 111 118 fvmptd 
 |-  ( ph -> ( C ` ( X + ( M - I ) ) ) = ( ( X + ( M - I ) ) + H ) )
120 12 119 eqtrd 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = ( ( X + ( M - I ) ) + H ) )