Theorem pw2divscan4d

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

	Ref	Expression
Hypotheses	pw2divscan4d.1	$$⊢\phi \to A\in \mathrm{No}$$
	pw2divscan4d.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
	pw2divscan4d.3	$$⊢\phi \to M\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2divscan4d	Could not format assertion : No typesetting found for |- ( ph -> ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pw2divscan4d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2divscan4d.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3		pw2divscan4d.3	$$⊢\phi \to M\in {\mathbb{N}}_{\mathrm{0s}}$$
4		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
5		expadds	Could not format ( ( 2s e. No /\ N e. NN0_s /\ M e. NN0_s ) -> ( 2s ^su ( N +s M ) ) = ( ( 2s ^su N ) x.s ( 2s ^su M ) ) ) : No typesetting found for |- ( ( 2s e. No /\ N e. NN0_s /\ M e. NN0_s ) -> ( 2s ^su ( N +s M ) ) = ( ( 2s ^su N ) x.s ( 2s ^su M ) ) ) with typecode |-
6	4 2 3 5	mp3an2i	Could not format ( ph -> ( 2s ^su ( N +s M ) ) = ( ( 2s ^su N ) x.s ( 2s ^su M ) ) ) : No typesetting found for |- ( ph -> ( 2s ^su ( N +s M ) ) = ( ( 2s ^su N ) x.s ( 2s ^su M ) ) ) with typecode |-
7	6	oveq1d	Could not format ( ph -> ( ( 2s ^su ( N +s M ) ) x.s A ) = ( ( ( 2s ^su N ) x.s ( 2s ^su M ) ) x.s A ) ) : No typesetting found for |- ( ph -> ( ( 2s ^su ( N +s M ) ) x.s A ) = ( ( ( 2s ^su N ) x.s ( 2s ^su M ) ) x.s A ) ) with typecode |-
8		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 |-
9	4 2 8	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
10		expscl	Could not format ( ( 2s e. No /\ M e. NN0_s ) -> ( 2s ^su M ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ M e. NN0_s ) -> ( 2s ^su M ) e. No ) with typecode |-
11	4 3 10	sylancr	Could not format ( ph -> ( 2s ^su M ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su M ) e. No ) with typecode |-
12	9 11 1	mulsassd	Could not format ( ph -> ( ( ( 2s ^su N ) x.s ( 2s ^su M ) ) x.s A ) = ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su N ) x.s ( 2s ^su M ) ) x.s A ) = ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) ) with typecode |-
13	7 12	eqtrd	Could not format ( ph -> ( ( 2s ^su ( N +s M ) ) x.s A ) = ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) ) : No typesetting found for |- ( ph -> ( ( 2s ^su ( N +s M ) ) x.s A ) = ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) ) with typecode |-
14	13	oveq1d	Could not format ( ph -> ( ( ( 2s ^su ( N +s M ) ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) = ( ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) /su ( 2s ^su ( N +s M ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su ( N +s M ) ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) = ( ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) /su ( 2s ^su ( N +s M ) ) ) ) with typecode |-
15		n0addscl	$$⊢\left(N\in {\mathbb{N}}_{\mathrm{0s}}\wedge M\in {\mathbb{N}}_{\mathrm{0s}}\right)\to N{+}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}$$
16	2 3 15	syl2anc	$$⊢\phi \to N{+}_{s}M\in {\mathbb{N}}_{\mathrm{0s}}$$
17	1 16	pw2divscan3d	Could not format ( ph -> ( ( ( 2s ^su ( N +s M ) ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) = A ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su ( N +s M ) ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) = A ) with typecode |-
18	11 1	mulscld	Could not format ( ph -> ( ( 2s ^su M ) x.s A ) e. No ) : No typesetting found for |- ( ph -> ( ( 2s ^su M ) x.s A ) e. No ) with typecode |-
19	9 18 16	pw2divsassd	Could not format ( ph -> ( ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) /su ( 2s ^su ( N +s M ) ) ) = ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su N ) x.s ( ( 2s ^su M ) x.s A ) ) /su ( 2s ^su ( N +s M ) ) ) = ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) ) with typecode |-
20	14 17 19	3eqtr3rd	Could not format ( ph -> ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) = A ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) = A ) with typecode |-
21	18 16	pw2divscld	Could not format ( ph -> ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) e. No ) : No typesetting found for |- ( ph -> ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) e. No ) with typecode |-
22	1 21 2	pw2divsmuld	Could not format ( ph -> ( ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) <-> ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) = A ) ) : No typesetting found for |- ( ph -> ( ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) <-> ( ( 2s ^su N ) x.s ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) = A ) ) with typecode |-
23	20 22	mpbird	Could not format ( ph -> ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) : No typesetting found for |- ( ph -> ( A /su ( 2s ^su N ) ) = ( ( ( 2s ^su M ) x.s A ) /su ( 2s ^su ( N +s M ) ) ) ) with typecode |-