Metamath Proof Explorer

Theorem pw2divsrecd

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

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

Proof

Step Hyp Ref Expression
1 pw2divsrecd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 pw2divsrecd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3 1 mulsridd ⊢ ( 𝜑 → ( 𝐴 ·s 1s ) = 𝐴 )
4 2sno ⊢ 2s ∈ No
5 expscl ⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
6 4 2 5 sylancr ⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
7 1sno ⊢ 1s ∈ No
8 7 a1i ⊢ ( 𝜑 → 1s ∈ No )
9 8 2 pw2divscld ⊢ ( 𝜑 → ( 1s /su ( 2s ↑s 𝑁 ) ) ∈ No )
10 6 1 9 muls12d ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) = ( 𝐴 ·s ( ( 2s ↑s 𝑁 ) ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) )
11 8 2 pw2divscan2d ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) = 1s )
12 11 oveq2d ⊢ ( 𝜑 → ( 𝐴 ·s ( ( 2s ↑s 𝑁 ) ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) = ( 𝐴 ·s 1s ) )
13 10 12 eqtrd ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) = ( 𝐴 ·s 1s ) )
14 1 2 pw2divscan2d ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = 𝐴 )
15 3 13 14 3eqtr4rd ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) )
16 1 2 pw2divscld ⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ No )
17 1 9 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ∈ No )
18 2ne0s ⊢ 2s ≠ 0s
19 expsne0 ⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ≠ 0s )
20 4 18 2 19 mp3an12i ⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ≠ 0s )
21 16 17 6 20 mulscan1d ⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = ( ( 2s ↑s 𝑁 ) ·s ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) ↔ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) ) )
22 15 21 mpbid ⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 ·s ( 1s /su ( 2s ↑s 𝑁 ) ) ) )