Metamath Proof Explorer

Theorem expscl

Description: Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Assertion expscl Could not format assertion : No typesetting found for |- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su N ) e. No ) 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 eleq1d Could not format ( m = 0s -> ( ( A ^su m ) e. No <-> ( A ^su 0s ) e. No ) ) : No typesetting found for |- ( m = 0s -> ( ( A ^su m ) e. No <-> ( A ^su 0s ) e. No ) ) with typecode |-
3 2 imbi2d Could not format ( m = 0s -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su 0s ) e. No ) ) ) : No typesetting found for |- ( m = 0s -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su 0s ) e. No ) ) ) with typecode |-
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 eleq1d Could not format ( m = n -> ( ( A ^su m ) e. No <-> ( A ^su n ) e. No ) ) : No typesetting found for |- ( m = n -> ( ( A ^su m ) e. No <-> ( A ^su n ) e. No ) ) with typecode |-
6 5 imbi2d Could not format ( m = n -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su n ) e. No ) ) ) : No typesetting found for |- ( m = n -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su n ) e. No ) ) ) with typecode |-
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 eleq1d Could not format ( m = ( n +s 1s ) -> ( ( A ^su m ) e. No <-> ( A ^su ( n +s 1s ) ) e. No ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A ^su m ) e. No <-> ( A ^su ( n +s 1s ) ) e. No ) ) with typecode |-
9 8 imbi2d Could not format ( m = ( n +s 1s ) -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) ) with typecode |-
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 eleq1d Could not format ( m = N -> ( ( A ^su m ) e. No <-> ( A ^su N ) e. No ) ) : No typesetting found for |- ( m = N -> ( ( A ^su m ) e. No <-> ( A ^su N ) e. No ) ) with typecode |-
12 11 imbi2d Could not format ( m = N -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su N ) e. No ) ) ) : No typesetting found for |- ( m = N -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su N ) e. No ) ) ) with typecode |-
13 exps0 Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-
14 1sno ⊢ 1 s ∈ No
15 13 14 eqeltrdi Could not format ( A e. No -> ( A ^su 0s ) e. No ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) e. No ) with typecode |-
16 simp2 Could not format ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> A e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> A e. No ) with typecode |-
17 simp1 Could not format ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> n e. NN0_s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> n e. NN0_s ) with typecode |-
18 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 |-
19 16 17 18 syl2anc Could not format ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) with typecode |-
20 simp3 Could not format ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su n ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su n ) e. No ) with typecode |-
21 20 16 mulscld Could not format ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( ( A ^su n ) x.s A ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( ( A ^su n ) x.s A ) e. No ) with typecode |-
22 19 21 eqeltrd Could not format ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su ( n +s 1s ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su ( n +s 1s ) ) e. No ) with typecode |-
23 22 3exp Could not format ( n e. NN0_s -> ( A e. No -> ( ( A ^su n ) e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( A e. No -> ( ( A ^su n ) e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) ) with typecode |-
24 23 a2d Could not format ( n e. NN0_s -> ( ( A e. No -> ( A ^su n ) e. No ) -> ( A e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( ( A e. No -> ( A ^su n ) e. No ) -> ( A e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) ) with typecode |-
25 3 6 9 12 15 24 n0sind Could not format ( N e. NN0_s -> ( A e. No -> ( A ^su N ) e. No ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. No -> ( A ^su N ) e. No ) ) with typecode |-
26 25 impcom 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 |-