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 + 1 A ↾ ω
uzrdgxfr.2 ⊢ H = rec ⁡ x ∈ V ⟼ x + 1 B ↾ ω
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 + 1 A ↾ ω
2 uzrdgxfr.2 ⊢ H = rec ⁡ x ∈ V ⟼ x + 1 B ↾ ω
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