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	Could not format assertion : No typesetting found for |- ( ( A e. No /\ A =/= 0s /\ N e. NN0_s ) -> ( A ^su N ) =/= 0s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	Could not format ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) ) : No typesetting found for |- ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) ) with typecode |-
2	1	eqeq1d	Could not format ( m = 0s -> ( ( A ^su m ) = 0s <-> ( A ^su 0s ) = 0s ) ) : No typesetting found for |- ( m = 0s -> ( ( A ^su m ) = 0s <-> ( A ^su 0s ) = 0s ) ) with typecode |-
3	2	imbi1d	Could not format ( m = 0s -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su 0s ) = 0s -> A = 0s ) ) ) : No typesetting found for |- ( m = 0s -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su 0s ) = 0s -> A = 0s ) ) ) with typecode |-
4	3	imbi2d	Could not format ( m = 0s -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su 0s ) = 0s -> A = 0s ) ) ) ) : No typesetting found for |- ( m = 0s -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su 0s ) = 0s -> A = 0s ) ) ) ) with typecode |-
5		oveq2	Could not format ( m = n -> ( A ^su m ) = ( A ^su n ) ) : No typesetting found for |- ( m = n -> ( A ^su m ) = ( A ^su n ) ) with typecode |-
6	5	eqeq1d	Could not format ( m = n -> ( ( A ^su m ) = 0s <-> ( A ^su n ) = 0s ) ) : No typesetting found for |- ( m = n -> ( ( A ^su m ) = 0s <-> ( A ^su n ) = 0s ) ) with typecode |-
7	6	imbi1d	Could not format ( m = n -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su n ) = 0s -> A = 0s ) ) ) : No typesetting found for |- ( m = n -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su n ) = 0s -> A = 0s ) ) ) with typecode |-
8	7	imbi2d	Could not format ( m = n -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su n ) = 0s -> A = 0s ) ) ) ) : No typesetting found for |- ( m = n -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su n ) = 0s -> A = 0s ) ) ) ) with typecode |-
9		oveq2	Could not format ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) ) with typecode |-
10	9	eqeq1d	Could not format ( m = ( n +s 1s ) -> ( ( A ^su m ) = 0s <-> ( A ^su ( n +s 1s ) ) = 0s ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A ^su m ) = 0s <-> ( A ^su ( n +s 1s ) ) = 0s ) ) with typecode |-
11	10	imbi1d	Could not format ( m = ( n +s 1s ) -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) with typecode |-
12	11	imbi2d	Could not format ( m = ( n +s 1s ) -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) ) with typecode |-
13		oveq2	Could not format ( m = N -> ( A ^su m ) = ( A ^su N ) ) : No typesetting found for |- ( m = N -> ( A ^su m ) = ( A ^su N ) ) with typecode |-
14	13	eqeq1d	Could not format ( m = N -> ( ( A ^su m ) = 0s <-> ( A ^su N ) = 0s ) ) : No typesetting found for |- ( m = N -> ( ( A ^su m ) = 0s <-> ( A ^su N ) = 0s ) ) with typecode |-
15	14	imbi1d	Could not format ( m = N -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su N ) = 0s -> A = 0s ) ) ) : No typesetting found for |- ( m = N -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su N ) = 0s -> A = 0s ) ) ) with typecode |-
16	15	imbi2d	Could not format ( m = N -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su N ) = 0s -> A = 0s ) ) ) ) : No typesetting found for |- ( m = N -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su N ) = 0s -> A = 0s ) ) ) ) with typecode |-
17		0slt1s	$$⊢0_s{<}_s{1}_s$$
18		sgt0ne0	$$⊢0_s{<}_s{1}_s\to 1_s\ne 0_s$$
19	17 18	ax-mp	$$⊢1_s\ne 0_s$$
20		exps0	Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-
21	20	neeq1d	Could not format ( A e. No -> ( ( A ^su 0s ) =/= 0s <-> 1s =/= 0s ) ) : No typesetting found for |- ( A e. No -> ( ( A ^su 0s ) =/= 0s <-> 1s =/= 0s ) ) with typecode |-
22	19 21	mpbiri	Could not format ( A e. No -> ( A ^su 0s ) =/= 0s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) =/= 0s ) with typecode |-
23	22	neneqd	Could not format ( A e. No -> -. ( A ^su 0s ) = 0s ) : No typesetting found for |- ( A e. No -> -. ( A ^su 0s ) = 0s ) with typecode |-
24	23	pm2.21d	Could not format ( A e. No -> ( ( A ^su 0s ) = 0s -> A = 0s ) ) : No typesetting found for |- ( A e. No -> ( ( A ^su 0s ) = 0s -> A = 0s ) ) with typecode |-
25		expsp1	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) with typecode |-
26	25	eqeq1d	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) x.s A ) = 0s ) ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) x.s A ) = 0s ) ) with typecode |-
27		expscl	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( A ^su n ) e. No ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( A ^su n ) e. No ) with typecode |-
28		simpl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A\in \mathrm{No}$$
29	27 28	muls0ord	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( ( ( A ^su n ) x.s A ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( ( ( A ^su n ) x.s A ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) ) with typecode |-
30	26 29	bitrd	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) ) with typecode |-
31	30	adantr	Could not format ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) ) : No typesetting found for |- ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) ) with typecode |-
32		simpr	Could not format ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su n ) = 0s -> A = 0s ) ) : No typesetting found for |- ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su n ) = 0s -> A = 0s ) ) with typecode |-
33		idd	Could not format ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( A = 0s -> A = 0s ) ) : No typesetting found for |- ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( A = 0s -> A = 0s ) ) with typecode |-
34	32 33	jaod	Could not format ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( ( A ^su n ) = 0s \/ A = 0s ) -> A = 0s ) ) : No typesetting found for |- ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( ( A ^su n ) = 0s \/ A = 0s ) -> A = 0s ) ) with typecode |-
35	31 34	sylbid	Could not format ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) : No typesetting found for |- ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) with typecode |-
36	35	ex	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( ( ( A ^su n ) = 0s -> A = 0s ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( ( ( A ^su n ) = 0s -> A = 0s ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) with typecode |-
37	36	expcom	Could not format ( n e. NN0_s -> ( A e. No -> ( ( ( A ^su n ) = 0s -> A = 0s ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( A e. No -> ( ( ( A ^su n ) = 0s -> A = 0s ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) ) with typecode |-
38	37	a2d	Could not format ( n e. NN0_s -> ( ( A e. No -> ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( A e. No -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( ( A e. No -> ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( A e. No -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) ) with typecode |-
39	4 8 12 16 24 38	n0sind	Could not format ( N e. NN0_s -> ( A e. No -> ( ( A ^su N ) = 0s -> A = 0s ) ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. No -> ( ( A ^su N ) = 0s -> A = 0s ) ) ) with typecode |-
40	39	imp	Could not format ( ( N e. NN0_s /\ A e. No ) -> ( ( A ^su N ) = 0s -> A = 0s ) ) : No typesetting found for |- ( ( N e. NN0_s /\ A e. No ) -> ( ( A ^su N ) = 0s -> A = 0s ) ) with typecode |-
41	40	necon3d	Could not format ( ( N e. NN0_s /\ A e. No ) -> ( A =/= 0s -> ( A ^su N ) =/= 0s ) ) : No typesetting found for |- ( ( N e. NN0_s /\ A e. No ) -> ( A =/= 0s -> ( A ^su N ) =/= 0s ) ) with typecode |-
42	41	ex	Could not format ( N e. NN0_s -> ( A e. No -> ( A =/= 0s -> ( A ^su N ) =/= 0s ) ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. No -> ( A =/= 0s -> ( A ^su N ) =/= 0s ) ) ) with typecode |-
43	42	3imp231	Could not format ( ( A e. No /\ A =/= 0s /\ N e. NN0_s ) -> ( A ^su N ) =/= 0s ) : No typesetting found for |- ( ( A e. No /\ A =/= 0s /\ N e. NN0_s ) -> ( A ^su N ) =/= 0s ) with typecode |-