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∈V⟼x+1A↾ω
uzrdgxfr.2 ⊢H=rec⁡x∈V⟼x+1B↾ω
uzrdgxfr.3 ⊢A∈ℤ
uzrdgxfr.4 ⊢B∈ℤ
Assertion uzrdgxfr ⊢N∈ω→G⁡N=H⁡N+A-B

Proof

Step Hyp Ref Expression
1 uzrdgxfr.1 ⊢G=rec⁡x∈V⟼x+1A↾ω
2 uzrdgxfr.2 ⊢H=rec⁡x∈V⟼x+1B↾ω
3 uzrdgxfr.3 ⊢A∈ℤ
4 uzrdgxfr.4 ⊢B∈ℤ
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∈ℤ→B∈ℂ
22 4 21 ax-mp ⊢B∈ℂ
23 zcn ⊢A∈ℤ→A∈ℂ
24 3 23 ax-mp ⊢A∈ℂ
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∈ω→G⁡suc⁡k=G⁡k+1
32 4 2 om2uzsuci ⊢k∈ω→H⁡suc⁡k=H⁡k+1
33 32 oveq1d ⊢k∈ω→H⁡suc⁡k+A-B=H⁡k+1+A−B
34 4 2 om2uzuzi ⊢k∈ω→H⁡k∈ℤ≥B
35 eluzelz ⊢H⁡k∈ℤ≥B→H⁡k∈ℤ
36 34 35 syl ⊢k∈ω→H⁡k∈ℤ
37 36 zcnd ⊢k∈ω→H⁡k∈ℂ
38 ax-1cn ⊢1∈ℂ
39 24 22 subcli ⊢A−B∈ℂ
40 add32 ⊢H⁡k∈ℂ∧1∈ℂ∧A−B∈ℂ→H⁡k+1+A−B=H⁡k+A−B+1
41 38 39 40 mp3an23 ⊢H⁡k∈ℂ→H⁡k+1+A−B=H⁡k+A−B+1
42 37 41 syl ⊢k∈ω→H⁡k+1+A−B=H⁡k+A−B+1
43 33 42 eqtrd ⊢k∈ω→H⁡suc⁡k+A-B=H⁡k+A−B+1
44 31 43 eqeq12d ⊢k∈ω→G⁡suc⁡k=H⁡suc⁡k+A-B↔G⁡k+1=H⁡k+A−B+1
45 30 44 imbitrrid ⊢k∈ω→G⁡k=H⁡k+A-B→G⁡suc⁡k=H⁡suc⁡k+A-B
46 8 12 16 20 29 45 finds ⊢N∈ω→G⁡N=H⁡N+A-B