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	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2divs0d	Could not format assertion : No typesetting found for |- ( ph -> ( 0s /su ( 2s ^su N ) ) = 0s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pw2divs0d.1	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
2		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
3		expscl	Could not format ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ N e. NN0_s ) -> ( 2s ^su N ) e. No ) with typecode |-
4	2 1 3	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
5		muls01	Could not format ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s ) : No typesetting found for |- ( ( 2s ^su N ) e. No -> ( ( 2s ^su N ) x.s 0s ) = 0s ) with typecode |-
6	4 5	syl	Could not format ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s 0s ) = 0s ) with typecode |-
7		0sno	$$⊢0_s\in \mathrm{No}$$
8	7	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
9	8 8 1	pw2divsmuld	Could not format ( ph -> ( ( 0s /su ( 2s ^su N ) ) = 0s <-> ( ( 2s ^su N ) x.s 0s ) = 0s ) ) : No typesetting found for |- ( ph -> ( ( 0s /su ( 2s ^su N ) ) = 0s <-> ( ( 2s ^su N ) x.s 0s ) = 0s ) ) with typecode |-
10	6 9	mpbird	Could not format ( ph -> ( 0s /su ( 2s ^su N ) ) = 0s ) : No typesetting found for |- ( ph -> ( 0s /su ( 2s ^su N ) ) = 0s ) with typecode |-