Theorem pw2divsnegd

Description: Move negative sign inside of a power of two division. (Contributed by Scott Fenton, 8-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		pw2divsnegd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		pw2divsnegd.2	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3	1 2	pw2divscld	Could not format ( ph -> ( A /su ( 2s ^su N ) ) e. No ) : No typesetting found for |- ( ph -> ( A /su ( 2s ^su N ) ) e. No ) with typecode |-
4	3	negsidd	Could not format ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) = 0s ) : No typesetting found for |- ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) = 0s ) with typecode |-
5		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
6		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 |-
7	5 2 6	sylancr	Could not format ( ph -> ( 2s ^su N ) e. No ) : No typesetting found for |- ( ph -> ( 2s ^su N ) e. No ) with typecode |-
8		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 |-
9	7 8	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 |-
10	1	negsidd	$$⊢\phi \to A{+}_s{+}_s\left(A\right)=0_s$$
11	9 10	eqtr4d	Could not format ( ph -> ( ( 2s ^su N ) x.s 0s ) = ( A +s ( -us ` A ) ) ) : No typesetting found for |- ( ph -> ( ( 2s ^su N ) x.s 0s ) = ( A +s ( -us ` A ) ) ) with typecode |-
12	1	negscld	$$⊢\phi \to {+}_s\left(A\right)\in \mathrm{No}$$
13	1 12	addscld	$$⊢\phi \to A{+}_s{+}_s\left(A\right)\in \mathrm{No}$$
14		0sno	$$⊢0_s\in \mathrm{No}$$
15	14	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
16	13 15 2	pw2divsmuld	Could not format ( ph -> ( ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = 0s <-> ( ( 2s ^su N ) x.s 0s ) = ( A +s ( -us ` A ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = 0s <-> ( ( 2s ^su N ) x.s 0s ) = ( A +s ( -us ` A ) ) ) ) with typecode |-
17	11 16	mpbird	Could not format ( ph -> ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = 0s ) : No typesetting found for |- ( ph -> ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = 0s ) with typecode |-
18	1 12 2	pw2divsdird	Could not format ( ph -> ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) ) : No typesetting found for |- ( ph -> ( ( A +s ( -us ` A ) ) /su ( 2s ^su N ) ) = ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) ) with typecode |-
19	4 17 18	3eqtr2rd	Could not format ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) = ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) = ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) ) with typecode |-
20	12 2	pw2divscld	Could not format ( ph -> ( ( -us ` A ) /su ( 2s ^su N ) ) e. No ) : No typesetting found for |- ( ph -> ( ( -us ` A ) /su ( 2s ^su N ) ) e. No ) with typecode |-
21	3	negscld	Could not format ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) e. No ) : No typesetting found for |- ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) e. No ) with typecode |-
22	20 21 3	addscan1d	Could not format ( ph -> ( ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) = ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) <-> ( ( -us ` A ) /su ( 2s ^su N ) ) = ( -us ` ( A /su ( 2s ^su N ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( A /su ( 2s ^su N ) ) +s ( ( -us ` A ) /su ( 2s ^su N ) ) ) = ( ( A /su ( 2s ^su N ) ) +s ( -us ` ( A /su ( 2s ^su N ) ) ) ) <-> ( ( -us ` A ) /su ( 2s ^su N ) ) = ( -us ` ( A /su ( 2s ^su N ) ) ) ) ) with typecode |-
23	19 22	mpbid	Could not format ( ph -> ( ( -us ` A ) /su ( 2s ^su N ) ) = ( -us ` ( A /su ( 2s ^su N ) ) ) ) : No typesetting found for |- ( ph -> ( ( -us ` A ) /su ( 2s ^su N ) ) = ( -us ` ( A /su ( 2s ^su N ) ) ) ) with typecode |-
24	23	eqcomd	Could not format ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) = ( ( -us ` A ) /su ( 2s ^su N ) ) ) : No typesetting found for |- ( ph -> ( -us ` ( A /su ( 2s ^su N ) ) ) = ( ( -us ` A ) /su ( 2s ^su N ) ) ) with typecode |-