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 1sne0s ⊢ 1 s ≠ 0 s
4 2 3 pm3.2i ⊢ 1 s ∈ No ∧ 1 s ≠ 0 s
5 mulslid ⊢ 1 s ∈ No → 1 s ⋅ s 1 s = 1 s
6 2 5 ax-mp ⊢ 1 s ⋅ s 1 s = 1 s
7 oveq2 ⊢ x = 1 s → 1 s ⋅ s x = 1 s ⋅ s 1 s
8 7 eqeq1d ⊢ x = 1 s → 1 s ⋅ s x = 1 s ↔ 1 s ⋅ s 1 s = 1 s
9 8 rspcev ⊢ 1 s ∈ No ∧ 1 s ⋅ s 1 s = 1 s → ∃ x ∈ No 1 s ⋅ s x = 1 s
10 2 6 9 mp2an ⊢ ∃ x ∈ No 1 s ⋅ s x = 1 s
11 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
12 10 11 mpan2 ⊢ A ∈ No ∧ A ∈ No ∧ 1 s ∈ No ∧ 1 s ≠ 0 s → A / su 1 s = A ↔ 1 s ⋅ s A = A
13 4 12 mp3an3 ⊢ A ∈ No ∧ A ∈ No → A / su 1 s = A ↔ 1 s ⋅ s A = A
14 13 anidms ⊢ A ∈ No → A / su 1 s = A ↔ 1 s ⋅ s A = A
15 1 14 mpbird ⊢ A ∈ No → A / su 1 s = A