Theorem norecdiv

Description: If a surreal has a reciprocal, then it has any division. (Contributed by Scott Fenton, 12-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → 𝑤 ∈ No )
2		simpl3	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → 𝐵 ∈ No )
3	1 2	mulscld	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → ( 𝑤 ·s 𝐵 ) ∈ No )
4		oveq1	⊢ ( ( 𝐴 ·s 𝑤 ) = 1s → ( ( 𝐴 ·s 𝑤 ) ·s 𝐵 ) = ( 1s ·s 𝐵 ) )
5	4	adantl	⊢ ( ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) → ( ( 𝐴 ·s 𝑤 ) ·s 𝐵 ) = ( 1s ·s 𝐵 ) )
6	5	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → ( ( 𝐴 ·s 𝑤 ) ·s 𝐵 ) = ( 1s ·s 𝐵 ) )
7		simpl1	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → 𝐴 ∈ No )
8	7 1 2	mulsassd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → ( ( 𝐴 ·s 𝑤 ) ·s 𝐵 ) = ( 𝐴 ·s ( 𝑤 ·s 𝐵 ) ) )
9	2	mulslidd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → ( 1s ·s 𝐵 ) = 𝐵 )
10	6 8 9	3eqtr3d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → ( 𝐴 ·s ( 𝑤 ·s 𝐵 ) ) = 𝐵 )
11		oveq2	⊢ ( 𝑧 = ( 𝑤 ·s 𝐵 ) → ( 𝐴 ·s 𝑧 ) = ( 𝐴 ·s ( 𝑤 ·s 𝐵 ) ) )
12	11	eqeq1d	⊢ ( 𝑧 = ( 𝑤 ·s 𝐵 ) → ( ( 𝐴 ·s 𝑧 ) = 𝐵 ↔ ( 𝐴 ·s ( 𝑤 ·s 𝐵 ) ) = 𝐵 ) )
13	12	rspcev	⊢ ( ( ( 𝑤 ·s 𝐵 ) ∈ No ∧ ( 𝐴 ·s ( 𝑤 ·s 𝐵 ) ) = 𝐵 ) → ∃ 𝑧 ∈ No ( 𝐴 ·s 𝑧 ) = 𝐵 )
14	3 10 13	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( 𝐴 ·s 𝑤 ) = 1s ) ) → ∃ 𝑧 ∈ No ( 𝐴 ·s 𝑧 ) = 𝐵 )
15	14	rexlimdvaa	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) → ( ∃ 𝑤 ∈ No ( 𝐴 ·s 𝑤 ) = 1s → ∃ 𝑧 ∈ No ( 𝐴 ·s 𝑧 ) = 𝐵 ) )
16	15	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃ 𝑤 ∈ No ( 𝐴 ·s 𝑤 ) = 1s ) → ∃ 𝑧 ∈ No ( 𝐴 ·s 𝑧 ) = 𝐵 )
17		oveq2	⊢ ( 𝑥 = 𝑤 → ( 𝐴 ·s 𝑥 ) = ( 𝐴 ·s 𝑤 ) )
18	17	eqeq1d	⊢ ( 𝑥 = 𝑤 → ( ( 𝐴 ·s 𝑥 ) = 1s ↔ ( 𝐴 ·s 𝑤 ) = 1s ) )
19	18	cbvrexvw	⊢ ( ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ↔ ∃ 𝑤 ∈ No ( 𝐴 ·s 𝑤 ) = 1s )
20	19	anbi2i	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) ↔ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃ 𝑤 ∈ No ( 𝐴 ·s 𝑤 ) = 1s ) )
21		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝐴 ·s 𝑦 ) = ( 𝐴 ·s 𝑧 ) )
22	21	eqeq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 ·s 𝑦 ) = 𝐵 ↔ ( 𝐴 ·s 𝑧 ) = 𝐵 ) )
23	22	cbvrexvw	⊢ ( ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 𝐵 ↔ ∃ 𝑧 ∈ No ( 𝐴 ·s 𝑧 ) = 𝐵 )
24	16 20 23	3imtr4i	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ) → ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 𝐵 )