Metamath Proof Explorer

Theorem divsmulw

Description: Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex , we can eliminate the existence hypothesis (see divsmul ). (Contributed by Scott Fenton, 12-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 divsval Could not format ( ( A e. No /\ C e. No /\ C =/= 0s ) -> ( A /su C ) = ( iota_ y e. No ( C x.s y ) = A ) ) : No typesetting found for |- ( ( A e. No /\ C e. No /\ C =/= 0s ) -> ( A /su C ) = ( iota_ y e. No ( C x.s y ) = A ) ) with typecode |-
2 1 eqeq1d Could not format ( ( A e. No /\ C e. No /\ C =/= 0s ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) : No typesetting found for |- ( ( A e. No /\ C e. No /\ C =/= 0s ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) with typecode |-
3 2 3expb Could not format ( ( A e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) : No typesetting found for |- ( ( A e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) with typecode |-
4 3 3adant2 Could not format ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) with typecode |-
5 4 adantr Could not format ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) with typecode |-
6 simpl2 Could not format ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> B e. No ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> B e. No ) with typecode |-
7 simp3l Could not format ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> C e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> C e. No ) with typecode |-
8 simp3r Could not format ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> C =/= 0s ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> C =/= 0s ) with typecode |-
9 simp1 Could not format ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> A e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> A e. No ) with typecode |-
10 7 8 9 3jca Could not format ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( C e. No /\ C =/= 0s /\ A e. No ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( C e. No /\ C =/= 0s /\ A e. No ) ) with typecode |-
11 noreceuw Could not format ( ( ( C e. No /\ C =/= 0s /\ A e. No ) /\ E. x e. No ( C x.s x ) = 1s ) -> E! y e. No ( C x.s y ) = A ) : No typesetting found for |- ( ( ( C e. No /\ C =/= 0s /\ A e. No ) /\ E. x e. No ( C x.s x ) = 1s ) -> E! y e. No ( C x.s y ) = A ) with typecode |-
12 10 11 sylan Could not format ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> E! y e. No ( C x.s y ) = A ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> E! y e. No ( C x.s y ) = A ) with typecode |-
13 oveq2 Could not format ( y = B -> ( C x.s y ) = ( C x.s B ) ) : No typesetting found for |- ( y = B -> ( C x.s y ) = ( C x.s B ) ) with typecode |-
14 13 eqeq1d Could not format ( y = B -> ( ( C x.s y ) = A <-> ( C x.s B ) = A ) ) : No typesetting found for |- ( y = B -> ( ( C x.s y ) = A <-> ( C x.s B ) = A ) ) with typecode |-
15 14 riota2 Could not format ( ( B e. No /\ E! y e. No ( C x.s y ) = A ) -> ( ( C x.s B ) = A <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) : No typesetting found for |- ( ( B e. No /\ E! y e. No ( C x.s y ) = A ) -> ( ( C x.s B ) = A <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) with typecode |-
16 6 12 15 syl2anc Could not format ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( C x.s B ) = A <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( C x.s B ) = A <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) ) with typecode |-
17 5 16 bitr4d Could not format ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( C x.s B ) = A ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( C x.s B ) = A ) ) with typecode |-