Theorem recsex

Description: A nonzero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025)

	Ref	Expression
Assertion	recsex	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )

Proof

Step	Hyp	Ref	Expression
1		0no	⊢ 0s ∈ No
2		ltstrine	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 ≠ 0s ↔ ( 𝐴 <s 0s ∨ 0s <s 𝐴 ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ No → ( 𝐴 ≠ 0s ↔ ( 𝐴 <s 0s ∨ 0s <s 𝐴 ) ) )
4		ltnegs	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 <s 0s ↔ ( -us ‘ 0s ) <s ( -us ‘ 𝐴 ) ) )
5	1 4	mpan2	⊢ ( 𝐴 ∈ No → ( 𝐴 <s 0s ↔ ( -us ‘ 0s ) <s ( -us ‘ 𝐴 ) ) )
6		neg0s	⊢ ( -us ‘ 0s ) = 0s
7	6	breq1i	⊢ ( ( -us ‘ 0s ) <s ( -us ‘ 𝐴 ) ↔ 0s <s ( -us ‘ 𝐴 ) )
8	5 7	bitrdi	⊢ ( 𝐴 ∈ No → ( 𝐴 <s 0s ↔ 0s <s ( -us ‘ 𝐴 ) ) )
9		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
10		precsex	⊢ ( ( ( -us ‘ 𝐴 ) ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) → ∃ 𝑦 ∈ No ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s )
11	9 10	sylan	⊢ ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) → ∃ 𝑦 ∈ No ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s )
12		simprl	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ No ∧ ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s ) ) → 𝑦 ∈ No )
13	12	negscld	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ No ∧ ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s ) ) → ( -us ‘ 𝑦 ) ∈ No )
14		simpll	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → 𝐴 ∈ No )
15		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → 𝑦 ∈ No )
16	14 15	mulnegs1d	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = ( -us ‘ ( 𝐴 ·s 𝑦 ) ) )
17	14 15	mulnegs2d	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → ( 𝐴 ·s ( -us ‘ 𝑦 ) ) = ( -us ‘ ( 𝐴 ·s 𝑦 ) ) )
18	16 17	eqtr4d	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = ( 𝐴 ·s ( -us ‘ 𝑦 ) ) )
19	18	eqeq1d	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → ( ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s ↔ ( 𝐴 ·s ( -us ‘ 𝑦 ) ) = 1s ) )
20	19	biimpd	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ 𝑦 ∈ No ) → ( ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s → ( 𝐴 ·s ( -us ‘ 𝑦 ) ) = 1s ) )
21	20	impr	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ No ∧ ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s ) ) → ( 𝐴 ·s ( -us ‘ 𝑦 ) ) = 1s )
22		oveq2	⊢ ( 𝑥 = ( -us ‘ 𝑦 ) → ( 𝐴 ·s 𝑥 ) = ( 𝐴 ·s ( -us ‘ 𝑦 ) ) )
23	22	eqeq1d	⊢ ( 𝑥 = ( -us ‘ 𝑦 ) → ( ( 𝐴 ·s 𝑥 ) = 1s ↔ ( 𝐴 ·s ( -us ‘ 𝑦 ) ) = 1s ) )
24	23	rspcev	⊢ ( ( ( -us ‘ 𝑦 ) ∈ No ∧ ( 𝐴 ·s ( -us ‘ 𝑦 ) ) = 1s ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )
25	13 21 24	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ No ∧ ( ( -us ‘ 𝐴 ) ·s 𝑦 ) = 1s ) ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )
26	11 25	rexlimddv	⊢ ( ( 𝐴 ∈ No ∧ 0s <s ( -us ‘ 𝐴 ) ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )
27	26	ex	⊢ ( 𝐴 ∈ No → ( 0s <s ( -us ‘ 𝐴 ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) )
28	8 27	sylbid	⊢ ( 𝐴 ∈ No → ( 𝐴 <s 0s → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) )
29		precsex	⊢ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )
30	29	ex	⊢ ( 𝐴 ∈ No → ( 0s <s 𝐴 → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) )
31	28 30	jaod	⊢ ( 𝐴 ∈ No → ( ( 𝐴 <s 0s ∨ 0s <s 𝐴 ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) )
32	3 31	sylbid	⊢ ( 𝐴 ∈ No → ( 𝐴 ≠ 0s → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) )
33	32	imp	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )