Metamath Proof Explorer

Theorem metakunt30

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

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

Proof

Step Hyp Ref Expression
1 metakunt30.1 
 |-  ( ph -> M e. NN )
2 metakunt30.2 
 |-  ( ph -> I e. NN )
3 metakunt30.3 
 |-  ( ph -> I <_ M )
4 metakunt30.4 
 |-  ( ph -> X e. ( 1 ... M ) )
5 metakunt30.5 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
6 metakunt30.6 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
7 metakunt30.7 
 |-  ( ph -> -. X = I )
8 metakunt30.8 
 |-  ( ph -> -. X < I )
9 metakunt30.9 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
10 metakunt30.10 
 |-  H = if ( I <_ ( X - I ) , 1 , 0 )
11 1 2 3 4 5 6 7 8 metakunt28 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( X - I ) )
12 11 fveq2d 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = ( C ` ( X - 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 2 nnred 
 |-  ( ph -> I e. RR )
19 17 18 resubcld 
 |-  ( ph -> ( X - I ) e. RR )
20 1 nnred 
 |-  ( ph -> M e. RR )
21 20 18 resubcld 
 |-  ( ph -> ( M - I ) e. RR )
22 elfzle2 
 |-  ( X e. ( 1 ... M ) -> X <_ M )
23 4 22 syl 
 |-  ( ph -> X <_ M )
24 17 20 18 23 lesub1dd 
 |-  ( ph -> ( X - I ) <_ ( M - I ) )
25 2 nnrpd 
 |-  ( ph -> I e. RR+ )
26 20 25 ltsubrpd 
 |-  ( ph -> ( M - I ) < M )
27 19 21 20 24 26 lelttrd 
 |-  ( ph -> ( X - I ) < M )
28 19 27 ltned 
 |-  ( ph -> ( X - I ) =/= M )
29 28 adantr 
 |-  ( ( ph /\ y = ( X - I ) ) -> ( X - I ) =/= M )
30 neeq1 
 |-  ( y = ( X - I ) -> ( y =/= M <-> ( X - I ) =/= M ) )
31 30 adantl 
 |-  ( ( ph /\ y = ( X - I ) ) -> ( y =/= M <-> ( X - I ) =/= M ) )
32 29 31 mpbird 
 |-  ( ( ph /\ y = ( X - I ) ) -> y =/= M )
33 32 neneqd 
 |-  ( ( ph /\ y = ( X - I ) ) -> -. y = M )
34 33 iffalsed 
 |-  ( ( ph /\ y = ( X - I ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( y < I , y , ( y + 1 ) ) )
35 18 19 lenltd 
 |-  ( ph -> ( I <_ ( X - I ) <-> -. ( X - I ) < I ) )
36 35 biimpa 
 |-  ( ( ph /\ I <_ ( X - I ) ) -> -. ( X - I ) < I )
37 36 3adant2 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> -. ( X - I ) < I )
38 breq1 
 |-  ( y = ( X - I ) -> ( y < I <-> ( X - I ) < I ) )
39 38 3ad2ant2 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> ( y < I <-> ( X - I ) < I ) )
40 37 39 mtbird 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> -. y < I )
41 40 iffalsed 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = ( y + 1 ) )
42 simp2 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> y = ( X - I ) )
43 42 oveq1d 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> ( y + 1 ) = ( ( X - I ) + 1 ) )
44 simp3 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> I <_ ( X - I ) )
45 44 iftrued 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> if ( I <_ ( X - I ) , 1 , 0 ) = 1 )
46 45 eqcomd 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> 1 = if ( I <_ ( X - I ) , 1 , 0 ) )
47 10 a1i 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> H = if ( I <_ ( X - I ) , 1 , 0 ) )
48 47 eqcomd 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> if ( I <_ ( X - I ) , 1 , 0 ) = H )
49 46 48 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> 1 = H )
50 49 oveq2d 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> ( ( X - I ) + 1 ) = ( ( X - I ) + H ) )
51 43 50 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> ( y + 1 ) = ( ( X - I ) + H ) )
52 41 51 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ I <_ ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X - I ) + H ) )
53 52 3expa 
 |-  ( ( ( ph /\ y = ( X - I ) ) /\ I <_ ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X - I ) + H ) )
54 simpr 
 |-  ( ( ph /\ -. I <_ ( X - I ) ) -> -. I <_ ( X - I ) )
55 19 adantr 
 |-  ( ( ph /\ -. I <_ ( X - I ) ) -> ( X - I ) e. RR )
56 18 adantr 
 |-  ( ( ph /\ -. I <_ ( X - I ) ) -> I e. RR )
57 55 56 ltnled 
 |-  ( ( ph /\ -. I <_ ( X - I ) ) -> ( ( X - I ) < I <-> -. I <_ ( X - I ) ) )
58 54 57 mpbird 
 |-  ( ( ph /\ -. I <_ ( X - I ) ) -> ( X - I ) < I )
59 58 3adant2 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( X - I ) < I )
60 38 3ad2ant2 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( y < I <-> ( X - I ) < I ) )
61 59 60 mpbird 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> y < I )
62 61 iftrued 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = y )
63 simp2 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> y = ( X - I ) )
64 nncn 
 |-  ( X e. NN -> X e. CC )
65 15 64 syl 
 |-  ( ph -> X e. CC )
66 65 3ad2ant1 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> X e. CC )
67 2 nncnd 
 |-  ( ph -> I e. CC )
68 67 3ad2ant1 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> I e. CC )
69 66 68 subcld 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( X - I ) e. CC )
70 69 addridd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( ( X - I ) + 0 ) = ( X - I ) )
71 70 eqcomd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( X - I ) = ( ( X - I ) + 0 ) )
72 10 a1i 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> H = if ( I <_ ( X - I ) , 1 , 0 ) )
73 simp3 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> -. I <_ ( X - I ) )
74 73 iffalsed 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> if ( I <_ ( X - I ) , 1 , 0 ) = 0 )
75 72 74 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> H = 0 )
76 75 eqcomd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> 0 = H )
77 76 oveq2d 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( ( X - I ) + 0 ) = ( ( X - I ) + H ) )
78 71 77 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> ( X - I ) = ( ( X - I ) + H ) )
79 63 78 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> y = ( ( X - I ) + H ) )
80 62 79 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) /\ -. I <_ ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X - I ) + H ) )
81 80 3expa 
 |-  ( ( ( ph /\ y = ( X - I ) ) /\ -. I <_ ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X - I ) + H ) )
82 53 81 pm2.61dan 
 |-  ( ( ph /\ y = ( X - I ) ) -> if ( y < I , y , ( y + 1 ) ) = ( ( X - I ) + H ) )
83 34 82 eqtrd 
 |-  ( ( ph /\ y = ( X - I ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = ( ( X - I ) + H ) )
84 1zzd 
 |-  ( ph -> 1 e. ZZ )
85 1 nnzd 
 |-  ( ph -> M e. ZZ )
86 15 nnzd 
 |-  ( ph -> X e. ZZ )
87 2 nnzd 
 |-  ( ph -> I e. ZZ )
88 86 87 zsubcld 
 |-  ( ph -> ( X - I ) e. ZZ )
89 1m1e0 
 |-  ( 1 - 1 ) = 0
90 18 17 8 nltled 
 |-  ( ph -> I <_ X )
91 7 neqned 
 |-  ( ph -> X =/= I )
92 90 91 jca 
 |-  ( ph -> ( I <_ X /\ X =/= I ) )
93 18 17 ltlend 
 |-  ( ph -> ( I < X <-> ( I <_ X /\ X =/= I ) ) )
94 92 93 mpbird 
 |-  ( ph -> I < X )
95 18 17 posdifd 
 |-  ( ph -> ( I < X <-> 0 < ( X - I ) ) )
96 94 95 mpbid 
 |-  ( ph -> 0 < ( X - I ) )
97 89 96 eqbrtrid 
 |-  ( ph -> ( 1 - 1 ) < ( X - I ) )
98 zlem1lt 
 |-  ( ( 1 e. ZZ /\ ( X - I ) e. ZZ ) -> ( 1 <_ ( X - I ) <-> ( 1 - 1 ) < ( X - I ) ) )
99 84 88 98 syl2anc 
 |-  ( ph -> ( 1 <_ ( X - I ) <-> ( 1 - 1 ) < ( X - I ) ) )
100 97 99 mpbird 
 |-  ( ph -> 1 <_ ( X - I ) )
101 19 20 27 ltled 
 |-  ( ph -> ( X - I ) <_ M )
102 84 85 88 100 101 elfzd 
 |-  ( ph -> ( X - I ) e. ( 1 ... M ) )
103 0zd 
 |-  ( ph -> 0 e. ZZ )
104 84 103 ifcld 
 |-  ( ph -> if ( I <_ ( X - I ) , 1 , 0 ) e. ZZ )
105 10 a1i 
 |-  ( ph -> H = if ( I <_ ( X - I ) , 1 , 0 ) )
106 105 eleq1d 
 |-  ( ph -> ( H e. ZZ <-> if ( I <_ ( X - I ) , 1 , 0 ) e. ZZ ) )
107 104 106 mpbird 
 |-  ( ph -> H e. ZZ )
108 88 107 zaddcld 
 |-  ( ph -> ( ( X - I ) + H ) e. ZZ )
109 13 83 102 108 fvmptd 
 |-  ( ph -> ( C ` ( X - I ) ) = ( ( X - I ) + H ) )
110 12 109 eqtrd 
 |-  ( ph -> ( C ` ( B ` ( A ` X ) ) ) = ( ( X - I ) + H ) )