Step |
Hyp |
Ref |
Expression |
1 |
|
frmy |
⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ |
2 |
1
|
fovcl |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ ) |
3 |
2
|
zred |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℝ ) |
4 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) |
5 |
|
elnn0z |
⊢ ( 𝑎 ∈ ℕ0 ↔ ( 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) ) |
6 |
5
|
biimpri |
⊢ ( ( 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 𝑎 ∈ ℕ0 ) |
7 |
6
|
3adant1 |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 𝑎 ∈ ℕ0 ) |
8 |
|
rmxypos |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ) |
9 |
4 7 8
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ) |
10 |
9
|
simprd |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ∧ 0 ≤ 𝑎 ) → 0 ≤ ( 𝐴 Yrm 𝑎 ) ) |
11 |
|
rmyneg |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm - 𝑏 ) = - ( 𝐴 Yrm 𝑏 ) ) |
12 |
|
oveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) ) |
13 |
|
oveq2 |
⊢ ( 𝑎 = - 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm - 𝑏 ) ) |
14 |
|
oveq2 |
⊢ ( 𝑎 = 𝐵 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝐵 ) ) |
15 |
|
oveq2 |
⊢ ( 𝑎 = ( abs ‘ 𝐵 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( abs ‘ 𝐵 ) ) ) |
16 |
3 10 11 12 13 14 15
|
oddcomabszz |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( abs ‘ ( 𝐴 Yrm 𝐵 ) ) = ( 𝐴 Yrm ( abs ‘ 𝐵 ) ) ) |