Metamath Proof Explorer

Theorem lenegs

Description: Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion lenegs ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ + s ⁡ B ≤ s + s ⁡ A

Proof

Step Hyp Ref Expression
1 ltnegs ⊢ B ∈ No ∧ A ∈ No → B < s A ↔ + s ⁡ A < s + s ⁡ B
2 1 ancoms ⊢ A ∈ No ∧ B ∈ No → B < s A ↔ + s ⁡ A < s + s ⁡ B
3 2 notbid ⊢ A ∈ No ∧ B ∈ No → ¬ B < s A ↔ ¬ + s ⁡ A < s + s ⁡ B
4 lenlts ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ ¬ B < s A
5 negscl ⊢ B ∈ No → + s ⁡ B ∈ No
6 negscl ⊢ A ∈ No → + s ⁡ A ∈ No
7 lenlts ⊢ + s ⁡ B ∈ No ∧ + s ⁡ A ∈ No → + s ⁡ B ≤ s + s ⁡ A ↔ ¬ + s ⁡ A < s + s ⁡ B
8 5 6 7 syl2anr ⊢ A ∈ No ∧ B ∈ No → + s ⁡ B ≤ s + s ⁡ A ↔ ¬ + s ⁡ A < s + s ⁡ B
9 3 4 8 3bitr4d ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ + s ⁡ B ≤ s + s ⁡ A