Metamath Proof Explorer


Theorem relexpmulnn

Description: With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion relexpmulnn ( ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 𝐼 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = 1 → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅𝑟 𝐽 ) ↑𝑟 1 ) )
2 oveq2 ( 𝑥 = 1 → ( 𝐽 · 𝑥 ) = ( 𝐽 · 1 ) )
3 2 oveq2d ( 𝑥 = 1 → ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅𝑟 ( 𝐽 · 1 ) ) )
4 1 3 eqeq12d ( 𝑥 = 1 → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅𝑟 ( 𝐽 · 1 ) ) ) )
5 4 imbi2d ( 𝑥 = 1 → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅𝑟 ( 𝐽 · 1 ) ) ) ) )
6 oveq2 ( 𝑥 = 𝑦 → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) )
7 oveq2 ( 𝑥 = 𝑦 → ( 𝐽 · 𝑥 ) = ( 𝐽 · 𝑦 ) )
8 7 oveq2d ( 𝑥 = 𝑦 → ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) )
9 6 8 eqeq12d ( 𝑥 = 𝑦 → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) )
10 9 imbi2d ( 𝑥 = 𝑦 → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) ) )
11 oveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) )
12 oveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐽 · 𝑥 ) = ( 𝐽 · ( 𝑦 + 1 ) ) )
13 12 oveq2d ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
14 11 13 eqeq12d ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) )
15 14 imbi2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) ) )
16 oveq2 ( 𝑥 = 𝐾 → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) )
17 oveq2 ( 𝑥 = 𝐾 → ( 𝐽 · 𝑥 ) = ( 𝐽 · 𝐾 ) )
18 17 oveq2d ( 𝑥 = 𝐾 → ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) )
19 16 18 eqeq12d ( 𝑥 = 𝐾 → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ↔ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) ) )
20 19 imbi2d ( 𝑥 = 𝐾 → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑥 ) = ( 𝑅𝑟 ( 𝐽 · 𝑥 ) ) ) ↔ ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) ) ) )
21 ovexd ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( 𝑅𝑟 𝐽 ) ∈ V )
22 21 relexp1d ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅𝑟 𝐽 ) )
23 simp1 ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → 𝐽 ∈ ℕ )
24 nnre ( 𝐽 ∈ ℕ → 𝐽 ∈ ℝ )
25 ax-1rid ( 𝐽 ∈ ℝ → ( 𝐽 · 1 ) = 𝐽 )
26 23 24 25 3syl ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( 𝐽 · 1 ) = 𝐽 )
27 26 eqcomd ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → 𝐽 = ( 𝐽 · 1 ) )
28 27 oveq2d ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( 𝑅𝑟 𝐽 ) = ( 𝑅𝑟 ( 𝐽 · 1 ) ) )
29 22 28 eqtrd ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 1 ) = ( 𝑅𝑟 ( 𝐽 · 1 ) ) )
30 ovex ( 𝑅𝑟 𝐽 ) ∈ V
31 simp1 ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝑦 ∈ ℕ )
32 relexpsucnnr ( ( ( 𝑅𝑟 𝐽 ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅𝑟 𝐽 ) ) )
33 30 31 32 sylancr ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅𝑟 𝐽 ) ) )
34 simp3 ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) )
35 34 coeq1d ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅𝑟 𝐽 ) ) = ( ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ∘ ( 𝑅𝑟 𝐽 ) ) )
36 simp21 ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝐽 ∈ ℕ )
37 36 31 nnmulcld ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝐽 · 𝑦 ) ∈ ℕ )
38 simp22 ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝑅𝑉 )
39 relexpaddnn ( ( ( 𝐽 · 𝑦 ) ∈ ℕ ∧ 𝐽 ∈ ℕ ∧ 𝑅𝑉 ) → ( ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ∘ ( 𝑅𝑟 𝐽 ) ) = ( 𝑅𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) )
40 37 36 38 39 syl3anc ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ∘ ( 𝑅𝑟 𝐽 ) ) = ( 𝑅𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) )
41 35 40 eqtrd ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅𝑟 𝐽 ) ) = ( 𝑅𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) )
42 36 nncnd ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝐽 ∈ ℂ )
43 31 nncnd ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
44 1cnd ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → 1 ∈ ℂ )
45 42 43 44 adddid ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝐽 · ( 𝑦 + 1 ) ) = ( ( 𝐽 · 𝑦 ) + ( 𝐽 · 1 ) ) )
46 42 mulid1d ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝐽 · 1 ) = 𝐽 )
47 46 oveq2d ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝐽 · 𝑦 ) + ( 𝐽 · 1 ) ) = ( ( 𝐽 · 𝑦 ) + 𝐽 ) )
48 45 47 eqtr2d ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝐽 · 𝑦 ) + 𝐽 ) = ( 𝐽 · ( 𝑦 + 1 ) ) )
49 48 oveq2d ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( 𝑅𝑟 ( ( 𝐽 · 𝑦 ) + 𝐽 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
50 41 49 eqtrd ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) ∘ ( 𝑅𝑟 𝐽 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
51 33 50 eqtrd ( ( 𝑦 ∈ ℕ ∧ ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) )
52 51 3exp ( 𝑦 ∈ ℕ → ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) ) )
53 52 a2d ( 𝑦 ∈ ℕ → ( ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝑦 ) = ( 𝑅𝑟 ( 𝐽 · 𝑦 ) ) ) → ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅𝑟 ( 𝐽 · ( 𝑦 + 1 ) ) ) ) ) )
54 5 10 15 20 29 53 nnind ( 𝐾 ∈ ℕ → ( ( 𝐽 ∈ ℕ ∧ 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) ) )
55 54 3expd ( 𝐾 ∈ ℕ → ( 𝐽 ∈ ℕ → ( 𝑅𝑉 → ( 𝐼 = ( 𝐽 · 𝐾 ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) ) ) ) )
56 55 impcom ( ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑅𝑉 → ( 𝐼 = ( 𝐽 · 𝐾 ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) ) ) )
57 56 impd ( ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) ) )
58 57 impcom ( ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) )
59 simplr ( ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → 𝐼 = ( 𝐽 · 𝐾 ) )
60 59 eqcomd ( ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( 𝐽 · 𝐾 ) = 𝐼 )
61 60 oveq2d ( ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( 𝑅𝑟 ( 𝐽 · 𝐾 ) ) = ( 𝑅𝑟 𝐼 ) )
62 58 61 eqtrd ( ( ( 𝑅𝑉𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅𝑟 𝐼 ) )