Theorem expsgt0

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

	Ref	Expression
Assertion	expsgt0	|- ( ( A e. No /\ N e. NN0_s /\ 0s 0s

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) )
2	1	breq2d	|- ( m = 0s -> ( 0s 0s
3	2	imbi2d	|- ( m = 0s -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
4		oveq2	|- ( m = n -> ( A ^su m ) = ( A ^su n ) )
5	4	breq2d	|- ( m = n -> ( 0s 0s
6	5	imbi2d	|- ( m = n -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
7		oveq2	|- ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) )
8	7	breq2d	|- ( m = ( n +s 1s ) -> ( 0s 0s
9	8	imbi2d	|- ( m = ( n +s 1s ) -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
10		oveq2	|- ( m = N -> ( A ^su m ) = ( A ^su N ) )
11	10	breq2d	|- ( m = N -> ( 0s 0s
12	11	imbi2d	|- ( m = N -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
13		0slt1s	|- 0s
14		exps0	|- ( A e. No -> ( A ^su 0s ) = 1s )
15	13 14	breqtrrid	|- ( A e. No -> 0s
16	15	adantr	|- ( ( A e. No /\ 0s 0s
17		simp2l	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s A e. No )
18		simp1	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s n e. NN0_s )
19		expscl	|- ( ( A e. No /\ n e. NN0_s ) -> ( A ^su n ) e. No )
20	17 18 19	syl2anc	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s ( A ^su n ) e. No )
21		simp3	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s
22		simp2r	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s
23	20 17 21 22	mulsgt0d	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s
24		expsp1	|- ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
25	17 18 24	syl2anc	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
26	23 25	breqtrrd	|- ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s
27	26	3exp	|- ( n e. NN0_s -> ( ( A e. No /\ 0s ( 0s 0s
28	27	a2d	|- ( n e. NN0_s -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
29	3 6 9 12 16 28	n0sind	|- ( N e. NN0_s -> ( ( A e. No /\ 0s 0s
30	29	expd	|- ( N e. NN0_s -> ( A e. No -> ( 0s 0s
31	30	3imp21	|- ( ( A e. No /\ N e. NN0_s /\ 0s 0s