Description: Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. (Contributed by Scott Fenton, 12-Mar-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | divsmulwd.1 | ⊢ ( 𝜑 → 𝐴 ∈ No ) | |
| divsmulwd.2 | ⊢ ( 𝜑 → 𝐵 ∈ No ) | ||
| divsmulwd.3 | ⊢ ( 𝜑 → 𝐶 ∈ No ) | ||
| divsmulwd.4 | ⊢ ( 𝜑 → 𝐶 ≠ 0s ) | ||
| divsmulwd.5 | ⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) | ||
| Assertion | divsmulwd | ⊢ ( 𝜑 → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | divsmulwd.1 | ⊢ ( 𝜑 → 𝐴 ∈ No ) | |
| 2 | divsmulwd.2 | ⊢ ( 𝜑 → 𝐵 ∈ No ) | |
| 3 | divsmulwd.3 | ⊢ ( 𝜑 → 𝐶 ∈ No ) | |
| 4 | divsmulwd.4 | ⊢ ( 𝜑 → 𝐶 ≠ 0s ) | |
| 5 | divsmulwd.5 | ⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) | |
| 6 | 3 4 | jca | ⊢ ( 𝜑 → ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) |
| 7 | divsmulw | ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) ) | |
| 8 | 1 2 6 5 7 | syl31anc | ⊢ ( 𝜑 → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) ) |