Step |
Hyp |
Ref |
Expression |
1 |
|
rmbaserp |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℝ+ ) |
2 |
1
|
rpcnne0d |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℂ ∧ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≠ 0 ) ) |
3 |
|
expmulz |
⊢ ( ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℂ ∧ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑁 · 𝐽 ) ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ↑ 𝐽 ) ) |
4 |
2 3
|
sylan |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑁 · 𝐽 ) ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ↑ 𝐽 ) ) |
5 |
|
zmulcl |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝑁 · 𝐽 ) ∈ ℤ ) |
6 |
|
rmxyval |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 · 𝐽 ) ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑁 · 𝐽 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑁 · 𝐽 ) ) ) |
7 |
5 6
|
sylan2 |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( 𝐴 Xrm ( 𝑁 · 𝐽 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑁 · 𝐽 ) ) ) |
8 |
|
rmxyval |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) |
9 |
8
|
adantrr |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) |
10 |
9
|
oveq1d |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ↑ 𝐽 ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ↑ 𝐽 ) ) |
11 |
4 7 10
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( 𝐴 Xrm ( 𝑁 · 𝐽 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ↑ 𝐽 ) ) |
12 |
11
|
3impb |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑁 · 𝐽 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ↑ 𝐽 ) ) |