Theorem divs1

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

	Ref	Expression
Assertion	divs1	⊢ ( 𝐴 ∈ No → ( 𝐴 /su 1s ) = 𝐴 )

Proof

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