| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . 3
⊢ (𝑦 = ∅ → (𝐺‘𝑦) = (𝐺‘∅)) | 
| 2 |  | fveq2 6906 | . . . 4
⊢ (𝑦 = ∅ → (𝐻‘𝑦) = (𝐻‘∅)) | 
| 3 | 2 | oveq1d 7446 | . . 3
⊢ (𝑦 = ∅ → ((𝐻‘𝑦) + (𝐴 − 𝐵)) = ((𝐻‘∅) + (𝐴 − 𝐵))) | 
| 4 | 1, 3 | eqeq12d 2753 | . 2
⊢ (𝑦 = ∅ → ((𝐺‘𝑦) = ((𝐻‘𝑦) + (𝐴 − 𝐵)) ↔ (𝐺‘∅) = ((𝐻‘∅) + (𝐴 − 𝐵)))) | 
| 5 |  | fveq2 6906 | . . 3
⊢ (𝑦 = 𝑘 → (𝐺‘𝑦) = (𝐺‘𝑘)) | 
| 6 |  | fveq2 6906 | . . . 4
⊢ (𝑦 = 𝑘 → (𝐻‘𝑦) = (𝐻‘𝑘)) | 
| 7 | 6 | oveq1d 7446 | . . 3
⊢ (𝑦 = 𝑘 → ((𝐻‘𝑦) + (𝐴 − 𝐵)) = ((𝐻‘𝑘) + (𝐴 − 𝐵))) | 
| 8 | 5, 7 | eqeq12d 2753 | . 2
⊢ (𝑦 = 𝑘 → ((𝐺‘𝑦) = ((𝐻‘𝑦) + (𝐴 − 𝐵)) ↔ (𝐺‘𝑘) = ((𝐻‘𝑘) + (𝐴 − 𝐵)))) | 
| 9 |  | fveq2 6906 | . . 3
⊢ (𝑦 = suc 𝑘 → (𝐺‘𝑦) = (𝐺‘suc 𝑘)) | 
| 10 |  | fveq2 6906 | . . . 4
⊢ (𝑦 = suc 𝑘 → (𝐻‘𝑦) = (𝐻‘suc 𝑘)) | 
| 11 | 10 | oveq1d 7446 | . . 3
⊢ (𝑦 = suc 𝑘 → ((𝐻‘𝑦) + (𝐴 − 𝐵)) = ((𝐻‘suc 𝑘) + (𝐴 − 𝐵))) | 
| 12 | 9, 11 | eqeq12d 2753 | . 2
⊢ (𝑦 = suc 𝑘 → ((𝐺‘𝑦) = ((𝐻‘𝑦) + (𝐴 − 𝐵)) ↔ (𝐺‘suc 𝑘) = ((𝐻‘suc 𝑘) + (𝐴 − 𝐵)))) | 
| 13 |  | fveq2 6906 | . . 3
⊢ (𝑦 = 𝑁 → (𝐺‘𝑦) = (𝐺‘𝑁)) | 
| 14 |  | fveq2 6906 | . . . 4
⊢ (𝑦 = 𝑁 → (𝐻‘𝑦) = (𝐻‘𝑁)) | 
| 15 | 14 | oveq1d 7446 | . . 3
⊢ (𝑦 = 𝑁 → ((𝐻‘𝑦) + (𝐴 − 𝐵)) = ((𝐻‘𝑁) + (𝐴 − 𝐵))) | 
| 16 | 13, 15 | eqeq12d 2753 | . 2
⊢ (𝑦 = 𝑁 → ((𝐺‘𝑦) = ((𝐻‘𝑦) + (𝐴 − 𝐵)) ↔ (𝐺‘𝑁) = ((𝐻‘𝑁) + (𝐴 − 𝐵)))) | 
| 17 |  | uzrdgxfr.4 | . . . . 5
⊢ 𝐵 ∈ ℤ | 
| 18 |  | zcn 12618 | . . . . 5
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) | 
| 19 | 17, 18 | ax-mp 5 | . . . 4
⊢ 𝐵 ∈ ℂ | 
| 20 |  | uzrdgxfr.3 | . . . . 5
⊢ 𝐴 ∈ ℤ | 
| 21 |  | zcn 12618 | . . . . 5
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) | 
| 22 | 20, 21 | ax-mp 5 | . . . 4
⊢ 𝐴 ∈ ℂ | 
| 23 | 19, 22 | pncan3i 11586 | . . 3
⊢ (𝐵 + (𝐴 − 𝐵)) = 𝐴 | 
| 24 |  | uzrdgxfr.2 | . . . . 5
⊢ 𝐻 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐵) ↾ ω) | 
| 25 | 17, 24 | om2uz0i 13988 | . . . 4
⊢ (𝐻‘∅) = 𝐵 | 
| 26 | 25 | oveq1i 7441 | . . 3
⊢ ((𝐻‘∅) + (𝐴 − 𝐵)) = (𝐵 + (𝐴 − 𝐵)) | 
| 27 |  | uzrdgxfr.1 | . . . 4
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐴) ↾ ω) | 
| 28 | 20, 27 | om2uz0i 13988 | . . 3
⊢ (𝐺‘∅) = 𝐴 | 
| 29 | 23, 26, 28 | 3eqtr4ri 2776 | . 2
⊢ (𝐺‘∅) = ((𝐻‘∅) + (𝐴 − 𝐵)) | 
| 30 |  | oveq1 7438 | . . 3
⊢ ((𝐺‘𝑘) = ((𝐻‘𝑘) + (𝐴 − 𝐵)) → ((𝐺‘𝑘) + 1) = (((𝐻‘𝑘) + (𝐴 − 𝐵)) + 1)) | 
| 31 | 20, 27 | om2uzsuci 13989 | . . . 4
⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = ((𝐺‘𝑘) + 1)) | 
| 32 | 17, 24 | om2uzsuci 13989 | . . . . . 6
⊢ (𝑘 ∈ ω → (𝐻‘suc 𝑘) = ((𝐻‘𝑘) + 1)) | 
| 33 | 32 | oveq1d 7446 | . . . . 5
⊢ (𝑘 ∈ ω → ((𝐻‘suc 𝑘) + (𝐴 − 𝐵)) = (((𝐻‘𝑘) + 1) + (𝐴 − 𝐵))) | 
| 34 | 17, 24 | om2uzuzi 13990 | . . . . . . . 8
⊢ (𝑘 ∈ ω → (𝐻‘𝑘) ∈ (ℤ≥‘𝐵)) | 
| 35 |  | eluzelz 12888 | . . . . . . . 8
⊢ ((𝐻‘𝑘) ∈ (ℤ≥‘𝐵) → (𝐻‘𝑘) ∈ ℤ) | 
| 36 | 34, 35 | syl 17 | . . . . . . 7
⊢ (𝑘 ∈ ω → (𝐻‘𝑘) ∈ ℤ) | 
| 37 | 36 | zcnd 12723 | . . . . . 6
⊢ (𝑘 ∈ ω → (𝐻‘𝑘) ∈ ℂ) | 
| 38 |  | ax-1cn 11213 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 39 | 22, 19 | subcli 11585 | . . . . . . 7
⊢ (𝐴 − 𝐵) ∈ ℂ | 
| 40 |  | add32 11480 | . . . . . . 7
⊢ (((𝐻‘𝑘) ∈ ℂ ∧ 1 ∈ ℂ ∧
(𝐴 − 𝐵) ∈ ℂ) →
(((𝐻‘𝑘) + 1) + (𝐴 − 𝐵)) = (((𝐻‘𝑘) + (𝐴 − 𝐵)) + 1)) | 
| 41 | 38, 39, 40 | mp3an23 1455 | . . . . . 6
⊢ ((𝐻‘𝑘) ∈ ℂ → (((𝐻‘𝑘) + 1) + (𝐴 − 𝐵)) = (((𝐻‘𝑘) + (𝐴 − 𝐵)) + 1)) | 
| 42 | 37, 41 | syl 17 | . . . . 5
⊢ (𝑘 ∈ ω → (((𝐻‘𝑘) + 1) + (𝐴 − 𝐵)) = (((𝐻‘𝑘) + (𝐴 − 𝐵)) + 1)) | 
| 43 | 33, 42 | eqtrd 2777 | . . . 4
⊢ (𝑘 ∈ ω → ((𝐻‘suc 𝑘) + (𝐴 − 𝐵)) = (((𝐻‘𝑘) + (𝐴 − 𝐵)) + 1)) | 
| 44 | 31, 43 | eqeq12d 2753 | . . 3
⊢ (𝑘 ∈ ω → ((𝐺‘suc 𝑘) = ((𝐻‘suc 𝑘) + (𝐴 − 𝐵)) ↔ ((𝐺‘𝑘) + 1) = (((𝐻‘𝑘) + (𝐴 − 𝐵)) + 1))) | 
| 45 | 30, 44 | imbitrrid 246 | . 2
⊢ (𝑘 ∈ ω → ((𝐺‘𝑘) = ((𝐻‘𝑘) + (𝐴 − 𝐵)) → (𝐺‘suc 𝑘) = ((𝐻‘suc 𝑘) + (𝐴 − 𝐵)))) | 
| 46 | 4, 8, 12, 16, 29, 45 | finds 7918 | 1
⊢ (𝑁 ∈ ω → (𝐺‘𝑁) = ((𝐻‘𝑁) + (𝐴 − 𝐵))) |