Metamath Proof Explorer

Theorem expscl

Description: Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Assertion expscl ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ No )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑚 = 0s → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 0s ) )
2 1 eleq1d ⊢ ( 𝑚 = 0s → ( ( 𝐴 ↑s 𝑚 ) ∈ No ↔ ( 𝐴 ↑s 0s ) ∈ No ) )
3 2 imbi2d ⊢ ( 𝑚 = 0s → ( ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑚 ) ∈ No ) ↔ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) ∈ No ) ) )
4 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑛 ) )
5 4 eleq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ↑s 𝑚 ) ∈ No ↔ ( 𝐴 ↑s 𝑛 ) ∈ No ) )
6 5 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑚 ) ∈ No ) ↔ ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑛 ) ∈ No ) ) )
7 oveq2 ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s ( 𝑛 +s 1s ) ) )
8 7 eleq1d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ↑s 𝑚 ) ∈ No ↔ ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ No ) )
9 8 imbi2d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑚 ) ∈ No ) ↔ ( 𝐴 ∈ No → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ No ) ) )
10 oveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑁 ) )
11 10 eleq1d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ↑s 𝑚 ) ∈ No ↔ ( 𝐴 ↑s 𝑁 ) ∈ No ) )
12 11 imbi2d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑚 ) ∈ No ) ↔ ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑁 ) ∈ No ) ) )
13 exps0 ⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
14 1sno ⊢ 1s ∈ No
15 13 14 eqeltrdi ⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) ∈ No )
16 simp2 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ No ∧ ( 𝐴 ↑s 𝑛 ) ∈ No ) → 𝐴 ∈ No )
17 simp1 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ No ∧ ( 𝐴 ↑s 𝑛 ) ∈ No ) → 𝑛 ∈ ℕ0s )
18 expsp1 ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
19 16 17 18 syl2anc ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ No ∧ ( 𝐴 ↑s 𝑛 ) ∈ No ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
20 simp3 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ No ∧ ( 𝐴 ↑s 𝑛 ) ∈ No ) → ( 𝐴 ↑s 𝑛 ) ∈ No )
21 20 16 mulscld ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ No ∧ ( 𝐴 ↑s 𝑛 ) ∈ No ) → ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) ∈ No )
22 19 21 eqeltrd ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ No ∧ ( 𝐴 ↑s 𝑛 ) ∈ No ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ No )
23 22 3exp ⊢ ( 𝑛 ∈ ℕ0s → ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑛 ) ∈ No → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ No ) ) )
24 23 a2d ⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑛 ) ∈ No ) → ( 𝐴 ∈ No → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ No ) ) )
25 3 6 9 12 15 24 n0sind ⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ No → ( 𝐴 ↑s 𝑁 ) ∈ No ) )
26 25 impcom ⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ No )