Metamath Proof Explorer

Theorem divs1

Description: A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Assertion divs1 ⊢ A ∈ No → A / su 1 s = A

Proof

Step Hyp Ref Expression
1 mulslid ⊢ A ∈ No → 1 s ⋅ s A = A
2 1sno ⊢ 1 s ∈ No
3 0slt1s ⊢ 0 s < s 1 s
4 sgt0ne0 ⊢ 0 s < s 1 s → 1 s ≠ 0 s
5 3 4 ax-mp ⊢ 1 s ≠ 0 s
6 2 5 pm3.2i ⊢ 1 s ∈ No ∧ 1 s ≠ 0 s
7 mulslid ⊢ 1 s ∈ No → 1 s ⋅ s 1 s = 1 s
8 2 7 ax-mp ⊢ 1 s ⋅ s 1 s = 1 s
9 oveq2 ⊢ x = 1 s → 1 s ⋅ s x = 1 s ⋅ s 1 s
10 9 eqeq1d ⊢ x = 1 s → 1 s ⋅ s x = 1 s ↔ 1 s ⋅ s 1 s = 1 s
11 10 rspcev ⊢ 1 s ∈ No ∧ 1 s ⋅ s 1 s = 1 s → ∃ x ∈ No 1 s ⋅ s x = 1 s
12 2 8 11 mp2an ⊢ ∃ x ∈ No 1 s ⋅ s x = 1 s
13 divsmulw ⊢ A ∈ No ∧ A ∈ No ∧ 1 s ∈ No ∧ 1 s ≠ 0 s ∧ ∃ x ∈ No 1 s ⋅ s x = 1 s → A / su 1 s = A ↔ 1 s ⋅ s A = A
14 12 13 mpan2 ⊢ A ∈ No ∧ A ∈ No ∧ 1 s ∈ No ∧ 1 s ≠ 0 s → A / su 1 s = A ↔ 1 s ⋅ s A = A
15 6 14 mp3an3 ⊢ A ∈ No ∧ A ∈ No → A / su 1 s = A ↔ 1 s ⋅ s A = A
16 15 anidms ⊢ A ∈ No → A / su 1 s = A ↔ 1 s ⋅ s A = A
17 1 16 mpbird ⊢ A ∈ No → A / su 1 s = A