Metamath Proof Explorer

Theorem pw2divscan4d

Description: Cancellation law for divison by powers of two. (Contributed by Scott Fenton, 11-Dec-2025)

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

Proof

Step Hyp Ref Expression
1 pw2divscan4d.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 pw2divscan4d.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3 pw2divscan4d.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0s )
4 2no ⊢ 2s ∈ No
5 expadds ⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ∧ 𝑀 ∈ ℕ0s ) → ( 2s ↑s ( 𝑁 +s 𝑀 ) ) = ( ( 2s ↑s 𝑁 ) ·s ( 2s ↑s 𝑀 ) ) )
6 4 2 3 5 mp3an2i ⊢ ( 𝜑 → ( 2s ↑s ( 𝑁 +s 𝑀 ) ) = ( ( 2s ↑s 𝑁 ) ·s ( 2s ↑s 𝑀 ) ) )
7 6 oveq1d ⊢ ( 𝜑 → ( ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ·s 𝐴 ) = ( ( ( 2s ↑s 𝑁 ) ·s ( 2s ↑s 𝑀 ) ) ·s 𝐴 ) )
8 expscl ⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
9 4 2 8 sylancr ⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
10 expscl ⊢ ( ( 2s ∈ No ∧ 𝑀 ∈ ℕ0s ) → ( 2s ↑s 𝑀 ) ∈ No )
11 4 3 10 sylancr ⊢ ( 𝜑 → ( 2s ↑s 𝑀 ) ∈ No )
12 9 11 1 mulsassd ⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) ·s ( 2s ↑s 𝑀 ) ) ·s 𝐴 ) = ( ( 2s ↑s 𝑁 ) ·s ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) ) )
13 7 12 eqtrd ⊢ ( 𝜑 → ( ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ·s 𝐴 ) = ( ( 2s ↑s 𝑁 ) ·s ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) ) )
14 13 oveq1d ⊢ ( 𝜑 → ( ( ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) = ( ( ( 2s ↑s 𝑁 ) ·s ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) )
15 n0addscl ⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝑀 ∈ ℕ0s ) → ( 𝑁 +s 𝑀 ) ∈ ℕ0s )
16 2 3 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 +s 𝑀 ) ∈ ℕ0s )
17 1 16 pw2divscan3d ⊢ ( 𝜑 → ( ( ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) = 𝐴 )
18 11 1 mulscld ⊢ ( 𝜑 → ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) ∈ No )
19 9 18 16 pw2divsassd ⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) ·s ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) = ( ( 2s ↑s 𝑁 ) ·s ( ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) ) )
20 14 17 19 3eqtr3rd ⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s ( ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) ) = 𝐴 )
21 18 16 pw2divscld ⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) ∈ No )
22 1 21 2 pw2divmulsd ⊢ ( 𝜑 → ( ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) ↔ ( ( 2s ↑s 𝑁 ) ·s ( ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) ) = 𝐴 ) )
23 20 22 mpbird ⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( ( ( 2s ↑s 𝑀 ) ·s 𝐴 ) /su ( 2s ↑s ( 𝑁 +s 𝑀 ) ) ) )