Theorem pw2divsmuld

Description: Relationship between surreal division and multiplication for powers of two. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	pw2divsmuld.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2divsmuld.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	pw2divsmuld.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divsmuld	⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = 𝐵 ↔ ( ( 2s ↑s 𝑁 ) ·s 𝐵 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pw2divsmuld.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2divsmuld.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		pw2divsmuld.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
4		2sno	⊢ 2s ∈ No
5		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
6	4 3 5	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
7		2ne0s	⊢ 2s ≠ 0s
8		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ≠ 0s )
9	4 7 3 8	mp3an12i	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ≠ 0s )
10		pw2recs	⊢ ( 𝑁 ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
11	3 10	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
12	1 2 6 9 11	divsmulwd	⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = 𝐵 ↔ ( ( 2s ↑s 𝑁 ) ·s 𝐵 ) = 𝐴 ) )