Metamath Proof Explorer

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 
|- ( ( A e. No /\ A =/= 0s /\ N e. NN0_s ) -> ( A ^su N ) =/= 0s )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) )
2 1 eqeq1d 
 |-  ( m = 0s -> ( ( A ^su m ) = 0s <-> ( A ^su 0s ) = 0s ) )
3 2 imbi1d 
 |-  ( m = 0s -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su 0s ) = 0s -> A = 0s ) ) )
4 3 imbi2d 
 |-  ( m = 0s -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su 0s ) = 0s -> A = 0s ) ) ) )
5 oveq2 
 |-  ( m = n -> ( A ^su m ) = ( A ^su n ) )
6 5 eqeq1d 
 |-  ( m = n -> ( ( A ^su m ) = 0s <-> ( A ^su n ) = 0s ) )
7 6 imbi1d 
 |-  ( m = n -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su n ) = 0s -> A = 0s ) ) )
8 7 imbi2d 
 |-  ( m = n -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su n ) = 0s -> A = 0s ) ) ) )
9 oveq2 
 |-  ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) )
10 9 eqeq1d 
 |-  ( m = ( n +s 1s ) -> ( ( A ^su m ) = 0s <-> ( A ^su ( n +s 1s ) ) = 0s ) )
11 10 imbi1d 
 |-  ( m = ( n +s 1s ) -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) )
12 11 imbi2d 
 |-  ( m = ( n +s 1s ) -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) )
13 oveq2 
 |-  ( m = N -> ( A ^su m ) = ( A ^su N ) )
14 13 eqeq1d 
 |-  ( m = N -> ( ( A ^su m ) = 0s <-> ( A ^su N ) = 0s ) )
15 14 imbi1d 
 |-  ( m = N -> ( ( ( A ^su m ) = 0s -> A = 0s ) <-> ( ( A ^su N ) = 0s -> A = 0s ) ) )
16 15 imbi2d 
 |-  ( m = N -> ( ( A e. No -> ( ( A ^su m ) = 0s -> A = 0s ) ) <-> ( A e. No -> ( ( A ^su N ) = 0s -> A = 0s ) ) ) )
17 0slt1s 
 |-  0s
18 sgt0ne0 
 |-  ( 0s  1s =/= 0s )
19 17 18 ax-mp 
 |-  1s =/= 0s
20 exps0 
 |-  ( A e. No -> ( A ^su 0s ) = 1s )
21 20 neeq1d 
 |-  ( A e. No -> ( ( A ^su 0s ) =/= 0s <-> 1s =/= 0s ) )
22 19 21 mpbiri 
 |-  ( A e. No -> ( A ^su 0s ) =/= 0s )
23 22 neneqd 
 |-  ( A e. No -> -. ( A ^su 0s ) = 0s )
24 23 pm2.21d 
 |-  ( A e. No -> ( ( A ^su 0s ) = 0s -> A = 0s ) )
25 expsp1 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
26 25 eqeq1d 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) x.s A ) = 0s ) )
27 expscl 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( A ^su n ) e. No )
28 simpl 
 |-  ( ( A e. No /\ n e. NN0_s ) -> A e. No )
29 27 28 muls0ord 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( ( ( A ^su n ) x.s A ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) )
30 26 29 bitrd 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( ( A ^su ( n +s 1s ) ) = 0s <-> ( ( A ^su n ) = 0s \/ A = 0s ) ) )
31 30 adantr 
 |-  ( ( ( 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 ) ) )
32 simpr 
 |-  ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su n ) = 0s -> A = 0s ) )
33 idd 
 |-  ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( A = 0s -> A = 0s ) )
34 32 33 jaod 
 |-  ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( ( A ^su n ) = 0s \/ A = 0s ) -> A = 0s ) )
35 31 34 sylbid 
 |-  ( ( ( A e. No /\ n e. NN0_s ) /\ ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) )
36 35 ex 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( ( ( A ^su n ) = 0s -> A = 0s ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) )
37 36 expcom 
 |-  ( n e. NN0_s -> ( A e. No -> ( ( ( A ^su n ) = 0s -> A = 0s ) -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) )
38 37 a2d 
 |-  ( n e. NN0_s -> ( ( A e. No -> ( ( A ^su n ) = 0s -> A = 0s ) ) -> ( A e. No -> ( ( A ^su ( n +s 1s ) ) = 0s -> A = 0s ) ) ) )
39 4 8 12 16 24 38 n0sind 
 |-  ( N e. NN0_s -> ( A e. No -> ( ( A ^su N ) = 0s -> A = 0s ) ) )
40 39 imp 
 |-  ( ( N e. NN0_s /\ A e. No ) -> ( ( A ^su N ) = 0s -> A = 0s ) )
41 40 necon3d 
 |-  ( ( N e. NN0_s /\ A e. No ) -> ( A =/= 0s -> ( A ^su N ) =/= 0s ) )
42 41 ex 
 |-  ( N e. NN0_s -> ( A e. No -> ( A =/= 0s -> ( A ^su N ) =/= 0s ) ) )
43 42 3imp231 
 |-  ( ( A e. No /\ A =/= 0s /\ N e. NN0_s ) -> ( A ^su N ) =/= 0s )