Metamath Proof Explorer

Theorem divsclw

Description: Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion divsclw 
|- ( ( ( A e. No /\ B e. No /\ B =/= 0s ) /\ E. x e. No ( B x.s x ) = 1s ) -> ( A /su B ) e. No )

Proof

Step Hyp Ref Expression
1 divsval 
 |-  ( ( A e. No /\ B e. No /\ B =/= 0s ) -> ( A /su B ) = ( iota_ y e. No ( B x.s y ) = A ) )
2 1 adantr 
 |-  ( ( ( A e. No /\ B e. No /\ B =/= 0s ) /\ E. x e. No ( B x.s x ) = 1s ) -> ( A /su B ) = ( iota_ y e. No ( B x.s y ) = A ) )
3 3anrot 
 |-  ( ( A e. No /\ B e. No /\ B =/= 0s ) <-> ( B e. No /\ B =/= 0s /\ A e. No ) )
4 noreceuw 
 |-  ( ( ( B e. No /\ B =/= 0s /\ A e. No ) /\ E. x e. No ( B x.s x ) = 1s ) -> E! y e. No ( B x.s y ) = A )
5 3 4 sylanb 
 |-  ( ( ( A e. No /\ B e. No /\ B =/= 0s ) /\ E. x e. No ( B x.s x ) = 1s ) -> E! y e. No ( B x.s y ) = A )
6 riotacl 
 |-  ( E! y e. No ( B x.s y ) = A -> ( iota_ y e. No ( B x.s y ) = A ) e. No )
7 5 6 syl 
 |-  ( ( ( A e. No /\ B e. No /\ B =/= 0s ) /\ E. x e. No ( B x.s x ) = 1s ) -> ( iota_ y e. No ( B x.s y ) = A ) e. No )
8 2 7 eqeltrd 
 |-  ( ( ( A e. No /\ B e. No /\ B =/= 0s ) /\ E. x e. No ( B x.s x ) = 1s ) -> ( A /su B ) e. No )