Theorem renegmulnnass

Description: Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025)

	Ref	Expression
Hypotheses	renegmulnnass.a	$$⊢\phi \to A\in ℝ$$
	renegmulnnass.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	renegmulnnass	$$⊢\phi \to \left(0{-}_{ℝ}A\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0{-}_{ℝ}A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		renegmulnnass.a	$$⊢\phi \to A\in ℝ$$
2		renegmulnnass.n	$$⊢\phi \to N\in \mathbb{N}$$
3		oveq2	$$⊢x=1\to \left(0{-}_{ℝ}A\right)x=\left(0{-}_{ℝ}A\right)\cdot 1$$
4		oveq2	$$⊢x=1\to Ax=A\cdot 1$$
5	4	oveq2d	$$⊢x=1\to 0{-}_{ℝ}Ax=0{-}_{ℝ}A\cdot 1$$
6	3 5	eqeq12d	$$⊢x=1\to \left(\left(0{-}_{ℝ}A\right)x=0{-}_{ℝ}Ax\leftrightarrow \left(0{-}_{ℝ}A\right)\cdot 1=0{-}_{ℝ}A\cdot 1\right)$$
7		oveq2	$$⊢x=y\to \left(0{-}_{ℝ}A\right)x=\left(0{-}_{ℝ}A\right)y$$
8		oveq2	$$⊢x=y\to Ax=Ay$$
9	8	oveq2d	$$⊢x=y\to 0{-}_{ℝ}Ax=0{-}_{ℝ}Ay$$
10	7 9	eqeq12d	$$⊢x=y\to \left(\left(0{-}_{ℝ}A\right)x=0{-}_{ℝ}Ax\leftrightarrow \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)$$
11		oveq2	$$⊢x=y+1\to \left(0{-}_{ℝ}A\right)x=\left(0{-}_{ℝ}A\right)\left(y+1\right)$$
12		oveq2	$$⊢x=y+1\to Ax=A\left(y+1\right)$$
13	12	oveq2d	$$⊢x=y+1\to 0{-}_{ℝ}Ax=0{-}_{ℝ}A\left(y+1\right)$$
14	11 13	eqeq12d	$$⊢x=y+1\to \left(\left(0{-}_{ℝ}A\right)x=0{-}_{ℝ}Ax\leftrightarrow \left(0{-}_{ℝ}A\right)\left(y+1\right)=0{-}_{ℝ}A\left(y+1\right)\right)$$
15		oveq2	$$⊢x=N\to \left(0{-}_{ℝ}A\right)x=\left(0{-}_{ℝ}A\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
16		oveq2	$$⊢x=N\to Ax=A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
17	16	oveq2d	$$⊢x=N\to 0{-}_{ℝ}Ax=0{-}_{ℝ}A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
18	15 17	eqeq12d	$$⊢x=N\to \left(\left(0{-}_{ℝ}A\right)x=0{-}_{ℝ}Ax\leftrightarrow \left(0{-}_{ℝ}A\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0{-}_{ℝ}A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
19		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
20	1 19	syl	$$⊢\phi \to 0{-}_{ℝ}A\in ℝ$$
21		ax-1rid	$$⊢0{-}_{ℝ}A\in ℝ\to \left(0{-}_{ℝ}A\right)\cdot 1=0{-}_{ℝ}A$$
22	20 21	syl	$$⊢\phi \to \left(0{-}_{ℝ}A\right)\cdot 1=0{-}_{ℝ}A$$
23		ax-1rid	$$⊢A\in ℝ\to A\cdot 1=A$$
24	1 23	syl	$$⊢\phi \to A\cdot 1=A$$
25	24	oveq2d	$$⊢\phi \to 0{-}_{ℝ}A\cdot 1=0{-}_{ℝ}A$$
26	22 25	eqtr4d	$$⊢\phi \to \left(0{-}_{ℝ}A\right)\cdot 1=0{-}_{ℝ}A\cdot 1$$
27		simpr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay$$
28	27	oveq2d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}A\right)y=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}Ay\right)$$
29		0red	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 0\in ℝ$$
30	1	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to A\in ℝ$$
31		nnre	$$⊢y\in \mathbb{N}\to y\in ℝ$$
32	31	ad2antlr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to y\in ℝ$$
33	30 32	remulcld	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to Ay\in ℝ$$
34		rernegcl	$$⊢Ay\in ℝ\to 0{-}_{ℝ}Ay\in ℝ$$
35	33 34	syl	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 0{-}_{ℝ}Ay\in ℝ$$
36		readdsub	$$⊢\left(0\in ℝ\wedge 0{-}_{ℝ}Ay\in ℝ\wedge A\in ℝ\right)\to \left(0+\left(0{-}_{ℝ}Ay\right)\right){-}_{ℝ}A=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}Ay\right)$$
37	29 35 30 36	syl3anc	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0+\left(0{-}_{ℝ}Ay\right)\right){-}_{ℝ}A=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}Ay\right)$$
38		readdlid	$$⊢0{-}_{ℝ}Ay\in ℝ\to 0+\left(0{-}_{ℝ}Ay\right)=0{-}_{ℝ}Ay$$
39	35 38	syl	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 0+\left(0{-}_{ℝ}Ay\right)=0{-}_{ℝ}Ay$$
40	39	oveq1d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0+\left(0{-}_{ℝ}Ay\right)\right){-}_{ℝ}A=\left(0{-}_{ℝ}Ay\right){-}_{ℝ}A$$
41	37 40	eqtr3d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}Ay\right)=\left(0{-}_{ℝ}Ay\right){-}_{ℝ}A$$
42		resubsub4	$$⊢\left(0\in ℝ\wedge Ay\in ℝ\wedge A\in ℝ\right)\to \left(0{-}_{ℝ}Ay\right){-}_{ℝ}A=0{-}_{ℝ}\left(Ay+A\right)$$
43	29 33 30 42	syl3anc	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}Ay\right){-}_{ℝ}A=0{-}_{ℝ}\left(Ay+A\right)$$
44	28 41 43	3eqtrd	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}\left(Ay+A\right)$$
45	22	oveq1d	$$⊢\phi \to \left(0{-}_{ℝ}A\right)\cdot 1+\left(0{-}_{ℝ}A\right)y=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}A\right)y$$
46	45	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)\cdot 1+\left(0{-}_{ℝ}A\right)y=\left(0{-}_{ℝ}A\right)+\left(0{-}_{ℝ}A\right)y$$
47	24	oveq2d	$$⊢\phi \to Ay+A\cdot 1=Ay+A$$
48	47	oveq2d	$$⊢\phi \to 0{-}_{ℝ}\left(Ay+A\cdot 1\right)=0{-}_{ℝ}\left(Ay+A\right)$$
49	48	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 0{-}_{ℝ}\left(Ay+A\cdot 1\right)=0{-}_{ℝ}\left(Ay+A\right)$$
50	44 46 49	3eqtr4d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)\cdot 1+\left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}\left(Ay+A\cdot 1\right)$$
51		nnadd1com	$$⊢y\in \mathbb{N}\to y+1=1+y$$
52	51	oveq2d	$$⊢y\in \mathbb{N}\to \left(0{-}_{ℝ}A\right)\left(y+1\right)=\left(0{-}_{ℝ}A\right)\left(1+y\right)$$
53	52	ad2antlr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)\left(y+1\right)=\left(0{-}_{ℝ}A\right)\left(1+y\right)$$
54	20	recnd	$$⊢\phi \to 0{-}_{ℝ}A\in ℂ$$
55	54	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 0{-}_{ℝ}A\in ℂ$$
56		1cnd	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 1\in ℂ$$
57		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
58	57	ad2antlr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to y\in ℂ$$
59	55 56 58	adddid	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)\left(1+y\right)=\left(0{-}_{ℝ}A\right)\cdot 1+\left(0{-}_{ℝ}A\right)y$$
60	53 59	eqtrd	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)\left(y+1\right)=\left(0{-}_{ℝ}A\right)\cdot 1+\left(0{-}_{ℝ}A\right)y$$
61	1	recnd	$$⊢\phi \to A\in ℂ$$
62	61	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to A\in ℂ$$
63	62 58 56	adddid	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to A\left(y+1\right)=Ay+A\cdot 1$$
64	63	oveq2d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to 0{-}_{ℝ}A\left(y+1\right)=0{-}_{ℝ}\left(Ay+A\cdot 1\right)$$
65	50 60 64	3eqtr4d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge \left(0{-}_{ℝ}A\right)y=0{-}_{ℝ}Ay\right)\to \left(0{-}_{ℝ}A\right)\left(y+1\right)=0{-}_{ℝ}A\left(y+1\right)$$
66	6 10 14 18 26 65	nnindd	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to \left(0{-}_{ℝ}A\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0{-}_{ℝ}A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
67	2 66	mpdan	$$⊢\phi \to \left(0{-}_{ℝ}A\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0{-}_{ℝ}A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$