Theorem z12subscl

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

	Ref	Expression
Assertion	z12subscl	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2] ) → ( 𝐴 -s 𝐵 ) ∈ ℤs[1/2] )

Proof

Step	Hyp	Ref	Expression
1		z12no	⊢ ( 𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No )
2		z12no	⊢ ( 𝐵 ∈ ℤs[1/2] → 𝐵 ∈ No )
3		subsval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2] ) → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )
5		z12negscl	⊢ ( 𝐵 ∈ ℤs[1/2] → ( -us ‘ 𝐵 ) ∈ ℤs[1/2] )
6		z12addscl	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ ( -us ‘ 𝐵 ) ∈ ℤs[1/2] ) → ( 𝐴 +s ( -us ‘ 𝐵 ) ) ∈ ℤs[1/2] )
7	5 6	sylan2	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2] ) → ( 𝐴 +s ( -us ‘ 𝐵 ) ) ∈ ℤs[1/2] )
8	4 7	eqeltrd	⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 𝐵 ∈ ℤs[1/2] ) → ( 𝐴 -s 𝐵 ) ∈ ℤs[1/2] )