Metamath Proof Explorer

Theorem uzrdgxfr

Description: Transfer the value of the recursive sequence builder from one base to another. (Contributed by Mario Carneiro, 1-Apr-2014)

Ref Expression
Hypotheses uzrdgxfr.1 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om )
uzrdgxfr.2 
|- H = ( rec ( ( x e. _V |-> ( x + 1 ) ) , B ) |` _om )
uzrdgxfr.3 
|- A e. ZZ
uzrdgxfr.4 
|- B e. ZZ
Assertion uzrdgxfr 
|- ( N e. _om -> ( G ` N ) = ( ( H ` N ) + ( A - B ) ) )

Proof

Step Hyp Ref Expression
1 uzrdgxfr.1 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om )
2 uzrdgxfr.2 
 |-  H = ( rec ( ( x e. _V |-> ( x + 1 ) ) , B ) |` _om )
3 uzrdgxfr.3 
 |-  A e. ZZ
4 uzrdgxfr.4 
 |-  B e. ZZ
5 fveq2 
 |-  ( y = (/) -> ( G ` y ) = ( G ` (/) ) )
6 fveq2 
 |-  ( y = (/) -> ( H ` y ) = ( H ` (/) ) )
7 6 oveq1d 
 |-  ( y = (/) -> ( ( H ` y ) + ( A - B ) ) = ( ( H ` (/) ) + ( A - B ) ) )
8 5 7 eqeq12d 
 |-  ( y = (/) -> ( ( G ` y ) = ( ( H ` y ) + ( A - B ) ) <-> ( G ` (/) ) = ( ( H ` (/) ) + ( A - B ) ) ) )
9 fveq2 
 |-  ( y = k -> ( G ` y ) = ( G ` k ) )
10 fveq2 
 |-  ( y = k -> ( H ` y ) = ( H ` k ) )
11 10 oveq1d 
 |-  ( y = k -> ( ( H ` y ) + ( A - B ) ) = ( ( H ` k ) + ( A - B ) ) )
12 9 11 eqeq12d 
 |-  ( y = k -> ( ( G ` y ) = ( ( H ` y ) + ( A - B ) ) <-> ( G ` k ) = ( ( H ` k ) + ( A - B ) ) ) )
13 fveq2 
 |-  ( y = suc k -> ( G ` y ) = ( G ` suc k ) )
14 fveq2 
 |-  ( y = suc k -> ( H ` y ) = ( H ` suc k ) )
15 14 oveq1d 
 |-  ( y = suc k -> ( ( H ` y ) + ( A - B ) ) = ( ( H ` suc k ) + ( A - B ) ) )
16 13 15 eqeq12d 
 |-  ( y = suc k -> ( ( G ` y ) = ( ( H ` y ) + ( A - B ) ) <-> ( G ` suc k ) = ( ( H ` suc k ) + ( A - B ) ) ) )
17 fveq2 
 |-  ( y = N -> ( G ` y ) = ( G ` N ) )
18 fveq2 
 |-  ( y = N -> ( H ` y ) = ( H ` N ) )
19 18 oveq1d 
 |-  ( y = N -> ( ( H ` y ) + ( A - B ) ) = ( ( H ` N ) + ( A - B ) ) )
20 17 19 eqeq12d 
 |-  ( y = N -> ( ( G ` y ) = ( ( H ` y ) + ( A - B ) ) <-> ( G ` N ) = ( ( H ` N ) + ( A - B ) ) ) )
21 zcn 
 |-  ( B e. ZZ -> B e. CC )
22 4 21 ax-mp 
 |-  B e. CC
23 zcn 
 |-  ( A e. ZZ -> A e. CC )
24 3 23 ax-mp 
 |-  A e. CC
25 22 24 pncan3i 
 |-  ( B + ( A - B ) ) = A
26 4 2 om2uz0i 
 |-  ( H ` (/) ) = B
27 26 oveq1i 
 |-  ( ( H ` (/) ) + ( A - B ) ) = ( B + ( A - B ) )
28 3 1 om2uz0i 
 |-  ( G ` (/) ) = A
29 25 27 28 3eqtr4ri 
 |-  ( G ` (/) ) = ( ( H ` (/) ) + ( A - B ) )
30 oveq1 
 |-  ( ( G ` k ) = ( ( H ` k ) + ( A - B ) ) -> ( ( G ` k ) + 1 ) = ( ( ( H ` k ) + ( A - B ) ) + 1 ) )
31 3 1 om2uzsuci 
 |-  ( k e. _om -> ( G ` suc k ) = ( ( G ` k ) + 1 ) )
32 4 2 om2uzsuci 
 |-  ( k e. _om -> ( H ` suc k ) = ( ( H ` k ) + 1 ) )
33 32 oveq1d 
 |-  ( k e. _om -> ( ( H ` suc k ) + ( A - B ) ) = ( ( ( H ` k ) + 1 ) + ( A - B ) ) )
34 4 2 om2uzuzi 
 |-  ( k e. _om -> ( H ` k ) e. ( ZZ>= ` B ) )
35 eluzelz 
 |-  ( ( H ` k ) e. ( ZZ>= ` B ) -> ( H ` k ) e. ZZ )
36 34 35 syl 
 |-  ( k e. _om -> ( H ` k ) e. ZZ )
37 36 zcnd 
 |-  ( k e. _om -> ( H ` k ) e. CC )
38 ax-1cn 
 |-  1 e. CC
39 24 22 subcli 
 |-  ( A - B ) e. CC
40 add32 
 |-  ( ( ( H ` k ) e. CC /\ 1 e. CC /\ ( A - B ) e. CC ) -> ( ( ( H ` k ) + 1 ) + ( A - B ) ) = ( ( ( H ` k ) + ( A - B ) ) + 1 ) )
41 38 39 40 mp3an23 
 |-  ( ( H ` k ) e. CC -> ( ( ( H ` k ) + 1 ) + ( A - B ) ) = ( ( ( H ` k ) + ( A - B ) ) + 1 ) )
42 37 41 syl 
 |-  ( k e. _om -> ( ( ( H ` k ) + 1 ) + ( A - B ) ) = ( ( ( H ` k ) + ( A - B ) ) + 1 ) )
43 33 42 eqtrd 
 |-  ( k e. _om -> ( ( H ` suc k ) + ( A - B ) ) = ( ( ( H ` k ) + ( A - B ) ) + 1 ) )
44 31 43 eqeq12d 
 |-  ( k e. _om -> ( ( G ` suc k ) = ( ( H ` suc k ) + ( A - B ) ) <-> ( ( G ` k ) + 1 ) = ( ( ( H ` k ) + ( A - B ) ) + 1 ) ) )
45 30 44 imbitrrid 
 |-  ( k e. _om -> ( ( G ` k ) = ( ( H ` k ) + ( A - B ) ) -> ( G ` suc k ) = ( ( H ` suc k ) + ( A - B ) ) ) )
46 8 12 16 20 29 45 finds 
 |-  ( N e. _om -> ( G ` N ) = ( ( H ` N ) + ( A - B ) ) )