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	|- ( ph -> N e. NN0_s )
Assertion	pw2divs0d	|- ( ph -> ( 0s /su ( 2s ^su N ) ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		pw2divs0d.1	|- ( ph -> N e. NN0_s )
2		2sno	|- 2s e. No
3		expscl	|- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No )
4	2 1 3	sylancr	|- ( ph -> ( 2s ^su N ) e. No )
5		muls01	|- ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s )
6	4 5	syl	|- ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s )
7		0sno	|- 0s e. No
8	7	a1i	|- ( ph -> 0s e. No )
9	8 8 1	pw2divsmuld	|- ( ph -> ( ( 0s /su ( 2s ^su N ) ) = 0s <-> ( ( 2s ^su N ) x.s 0s ) = 0s ) )
10	6 9	mpbird	|- ( ph -> ( 0s /su ( 2s ^su N ) ) = 0s )