Theorem expsne0

Description: A non-negative surreal integer power is non-zero if its base is non-zero. (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		0slt1s	⊢ 0s <s 1s
18		sgt0ne0	⊢ ( 0s <s 1s → 1s ≠ 0s )
19	17 18	ax-mp	⊢ 1s ≠ 0s
20		exps0	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
21	20	neeq1d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 0s ) ≠ 0s ↔ 1s ≠ 0s ) )
22	19 21	mpbiri	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) ≠ 0s )
23	22	neneqd	⊢ ( 𝐴 ∈ No → ¬ ( 𝐴 ↑s 0s ) = 0s )
24	23	pm2.21d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ↑s 0s ) = 0s → 𝐴 = 0s ) )
25		expsp1	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
26	25	eqeq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) = 0s ) )
27		expscl	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑛 ) ∈ No )
28		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → 𝐴 ∈ No )
29	27 28	muls0ord	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) ) )
30	26 29	bitrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) ) )
31	30	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s ↔ ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) ) )
32		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) )
33		idd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( 𝐴 = 0s → 𝐴 = 0s ) )
34	32 33	jaod	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( ( 𝐴 ↑s 𝑛 ) = 0s ∨ 𝐴 = 0s ) → 𝐴 = 0s ) )
35	31 34	sylbid	⊢ ( ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) ∧ ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) )
36	35	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) )
37	36	expcom	⊢ ( 𝑛 ∈ ℕ0s → ( 𝐴 ∈ No → ( ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) ) )
38	37	a2d	⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑛 ) = 0s → 𝐴 = 0s ) ) → ( 𝐴 ∈ No → ( ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = 0s → 𝐴 = 0s ) ) ) )
39	4 8 12 16 24 38	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ No → ( ( 𝐴 ↑s 𝑁 ) = 0s → 𝐴 = 0s ) ) )
40	39	imp	⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝐴 ∈ No ) → ( ( 𝐴 ↑s 𝑁 ) = 0s → 𝐴 = 0s ) )
41	40	necon3d	⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝐴 ∈ No ) → ( 𝐴 ≠ 0s → ( 𝐴 ↑s 𝑁 ) ≠ 0s ) )
42	41	ex	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ No → ( 𝐴 ≠ 0s → ( 𝐴 ↑s 𝑁 ) ≠ 0s ) ) )
43	42	3imp231	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ≠ 0s )