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