Metamath Proof Explorer

Theorem pw2divsnegd

Description: Move negative sign inside of a power of two division. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Hypotheses pw2divsnegd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
pw2divsnegd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion pw2divsnegd ( 𝜑 → ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 pw2divsnegd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 pw2divsnegd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3 1 2 pw2divscld ⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ No )
4 3 negsidd ⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ) = 0s )
5 2sno ⊢ 2s ∈ No
6 expscl ⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
7 5 2 6 sylancr ⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
8 muls01 ⊢ ( ( 2s ↑s 𝑁 ) ∈ No → ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s )
9 7 8 syl ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s )
10 1 negsidd ⊢ ( 𝜑 → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )
11 9 10 eqtr4d ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s 0s ) = ( 𝐴 +s ( -us ‘ 𝐴 ) ) )
12 1 negscld ⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ No )
13 1 12 addscld ⊢ ( 𝜑 → ( 𝐴 +s ( -us ‘ 𝐴 ) ) ∈ No )
14 0sno ⊢ 0s ∈ No
15 14 a1i ⊢ ( 𝜑 → 0s ∈ No )
16 13 15 2 pw2divsmuld ⊢ ( 𝜑 → ( ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) /su ( 2s ↑s 𝑁 ) ) = 0s ↔ ( ( 2s ↑s 𝑁 ) ·s 0s ) = ( 𝐴 +s ( -us ‘ 𝐴 ) ) ) )
17 11 16 mpbird ⊢ ( 𝜑 → ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) /su ( 2s ↑s 𝑁 ) ) = 0s )
18 1 12 2 pw2divsdird ⊢ ( 𝜑 → ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) /su ( 2s ↑s 𝑁 ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) ) )
19 4 17 18 3eqtr2rd ⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ) )
20 12 2 pw2divscld ⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) ∈ No )
21 3 negscld ⊢ ( 𝜑 → ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ∈ No )
22 20 21 3 addscan1d ⊢ ( 𝜑 → ( ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) ) = ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) +s ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ) ↔ ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) = ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ) )
23 19 22 mpbid ⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) = ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) )
24 23 eqcomd ⊢ ( 𝜑 → ( -us ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = ( ( -us ‘ 𝐴 ) /su ( 2s ↑s 𝑁 ) ) )