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 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐴 ) ↾ ω )
uzrdgxfr.2 𝐻 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐵 ) ↾ ω )
uzrdgxfr.3 𝐴 ∈ ℤ
uzrdgxfr.4 𝐵 ∈ ℤ
Assertion uzrdgxfr ( 𝑁 ∈ ω → ( 𝐺𝑁 ) = ( ( 𝐻𝑁 ) + ( 𝐴𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 uzrdgxfr.1 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐴 ) ↾ ω )
2 uzrdgxfr.2 𝐻 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐵 ) ↾ ω )
3 uzrdgxfr.3 𝐴 ∈ ℤ
4 uzrdgxfr.4 𝐵 ∈ ℤ
5 fveq2 ( 𝑦 = ∅ → ( 𝐺𝑦 ) = ( 𝐺 ‘ ∅ ) )
6 fveq2 ( 𝑦 = ∅ → ( 𝐻𝑦 ) = ( 𝐻 ‘ ∅ ) )
7 6 oveq1d ( 𝑦 = ∅ → ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) = ( ( 𝐻 ‘ ∅ ) + ( 𝐴𝐵 ) ) )
8 5 7 eqeq12d ( 𝑦 = ∅ → ( ( 𝐺𝑦 ) = ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) ↔ ( 𝐺 ‘ ∅ ) = ( ( 𝐻 ‘ ∅ ) + ( 𝐴𝐵 ) ) ) )
9 fveq2 ( 𝑦 = 𝑘 → ( 𝐺𝑦 ) = ( 𝐺𝑘 ) )
10 fveq2 ( 𝑦 = 𝑘 → ( 𝐻𝑦 ) = ( 𝐻𝑘 ) )
11 10 oveq1d ( 𝑦 = 𝑘 → ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) = ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) )
12 9 11 eqeq12d ( 𝑦 = 𝑘 → ( ( 𝐺𝑦 ) = ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) ↔ ( 𝐺𝑘 ) = ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) ) )
13 fveq2 ( 𝑦 = suc 𝑘 → ( 𝐺𝑦 ) = ( 𝐺 ‘ suc 𝑘 ) )
14 fveq2 ( 𝑦 = suc 𝑘 → ( 𝐻𝑦 ) = ( 𝐻 ‘ suc 𝑘 ) )
15 14 oveq1d ( 𝑦 = suc 𝑘 → ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) = ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴𝐵 ) ) )
16 13 15 eqeq12d ( 𝑦 = suc 𝑘 → ( ( 𝐺𝑦 ) = ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) ↔ ( 𝐺 ‘ suc 𝑘 ) = ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴𝐵 ) ) ) )
17 fveq2 ( 𝑦 = 𝑁 → ( 𝐺𝑦 ) = ( 𝐺𝑁 ) )
18 fveq2 ( 𝑦 = 𝑁 → ( 𝐻𝑦 ) = ( 𝐻𝑁 ) )
19 18 oveq1d ( 𝑦 = 𝑁 → ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) = ( ( 𝐻𝑁 ) + ( 𝐴𝐵 ) ) )
20 17 19 eqeq12d ( 𝑦 = 𝑁 → ( ( 𝐺𝑦 ) = ( ( 𝐻𝑦 ) + ( 𝐴𝐵 ) ) ↔ ( 𝐺𝑁 ) = ( ( 𝐻𝑁 ) + ( 𝐴𝐵 ) ) ) )
21 zcn ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
22 4 21 ax-mp 𝐵 ∈ ℂ
23 zcn ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
24 3 23 ax-mp 𝐴 ∈ ℂ
25 22 24 pncan3i ( 𝐵 + ( 𝐴𝐵 ) ) = 𝐴
26 4 2 om2uz0i ( 𝐻 ‘ ∅ ) = 𝐵
27 26 oveq1i ( ( 𝐻 ‘ ∅ ) + ( 𝐴𝐵 ) ) = ( 𝐵 + ( 𝐴𝐵 ) )
28 3 1 om2uz0i ( 𝐺 ‘ ∅ ) = 𝐴
29 25 27 28 3eqtr4ri ( 𝐺 ‘ ∅ ) = ( ( 𝐻 ‘ ∅ ) + ( 𝐴𝐵 ) )
30 oveq1 ( ( 𝐺𝑘 ) = ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) → ( ( 𝐺𝑘 ) + 1 ) = ( ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) + 1 ) )
31 3 1 om2uzsuci ( 𝑘 ∈ ω → ( 𝐺 ‘ suc 𝑘 ) = ( ( 𝐺𝑘 ) + 1 ) )
32 4 2 om2uzsuci ( 𝑘 ∈ ω → ( 𝐻 ‘ suc 𝑘 ) = ( ( 𝐻𝑘 ) + 1 ) )
33 32 oveq1d ( 𝑘 ∈ ω → ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴𝐵 ) ) = ( ( ( 𝐻𝑘 ) + 1 ) + ( 𝐴𝐵 ) ) )
34 4 2 om2uzuzi ( 𝑘 ∈ ω → ( 𝐻𝑘 ) ∈ ( ℤ𝐵 ) )
35 eluzelz ( ( 𝐻𝑘 ) ∈ ( ℤ𝐵 ) → ( 𝐻𝑘 ) ∈ ℤ )
36 34 35 syl ( 𝑘 ∈ ω → ( 𝐻𝑘 ) ∈ ℤ )
37 36 zcnd ( 𝑘 ∈ ω → ( 𝐻𝑘 ) ∈ ℂ )
38 ax-1cn 1 ∈ ℂ
39 24 22 subcli ( 𝐴𝐵 ) ∈ ℂ
40 add32 ( ( ( 𝐻𝑘 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴𝐵 ) ∈ ℂ ) → ( ( ( 𝐻𝑘 ) + 1 ) + ( 𝐴𝐵 ) ) = ( ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) + 1 ) )
41 38 39 40 mp3an23 ( ( 𝐻𝑘 ) ∈ ℂ → ( ( ( 𝐻𝑘 ) + 1 ) + ( 𝐴𝐵 ) ) = ( ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) + 1 ) )
42 37 41 syl ( 𝑘 ∈ ω → ( ( ( 𝐻𝑘 ) + 1 ) + ( 𝐴𝐵 ) ) = ( ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) + 1 ) )
43 33 42 eqtrd ( 𝑘 ∈ ω → ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴𝐵 ) ) = ( ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) + 1 ) )
44 31 43 eqeq12d ( 𝑘 ∈ ω → ( ( 𝐺 ‘ suc 𝑘 ) = ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴𝐵 ) ) ↔ ( ( 𝐺𝑘 ) + 1 ) = ( ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) + 1 ) ) )
45 30 44 syl5ibr ( 𝑘 ∈ ω → ( ( 𝐺𝑘 ) = ( ( 𝐻𝑘 ) + ( 𝐴𝐵 ) ) → ( 𝐺 ‘ suc 𝑘 ) = ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴𝐵 ) ) ) )
46 8 12 16 20 29 45 finds ( 𝑁 ∈ ω → ( 𝐺𝑁 ) = ( ( 𝐻𝑁 ) + ( 𝐴𝐵 ) ) )