Metamath Proof Explorer

Theorem metakunt28

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

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

Proof

Step Hyp Ref Expression
1 metakunt28.1 
 |-  ( ph -> M e. NN )
2 metakunt28.2 
 |-  ( ph -> I e. NN )
3 metakunt28.3 
 |-  ( ph -> I <_ M )
4 metakunt28.4 
 |-  ( ph -> X e. ( 1 ... M ) )
5 metakunt28.5 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
6 metakunt28.6 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
7 metakunt28.7 
 |-  ( ph -> -. X = I )
8 metakunt28.8 
 |-  ( ph -> -. X < I )
9 5 a1i 
 |-  ( ph -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
10 7 adantr 
 |-  ( ( ph /\ x = X ) -> -. X = I )
11 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
12 11 eqeq1d 
 |-  ( ( ph /\ x = X ) -> ( x = I <-> X = I ) )
13 12 notbid 
 |-  ( ( ph /\ x = X ) -> ( -. x = I <-> -. X = I ) )
14 10 13 mpbird 
 |-  ( ( ph /\ x = X ) -> -. x = I )
15 14 iffalsed 
 |-  ( ( ph /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( x < I , x , ( x - 1 ) ) )
16 8 adantr 
 |-  ( ( ph /\ x = X ) -> -. X < I )
17 11 breq1d 
 |-  ( ( ph /\ x = X ) -> ( x < I <-> X < I ) )
18 17 notbid 
 |-  ( ( ph /\ x = X ) -> ( -. x < I <-> -. X < I ) )
19 16 18 mpbird 
 |-  ( ( ph /\ x = X ) -> -. x < I )
20 19 iffalsed 
 |-  ( ( ph /\ x = X ) -> if ( x < I , x , ( x - 1 ) ) = ( x - 1 ) )
21 11 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( x - 1 ) = ( X - 1 ) )
22 20 21 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x < I , x , ( x - 1 ) ) = ( X - 1 ) )
23 15 22 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = ( X - 1 ) )
24 4 elfzelzd 
 |-  ( ph -> X e. ZZ )
25 1zzd 
 |-  ( ph -> 1 e. ZZ )
26 24 25 zsubcld 
 |-  ( ph -> ( X - 1 ) e. ZZ )
27 9 23 4 26 fvmptd 
 |-  ( ph -> ( A ` X ) = ( X - 1 ) )
28 27 fveq2d 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( B ` ( X - 1 ) ) )
29 6 a1i 
 |-  ( ph -> B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) ) )
30 26 zred 
 |-  ( ph -> ( X - 1 ) e. RR )
31 24 zred 
 |-  ( ph -> X e. RR )
32 1 nnred 
 |-  ( ph -> M e. RR )
33 1rp 
 |-  1 e. RR+
34 33 a1i 
 |-  ( ph -> 1 e. RR+ )
35 31 34 ltsubrpd 
 |-  ( ph -> ( X - 1 ) < X )
36 elfzle2 
 |-  ( X e. ( 1 ... M ) -> X <_ M )
37 4 36 syl 
 |-  ( ph -> X <_ M )
38 30 31 32 35 37 ltletrd 
 |-  ( ph -> ( X - 1 ) < M )
39 30 38 ltned 
 |-  ( ph -> ( X - 1 ) =/= M )
40 39 adantr 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( X - 1 ) =/= M )
41 40 neneqd 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> -. ( X - 1 ) = M )
42 simpr 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> z = ( X - 1 ) )
43 42 eqeq1d 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( z = M <-> ( X - 1 ) = M ) )
44 43 notbid 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( -. z = M <-> -. ( X - 1 ) = M ) )
45 41 44 mpbird 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> -. z = M )
46 45 iffalsed 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) = if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) )
47 7 neqned 
 |-  ( ph -> X =/= I )
48 2 nnred 
 |-  ( ph -> I e. RR )
49 48 31 8 nltled 
 |-  ( ph -> I <_ X )
50 48 31 49 leltned 
 |-  ( ph -> ( I < X <-> X =/= I ) )
51 47 50 mpbird 
 |-  ( ph -> I < X )
52 2 nnzd 
 |-  ( ph -> I e. ZZ )
53 52 24 zltlem1d 
 |-  ( ph -> ( I < X <-> I <_ ( X - 1 ) ) )
54 51 53 mpbid 
 |-  ( ph -> I <_ ( X - 1 ) )
55 48 30 lenltd 
 |-  ( ph -> ( I <_ ( X - 1 ) <-> -. ( X - 1 ) < I ) )
56 54 55 mpbid 
 |-  ( ph -> -. ( X - 1 ) < I )
57 56 adantr 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> -. ( X - 1 ) < I )
58 42 breq1d 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( z < I <-> ( X - 1 ) < I ) )
59 58 notbid 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( -. z < I <-> -. ( X - 1 ) < I ) )
60 57 59 mpbird 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> -. z < I )
61 60 iffalsed 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) = ( z + ( 1 - I ) ) )
62 42 oveq1d 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( z + ( 1 - I ) ) = ( ( X - 1 ) + ( 1 - I ) ) )
63 24 zcnd 
 |-  ( ph -> X e. CC )
64 1cnd 
 |-  ( ph -> 1 e. CC )
65 2 nncnd 
 |-  ( ph -> I e. CC )
66 63 64 65 npncand 
 |-  ( ph -> ( ( X - 1 ) + ( 1 - I ) ) = ( X - I ) )
67 66 adantr 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( ( X - 1 ) + ( 1 - I ) ) = ( X - I ) )
68 62 67 eqtrd 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> ( z + ( 1 - I ) ) = ( X - I ) )
69 61 68 eqtrd 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) = ( X - I ) )
70 46 69 eqtrd 
 |-  ( ( ph /\ z = ( X - 1 ) ) -> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) = ( X - I ) )
71 1 nnzd 
 |-  ( ph -> M e. ZZ )
72 1red 
 |-  ( ph -> 1 e. RR )
73 2 nnge1d 
 |-  ( ph -> 1 <_ I )
74 72 48 31 73 51 lelttrd 
 |-  ( ph -> 1 < X )
75 25 24 zltlem1d 
 |-  ( ph -> ( 1 < X <-> 1 <_ ( X - 1 ) ) )
76 74 75 mpbid 
 |-  ( ph -> 1 <_ ( X - 1 ) )
77 31 72 resubcld 
 |-  ( ph -> ( X - 1 ) e. RR )
78 0le1 
 |-  0 <_ 1
79 78 a1i 
 |-  ( ph -> 0 <_ 1 )
80 31 72 subge02d 
 |-  ( ph -> ( 0 <_ 1 <-> ( X - 1 ) <_ X ) )
81 79 80 mpbid 
 |-  ( ph -> ( X - 1 ) <_ X )
82 77 31 32 81 37 letrd 
 |-  ( ph -> ( X - 1 ) <_ M )
83 25 71 26 76 82 elfzd 
 |-  ( ph -> ( X - 1 ) e. ( 1 ... M ) )
84 24 52 zsubcld 
 |-  ( ph -> ( X - I ) e. ZZ )
85 29 70 83 84 fvmptd 
 |-  ( ph -> ( B ` ( X - 1 ) ) = ( X - I ) )
86 28 85 eqtrd 
 |-  ( ph -> ( B ` ( A ` X ) ) = ( X - I ) )