Step |
Hyp |
Ref |
Expression |
1 |
|
eluzge2nn0 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 ) |
2 |
1
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℕ0 ) |
3 |
|
simpr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 ) |
4 |
|
eluz2b3 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) ) |
5 |
4
|
simprbi |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≠ 1 ) |
6 |
5
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ≠ 1 ) |
7 |
6
|
neneqd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ¬ 𝑁 = 1 ) |
8 |
7
|
pm2.21d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 = 1 → Rel 𝑅 ) ) |
9 |
|
relexprelg |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( 𝑁 = 1 → Rel 𝑅 ) ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) |
10 |
2 3 8 9
|
syl3anc |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) ) |