This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid ⊢ ( 𝑘 ∈ ω → ( ( 𝐺 ‘ 𝑘 ) = ( ( 𝐻 ‘ 𝑘 ) + ( 𝐴 − 𝐵 ) ) → ( 𝐺 ‘ suc 𝑘 ) = ( ( 𝐻 ‘ suc 𝑘 ) + ( 𝐴 − 𝐵 ) ) ) )
46 8 12 16 20 29 45 finds ⊢ ( 𝑁 ∈ ω → ( 𝐺 ‘ 𝑁 ) = ( ( 𝐻 ‘ 𝑁 ) + ( 𝐴 − 𝐵 ) ) )