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	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in B\wedge \forall y\in \left(V\mathrm{PrimRoots}R\right)e\underset{\dot{}}{\times }O\left(f\right)\left(y\right)=O\left(f\right)\left(e\underset{\dot{}}{\times }y\right)\right)\right\}$$
	aks6d1c1.2	$$⊢S={\mathrm{Poly}}_1\left(K\right)$$
	aks6d1c1.3	$$⊢B={\mathrm{Base}}_S$$
	aks6d1c1.4	$$⊢X={\mathrm{var}}_1\left(K\right)$$
	aks6d1c1.5	$$⊢W={\mathrm{mulGrp}}_S$$
	aks6d1c1.6	$$⊢V={\mathrm{mulGrp}}_K$$
	aks6d1c1.7	$$⊢\underset{\dot{}}{\times }={\cdot }_V$$
	aks6d1c1.8	$$⊢C=\mathrm{algSc}\left(S\right)$$
	aks6d1c1.9	$$⊢D={\cdot }_W$$
	aks6d1c1.10	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c1.11	$$⊢O={\mathrm{eval}}_1\left(K\right)$$
	aks6d1c1.12	$$⊢\underset{\dot{}}{+}={+}_S$$
	aks6d1c1.13	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1c1.14	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c1.15	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c1.16	$$⊢\phi \to N\in \mathbb{N}$$
	aks6d1c1.17	$$⊢\phi \to P\parallel N$$
	aks6d1c1.18	$$⊢\phi \to N\gcd R=1$$
	aks6d1c1p8.1	$$⊢\phi \to E\underset{\dot{}}{\sim }F$$
	aks6d1c1p8.2	$$⊢\phi \to L\in {\mathbb{N}}_0$$
	aks6d1c1p8.3	$$⊢\phi \to E\gcd R=1$$
