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 |
⊢ ( 𝑁 ∈ ω → ( 𝐺 ‘ 𝑁 ) = ( ( 𝐻 ‘ 𝑁 ) + ( 𝐴 − 𝐵 ) ) ) |