Theorem subsge0d

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

	Ref	Expression
Hypotheses	subsge0d.1	|- ( ph -> A e. No )
	subsge0d.2	|- ( ph -> B e. No )
Assertion	subsge0d	|- ( ph -> ( 0s <_s ( A -s B ) <-> B <_s A ) )

Proof

Step	Hyp	Ref	Expression
1		subsge0d.1	|- ( ph -> A e. No )
2		subsge0d.2	|- ( ph -> B e. No )
3		0sno	|- 0s e. No
4	3	a1i	|- ( ph -> 0s e. No )
5	1 2	subscld	|- ( ph -> ( A -s B ) e. No )
6	4 5 2	sleadd1d	|- ( ph -> ( 0s <_s ( A -s B ) <-> ( 0s +s B ) <_s ( ( A -s B ) +s B ) ) )
7		addslid	|- ( B e. No -> ( 0s +s B ) = B )
8	2 7	syl	|- ( ph -> ( 0s +s B ) = B )
9		npcans	|- ( ( A e. No /\ B e. No ) -> ( ( A -s B ) +s B ) = A )
10	1 2 9	syl2anc	|- ( ph -> ( ( A -s B ) +s B ) = A )
11	8 10	breq12d	|- ( ph -> ( ( 0s +s B ) <_s ( ( A -s B ) +s B ) <-> B <_s A ) )
12	6 11	bitrd	|- ( ph -> ( 0s <_s ( A -s B ) <-> B <_s A ) )