Theorem subsge0d

Description: Non-negative subtraction. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Hypotheses	subsge0d.1	$$⊢\phi \to A\in \mathrm{No}$$
	subsge0d.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	subsge0d	$$⊢\phi \to \left(0_s{\le }_s\left(A{-}_{s}B\right)\leftrightarrow B{\le }_{s}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		subsge0d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		subsge0d.2	$$⊢\phi \to B\in \mathrm{No}$$
3		0sno	$$⊢0_s\in \mathrm{No}$$
4	3	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
5	1 2	subscld	$$⊢\phi \to A{-}_{s}B\in \mathrm{No}$$
6	4 5 2	sleadd1d	$$⊢\phi \to \left(0_s{\le }_s\left(A{-}_{s}B\right)\leftrightarrow \left(0_s{+}_{s}B\right){\le }_s\left(\left(A{-}_{s}B\right){+}_{s}B\right)\right)$$
7		addslid	$$⊢B\in \mathrm{No}\to 0_s{+}_{s}B=B$$
8	2 7	syl	$$⊢\phi \to 0_s{+}_{s}B=B$$
9		npcans	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{-}_{s}B\right){+}_{s}B=A$$
10	1 2 9	syl2anc	$$⊢\phi \to \left(A{-}_{s}B\right){+}_{s}B=A$$
11	8 10	breq12d	$$⊢\phi \to \left(\left(0_s{+}_{s}B\right){\le }_s\left(\left(A{-}_{s}B\right){+}_{s}B\right)\leftrightarrow B{\le }_{s}A\right)$$
12	6 11	bitrd	$$⊢\phi \to \left(0_s{\le }_s\left(A{-}_{s}B\right)\leftrightarrow B{\le }_{s}A\right)$$