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 addid1d
 |-  ( ( 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 ) )