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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rprmdvdspow.p	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
	rprmdvdspow.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
	rprmdvdspow.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	rprmdvdspow.o	⊢ ↑ = ( .g ‘ 𝑀 )
	rprmdvdspow.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	rprmdvdspow.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	rprmdvdspow.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
	rprmdvdspow.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	rprmdvdspow.1	⊢ ( 𝜑 → 𝑄 ∥ ( 𝑁 ↑ 𝑋 ) )
Assertion	rprmdvdspow	⊢ ( 𝜑 → 𝑄 ∥ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		rprmdvdspow.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rprmdvdspow.p	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3		rprmdvdspow.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		rprmdvdspow.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
5		rprmdvdspow.o	⊢ ↑ = ( .g ‘ 𝑀 )
6		rprmdvdspow.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		rprmdvdspow.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		rprmdvdspow.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
9		rprmdvdspow.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10		rprmdvdspow.1	⊢ ( 𝜑 → 𝑄 ∥ ( 𝑁 ↑ 𝑋 ) )
11		oveq1	⊢ ( 𝑖 = 0 → ( 𝑖 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
12	11	breq2d	⊢ ( 𝑖 = 0 → ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) ↔ 𝑄 ∥ ( 0 ↑ 𝑋 ) ) )
13	12	imbi1d	⊢ ( 𝑖 = 0 → ( ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ↔ ( 𝑄 ∥ ( 0 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) )
14		oveq1	⊢ ( 𝑖 = 𝑛 → ( 𝑖 ↑ 𝑋 ) = ( 𝑛 ↑ 𝑋 ) )
15	14	breq2d	⊢ ( 𝑖 = 𝑛 → ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) ↔ 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) ) )
16	15	imbi1d	⊢ ( 𝑖 = 𝑛 → ( ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ↔ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) )
17		oveq1	⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( 𝑖 ↑ 𝑋 ) = ( ( 𝑛 + 1 ) ↑ 𝑋 ) )
18	17	breq2d	⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) ↔ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) )
19	18	imbi1d	⊢ ( 𝑖 = ( 𝑛 + 1 ) → ( ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ↔ ( 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) )
20		oveq1	⊢ ( 𝑖 = 𝑁 → ( 𝑖 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) )
21	20	breq2d	⊢ ( 𝑖 = 𝑁 → ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) ↔ 𝑄 ∥ ( 𝑁 ↑ 𝑋 ) ) )
22	21	imbi1d	⊢ ( 𝑖 = 𝑁 → ( ( 𝑄 ∥ ( 𝑖 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ↔ ( 𝑄 ∥ ( 𝑁 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) )
23	4 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
24		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
25	4 24	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
26	23 25 5	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑅 ) )
27	7 26	syl	⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑅 ) )
28	27	breq2d	⊢ ( 𝜑 → ( 𝑄 ∥ ( 0 ↑ 𝑋 ) ↔ 𝑄 ∥ ( 1r ‘ 𝑅 ) ) )
29	28	biimpa	⊢ ( ( 𝜑 ∧ 𝑄 ∥ ( 0 ↑ 𝑋 ) ) → 𝑄 ∥ ( 1r ‘ 𝑅 ) )
30	24 3 2 6 8	rprmndvdsr1	⊢ ( 𝜑 → ¬ 𝑄 ∥ ( 1r ‘ 𝑅 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑄 ∥ ( 0 ↑ 𝑋 ) ) → ¬ 𝑄 ∥ ( 1r ‘ 𝑅 ) )
32	29 31	pm2.21dd	⊢ ( ( 𝜑 ∧ 𝑄 ∥ ( 0 ↑ 𝑋 ) ) → 𝑄 ∥ 𝑋 )
33	32	ex	⊢ ( 𝜑 → ( 𝑄 ∥ ( 0 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) )
34		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) ∧ 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) ) → ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) )
35	34	syldbl2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) ∧ 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) ) → 𝑄 ∥ 𝑋 )
36		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) ∧ 𝑄 ∥ 𝑋 ) → 𝑄 ∥ 𝑋 )
37		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
38	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑅 ∈ CRing )
39	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑄 ∈ 𝑃 )
40	6	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
41	4	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
42	40 41	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
43	42	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑀 ∈ Mnd )
44		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑛 ∈ ℕ0 )
45	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
46	23 5 43 44 45	mulgnn0cld	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → ( 𝑛 ↑ 𝑋 ) ∈ 𝐵 )
47	42	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
48		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
49	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
50	4 37	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
51	23 5 50	mulgnn0p1	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑛 + 1 ) ↑ 𝑋 ) = ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) )
52	47 48 49 51	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ↑ 𝑋 ) = ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) )
53	52	breq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ↔ 𝑄 ∥ ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) ) )
54	53	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑄 ∥ ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) )
55	54	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑄 ∥ ( ( 𝑛 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) )
56	1 2 3 37 38 39 46 45 55	rprmdvds	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) ∨ 𝑄 ∥ 𝑋 ) )
57	35 36 56	mpjaodan	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) ∧ 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) ) → 𝑄 ∥ 𝑋 )
58	57	ex	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑄 ∥ ( 𝑛 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) ) → ( 𝑄 ∥ ( ( 𝑛 + 1 ) ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) )
59	13 16 19 22 33 58	nn0indd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑄 ∥ ( 𝑁 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) )
60	9 59	mpdan	⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑁 ↑ 𝑋 ) → 𝑄 ∥ 𝑋 ) )
61	10 60	mpd	⊢ ( 𝜑 → 𝑄 ∥ 𝑋 )