Metamath Proof Explorer

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 𝑦 ) = 𝐵 )