aks6d1c2lem4

Description: Claim 2 of Theorem 6.1 AKS, Preparation for injectivity proof. (Contributed by metakunt, 1-May-2025)

	Ref	Expression
Hypotheses	aks6d1c2.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
	aks6d1c2.2	$⊢ P = chr (K)$
	aks6d1c2.3	$⊢ φ \to K \in Field$
	aks6d1c2.4	$⊢ φ \to P \in ℙ$
	aks6d1c2.5	$⊢ φ \to R \in ℕ$
	aks6d1c2.6	$⊢ φ \to N \in ℕ$
	aks6d1c2.7	$⊢ φ \to P ∥ N$
	aks6d1c2.8	$⊢ φ \to N \gcd R = 1$
	aks6d1c2.9	$⊢ φ \to F : (0 \dots A) ⟶ ℕ_{0}$
	aks6d1c2.10	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \cdot_{{mulGrp}_{{Poly}_{1} (K)}} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
	aks6d1c2.11	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c2.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c2.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
	aks6d1c2.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
	aks6d1c2.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks6d1c2.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks6d1c2.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
	aks6d1c2.18	$⊢ B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
	aks6d1c2.19	$⊢ C = E [(0 \dots B) \times (0 \dots B)]$
	aks6d1c2.20	$⊢ φ \to I \in C$
	aks6d1c2.21	$⊢ φ \to J \in C$
	aks6d1c2.22	$⊢ φ \to I < J$
	aks6d1c2.23	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
	aks6d1c2.24	$⊢ X = {var}_{1} (K)$
	aks6d1c2.25	$⊢ S = (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)$
	aks6d1c2.26	$⊢ φ \to U \in ℕ$
	aks6d1c2.27	$⊢ φ \to J = I + U R$
