Metamath Proof Explorer

Theorem zs12subscl

Description: The dyadics are closed under subtraction. (Contributed by Scott Fenton, 12-Dec-2025)

Ref Expression
Assertion zs12subscl 
|- ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A -s B ) e. ZZ_s[1/2] )

Proof

Step Hyp Ref Expression
1 zs12no 
 |-  ( A e. ZZ_s[1/2] -> A e. No )
2 zs12no 
 |-  ( B e. ZZ_s[1/2] -> B e. No )
3 subsval 
 |-  ( ( A e. No /\ B e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )
5 zs12negscl 
 |-  ( B e. ZZ_s[1/2] -> ( -us ` B ) e. ZZ_s[1/2] )
6 zs12addscl 
 |-  ( ( A e. ZZ_s[1/2] /\ ( -us ` B ) e. ZZ_s[1/2] ) -> ( A +s ( -us ` B ) ) e. ZZ_s[1/2] )
7 5 6 sylan2 
 |-  ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A +s ( -us ` B ) ) e. ZZ_s[1/2] )
8 4 7 eqeltrd 
 |-  ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A -s B ) e. ZZ_s[1/2] )