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		1sne0s	$$⊢1_s\ne 0_s$$
18		exps0	Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-
19	18	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 |-
20	17 19	mpbiri	Could not format ( A e. No -> ( A ^su 0s ) =/= 0s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) =/= 0s ) with typecode |-
21	20	neneqd	Could not format ( A e. No -> -. ( A ^su 0s ) = 0s ) : No typesetting found for |- ( A e. No -> -. ( A ^su 0s ) = 0s ) with typecode |-
22	21	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 |-
23		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 |-
24	23	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 |-
25		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 |-
26		simpl	$$⊢\left(A\in \mathrm{No}\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A\in \mathrm{No}$$
27	25 26	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 |-
28	24 27	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 |-
29	28	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 |-
30		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 |-
31		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 |-
32	30 31	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 |-
33	29 32	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 |-
34	33	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 |-
35	34	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 |-
36	35	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 |-
37	4 8 12 16 22 36	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 |-
38	37	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 |-
39	38	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 |-
40	39	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 |-
41	40	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 |-