Metamath Proof Explorer

Theorem abssge0

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

Ref Expression
Assertion abssge0 ⊢ A ∈ No → 0 s ≤ s abs s ⁡ A

Proof

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