Theorem pw2divsassd

Description: An associative law for division by powers of two. (Contributed by Scott Fenton, 11-Dec-2025)

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

Proof

Step	Hyp	Ref	Expression
1		pw2divsassd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2divsassd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		pw2divsassd.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
4		2no	⊢ 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	divsasswd	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 ·s ( 𝐵 /su ( 2s ↑s 𝑁 ) ) ) )