Metamath Proof Explorer

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

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 breq2d Could not format ( m = 0s -> ( 0s 0s ( 0s 0s
3 2 imbi2d Could not format ( m = 0s -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
4 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 |-
5 4 breq2d Could not format ( m = n -> ( 0s 0s ( 0s 0s
6 5 imbi2d Could not format ( m = n -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
7 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 |-
8 7 breq2d Could not format ( m = ( n +s 1s ) -> ( 0s 0s ( 0s 0s
9 8 imbi2d Could not format ( m = ( n +s 1s ) -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
10 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 |-
11 10 breq2d Could not format ( m = N -> ( 0s 0s ( 0s 0s
12 11 imbi2d Could not format ( m = N -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
13 0slt1s ⊢ 0 s < s 1 s
14 exps0 Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-
15 13 14 breqtrrid Could not format ( A e. No -> 0s 0s
16 15 adantr Could not format ( ( A e. No /\ 0s 0s 0s
17 simp2l Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s A e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( A e. No /\ 0s A e. No ) with typecode |-
18 simp1 Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s n e. NN0_s ) : No typesetting found for |- ( ( n e. NN0_s /\ ( A e. No /\ 0s n e. NN0_s ) with typecode |-
19 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 |-
20 17 18 19 syl2anc Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s ( A ^su n ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ ( A e. No /\ 0s ( A ^su n ) e. No ) with typecode |-
21 simp3 Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s 0s
22 simp2r Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s 0s
23 20 17 21 22 mulsgt0d Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s 0s
24 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 |-
25 17 18 24 syl2anc Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ ( A e. No /\ 0s ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) with typecode |-
26 23 25 breqtrrd Could not format ( ( n e. NN0_s /\ ( A e. No /\ 0s 0s 0s
27 26 3exp Could not format ( n e. NN0_s -> ( ( A e. No /\ 0s ( 0s 0s ( ( A e. No /\ 0s ( 0s 0s
28 27 a2d Could not format ( n e. NN0_s -> ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s ( ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
29 3 6 9 12 16 28 n0sind Could not format ( N e. NN0_s -> ( ( A e. No /\ 0s 0s ( ( A e. No /\ 0s 0s
30 29 expd Could not format ( N e. NN0_s -> ( A e. No -> ( 0s 0s ( A e. No -> ( 0s 0s
31 30 3imp21 Could not format ( ( A e. No /\ N e. NN0_s /\ 0s 0s 0s