Theorem aks6d1c1p8

Description: If a number E is introspective to F , then so are its powers. (Contributed by metakunt, 30-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c1.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
	aks6d1c1.2	⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
	aks6d1c1.3	⊢ 𝐵 = ( Base ‘ 𝑆 )
	aks6d1c1.4	⊢ 𝑋 = ( var1 ‘ 𝐾 )
	aks6d1c1.5	⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
	aks6d1c1.6	⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
	aks6d1c1.7	⊢ ↑ = ( .g ‘ 𝑉 )
	aks6d1c1.8	⊢ 𝐶 = ( algSc ‘ 𝑆 )
	aks6d1c1.9	⊢ 𝐷 = ( .g ‘ 𝑊 )
	aks6d1c1.10	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks6d1c1.11	⊢ 𝑂 = ( eval1 ‘ 𝐾 )
	aks6d1c1.12	⊢ + = ( +g ‘ 𝑆 )
	aks6d1c1.13	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks6d1c1.14	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c1.15	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	aks6d1c1.16	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	aks6d1c1.17	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c1.18	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	aks6d1c1p8.1	⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
	aks6d1c1p8.2	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
	aks6d1c1p8.3	⊢ ( 𝜑 → ( 𝐸 gcd 𝑅 ) = 1 )
Assertion	aks6d1c1p8	⊢ ( 𝜑 → ( 𝐸 ↑ 𝐿 ) ∼ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
2		aks6d1c1.2	⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
3		aks6d1c1.3	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		aks6d1c1.4	⊢ 𝑋 = ( var1 ‘ 𝐾 )
5		aks6d1c1.5	⊢ 𝑊 = ( mulGrp ‘ 𝑆 )
6		aks6d1c1.6	⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
7		aks6d1c1.7	⊢ ↑ = ( .g ‘ 𝑉 )
8		aks6d1c1.8	⊢ 𝐶 = ( algSc ‘ 𝑆 )
9		aks6d1c1.9	⊢ 𝐷 = ( .g ‘ 𝑊 )
10		aks6d1c1.10	⊢ 𝑃 = ( chr ‘ 𝐾 )
11		aks6d1c1.11	⊢ 𝑂 = ( eval1 ‘ 𝐾 )
12		aks6d1c1.12	⊢ + = ( +g ‘ 𝑆 )
13		aks6d1c1.13	⊢ ( 𝜑 → 𝐾 ∈ Field )
14		aks6d1c1.14	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
15		aks6d1c1.15	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
16		aks6d1c1.16	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
17		aks6d1c1.17	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
18		aks6d1c1.18	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
19		aks6d1c1p8.1	⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
20		aks6d1c1p8.2	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
21		aks6d1c1p8.3	⊢ ( 𝜑 → ( 𝐸 gcd 𝑅 ) = 1 )
22		oveq2	⊢ ( ℎ = 0 → ( 𝐸 ↑ ℎ ) = ( 𝐸 ↑ 0 ) )
23	22	breq1d	⊢ ( ℎ = 0 → ( ( 𝐸 ↑ ℎ ) ∼ 𝐹 ↔ ( 𝐸 ↑ 0 ) ∼ 𝐹 ) )
24		oveq2	⊢ ( ℎ = 𝑖 → ( 𝐸 ↑ ℎ ) = ( 𝐸 ↑ 𝑖 ) )
25	24	breq1d	⊢ ( ℎ = 𝑖 → ( ( 𝐸 ↑ ℎ ) ∼ 𝐹 ↔ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) )
26		oveq2	⊢ ( ℎ = ( 𝑖 + 1 ) → ( 𝐸 ↑ ℎ ) = ( 𝐸 ↑ ( 𝑖 + 1 ) ) )
27	26	breq1d	⊢ ( ℎ = ( 𝑖 + 1 ) → ( ( 𝐸 ↑ ℎ ) ∼ 𝐹 ↔ ( 𝐸 ↑ ( 𝑖 + 1 ) ) ∼ 𝐹 ) )
28		oveq2	⊢ ( ℎ = 𝐿 → ( 𝐸 ↑ ℎ ) = ( 𝐸 ↑ 𝐿 ) )
29	28	breq1d	⊢ ( ℎ = 𝐿 → ( ( 𝐸 ↑ ℎ ) ∼ 𝐹 ↔ ( 𝐸 ↑ 𝐿 ) ∼ 𝐹 ) )
30	1 19	aks6d1c1p1rcl	⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
31	30	simpld	⊢ ( 𝜑 → 𝐸 ∈ ℕ )
32	31	nncnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
33	32	exp0d	⊢ ( 𝜑 → ( 𝐸 ↑ 0 ) = 1 )
34		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
35	13	fldcrngd	⊢ ( 𝜑 → 𝐾 ∈ CRing )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ CRing )
37	6	crngmgp	⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
38	35 37	syl	⊢ ( 𝜑 → 𝑉 ∈ CMnd )
39	15	nnnn0d	⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
40	38 39 7	isprimroot	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
41	40	biimpd	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
42	41	imp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) )
43	42	simp1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
44	6 34	mgpbas	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
45	43 44	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
46	30	simprd	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐹 ∈ 𝐵 )
48	11 2 34 3 36 45 47	fveval1fvcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
49	48 44	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
50		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
51	50 7	mulg1	⊢ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑉 ) → ( 1 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
52	49 51	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
53	50 7	mulg1	⊢ ( 𝑦 ∈ ( Base ‘ 𝑉 ) → ( 1 ↑ 𝑦 ) = 𝑦 )
54	43 53	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1 ↑ 𝑦 ) = 𝑦 )
55	54	eqcomd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 = ( 1 ↑ 𝑦 ) )
56	55	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 1 ↑ 𝑦 ) ) )
57	52 56	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 1 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 1 ↑ 𝑦 ) ) )
58	57	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 1 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 1 ↑ 𝑦 ) ) )
59		1nn	⊢ 1 ∈ ℕ
60	59	a1i	⊢ ( 𝜑 → 1 ∈ ℕ )
61	1 46 60	aks6d1c1p1	⊢ ( 𝜑 → ( 1 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 1 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 1 ↑ 𝑦 ) ) ) )
62	58 61	mpbird	⊢ ( 𝜑 → 1 ∼ 𝐹 )
63	33 62	eqbrtrd	⊢ ( 𝜑 → ( 𝐸 ↑ 0 ) ∼ 𝐹 )
64	32	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝐸 ∈ ℂ )
65		1nn0	⊢ 1 ∈ ℕ0
66	65	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 1 ∈ ℕ0 )
67		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝑖 ∈ ℕ0 )
68	64 66 67	expaddd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( 𝐸 ↑ ( 𝑖 + 1 ) ) = ( ( 𝐸 ↑ 𝑖 ) · ( 𝐸 ↑ 1 ) ) )
69	64	exp1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( 𝐸 ↑ 1 ) = 𝐸 )
70	69	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( ( 𝐸 ↑ 𝑖 ) · ( 𝐸 ↑ 1 ) ) = ( ( 𝐸 ↑ 𝑖 ) · 𝐸 ) )
71	68 70	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( 𝐸 ↑ ( 𝑖 + 1 ) ) = ( ( 𝐸 ↑ 𝑖 ) · 𝐸 ) )
72	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝐾 ∈ Field )
73	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝑃 ∈ ℙ )
74	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝑅 ∈ ℕ )
75	21	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( 𝐸 gcd 𝑅 ) = 1 )
76	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝑃 ∥ 𝑁 )
77		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 )
78	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → 𝐸 ∼ 𝐹 )
79	1 2 3 4 5 6 7 8 10 11 12 72 73 74 75 76 77 78	aks6d1c1p5	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( ( 𝐸 ↑ 𝑖 ) · 𝐸 ) ∼ 𝐹 )
80	71 79	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ ( 𝐸 ↑ 𝑖 ) ∼ 𝐹 ) → ( 𝐸 ↑ ( 𝑖 + 1 ) ) ∼ 𝐹 )
81	23 25 27 29 63 80	nn0indd	⊢ ( ( 𝜑 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐸 ↑ 𝐿 ) ∼ 𝐹 )
82	20 81	mpdan	⊢ ( 𝜑 → ( 𝐸 ↑ 𝐿 ) ∼ 𝐹 )