Theorem abssge0

Description: The absolute value of a surreal number is non-negative. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abssge0	⊢ ( 𝐴 ∈ No → 0s ≤s ( abss ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 0s ≤s 𝐴 → 0s ≤s 𝐴 )
2		iftrue	⊢ ( 0s ≤s 𝐴 → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = 𝐴 )
3	1 2	breqtrrd	⊢ ( 0s ≤s 𝐴 → 0s ≤s if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
4	3	adantr	⊢ ( ( 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → 0s ≤s if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
5		neg0s	⊢ ( -us ‘ 0s ) = 0s
6		0no	⊢ 0s ∈ No
7		lestric	⊢ ( ( 0s ∈ No ∧ 𝐴 ∈ No ) → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
8	6 7	mpan	⊢ ( 𝐴 ∈ No → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s ) )
9	8	ord	⊢ ( 𝐴 ∈ No → ( ¬ 0s ≤s 𝐴 → 𝐴 ≤s 0s ) )
10	9	impcom	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → 𝐴 ≤s 0s )
11		simpr	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → 𝐴 ∈ No )
12	6	a1i	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → 0s ∈ No )
13	11 12	lenegsd	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → ( 𝐴 ≤s 0s ↔ ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) ) )
14	10 13	mpbid	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → ( -us ‘ 0s ) ≤s ( -us ‘ 𝐴 ) )
15	5 14	eqbrtrrid	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → 0s ≤s ( -us ‘ 𝐴 ) )
16		iffalse	⊢ ( ¬ 0s ≤s 𝐴 → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) )
17	16	adantr	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) )
18	15 17	breqtrrd	⊢ ( ( ¬ 0s ≤s 𝐴 ∧ 𝐴 ∈ No ) → 0s ≤s if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
19	4 18	pm2.61ian	⊢ ( 𝐴 ∈ No → 0s ≤s if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
20		abssval	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
21	19 20	breqtrrd	⊢ ( 𝐴 ∈ No → 0s ≤s ( abss ‘ 𝐴 ) )