Assertion	aks6d1c2lem4	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c2.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
2		aks6d1c2.2	$⊢ P = chr (K)$
3		aks6d1c2.3	$⊢ φ \to K \in Field$
4		aks6d1c2.4	$⊢ φ \to P \in ℙ$
5		aks6d1c2.5	$⊢ φ \to R \in ℕ$
6		aks6d1c2.6	$⊢ φ \to N \in ℕ$
7		aks6d1c2.7	$⊢ φ \to P ∥ N$
8		aks6d1c2.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c2.9	$⊢ φ \to F : (0 \dots A) ⟶ ℕ_{0}$
10		aks6d1c2.10	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \cdot_{{mulGrp}_{{Poly}_{1} (K)}} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
11		aks6d1c2.11	$⊢ φ \to A \in ℕ_{0}$
12		aks6d1c2.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
13		aks6d1c2.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
14		aks6d1c2.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
15		aks6d1c2.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
16		aks6d1c2.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
17		aks6d1c2.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
18		aks6d1c2.18	$⊢ B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
19		aks6d1c2.19	$⊢ C = E [(0 \dots B) \times (0 \dots B)]$
20		aks6d1c2.20	$⊢ φ \to I \in C$
21		aks6d1c2.21	$⊢ φ \to J \in C$
22		aks6d1c2.22	$⊢ φ \to I < J$
23		aks6d1c2.23	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
24		aks6d1c2.24	$⊢ X = {var}_{1} (K)$
25		aks6d1c2.25	$⊢ S = (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)$
26		aks6d1c2.26	$⊢ φ \to U \in ℕ$
27		aks6d1c2.27	$⊢ φ \to J = I + U R$
28		fvexd	$⊢ φ \to {eval}_{1} (K) (S) \in V$
29		cnvexg	$⊢ {eval}_{1} (K) (S) \in V \to {{eval}_{1} (K) (S)}^{-1} \in V$
30	28 29	syl	$⊢ φ \to {{eval}_{1} (K) (S)}^{-1} \in V$
31	30	imaexd	$⊢ φ \to {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}] \in V$
32		nfv	$⊢ Ⅎ s φ$
33		fvexd	$⊢ (φ \land h \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (G (h)) (M) \in V$
34	33 17	fmptd	$⊢ φ \to H : {ℕ_{0}}^{(0 \dots A)} ⟶ V$
35	34	ffnd	$⊢ φ \to H Fn ({ℕ_{0}}^{(0 \dots A)})$
36	35	fnfund	$⊢ φ \to Fun H$
37	25	a1i	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to S = (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)$
38	37	fveq2d	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (S) = {eval}_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X))$
39	38	fveq1d	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (S) (H (s)) = {eval}_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) (H (s))$
40		eqid	$⊢ {eval}_{1} (K) = {eval}_{1} (K)$
41		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
42		eqid	$⊢ {Base}_{K} = {Base}_{K}$
43		eqid	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{Poly}_{1} (K)}$
44	3	fldcrngd	$⊢ φ \to K \in CRing$
45	44	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to K \in CRing$
46	17	a1i	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
47		simpr	$⊢ ((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land h = s) \to h = s$
48	47	fveq2d	$⊢ ((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land h = s) \to G (h) = G (s)$
49	48	fveq2d	$⊢ ((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land h = s) \to {eval}_{1} (K) (G (h)) = {eval}_{1} (K) (G (s))$
50	49	fveq1d	$⊢ ((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land h = s) \to {eval}_{1} (K) (G (h)) (M) = {eval}_{1} (K) (G (s)) (M)$
51		simpr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to s \in ({ℕ_{0}}^{(0 \dots A)})$
52		fvexd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (G (s)) (M) \in V$
53	46 50 51 52	fvmptd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to H (s) = {eval}_{1} (K) (G (s)) (M)$
54		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
55	54	crngmgp	$⊢ K \in CRing \to {mulGrp}_{K} \in CMnd$
56	44 55	syl	$⊢ φ \to {mulGrp}_{K} \in CMnd$
57	5	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
58		eqid	$⊢ \cdot_{{mulGrp}_{K}} = \cdot_{{mulGrp}_{K}}$
59	56 57 58	isprimroot	$⊢ φ \to (M \in ({mulGrp}_{K} PrimRoots R) \leftrightarrow (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall v \in ℕ_{0} (v \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ v)))$
60	59	biimpd	$⊢ φ \to (M \in ({mulGrp}_{K} PrimRoots R) \to (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall v \in ℕ_{0} (v \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ v)))$
61	16 60	mpd	$⊢ φ \to (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall v \in ℕ_{0} (v \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ v))$
62	61	simp1d	$⊢ φ \to M \in {Base}_{{mulGrp}_{K}}$
63	54 42	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
64	62 63	eleqtrrdi	$⊢ φ \to M \in {Base}_{K}$
65	64	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to M \in {Base}_{K}$
66	3	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to K \in Field$
67	4	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to P \in ℙ$
68	5	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to R \in ℕ$
69	6	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to N \in ℕ$
70	7	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to P ∥ N$
71	8	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to N \gcd R = 1$
72		elmapi	$⊢ s \in ({ℕ_{0}}^{(0 \dots A)}) \to s : (0 \dots A) ⟶ ℕ_{0}$
73	72	adantl	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to s : (0 \dots A) ⟶ ℕ_{0}$
74	11	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to A \in ℕ_{0}$
75		0nn0	$⊢ 0 \in ℕ_{0}$
76	75	a1i	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to 0 \in ℕ_{0}$
77		eqid	$⊢ P^{0} {(\frac{N}{P})}^{0} = P^{0} {(\frac{N}{P})}^{0}$
78	14	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
79	15	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
80	1 2 66 67 68 69 70 71 73 10 74 76 76 77 78 79	aks6d1c1rh	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to P^{0} {(\frac{N}{P})}^{0} \underset{˙}{\sim} G (s)$
81	1 80	aks6d1c1p1rcl	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (P^{0} {(\frac{N}{P})}^{0} \in ℕ \land G (s) \in {Base}_{{Poly}_{1} (K)})$
82	81	simprd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to G (s) \in {Base}_{{Poly}_{1} (K)}$
83	40 41 42 43 45 65 82	fveval1fvcl	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (G (s)) (M) \in {Base}_{K}$
84	53 83	eqeltrd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to H (s) \in {Base}_{K}$
85		eqid	$⊢ {Base}_{{mulGrp}_{{Poly}_{1} (K)}} = {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
86	41	ply1crng	$⊢ K \in CRing \to {Poly}_{1} (K) \in CRing$
87	44 86	syl	$⊢ φ \to {Poly}_{1} (K) \in CRing$
88		eqid	$⊢ {mulGrp}_{{Poly}_{1} (K)} = {mulGrp}_{{Poly}_{1} (K)}$
89	88	crngmgp	$⊢ {Poly}_{1} (K) \in CRing \to {mulGrp}_{{Poly}_{1} (K)} \in CMnd$
90	87 89	syl	$⊢ φ \to {mulGrp}_{{Poly}_{1} (K)} \in CMnd$
91	90	cmnmndd	$⊢ φ \to {mulGrp}_{{Poly}_{1} (K)} \in Mnd$
92		simpr	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to J = r E o$
93	12	a1i	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
94		simprl	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land (k = r \land l = o)) \to k = r$
95	94	oveq2d	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land (k = r \land l = o)) \to P^{k} = P^{r}$
96		simprr	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land (k = r \land l = o)) \to l = o$
97	96	oveq2d	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land (k = r \land l = o)) \to {(\frac{N}{P})}^{l} = {(\frac{N}{P})}^{o}$
98	95 97	oveq12d	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land (k = r \land l = o)) \to P^{k} {(\frac{N}{P})}^{l} = P^{r} {(\frac{N}{P})}^{o}$
99		fz0ssnn0	$⊢ (0 \dots B) \subseteq ℕ_{0}$
100	99	a1i	$⊢ φ \to (0 \dots B) \subseteq ℕ_{0}$
101	100	sselda	$⊢ (φ \land r \in (0 \dots B)) \to r \in ℕ_{0}$
102	101	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to r \in ℕ_{0}$
103	99	sseli	$⊢ o \in (0 \dots B) \to o \in ℕ_{0}$
104	103	adantl	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to o \in ℕ_{0}$
105		ovexd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} {(\frac{N}{P})}^{o} \in V$
106	93 98 102 104 105	ovmpod	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to r E o = P^{r} {(\frac{N}{P})}^{o}$
107		prmnn	$⊢ P \in ℙ \to P \in ℕ$
108	4 107	syl	$⊢ φ \to P \in ℕ$
109	108	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
110	109	adantr	$⊢ (φ \land r \in (0 \dots B)) \to P \in ℕ_{0}$
111	110	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P \in ℕ_{0}$
112	111 102	nn0expcld	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} \in ℕ_{0}$
113	109	nn0zd	$⊢ φ \to P \in ℤ$
114	108	nnne0d	$⊢ φ \to P \neq 0$
115	6	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
116	115	nn0zd	$⊢ φ \to N \in ℤ$
117		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land N \in ℤ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
118	113 114 116 117	syl3anc	$⊢ φ \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
119	7 118	mpbid	$⊢ φ \to \frac{N}{P} \in ℤ$
120	6	nnred	$⊢ φ \to N \in ℝ$
121	108	nnrpd	$⊢ φ \to P \in ℝ^{+}$
122	115	nn0ge0d	$⊢ φ \to 0 \leq N$
123	120 121 122	divge0d	$⊢ φ \to 0 \leq \frac{N}{P}$
124	119 123	jca	$⊢ φ \to (\frac{N}{P} \in ℤ \land 0 \leq \frac{N}{P})$
125		elnn0z	$⊢ \frac{N}{P} \in ℕ_{0} \leftrightarrow (\frac{N}{P} \in ℤ \land 0 \leq \frac{N}{P})$
126	124 125	sylibr	$⊢ φ \to \frac{N}{P} \in ℕ_{0}$
127	126	adantr	$⊢ (φ \land r \in (0 \dots B)) \to \frac{N}{P} \in ℕ_{0}$
128	127	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to \frac{N}{P} \in ℕ_{0}$
129	128 104	nn0expcld	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to {(\frac{N}{P})}^{o} \in ℕ_{0}$
130	112 129	nn0mulcld	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} {(\frac{N}{P})}^{o} \in ℕ_{0}$
131	106 130	eqeltrd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to r E o \in ℕ_{0}$
132	131	adantr	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to r E o \in ℕ_{0}$
133	92 132	eqeltrd	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to J \in ℕ_{0}$
134	19	a1i	$⊢ φ \to C = E [(0 \dots B) \times (0 \dots B)]$
135	21 134	eleqtrd	$⊢ φ \to J \in E [(0 \dots B) \times (0 \dots B)]$
136	6 4 7 12	aks6d1c2p1	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ$
137	136	ffnd	$⊢ φ \to E Fn (ℕ_{0} \times ℕ_{0})$
138	100 100	jca	$⊢ φ \to ((0 \dots B) \subseteq ℕ_{0} \land (0 \dots B) \subseteq ℕ_{0})$
139	18	a1i	$⊢ φ \to B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
140		eqid	$⊢ ℤ / R ℤ = ℤ / R ℤ$
141	6 4 7 5 8 12 13 140	hashscontpowcl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
142	141	nn0red	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ$
143	141	nn0ge0d	$⊢ φ \to 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
144	142 143	resqrtcld	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \in ℝ$
145	144	flcld	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ$
146	142 143	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
147		0zd	$⊢ φ \to 0 \in ℤ$
148		flge	$⊢ (\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \in ℝ \land 0 \in ℤ) \to (0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \leftrightarrow 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
149	144 147 148	syl2anc	$⊢ φ \to (0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \leftrightarrow 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
150	146 149	mpbid	$⊢ φ \to 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
151	145 150	jca	$⊢ φ \to (⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ \land 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
152		elnn0z	$⊢ ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℕ_{0} \leftrightarrow (⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ \land 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
153	151 152	sylibr	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℕ_{0}$
154	139 153	eqeltrd	$⊢ φ \to B \in ℕ_{0}$
155		elnn0z	$⊢ B \in ℕ_{0} \leftrightarrow (B \in ℤ \land 0 \leq B)$
156	154 155	sylib	$⊢ φ \to (B \in ℤ \land 0 \leq B)$
157		0z	$⊢ 0 \in ℤ$
158		eluz1	$⊢ 0 \in ℤ \to (B \in ℤ_{\geq 0} \leftrightarrow (B \in ℤ \land 0 \leq B))$
159	157 158	ax-mp	$⊢ B \in ℤ_{\geq 0} \leftrightarrow (B \in ℤ \land 0 \leq B)$
160	156 159	sylibr	$⊢ φ \to B \in ℤ_{\geq 0}$
161		fzn0	$⊢ (0 \dots B) \neq \emptyset \leftrightarrow B \in ℤ_{\geq 0}$
162	160 161	sylibr	$⊢ φ \to (0 \dots B) \neq \emptyset$
163	162 162	jca	$⊢ φ \to ((0 \dots B) \neq \emptyset \land (0 \dots B) \neq \emptyset)$
164		xpnz	$⊢ ((0 \dots B) \neq \emptyset \land (0 \dots B) \neq \emptyset) \leftrightarrow (0 \dots B) \times (0 \dots B) \neq \emptyset$
165	163 164	sylib	$⊢ φ \to (0 \dots B) \times (0 \dots B) \neq \emptyset$
166		ssxpb	$⊢ (0 \dots B) \times (0 \dots B) \neq \emptyset \to ((0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0} \leftrightarrow ((0 \dots B) \subseteq ℕ_{0} \land (0 \dots B) \subseteq ℕ_{0}))$
167	165 166	syl	$⊢ φ \to ((0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0} \leftrightarrow ((0 \dots B) \subseteq ℕ_{0} \land (0 \dots B) \subseteq ℕ_{0}))$
168	138 167	mpbird	$⊢ φ \to (0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0}$
169		ovelimab	$⊢ (E Fn (ℕ_{0} \times ℕ_{0}) \land (0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0}) \to (J \in E [(0 \dots B) \times (0 \dots B)] \leftrightarrow \exists r \in (0 \dots B) \exists o \in (0 \dots B) J = r E o)$
170	137 168 169	syl2anc	$⊢ φ \to (J \in E [(0 \dots B) \times (0 \dots B)] \leftrightarrow \exists r \in (0 \dots B) \exists o \in (0 \dots B) J = r E o)$
171	135 170	mpbid	$⊢ φ \to \exists r \in (0 \dots B) \exists o \in (0 \dots B) J = r E o$
172	133 171	r19.29vva	$⊢ φ \to J \in ℕ_{0}$
173	44	crngringd	$⊢ φ \to K \in Ring$
174	24 41 43	vr1cl	$⊢ K \in Ring \to X \in {Base}_{{Poly}_{1} (K)}$
175	173 174	syl	$⊢ φ \to X \in {Base}_{{Poly}_{1} (K)}$
176	88 43	mgpbas	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
177	176	eqcomi	$⊢ {Base}_{{mulGrp}_{{Poly}_{1} (K)}} = {Base}_{{Poly}_{1} (K)}$
178	177	eleq2i	$⊢ X \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}} \leftrightarrow X \in {Base}_{{Poly}_{1} (K)}$
179	175 178	sylibr	$⊢ φ \to X \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
180	85 23 91 172 179	mulgnn0cld	$⊢ φ \to J \underset{˙}{\times} X \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
181	180 176	eleqtrrdi	$⊢ φ \to J \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)}$
182	181	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to J \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)}$
183	175	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to X \in {Base}_{{Poly}_{1} (K)}$
184	40 24 42 41 43 45 84	evl1vard	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (X) (H (s)) = H (s))$
185	184	simprd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (X) (H (s)) = H (s)$
186	183 185	jca	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (X) (H (s)) = H (s))$
187	172	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to J \in ℕ_{0}$
188	40 41 42 43 45 84 186 23 58 187	evl1expd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (J \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (J \underset{˙}{\times} X) (H (s)) = J \cdot_{{mulGrp}_{K}} H (s))$
189	188	simprd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (J \underset{˙}{\times} X) (H (s)) = J \cdot_{{mulGrp}_{K}} H (s)$
190	53	oveq2d	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to J \cdot_{{mulGrp}_{K}} H (s) = J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
191	3	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to K \in Field$
192	4	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to P \in ℙ$
193	5	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to R \in ℕ$
194	6	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to N \in ℕ$
195	7	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to P ∥ N$
196	8	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to N \gcd R = 1$
197	9	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to F : (0 \dots A) ⟶ ℕ_{0}$
198	11	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to A \in ℕ_{0}$
199	14	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
200	15	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
201	16	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to M \in ({mulGrp}_{K} PrimRoots R)$
202	20	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I \in C$
203	21	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to J \in C$
204	22	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I < J$
205	26	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to U \in ℕ$
206	27	ad7antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to J = I + U R$
207	51	ad6antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to s \in ({ℕ_{0}}^{(0 \dots A)})$
208		simp-6r	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to r \in (0 \dots B)$
209		simp-5r	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to o \in (0 \dots B)$
210		simp-4r	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to J = r E o$
211		simpllr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to p \in (0 \dots B)$
212		simplr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to q \in (0 \dots B)$
213		simpr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I = p E q$
214		simpr	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I = p E q$
215	12	a1i	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
216		simprl	$⊢ ((((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \land (k = p \land l = q)) \to k = p$
217	216	oveq2d	$⊢ ((((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \land (k = p \land l = q)) \to P^{k} = P^{p}$
218		simprr	$⊢ ((((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \land (k = p \land l = q)) \to l = q$
219	218	oveq2d	$⊢ ((((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \land (k = p \land l = q)) \to {(\frac{N}{P})}^{l} = {(\frac{N}{P})}^{q}$
220	217 219	oveq12d	$⊢ ((((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \land (k = p \land l = q)) \to P^{k} {(\frac{N}{P})}^{l} = P^{p} {(\frac{N}{P})}^{q}$
221	100	sselda	$⊢ (φ \land p \in (0 \dots B)) \to p \in ℕ_{0}$
222	221	adantr	$⊢ ((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \to p \in ℕ_{0}$
223	222	adantr	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to p \in ℕ_{0}$
224	99	sseli	$⊢ q \in (0 \dots B) \to q \in ℕ_{0}$
225	224	adantl	$⊢ ((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \to q \in ℕ_{0}$
226	225	adantr	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to q \in ℕ_{0}$
227		ovexd	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to P^{p} {(\frac{N}{P})}^{q} \in V$
228	215 220 223 226 227	ovmpod	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to p E q = P^{p} {(\frac{N}{P})}^{q}$
229	214 228	eqtrd	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I = P^{p} {(\frac{N}{P})}^{q}$
230	109	ad3antrrr	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to P \in ℕ_{0}$
231	230 223	nn0expcld	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to P^{p} \in ℕ_{0}$
232	126	ad2antrr	$⊢ ((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \to \frac{N}{P} \in ℕ_{0}$
233	232	adantr	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to \frac{N}{P} \in ℕ_{0}$
234	233 226	nn0expcld	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to {(\frac{N}{P})}^{q} \in ℕ_{0}$
235	231 234	nn0mulcld	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to P^{p} {(\frac{N}{P})}^{q} \in ℕ_{0}$
236	229 235	eqeltrd	$⊢ (((φ \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I \in ℕ_{0}$
237	20 134	eleqtrd	$⊢ φ \to I \in E [(0 \dots B) \times (0 \dots B)]$
238		ovelimab	$⊢ (E Fn (ℕ_{0} \times ℕ_{0}) \land (0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0}) \to (I \in E [(0 \dots B) \times (0 \dots B)] \leftrightarrow \exists p \in (0 \dots B) \exists q \in (0 \dots B) I = p E q)$
239	137 168 238	syl2anc	$⊢ φ \to (I \in E [(0 \dots B) \times (0 \dots B)] \leftrightarrow \exists p \in (0 \dots B) \exists q \in (0 \dots B) I = p E q)$
240	237 239	mpbid	$⊢ φ \to \exists p \in (0 \dots B) \exists q \in (0 \dots B) I = p E q$
241	236 240	r19.29vva	$⊢ φ \to I \in ℕ_{0}$
242	241	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to I \in ℕ_{0}$
243	242	ad6antr	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to I \in ℕ_{0}$
244	1 2 191 192 193 194 195 196 197 10 198 12 13 199 200 201 17 18 19 202 203 204 23 24 25 205 206 207 208 209 210 211 212 213 243	aks6d1c2lem3	$⊢ (((((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \land p \in (0 \dots B)) \land q \in (0 \dots B)) \land I = p E q) \to J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
245	240	ad4antr	$⊢ ((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to \exists p \in (0 \dots B) \exists q \in (0 \dots B) I = p E q$
246	244 245	r19.29vva	$⊢ ((((φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
247	171	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to \exists r \in (0 \dots B) \exists o \in (0 \dots B) J = r E o$
248	246 247	r19.29vva	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
249	53	eqcomd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (G (s)) (M) = H (s)$
250	249	oveq2d	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} H (s)$
251	190 248 250	3eqtrd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to J \cdot_{{mulGrp}_{K}} H (s) = I \cdot_{{mulGrp}_{K}} H (s)$
252	40 41 42 43 45 84 186 23 58 242	evl1expd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (I \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) = I \cdot_{{mulGrp}_{K}} H (s))$
253	252	simprd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) = I \cdot_{{mulGrp}_{K}} H (s)$
254	253	eqcomd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to I \cdot_{{mulGrp}_{K}} H (s) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s))$
255	189 251 254	3eqtrd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (J \underset{˙}{\times} X) (H (s)) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s))$
256	182 255	jca	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (J \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (J \underset{˙}{\times} X) (H (s)) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)))$
257	85 23 91 241 179	mulgnn0cld	$⊢ φ \to I \underset{˙}{\times} X \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
258	176	eleq2i	$⊢ I \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)} \leftrightarrow I \underset{˙}{\times} X \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
259	257 258	sylibr	$⊢ φ \to I \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)}$
260	259	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to I \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)}$
261		eqidd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s))$
262	260 261	jca	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to (I \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)))$
263		eqid	$⊢ -_{{Poly}_{1} (K)} = -_{{Poly}_{1} (K)}$
264		eqid	$⊢ -_{K} = -_{K}$
265	40 41 42 43 45 84 256 262 263 264	evl1subd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X) \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) (H (s)) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) -_{K} {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)))$
266	265	simprd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) (H (s)) = {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) -_{K} {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s))$
267	45	crnggrpd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to K \in Grp$
268	40 41 42 43 45 84 260	fveval1fvcl	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) \in {Base}_{K}$
269		eqid	$⊢ 0_{K} = 0_{K}$
270	42 269 264	grpsubid	$⊢ (K \in Grp \land {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) \in {Base}_{K}) \to {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) -_{K} {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) = 0_{K}$
271	267 268 270	syl2anc	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) -_{K} {eval}_{1} (K) (I \underset{˙}{\times} X) (H (s)) = 0_{K}$
272	266 271	eqtrd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) (H (s)) = 0_{K}$
273	39 272	eqtrd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (S) (H (s)) = 0_{K}$
274		fvexd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (S) (H (s)) \in V$
275		elsng	$⊢ {eval}_{1} (K) (S) (H (s)) \in V \to ({eval}_{1} (K) (S) (H (s)) \in \{0_{K}\} \leftrightarrow {eval}_{1} (K) (S) (H (s)) = 0_{K})$
276	274 275	syl	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to ({eval}_{1} (K) (S) (H (s)) \in \{0_{K}\} \leftrightarrow {eval}_{1} (K) (S) (H (s)) = 0_{K})$
277	273 276	mpbird	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (S) (H (s)) \in \{0_{K}\}$
278	87	crnggrpd	$⊢ φ \to {Poly}_{1} (K) \in Grp$
279	43 263	grpsubcl	$⊢ ({Poly}_{1} (K) \in Grp \land J \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)} \land I \underset{˙}{\times} X \in {Base}_{{Poly}_{1} (K)}) \to (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X) \in {Base}_{{Poly}_{1} (K)}$
280	278 181 259 279	syl3anc	$⊢ φ \to (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X) \in {Base}_{{Poly}_{1} (K)}$
281	25 280	eqeltrid	$⊢ φ \to S \in {Base}_{{Poly}_{1} (K)}$
282		eqid	$⊢ K ↑_{𝑠} {Base}_{K} = K ↑_{𝑠} {Base}_{K}$
283	40 41 282 42	evl1rhm	$⊢ K \in CRing \to {eval}_{1} (K) \in ({Poly}_{1} (K) RingHom (K ↑_{𝑠} {Base}_{K}))$
284	44 283	syl	$⊢ φ \to {eval}_{1} (K) \in ({Poly}_{1} (K) RingHom (K ↑_{𝑠} {Base}_{K}))$
285		eqid	$⊢ {Base}_{(K ↑_{𝑠} {Base}_{K})} = {Base}_{(K ↑_{𝑠} {Base}_{K})}$
286	43 285	rhmf	$⊢ {eval}_{1} (K) \in ({Poly}_{1} (K) RingHom (K ↑_{𝑠} {Base}_{K})) \to {eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{(K ↑_{𝑠} {Base}_{K})}$
287	284 286	syl	$⊢ φ \to {eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{(K ↑_{𝑠} {Base}_{K})}$
288	287	ffvelcdmda	$⊢ (φ \land S \in {Base}_{{Poly}_{1} (K)}) \to {eval}_{1} (K) (S) \in {Base}_{(K ↑_{𝑠} {Base}_{K})}$
289	288	ex	$⊢ φ \to (S \in {Base}_{{Poly}_{1} (K)} \to {eval}_{1} (K) (S) \in {Base}_{(K ↑_{𝑠} {Base}_{K})})$
290	281 289	mpd	$⊢ φ \to {eval}_{1} (K) (S) \in {Base}_{(K ↑_{𝑠} {Base}_{K})}$
291		fvexd	$⊢ φ \to {Base}_{K} \in V$
292	282 42	pwsbas	$⊢ (K \in Field \land {Base}_{K} \in V) \to {Base}_{K}^{{Base}_{K}} = {Base}_{(K ↑_{𝑠} {Base}_{K})}$
293	3 291 292	syl2anc	$⊢ φ \to {Base}_{K}^{{Base}_{K}} = {Base}_{(K ↑_{𝑠} {Base}_{K})}$
294	290 293	eleqtrrd	$⊢ φ \to {eval}_{1} (K) (S) \in ({Base}_{K}^{{Base}_{K}})$
295	291 291	elmapd	$⊢ φ \to ({eval}_{1} (K) (S) \in ({Base}_{K}^{{Base}_{K}}) \leftrightarrow {eval}_{1} (K) (S) : {Base}_{K} ⟶ {Base}_{K})$
296	294 295	mpbid	$⊢ φ \to {eval}_{1} (K) (S) : {Base}_{K} ⟶ {Base}_{K}$
297		ffn	$⊢ {eval}_{1} (K) (S) : {Base}_{K} ⟶ {Base}_{K} \to {eval}_{1} (K) (S) Fn {Base}_{K}$
298	296 297	syl	$⊢ φ \to {eval}_{1} (K) (S) Fn {Base}_{K}$
299	298	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (S) Fn {Base}_{K}$
300		fnfun	$⊢ {eval}_{1} (K) (S) Fn {Base}_{K} \to Fun {eval}_{1} (K) (S)$
301	299 300	syl	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to Fun {eval}_{1} (K) (S)$
302		fndm	$⊢ {eval}_{1} (K) (S) Fn {Base}_{K} \to dom {eval}_{1} (K) (S) = {Base}_{K}$
303	298 302	syl	$⊢ φ \to dom {eval}_{1} (K) (S) = {Base}_{K}$
304	303	adantr	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to dom {eval}_{1} (K) (S) = {Base}_{K}$
305	84 304	eleqtrrd	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to H (s) \in dom {eval}_{1} (K) (S)$
306		fvimacnv	$⊢ (Fun {eval}_{1} (K) (S) \land H (s) \in dom {eval}_{1} (K) (S)) \to ({eval}_{1} (K) (S) (H (s)) \in \{0_{K}\} \leftrightarrow H (s) \in {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}])$
307	301 305 306	syl2anc	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to ({eval}_{1} (K) (S) (H (s)) \in \{0_{K}\} \leftrightarrow H (s) \in {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}])$
308	277 307	mpbid	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)})) \to H (s) \in {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]$
309	32 36 308	funimassd	$⊢ φ \to H [{ℕ_{0}}^{(0 \dots A)}] \subseteq {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]$
310	31 309	ssexd	$⊢ φ \to H [{ℕ_{0}}^{(0 \dots A)}] \in V$
311	25	a1i	$⊢ φ \to S = (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)$
312	311	fveq2d	$⊢ φ \to \deg_{1} (K) (S) = \deg_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X))$
313		eqid	$⊢ \deg_{1} (K) = \deg_{1} (K)$
314		isfld	$⊢ K \in Field \leftrightarrow (K \in DivRing \land K \in CRing)$
315	314	biimpi	$⊢ K \in Field \to (K \in DivRing \land K \in CRing)$
316	315	simpld	$⊢ K \in Field \to K \in DivRing$
317		drngnzr	$⊢ K \in DivRing \to K \in NzRing$
318	316 317	syl	$⊢ K \in Field \to K \in NzRing$
319	3 318	syl	$⊢ φ \to K \in NzRing$
320	313 41 24 88 23	deg1pw	$⊢ (K \in NzRing \land I \in ℕ_{0}) \to \deg_{1} (K) (I \underset{˙}{\times} X) = I$
321	319 241 320	syl2anc	$⊢ φ \to \deg_{1} (K) (I \underset{˙}{\times} X) = I$
322	321	eqcomd	$⊢ φ \to I = \deg_{1} (K) (I \underset{˙}{\times} X)$
323	313 41 24 88 23	deg1pw	$⊢ (K \in NzRing \land J \in ℕ_{0}) \to \deg_{1} (K) (J \underset{˙}{\times} X) = J$
324	319 172 323	syl2anc	$⊢ φ \to \deg_{1} (K) (J \underset{˙}{\times} X) = J$
325	324	eqcomd	$⊢ φ \to J = \deg_{1} (K) (J \underset{˙}{\times} X)$
326	22 322 325	3brtr3d	$⊢ φ \to \deg_{1} (K) (I \underset{˙}{\times} X) < \deg_{1} (K) (J \underset{˙}{\times} X)$
327	41 313 173 43 263 181 259 326	deg1sub	$⊢ φ \to \deg_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) = \deg_{1} (K) (J \underset{˙}{\times} X)$
328	312 327	eqtrd	$⊢ φ \to \deg_{1} (K) (S) = \deg_{1} (K) (J \underset{˙}{\times} X)$
329	328 324	eqtrd	$⊢ φ \to \deg_{1} (K) (S) = J$
330	329 172	eqeltrd	$⊢ φ \to \deg_{1} (K) (S) \in ℕ_{0}$
331		eqid	$⊢ 0_{{Poly}_{1} (K)} = 0_{{Poly}_{1} (K)}$
332		fldidom	$⊢ K \in Field \to K \in IDomn$
333	3 332	syl	$⊢ φ \to K \in IDomn$
334	313 41 331 43	deg1nn0clb	$⊢ (K \in Ring \land S \in {Base}_{{Poly}_{1} (K)}) \to (S \neq 0_{{Poly}_{1} (K)} \leftrightarrow \deg_{1} (K) (S) \in ℕ_{0})$
335	173 281 334	syl2anc	$⊢ φ \to (S \neq 0_{{Poly}_{1} (K)} \leftrightarrow \deg_{1} (K) (S) \in ℕ_{0})$
336	330 335	mpbird	$⊢ φ \to S \neq 0_{{Poly}_{1} (K)}$
337	41 43 313 40 269 331 333 281 336	fta1g	$⊢ φ \to \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \leq \deg_{1} (K) (S)$
338		hashbnd	$⊢ ({{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}] \in V \land \deg_{1} (K) (S) \in ℕ_{0} \land \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \leq \deg_{1} (K) (S)) \to {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}] \in Fin$
339	31 330 337 338	syl3anc	$⊢ φ \to {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}] \in Fin$
340		hashcl	$⊢ {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}] \in Fin \to \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \in ℕ_{0}$
341	339 340	syl	$⊢ φ \to \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \in ℕ_{0}$
342		hashss	$⊢ ({{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}] \in V \land H [{ℕ_{0}}^{(0 \dots A)}] \subseteq {{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]) \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\|$
343	31 309 342	syl2anc	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\|$
344		hashbnd	$⊢ (H [{ℕ_{0}}^{(0 \dots A)}] \in V \land \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \in ℕ_{0} \land \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\|) \to H [{ℕ_{0}}^{(0 \dots A)}] \in Fin$
345	310 341 343 344	syl3anc	$⊢ φ \to H [{ℕ_{0}}^{(0 \dots A)}] \in Fin$
346		hashcl	$⊢ H [{ℕ_{0}}^{(0 \dots A)}] \in Fin \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℕ_{0}$
347	345 346	syl	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℕ_{0}$
348	347	nn0red	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℝ$
349	341	nn0red	$⊢ φ \to \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \in ℝ$
350	115 154	nn0expcld	$⊢ φ \to N^{B} \in ℕ_{0}$
351	350	nn0red	$⊢ φ \to N^{B} \in ℝ$
352	172	nn0red	$⊢ φ \to J \in ℝ$
353	324 352	eqeltrd	$⊢ φ \to \deg_{1} (K) (J \underset{˙}{\times} X) \in ℝ$
354	327 353	eqeltrd	$⊢ φ \to \deg_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) \in ℝ$
355	312 354	eqeltrd	$⊢ φ \to \deg_{1} (K) (S) \in ℝ$
356	107	nnred	$⊢ P \in ℙ \to P \in ℝ$
357	4 356	syl	$⊢ φ \to P \in ℝ$
358	357	adantr	$⊢ (φ \land r \in (0 \dots B)) \to P \in ℝ$
359	358	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P \in ℝ$
360	359 102	reexpcld	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} \in ℝ$
361	120 357 114	redivcld	$⊢ φ \to \frac{N}{P} \in ℝ$
362	361	adantr	$⊢ (φ \land r \in (0 \dots B)) \to \frac{N}{P} \in ℝ$
363	362	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to \frac{N}{P} \in ℝ$
364	363 104	reexpcld	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to {(\frac{N}{P})}^{o} \in ℝ$
365	360 364	remulcld	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} {(\frac{N}{P})}^{o} \in ℝ$
366	357 154	reexpcld	$⊢ φ \to P^{B} \in ℝ$
367	366	adantr	$⊢ (φ \land r \in (0 \dots B)) \to P^{B} \in ℝ$
368	361 154	reexpcld	$⊢ φ \to {(\frac{N}{P})}^{B} \in ℝ$
369	368	adantr	$⊢ (φ \land r \in (0 \dots B)) \to {(\frac{N}{P})}^{B} \in ℝ$
370	367 369	remulcld	$⊢ (φ \land r \in (0 \dots B)) \to P^{B} {(\frac{N}{P})}^{B} \in ℝ$
371	370	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{B} {(\frac{N}{P})}^{B} \in ℝ$
372	120 154	reexpcld	$⊢ φ \to N^{B} \in ℝ$
373	372	adantr	$⊢ (φ \land r \in (0 \dots B)) \to N^{B} \in ℝ$
374	373	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to N^{B} \in ℝ$
375	367	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{B} \in ℝ$
376	369	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to {(\frac{N}{P})}^{B} \in ℝ$
377		0red	$⊢ φ \to 0 \in ℝ$
378		1red	$⊢ φ \to 1 \in ℝ$
379		0le1	$⊢ 0 \leq 1$
380	379	a1i	$⊢ φ \to 0 \leq 1$
381		prmgt1	$⊢ P \in ℙ \to 1 < P$
382	4 381	syl	$⊢ φ \to 1 < P$
383	378 357 382	ltled	$⊢ φ \to 1 \leq P$
384	377 378 357 380 383	letrd	$⊢ φ \to 0 \leq P$
385	384	adantr	$⊢ (φ \land r \in (0 \dots B)) \to 0 \leq P$
386	385	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to 0 \leq P$
387	359 102 386	expge0d	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to 0 \leq P^{r}$
388	123	adantr	$⊢ (φ \land r \in (0 \dots B)) \to 0 \leq \frac{N}{P}$
389	388	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to 0 \leq \frac{N}{P}$
390	363 104 389	expge0d	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to 0 \leq {(\frac{N}{P})}^{o}$
391	108	nnge1d	$⊢ φ \to 1 \leq P$
392	391	adantr	$⊢ (φ \land r \in (0 \dots B)) \to 1 \leq P$
393	392	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to 1 \leq P$
394		elfzuz3	$⊢ r \in (0 \dots B) \to B \in ℤ_{\geq r}$
395	394	adantl	$⊢ (φ \land r \in (0 \dots B)) \to B \in ℤ_{\geq r}$
396	395	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to B \in ℤ_{\geq r}$
397	359 393 396	leexp2ad	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} \leq P^{B}$
398	357	recnd	$⊢ φ \to P \in ℂ$
399	398	mullidd	$⊢ φ \to 1 P = P$
400	108	nnzd	$⊢ φ \to P \in ℤ$
401		dvdsle	$⊢ (P \in ℤ \land N \in ℕ) \to (P ∥ N \to P \leq N)$
402	400 6 401	syl2anc	$⊢ φ \to (P ∥ N \to P \leq N)$
403	7 402	mpd	$⊢ φ \to P \leq N$
404	399 403	eqbrtrd	$⊢ φ \to 1 P \leq N$
405	378 120 121	lemuldivd	$⊢ φ \to (1 P \leq N \leftrightarrow 1 \leq \frac{N}{P})$
406	404 405	mpbid	$⊢ φ \to 1 \leq \frac{N}{P}$
407	406	adantr	$⊢ (φ \land r \in (0 \dots B)) \to 1 \leq \frac{N}{P}$
408	407	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to 1 \leq \frac{N}{P}$
409		elfzuz3	$⊢ o \in (0 \dots B) \to B \in ℤ_{\geq o}$
410	409	adantl	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to B \in ℤ_{\geq o}$
411	363 408 410	leexp2ad	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to {(\frac{N}{P})}^{o} \leq {(\frac{N}{P})}^{B}$
412	360 375 364 376 387 390 397 411	lemul12ad	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} {(\frac{N}{P})}^{o} \leq P^{B} {(\frac{N}{P})}^{B}$
413	120	recnd	$⊢ φ \to N \in ℂ$
414	413 398 114	divcan2d	$⊢ φ \to P (\frac{N}{P}) = N$
415	414	eqcomd	$⊢ φ \to N = P (\frac{N}{P})$
416	415	adantr	$⊢ (φ \land r \in (0 \dots B)) \to N = P (\frac{N}{P})$
417	416	adantr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to N = P (\frac{N}{P})$
418	417	oveq1d	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to N^{B} = {P (\frac{N}{P})}^{B}$
419	359	recnd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P \in ℂ$
420	363	recnd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to \frac{N}{P} \in ℂ$
421	154	ad2antrr	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to B \in ℕ_{0}$
422	419 420 421	mulexpd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to {P (\frac{N}{P})}^{B} = P^{B} {(\frac{N}{P})}^{B}$
423	418 422	eqtr2d	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{B} {(\frac{N}{P})}^{B} = N^{B}$
424	374	leidd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to N^{B} \leq N^{B}$
425	423 424	eqbrtrd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{B} {(\frac{N}{P})}^{B} \leq N^{B}$
426	365 371 374 412 425	letrd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to P^{r} {(\frac{N}{P})}^{o} \leq N^{B}$
427	106 426	eqbrtrd	$⊢ ((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \to r E o \leq N^{B}$
428	427	adantr	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to r E o \leq N^{B}$
429	92 428	eqbrtrd	$⊢ (((φ \land r \in (0 \dots B)) \land o \in (0 \dots B)) \land J = r E o) \to J \leq N^{B}$
430	429 171	r19.29vva	$⊢ φ \to J \leq N^{B}$
431	324 430	eqbrtrd	$⊢ φ \to \deg_{1} (K) (J \underset{˙}{\times} X) \leq N^{B}$
432	327 431	eqbrtrd	$⊢ φ \to \deg_{1} (K) ((J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)) \leq N^{B}$
433	312 432	eqbrtrd	$⊢ φ \to \deg_{1} (K) (S) \leq N^{B}$
434	349 355 351 337 433	letrd	$⊢ φ \to \|{{eval}_{1} (K) (S)}^{-1} [\{0_{K}\}]\| \leq N^{B}$
435	348 349 351 343 434	letrd	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$

Metamath Proof Explorer

Theorem aks6d1c2lem4

Proof