Theorem divs1

Description: A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Assertion	divs1	Could not format assertion : No typesetting found for |- ( A e. No -> ( A /su 1s ) = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulslid	Could not format ( A e. No -> ( 1s x.s A ) = A ) : No typesetting found for |- ( A e. No -> ( 1s x.s A ) = A ) with typecode |-
2		1sno	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-
3		0slt1s	Could not format 0s
4		sgt0ne0	Could not format ( 0s 1s =/= 0s ) : No typesetting found for |- ( 0s 1s =/= 0s ) with typecode |-
5	3 4	ax-mp	Could not format 1s =/= 0s : No typesetting found for |- 1s =/= 0s with typecode |-
6	2 5	pm3.2i	Could not format ( 1s e. No /\ 1s =/= 0s ) : No typesetting found for |- ( 1s e. No /\ 1s =/= 0s ) with typecode |-
7		mulslid	Could not format ( 1s e. No -> ( 1s x.s 1s ) = 1s ) : No typesetting found for |- ( 1s e. No -> ( 1s x.s 1s ) = 1s ) with typecode |-
8	2 7	ax-mp	Could not format ( 1s x.s 1s ) = 1s : No typesetting found for |- ( 1s x.s 1s ) = 1s with typecode |-
9		oveq2	Could not format ( x = 1s -> ( 1s x.s x ) = ( 1s x.s 1s ) ) : No typesetting found for |- ( x = 1s -> ( 1s x.s x ) = ( 1s x.s 1s ) ) with typecode |-
10	9	eqeq1d	Could not format ( x = 1s -> ( ( 1s x.s x ) = 1s <-> ( 1s x.s 1s ) = 1s ) ) : No typesetting found for |- ( x = 1s -> ( ( 1s x.s x ) = 1s <-> ( 1s x.s 1s ) = 1s ) ) with typecode |-
11	10	rspcev	Could not format ( ( 1s e. No /\ ( 1s x.s 1s ) = 1s ) -> E. x e. No ( 1s x.s x ) = 1s ) : No typesetting found for |- ( ( 1s e. No /\ ( 1s x.s 1s ) = 1s ) -> E. x e. No ( 1s x.s x ) = 1s ) with typecode |-
12	2 8 11	mp2an	Could not format E. x e. No ( 1s x.s x ) = 1s : No typesetting found for |- E. x e. No ( 1s x.s x ) = 1s with typecode |-
13		divsmulw	Could not format ( ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) /\ E. x e. No ( 1s x.s x ) = 1s ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) : No typesetting found for |- ( ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) /\ E. x e. No ( 1s x.s x ) = 1s ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) with typecode |-
14	12 13	mpan2	Could not format ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) : No typesetting found for |- ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) with typecode |-
15	6 14	mp3an3	Could not format ( ( A e. No /\ A e. No ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) : No typesetting found for |- ( ( A e. No /\ A e. No ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) with typecode |-
16	15	anidms	Could not format ( A e. No -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) : No typesetting found for |- ( A e. No -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) ) with typecode |-
17	1 16	mpbird	Could not format ( A e. No -> ( A /su 1s ) = A ) : No typesetting found for |- ( A e. No -> ( A /su 1s ) = A ) with typecode |-