Theorem rprmdvdspow

Description: If a prime element divides a ring "power", it divides the term. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmdvdspow.b	$$⊢B={\mathrm{Base}}_R$$
	rprmdvdspow.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmdvdspow.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	rprmdvdspow.m	$$⊢M={\mathrm{mulGrp}}_R$$
	rprmdvdspow.o	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	rprmdvdspow.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	rprmdvdspow.x	$$⊢\phi \to X\in B$$
	rprmdvdspow.q	$$⊢\phi \to Q\in P$$
	rprmdvdspow.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	rprmdvdspow.1	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left(N\underset{\dot{}}{\times }X\right)$$
Assertion	rprmdvdspow	$$⊢\phi \to Q\underset{\dot{}}{\parallel }X$$

Proof

Step	Hyp	Ref	Expression
1		rprmdvdspow.b	$$⊢B={\mathrm{Base}}_R$$
2		rprmdvdspow.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		rprmdvdspow.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		rprmdvdspow.m	$$⊢M={\mathrm{mulGrp}}_R$$
5		rprmdvdspow.o	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
6		rprmdvdspow.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		rprmdvdspow.x	$$⊢\phi \to X\in B$$
8		rprmdvdspow.q	$$⊢\phi \to Q\in P$$
9		rprmdvdspow.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
10		rprmdvdspow.1	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left(N\underset{\dot{}}{\times }X\right)$$
11		oveq1	$$⊢i=0\to i\underset{\dot{}}{\times }X=0\underset{\dot{}}{\times }X$$
12	11	breq2d	$$⊢i=0\to \left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\right)$$
13	12	imbi1d	$$⊢i=0\to \left(\left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)$$
14		oveq1	$$⊢i=n\to i\underset{\dot{}}{\times }X=n\underset{\dot{}}{\times }X$$
15	14	breq2d	$$⊢i=n\to \left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\right)$$
16	15	imbi1d	$$⊢i=n\to \left(\left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)$$
17		oveq1	$$⊢i=n+1\to i\underset{\dot{}}{\times }X=\left(n+1\right)\underset{\dot{}}{\times }X$$
18	17	breq2d	$$⊢i=n+1\to \left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)$$
19	18	imbi1d	$$⊢i=n+1\to \left(\left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)$$
20		oveq1	$$⊢i=N\to i\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X$$
21	20	breq2d	$$⊢i=N\to \left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(N\underset{\dot{}}{\times }X\right)\right)$$
22	21	imbi1d	$$⊢i=N\to \left(\left(Q\underset{\dot{}}{\parallel }\left(i\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left(N\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)$$
23	4 1	mgpbas	$$⊢B={\mathrm{Base}}_M$$
24		eqid	$$⊢1_R=1_R$$
25	4 24	ringidval	$$⊢1_R=0_M$$
26	23 25 5	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{\times }X=1_R$$
27	7 26	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }X=1_R$$
28	27	breq2d	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\leftrightarrow Q\underset{\dot{}}{\parallel }{1}_R\right)$$
29	28	biimpa	$$⊢\left(\phi \wedge Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\right)\to Q\underset{\dot{}}{\parallel }{1}_R$$
30	24 3 2 6 8	rprmndvdsr1	$$⊢\phi \to \neg Q\underset{\dot{}}{\parallel }{1}_R$$
31	30	adantr	$$⊢\left(\phi \wedge Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\right)\to \neg Q\underset{\dot{}}{\parallel }{1}_R$$
32	29 31	pm2.21dd	$$⊢\left(\phi \wedge Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\right)\to Q\underset{\dot{}}{\parallel }X$$
33	32	ex	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left(0\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)$$
34		simpllr	$$⊢\left(\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)$$
35	34	syldbl2	$$⊢\left(\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\right)\to Q\underset{\dot{}}{\parallel }X$$
36		simpr	$$⊢\left(\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }X\right)\to Q\underset{\dot{}}{\parallel }X$$
37		eqid	$$⊢{\cdot }_R={\cdot }_R$$
38	6	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to R\in \mathrm{CRing}$$
39	8	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to Q\in P$$
40	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
41	4	ringmgp	$$⊢R\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
42	40 41	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
43	42	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to M\in \mathrm{Mnd}$$
44		simpllr	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to n\in {\mathbb{N}}_0$$
45	7	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to X\in B$$
46	23 5 43 44 45	mulgnn0cld	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to n\underset{\dot{}}{\times }X\in B$$
47	42	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to M\in \mathrm{Mnd}$$
48		simpr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
49	7	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to X\in B$$
50	4 37	mgpplusg	$$⊢{\cdot }_R={+}_M$$
51	23 5 50	mulgnn0p1	$$⊢\left(M\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\wedge X\in B\right)\to \left(n+1\right)\underset{\dot{}}{\times }X=\left(n\underset{\dot{}}{\times }X\right){\cdot }_{R}X$$
52	47 48 49 51	syl3anc	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(n+1\right)\underset{\dot{}}{\times }X=\left(n\underset{\dot{}}{\times }X\right){\cdot }_{R}X$$
53	52	breq2d	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(\left(n\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)\right)$$
54	53	biimpa	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to Q\underset{\dot{}}{\parallel }\left(\left(n\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)$$
55	54	adantlr	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to Q\underset{\dot{}}{\parallel }\left(\left(n\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)$$
56	1 2 3 37 38 39 46 45 55	rprmdvds	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\vee Q\underset{\dot{}}{\parallel }X\right)$$
57	35 36 56	mpjaodan	$$⊢\left(\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\right)\to Q\underset{\dot{}}{\parallel }X$$
58	57	ex	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left(n\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left(\left(n+1\right)\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)$$
59	13 16 19 22 33 58	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to \left(Q\underset{\dot{}}{\parallel }\left(N\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)$$
60	9 59	mpdan	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left(N\underset{\dot{}}{\times }X\right)\to Q\underset{\dot{}}{\parallel }X\right)$$
61	10 60	mpd	$$⊢\phi \to Q\underset{\dot{}}{\parallel }X$$