Theorem subsge0d

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

	Ref	Expression
Hypotheses	subsge0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	subsge0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	subsge0d	⊢ ( 𝜑 → ( 0s ≤s ( 𝐴 -s 𝐵 ) ↔ 𝐵 ≤s 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		subsge0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		subsge0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		0no	⊢ 0s ∈ No
4	3	a1i	⊢ ( 𝜑 → 0s ∈ No )
5	1 2	subscld	⊢ ( 𝜑 → ( 𝐴 -s 𝐵 ) ∈ No )
6	4 5 2	leadds1d	⊢ ( 𝜑 → ( 0s ≤s ( 𝐴 -s 𝐵 ) ↔ ( 0s +s 𝐵 ) ≤s ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) ) )
7		addslid	⊢ ( 𝐵 ∈ No → ( 0s +s 𝐵 ) = 𝐵 )
8	2 7	syl	⊢ ( 𝜑 → ( 0s +s 𝐵 ) = 𝐵 )
9		npcans	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) = 𝐴 )
10	1 2 9	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) = 𝐴 )
11	8 10	breq12d	⊢ ( 𝜑 → ( ( 0s +s 𝐵 ) ≤s ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) ↔ 𝐵 ≤s 𝐴 ) )
12	6 11	bitrd	⊢ ( 𝜑 → ( 0s ≤s ( 𝐴 -s 𝐵 ) ↔ 𝐵 ≤s 𝐴 ) )