Step |
Hyp |
Ref |
Expression |
1 |
|
1z |
⊢ 1 ∈ ℤ |
2 |
|
rmxadd |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) ) ) |
3 |
1 2
|
mp3an3 |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) ) ) |
4 |
|
rmx1 |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 1 ) = 𝐴 ) |
6 |
5
|
oveq2d |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) = ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) ) |
7 |
|
rmy1 |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 ) |
8 |
7
|
oveq2d |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 1 ) ) |
9 |
8
|
adantr |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( ( 𝐴 Yrm 𝑁 ) · 1 ) ) |
10 |
|
frmy |
⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ |
11 |
10
|
fovcl |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ ) |
12 |
11
|
zcnd |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ ) |
13 |
12
|
mulid1d |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · 1 ) = ( 𝐴 Yrm 𝑁 ) ) |
14 |
9 13
|
eqtrd |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) = ( 𝐴 Yrm 𝑁 ) ) |
15 |
14
|
oveq2d |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) |
16 |
6 15
|
oveq12d |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Xrm 1 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 1 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) |
17 |
3 16
|
eqtrd |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) |