Metamath Proof Explorer

Theorem divdivs1d

Description: Surreal division into a fraction. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Hypotheses divdivs1d.1 
|- ( ph -> A e. No )
divdivs1d.2 
|- ( ph -> B e. No )
divdivs1d.3 
|- ( ph -> C e. No )
divdivs1d.4 
|- ( ph -> B =/= 0s )
divdivs1d.5 
|- ( ph -> C =/= 0s )
Assertion divdivs1d 
|- ( ph -> ( ( A /su B ) /su C ) = ( A /su ( B x.s C ) ) )

Proof

Step Hyp Ref Expression
1 divdivs1d.1 
 |-  ( ph -> A e. No )
2 divdivs1d.2 
 |-  ( ph -> B e. No )
3 divdivs1d.3 
 |-  ( ph -> C e. No )
4 divdivs1d.4 
 |-  ( ph -> B =/= 0s )
5 divdivs1d.5 
 |-  ( ph -> C =/= 0s )
6 2 3 mulscld 
 |-  ( ph -> ( B x.s C ) e. No )
7 2 3 mulsne0bd 
 |-  ( ph -> ( ( B x.s C ) =/= 0s <-> ( B =/= 0s /\ C =/= 0s ) ) )
8 4 5 7 mpbir2and 
 |-  ( ph -> ( B x.s C ) =/= 0s )
9 1 6 8 divscld 
 |-  ( ph -> ( A /su ( B x.s C ) ) e. No )
10 2 3 9 mulsassd 
 |-  ( ph -> ( ( B x.s C ) x.s ( A /su ( B x.s C ) ) ) = ( B x.s ( C x.s ( A /su ( B x.s C ) ) ) ) )
11 1 6 8 divscan2d 
 |-  ( ph -> ( ( B x.s C ) x.s ( A /su ( B x.s C ) ) ) = A )
12 10 11 eqtr3d 
 |-  ( ph -> ( B x.s ( C x.s ( A /su ( B x.s C ) ) ) ) = A )
13 3 9 mulscld 
 |-  ( ph -> ( C x.s ( A /su ( B x.s C ) ) ) e. No )
14 1 13 2 4 divsmuld 
 |-  ( ph -> ( ( A /su B ) = ( C x.s ( A /su ( B x.s C ) ) ) <-> ( B x.s ( C x.s ( A /su ( B x.s C ) ) ) ) = A ) )
15 12 14 mpbird 
 |-  ( ph -> ( A /su B ) = ( C x.s ( A /su ( B x.s C ) ) ) )
16 15 eqcomd 
 |-  ( ph -> ( C x.s ( A /su ( B x.s C ) ) ) = ( A /su B ) )
17 1 2 4 divscld 
 |-  ( ph -> ( A /su B ) e. No )
18 17 9 3 5 divsmuld 
 |-  ( ph -> ( ( ( A /su B ) /su C ) = ( A /su ( B x.s C ) ) <-> ( C x.s ( A /su ( B x.s C ) ) ) = ( A /su B ) ) )
19 16 18 mpbird 
 |-  ( ph -> ( ( A /su B ) /su C ) = ( A /su ( B x.s C ) ) )