Theorem pw2divs0d

Description: Division into zero is zero for a power of two. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Hypothesis	pw2divs0d.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divs0d	⊢ ( 𝜑 → ( 0s /su ( 2s ↑s 𝑁 ) ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		pw2divs0d.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2		2no	⊢ 2s ∈ No
3		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
4	2 1 3	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
5		muls01	⊢ ( ( 2s ↑s 𝑁 ) ∈ No → ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s )
6	4 5	syl	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s )
7		0no	⊢ 0s ∈ No
8	7	a1i	⊢ ( 𝜑 → 0s ∈ No )
9	8 8 1	pw2divmulsd	⊢ ( 𝜑 → ( ( 0s /su ( 2s ↑s 𝑁 ) ) = 0s ↔ ( ( 2s ↑s 𝑁 ) ·s 0s ) = 0s ) )
10	6 9	mpbird	⊢ ( 𝜑 → ( 0s /su ( 2s ↑s 𝑁 ) ) = 0s )