Theorem divsval

Description: The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025)

	Ref	Expression
Assertion	divsval	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No /\ B =/= 0s ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eldifsn	Could not format ( B e. ( No \ { 0s } ) <-> ( B e. No /\ B =/= 0s ) ) : No typesetting found for |- ( B e. ( No \ { 0s } ) <-> ( B e. No /\ B =/= 0s ) ) with typecode |-
2		eqeq2	Could not format ( y = A -> ( ( z x.s x ) = y <-> ( z x.s x ) = A ) ) : No typesetting found for |- ( y = A -> ( ( z x.s x ) = y <-> ( z x.s x ) = A ) ) with typecode |-
3	2	riotabidv	Could not format ( y = A -> ( iota_ x e. No ( z x.s x ) = y ) = ( iota_ x e. No ( z x.s x ) = A ) ) : No typesetting found for |- ( y = A -> ( iota_ x e. No ( z x.s x ) = y ) = ( iota_ x e. No ( z x.s x ) = A ) ) with typecode |-
4		oveq1	Could not format ( z = B -> ( z x.s x ) = ( B x.s x ) ) : No typesetting found for |- ( z = B -> ( z x.s x ) = ( B x.s x ) ) with typecode |-
5	4	eqeq1d	Could not format ( z = B -> ( ( z x.s x ) = A <-> ( B x.s x ) = A ) ) : No typesetting found for |- ( z = B -> ( ( z x.s x ) = A <-> ( B x.s x ) = A ) ) with typecode |-
6	5	riotabidv	Could not format ( z = B -> ( iota_ x e. No ( z x.s x ) = A ) = ( iota_ x e. No ( B x.s x ) = A ) ) : No typesetting found for |- ( z = B -> ( iota_ x e. No ( z x.s x ) = A ) = ( iota_ x e. No ( B x.s x ) = A ) ) with typecode |-
7		df-divs	Could not format /su = ( y e. No , z e. ( No \ { 0s } ) |-> ( iota_ x e. No ( z x.s x ) = y ) ) : No typesetting found for |- /su = ( y e. No , z e. ( No \ { 0s } ) |-> ( iota_ x e. No ( z x.s x ) = y ) ) with typecode |-
8		riotaex	Could not format ( iota_ x e. No ( B x.s x ) = A ) e. _V : No typesetting found for |- ( iota_ x e. No ( B x.s x ) = A ) e. _V with typecode |-
9	3 6 7 8	ovmpo	Could not format ( ( A e. No /\ B e. ( No \ { 0s } ) ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) : No typesetting found for |- ( ( A e. No /\ B e. ( No \ { 0s } ) ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) with typecode |-
10	1 9	sylan2br	Could not format ( ( A e. No /\ ( B e. No /\ B =/= 0s ) ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) : No typesetting found for |- ( ( A e. No /\ ( B e. No /\ B =/= 0s ) ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) with typecode |-
11	10	3impb	Could not format ( ( A e. No /\ B e. No /\ B =/= 0s ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ B =/= 0s ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) ) with typecode |-