Theorem expsne0

Description: A non-negative surreal integer power is nonzero if its base is nonzero. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	expsne0	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ≠ 0s )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑚 = 0s → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 0s ) )
2	1	eqeq1d	⊢ ( 𝑚 = 0s → ( ( 𝐴 ↑s 𝑚 ) = 0s ↔ ( 𝐴 ↑s 0s ) = 0s ) )
3	2	imbi1d	⊢ ( 𝑚 = 0s → ( ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ↔ ( ( 𝐴 ↑s 0s ) = 0s → 𝐴 = 0s ) ) )
4	3	imbi2d	⊢ ( 𝑚 = 0s → ( ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ) ↔ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 0s ) = 0s → 𝐴 = 0s ) ) ) )
5		oveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑛 ) )
6	5	eqeq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ↑s 𝑚 ) = 0s ↔ ( 𝐴 ↑s 𝑛 ) = 0s ) )
7	6	imbi1d	⊢ ( 𝑚 = 𝑛 → ( ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) )
8	7	imbi2d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ) ↔ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) ) )
9		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s ( 𝑛 +s 1s ) ) )
10	9	eqeq1d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ↑s 𝑚 ) = 0s ↔ ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ) )
11	10	imbi1d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ↔ ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) )
12	11	imbi2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ) ↔ ( 𝐴 ∈ No → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) ) )
13		oveq2	⊢ ( 𝑚 = 𝑁 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑁 ) )
14	13	eqeq1d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ↑s 𝑚 ) = 0s ↔ ( 𝐴 ↑s 𝑁 ) = 0s ) )
15	14	imbi1d	⊢ ( 𝑚 = 𝑁 → ( ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ↔ ( ( 𝐴 ↑s 𝑁 ) = 0s → 𝐴 = 0s ) ) )
16	15	imbi2d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑚 ) = 0s → 𝐴 = 0s ) ) ↔ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑁 ) = 0s → 𝐴 = 0s ) ) ) )
17		1ne0s	⊢ 1s ≠ 0s
18		exps0	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
19	18	neeq1d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 0s ) ≠ 0s ↔ 1s ≠ 0s ) )
20	17 19	mpbiri	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) ≠ 0s )
21	20	neneqd	⊢ ( 𝐴 ∈ No → ¬ ( 𝐴 ↑s 0s ) = 0s )
22	21	pm2.21d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 0s ) = 0s → 𝐴 = 0s ) )
23		expsp1	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
24	23	eqeq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) = 0s ) )
25		expscl	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑛 ) ∈ No )
26		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → 𝐴 ∈ No )
27	25 26	muls0ord	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) ) )
28	24 27	bitrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) ) )
29	28	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) ) )
30		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) )
31		idd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( 𝐴 = 0s → 𝐴 = 0s ) )
32	30 31	jaod	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) → 𝐴 = 0s ) )
33	29 32	sylbid	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) )
34	33	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) )
35	34	expcom	⊢ ( 𝑛 ∈ ℕ0s → ( 𝐴 ∈ No → ( ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) ) )
36	35	a2d	⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( 𝐴 ∈ No → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) ) )
37	4 8 12 16 22 36	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑁 ) = 0s → 𝐴 = 0s ) ) )
38	37	imp	⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝐴 ∈ No ) → ( ( 𝐴 ↑s 𝑁 ) = 0s → 𝐴 = 0s ) )
39	38	necon3d	⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝐴 ∈ No ) → ( 𝐴 ≠ 0s → ( 𝐴 ↑s 𝑁 ) ≠ 0s ) )
40	39	ex	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ No → ( 𝐴 ≠ 0s → ( 𝐴 ↑s 𝑁 ) ≠ 0s ) ) )
41	40	3imp231	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ≠ 0s )