Metamath Proof Explorer

Theorem expadds

Description: Sum of exponents law for surreals. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion expadds ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑗 = 0s → ( 𝑀 +s 𝑗 ) = ( 𝑀 +s 0s ) )
2 1 oveq2d ⊢ ( 𝑗 = 0s → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( 𝐴 ↑s ( 𝑀 +s 0s ) ) )
3 oveq2 ⊢ ( 𝑗 = 0s → ( 𝐴 ↑s 𝑗 ) = ( 𝐴 ↑s 0s ) )
4 3 oveq2d ⊢ ( 𝑗 = 0s → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 0s ) ) )
5 2 4 eqeq12d ⊢ ( 𝑗 = 0s → ( ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ↔ ( 𝐴 ↑s ( 𝑀 +s 0s ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 0s ) ) ) )
6 5 imbi2d ⊢ ( 𝑗 = 0s → ( ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 0s ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 0s ) ) ) ) )
7 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑀 +s 𝑗 ) = ( 𝑀 +s 𝑘 ) )
8 7 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) )
9 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑s 𝑗 ) = ( 𝐴 ↑s 𝑘 ) )
10 9 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) )
11 8 10 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ↔ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) )
12 11 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) )
13 oveq2 ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( 𝑀 +s 𝑗 ) = ( 𝑀 +s ( 𝑘 +s 1s ) ) )
14 13 oveq2d ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) )
15 oveq2 ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( 𝐴 ↑s 𝑗 ) = ( 𝐴 ↑s ( 𝑘 +s 1s ) ) )
16 15 oveq2d ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) )
17 14 16 eqeq12d ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ↔ ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) ) )
18 17 imbi2d ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) ) ) )
19 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝑀 +s 𝑗 ) = ( 𝑀 +s 𝑁 ) )
20 19 oveq2d ⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) )
21 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑s 𝑗 ) = ( 𝐴 ↑s 𝑁 ) )
22 21 oveq2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) )
23 20 22 eqeq12d ⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ↔ ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) ) )
24 23 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑗 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) ) ) )
25 expscl ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑀 ) ∈ No )
26 25 mulsridd ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( ( 𝐴 ↑s 𝑀 ) ·s 1s ) = ( 𝐴 ↑s 𝑀 ) )
27 exps0 ⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
28 27 oveq2d ⊢ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 0s ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s 1s ) )
29 28 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 0s ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s 1s ) )
30 n0sno ⊢ ( 𝑀 ∈ ℕ0s → 𝑀 ∈ No )
31 30 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → 𝑀 ∈ No )
32 31 addsridd ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝑀 +s 0s ) = 𝑀 )
33 32 oveq2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 0s ) ) = ( 𝐴 ↑s 𝑀 ) )
34 26 29 33 3eqtr4rd ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 0s ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 0s ) ) )
35 simprr ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) )
36 35 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) ·s 𝐴 ) = ( ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ·s 𝐴 ) )
37 25 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) → ( 𝐴 ↑s 𝑀 ) ∈ No )
38 37 adantl ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s 𝑀 ) ∈ No )
39 simprll ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → 𝐴 ∈ No )
40 simpl ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → 𝑘 ∈ ℕ0s )
41 expscl ⊢ ( ( 𝐴 ∈ No ∧ 𝑘 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑘 ) ∈ No )
42 39 40 41 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s 𝑘 ) ∈ No )
43 38 42 39 mulsassd ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ·s 𝐴 ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( ( 𝐴 ↑s 𝑘 ) ·s 𝐴 ) ) )
44 36 43 eqtrd ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) ·s 𝐴 ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( ( 𝐴 ↑s 𝑘 ) ·s 𝐴 ) ) )
45 simprlr ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → 𝑀 ∈ ℕ0s )
46 45 n0snod ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → 𝑀 ∈ No )
47 40 n0snod ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → 𝑘 ∈ No )
48 1sno ⊢ 1s ∈ No
49 48 a1i ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → 1s ∈ No )
50 46 47 49 addsassd ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( ( 𝑀 +s 𝑘 ) +s 1s ) = ( 𝑀 +s ( 𝑘 +s 1s ) ) )
51 50 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s ( ( 𝑀 +s 𝑘 ) +s 1s ) ) = ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) )
52 n0addscl ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑘 ∈ ℕ0s ) → ( 𝑀 +s 𝑘 ) ∈ ℕ0s )
53 45 40 52 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝑀 +s 𝑘 ) ∈ ℕ0s )
54 expsp1 ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑀 +s 𝑘 ) ∈ ℕ0s ) → ( 𝐴 ↑s ( ( 𝑀 +s 𝑘 ) +s 1s ) ) = ( ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) ·s 𝐴 ) )
55 39 53 54 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s ( ( 𝑀 +s 𝑘 ) +s 1s ) ) = ( ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) ·s 𝐴 ) )
56 51 55 eqtr3d ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) ·s 𝐴 ) )
57 expsp1 ⊢ ( ( 𝐴 ∈ No ∧ 𝑘 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑘 +s 1s ) ) = ( ( 𝐴 ↑s 𝑘 ) ·s 𝐴 ) )
58 39 40 57 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s ( 𝑘 +s 1s ) ) = ( ( 𝐴 ↑s 𝑘 ) ·s 𝐴 ) )
59 58 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( ( 𝐴 ↑s 𝑘 ) ·s 𝐴 ) ) )
60 44 56 59 3eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0s ∧ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) ∧ ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) ) → ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) )
61 60 exp32 ⊢ ( 𝑘 ∈ ℕ0s → ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) → ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) ) ) )
62 61 a2d ⊢ ( 𝑘 ∈ ℕ0s → ( ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑘 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑘 ) ) ) → ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s ( 𝑘 +s 1s ) ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s ( 𝑘 +s 1s ) ) ) ) ) )
63 6 12 18 24 34 62 n0sind ⊢ ( 𝑁 ∈ ℕ0s → ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) ) )
64 63 com12 ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 𝑁 ∈ ℕ0s → ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) ) )
65 64 3impia ⊢ ( ( 𝐴 ∈ No ∧ 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑀 +s 𝑁 ) ) = ( ( 𝐴 ↑s 𝑀 ) ·s ( 𝐴 ↑s 𝑁 ) ) )