Step |
Hyp |
Ref |
Expression |
1 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
2 |
|
fveq2 |
|- ( M = if ( M e. ZZ , M , 0 ) -> ( ZZ>= ` M ) = ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ) |
3 |
2
|
eleq2d |
|- ( M = if ( M e. ZZ , M , 0 ) -> ( N e. ( ZZ>= ` M ) <-> N e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ) ) |
4 |
|
fvoveq1 |
|- ( M = if ( M e. ZZ , M , 0 ) -> ( ZZ>= ` ( M + K ) ) = ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + K ) ) ) |
5 |
4
|
eleq2d |
|- ( M = if ( M e. ZZ , M , 0 ) -> ( ( N + K ) e. ( ZZ>= ` ( M + K ) ) <-> ( N + K ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + K ) ) ) ) |
6 |
3 5
|
imbi12d |
|- ( M = if ( M e. ZZ , M , 0 ) -> ( ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) ) <-> ( N e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) -> ( N + K ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + K ) ) ) ) ) |
7 |
|
oveq2 |
|- ( K = if ( K e. ZZ , K , 0 ) -> ( N + K ) = ( N + if ( K e. ZZ , K , 0 ) ) ) |
8 |
|
oveq2 |
|- ( K = if ( K e. ZZ , K , 0 ) -> ( if ( M e. ZZ , M , 0 ) + K ) = ( if ( M e. ZZ , M , 0 ) + if ( K e. ZZ , K , 0 ) ) ) |
9 |
8
|
fveq2d |
|- ( K = if ( K e. ZZ , K , 0 ) -> ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + K ) ) = ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + if ( K e. ZZ , K , 0 ) ) ) ) |
10 |
7 9
|
eleq12d |
|- ( K = if ( K e. ZZ , K , 0 ) -> ( ( N + K ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + K ) ) <-> ( N + if ( K e. ZZ , K , 0 ) ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + if ( K e. ZZ , K , 0 ) ) ) ) ) |
11 |
10
|
imbi2d |
|- ( K = if ( K e. ZZ , K , 0 ) -> ( ( N e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) -> ( N + K ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + K ) ) ) <-> ( N e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) -> ( N + if ( K e. ZZ , K , 0 ) ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + if ( K e. ZZ , K , 0 ) ) ) ) ) ) |
12 |
|
0z |
|- 0 e. ZZ |
13 |
12
|
elimel |
|- if ( M e. ZZ , M , 0 ) e. ZZ |
14 |
12
|
elimel |
|- if ( K e. ZZ , K , 0 ) e. ZZ |
15 |
13 14
|
eluzaddi |
|- ( N e. ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) -> ( N + if ( K e. ZZ , K , 0 ) ) e. ( ZZ>= ` ( if ( M e. ZZ , M , 0 ) + if ( K e. ZZ , K , 0 ) ) ) ) |
16 |
6 11 15
|
dedth2h |
|- ( ( M e. ZZ /\ K e. ZZ ) -> ( N e. ( ZZ>= ` M ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) ) ) |
17 |
16
|
com12 |
|- ( N e. ( ZZ>= ` M ) -> ( ( M e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) ) ) |
18 |
1 17
|
mpand |
|- ( N e. ( ZZ>= ` M ) -> ( K e. ZZ -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) ) ) |
19 |
18
|
imp |
|- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( N + K ) e. ( ZZ>= ` ( M + K ) ) ) |