Assertion	aks6d1c1p8	$$⊢\phi \to E^L\underset{\dot{}}{\sim }F$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in B\wedge \forall y\in \left(V\mathrm{PrimRoots}R\right)e\underset{\dot{}}{\times }O\left(f\right)\left(y\right)=O\left(f\right)\left(e\underset{\dot{}}{\times }y\right)\right)\right\}$$
2		aks6d1c1.2	$$⊢S={\mathrm{Poly}}_1\left(K\right)$$
3		aks6d1c1.3	$$⊢B={\mathrm{Base}}_S$$
4		aks6d1c1.4	$$⊢X={\mathrm{var}}_1\left(K\right)$$
5		aks6d1c1.5	$$⊢W={\mathrm{mulGrp}}_S$$
6		aks6d1c1.6	$$⊢V={\mathrm{mulGrp}}_K$$
7		aks6d1c1.7	$$⊢\underset{\dot{}}{\times }={\cdot }_V$$
8		aks6d1c1.8	$$⊢C=\mathrm{algSc}\left(S\right)$$
9		aks6d1c1.9	$$⊢D={\cdot }_W$$
10		aks6d1c1.10	$$⊢P=\mathrm{chr}\left(K\right)$$
11		aks6d1c1.11	$$⊢O={\mathrm{eval}}_1\left(K\right)$$
12		aks6d1c1.12	$$⊢\underset{\dot{}}{+}={+}_S$$
13		aks6d1c1.13	$$⊢\phi \to K\in \mathrm{Field}$$
14		aks6d1c1.14	$$⊢\phi \to P\in \mathbb{P}$$
15		aks6d1c1.15	$$⊢\phi \to R\in \mathbb{N}$$
16		aks6d1c1.16	$$⊢\phi \to N\in \mathbb{N}$$
17		aks6d1c1.17	$$⊢\phi \to P\parallel N$$
18		aks6d1c1.18	$$⊢\phi \to N\gcd R=1$$
19		aks6d1c1p8.1	$$⊢\phi \to E\underset{\dot{}}{\sim }F$$
20		aks6d1c1p8.2	$$⊢\phi \to L\in {\mathbb{N}}_0$$
21		aks6d1c1p8.3	$$⊢\phi \to E\gcd R=1$$
22		oveq2	$$⊢h=0\to E^h=E^0$$
23	22	breq1d	$$⊢h=0\to \left(E^h\underset{\dot{}}{\sim }F\leftrightarrow E^0\underset{\dot{}}{\sim }F\right)$$
24		oveq2	$$⊢h=i\to E^h=E^i$$
25	24	breq1d	$$⊢h=i\to \left(E^h\underset{\dot{}}{\sim }F\leftrightarrow E^i\underset{\dot{}}{\sim }F\right)$$
26		oveq2	$$⊢h=i+1\to E^h=E^{i+1}$$
27	26	breq1d	$$⊢h=i+1\to \left(E^h\underset{\dot{}}{\sim }F\leftrightarrow E^{i+1}\underset{\dot{}}{\sim }F\right)$$
28		oveq2	$$⊢h=L\to E^h=E^L$$
29	28	breq1d	$$⊢h=L\to \left(E^h\underset{\dot{}}{\sim }F\leftrightarrow E^L\underset{\dot{}}{\sim }F\right)$$
30	1 19	aks6d1c1p1rcl	$$⊢\phi \to \left(E\in \mathbb{N}\wedge F\in B\right)$$
31	30	simpld	$$⊢\phi \to E\in \mathbb{N}$$
32	31	nncnd	$$⊢\phi \to E\in ℂ$$
33	32	exp0d	$$⊢\phi \to E^0=1$$
34		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
35	13	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
36	35	adantr	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to K\in \mathrm{CRing}$$
37	6	crngmgp	$$⊢K\in \mathrm{CRing}\to V\in \mathrm{CMnd}$$
38	35 37	syl	$$⊢\phi \to V\in \mathrm{CMnd}$$
39	15	nnnn0d	$$⊢\phi \to R\in {\mathbb{N}}_0$$
40	38 39 7	isprimroot	$$⊢\phi \to \left(y\in \left(V\mathrm{PrimRoots}R\right)\leftrightarrow \left(y\in {\mathrm{Base}}_V\wedge R\underset{\dot{}}{\times }y=0_V\wedge \forall l\in {\mathbb{N}}_0\left(l\underset{\dot{}}{\times }y=0_V\to R\parallel l\right)\right)\right)$$
41	40	biimpd	$$⊢\phi \to \left(y\in \left(V\mathrm{PrimRoots}R\right)\to \left(y\in {\mathrm{Base}}_V\wedge R\underset{\dot{}}{\times }y=0_V\wedge \forall l\in {\mathbb{N}}_0\left(l\underset{\dot{}}{\times }y=0_V\to R\parallel l\right)\right)\right)$$
42	41	imp	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to \left(y\in {\mathrm{Base}}_V\wedge R\underset{\dot{}}{\times }y=0_V\wedge \forall l\in {\mathbb{N}}_0\left(l\underset{\dot{}}{\times }y=0_V\to R\parallel l\right)\right)$$
43	42	simp1d	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to y\in {\mathrm{Base}}_V$$
44	6 34	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_V$$
45	43 44	eleqtrrdi	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to y\in {\mathrm{Base}}_K$$
46	30	simprd	$$⊢\phi \to F\in B$$
47	46	adantr	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to F\in B$$
48	11 2 34 3 36 45 47	fveval1fvcl	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to O\left(F\right)\left(y\right)\in {\mathrm{Base}}_K$$
49	48 44	eleqtrdi	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to O\left(F\right)\left(y\right)\in {\mathrm{Base}}_V$$
50		eqid	$$⊢{\mathrm{Base}}_V={\mathrm{Base}}_V$$
51	50 7	mulg1	$$⊢O\left(F\right)\left(y\right)\in {\mathrm{Base}}_V\to 1\underset{\dot{}}{\times }O\left(F\right)\left(y\right)=O\left(F\right)\left(y\right)$$
52	49 51	syl	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to 1\underset{\dot{}}{\times }O\left(F\right)\left(y\right)=O\left(F\right)\left(y\right)$$
53	50 7	mulg1	$$⊢y\in {\mathrm{Base}}_V\to 1\underset{\dot{}}{\times }y=y$$
54	43 53	syl	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to 1\underset{\dot{}}{\times }y=y$$
55	54	eqcomd	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to y=1\underset{\dot{}}{\times }y$$
56	55	fveq2d	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to O\left(F\right)\left(y\right)=O\left(F\right)\left(1\underset{\dot{}}{\times }y\right)$$
57	52 56	eqtrd	$$⊢\left(\phi \wedge y\in \left(V\mathrm{PrimRoots}R\right)\right)\to 1\underset{\dot{}}{\times }O\left(F\right)\left(y\right)=O\left(F\right)\left(1\underset{\dot{}}{\times }y\right)$$
58	57	ralrimiva	$$⊢\phi \to \forall y\in \left(V\mathrm{PrimRoots}R\right)1\underset{\dot{}}{\times }O\left(F\right)\left(y\right)=O\left(F\right)\left(1\underset{\dot{}}{\times }y\right)$$
59		1nn	$$⊢1\in \mathbb{N}$$
60	59	a1i	$$⊢\phi \to 1\in \mathbb{N}$$
61	1 46 60	aks6d1c1p1	$$⊢\phi \to \left(1\underset{\dot{}}{\sim }F\leftrightarrow \forall y\in \left(V\mathrm{PrimRoots}R\right)1\underset{\dot{}}{\times }O\left(F\right)\left(y\right)=O\left(F\right)\left(1\underset{\dot{}}{\times }y\right)\right)$$
62	58 61	mpbird	$$⊢\phi \to 1\underset{\dot{}}{\sim }F$$
63	33 62	eqbrtrd	$$⊢\phi \to E^0\underset{\dot{}}{\sim }F$$
64	32	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E\in ℂ$$
65		1nn0	$$⊢1\in {\mathbb{N}}_0$$
66	65	a1i	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to 1\in {\mathbb{N}}_0$$
67		simplr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to i\in {\mathbb{N}}_0$$
68	64 66 67	expaddd	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^{i+1}=E^i{E}^1$$
69	64	exp1d	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^1=E$$
70	69	oveq2d	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^i{E}^1=E^{i}E$$
71	68 70	eqtrd	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^{i+1}=E^{i}E$$
72	13	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to K\in \mathrm{Field}$$
73	14	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to P\in \mathbb{P}$$
74	15	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to R\in \mathbb{N}$$
75	21	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E\gcd R=1$$
76	17	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to P\parallel N$$
77		simpr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^i\underset{\dot{}}{\sim }F$$
78	19	ad2antrr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E\underset{\dot{}}{\sim }F$$
79	1 2 3 4 5 6 7 8 10 11 12 72 73 74 75 76 77 78	aks6d1c1p5	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^{i}E\underset{\dot{}}{\sim }F$$
80	71 79	eqbrtrd	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge E^i\underset{\dot{}}{\sim }F\right)\to E^{i+1}\underset{\dot{}}{\sim }F$$
81	23 25 27 29 63 80	nn0indd	$$⊢\left(\phi \wedge L\in {\mathbb{N}}_0\right)\to E^L\underset{\dot{}}{\sim }F$$
82	20 81	mpdan	$$⊢\phi \to E^L\underset{\dot{}}{\sim }F$$