aks6d1c6lem3

	Ref	Expression
Hypotheses	aks6d1c6.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))\}$
	aks6d1c6.2	$⊢ P = chr (K)$
	aks6d1c6.3	$⊢ φ \to K \in Field$
	aks6d1c6.4	$⊢ φ \to P \in ℙ$
	aks6d1c6.5	$⊢ φ \to R \in ℕ$
	aks6d1c6.6	$⊢ φ \to N \in ℕ$
	aks6d1c6.7	$⊢ φ \to P ∥ N$
	aks6d1c6.8	$⊢ φ \to N \gcd R = 1$
	aks6d1c6.9	$⊢ φ \to A < P$
	aks6d1c6.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)))))$
	aks6d1c6.11	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c6.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c6.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
	aks6d1c6.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
	aks6d1c6.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks6d1c6.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks6d1c6.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
	aks6d1c6.18	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
	aks6d1c6.19	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
	aks6d1c6lem3.1	$⊢ J = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
	aks6d1c6lem3.2	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [ℕ_{0} \times ℕ_{0}]\|$
Assertion	aks6d1c6lem3	$⊢ φ \to (\binom{D + A}{D - 1}) \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6.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		aks6d1c6.2	$⊢ P = chr (K)$
3		aks6d1c6.3	$⊢ φ \to K \in Field$
4		aks6d1c6.4	$⊢ φ \to P \in ℙ$
5		aks6d1c6.5	$⊢ φ \to R \in ℕ$
6		aks6d1c6.6	$⊢ φ \to N \in ℕ$
7		aks6d1c6.7	$⊢ φ \to P ∥ N$
8		aks6d1c6.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c6.9	$⊢ φ \to A < P$
10		aks6d1c6.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		aks6d1c6.11	$⊢ φ \to A \in ℕ_{0}$
12		aks6d1c6.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
13		aks6d1c6.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
14		aks6d1c6.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		aks6d1c6.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
16		aks6d1c6.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
17		aks6d1c6.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
18		aks6d1c6.18	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
19		aks6d1c6.19	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
20		aks6d1c6lem3.1	$⊢ J = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
21		aks6d1c6lem3.2	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [ℕ_{0} \times ℕ_{0}]\|$
22		eqid	$⊢ ℤ / R ℤ = ℤ / R ℤ$
23	6 4 7 5 8 12 13 22	hashscontpowcl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
24	18 23	eqeltrid	$⊢ φ \to D \in ℕ_{0}$
25	24	nn0zd	$⊢ φ \to D \in ℤ$
26	25	zcnd	$⊢ φ \to D \in ℂ$
27		1cnd	$⊢ φ \to 1 \in ℂ$
28	11	nn0cnd	$⊢ φ \to A \in ℂ$
29	26 27 28	nppcan3d	$⊢ φ \to (D - 1) + A + 1 = D + A$
30	29	eqcomd	$⊢ φ \to D + A = (D - 1) + A + 1$
31		hashfz0	$⊢ A \in ℕ_{0} \to \|(0 \dots A)\| = A + 1$
32	11 31	syl	$⊢ φ \to \|(0 \dots A)\| = A + 1$
33	32	eqcomd	$⊢ φ \to A + 1 = \|(0 \dots A)\|$
34	33	oveq2d	$⊢ φ \to (D - 1) + A + 1 = D - 1 + \|(0 \dots A)\|$
35	30 34	eqtrd	$⊢ φ \to D + A = D - 1 + \|(0 \dots A)\|$
36		1zzd	$⊢ φ \to 1 \in ℤ$
37	25 36	zsubcld	$⊢ φ \to D - 1 \in ℤ$
38		0p1e1	$⊢ 0 + 1 = 1$
39	38	a1i	$⊢ φ \to 0 + 1 = 1$
40		fvexd	$⊢ φ \to ℤRHom (ℤ / R ℤ) \in V$
41	13 40	eqeltrid	$⊢ φ \to L \in V$
42	41	imaexd	$⊢ φ \to L [E [ℕ_{0} \times ℕ_{0}]] \in V$
43	11	ne0d	$⊢ φ \to ℕ_{0} \neq \emptyset$
44	43 43	jca	$⊢ φ \to (ℕ_{0} \neq \emptyset \land ℕ_{0} \neq \emptyset)$
45		xpnz	$⊢ (ℕ_{0} \neq \emptyset \land ℕ_{0} \neq \emptyset) \leftrightarrow ℕ_{0} \times ℕ_{0} \neq \emptyset$
46	44 45	sylib	$⊢ φ \to ℕ_{0} \times ℕ_{0} \neq \emptyset$
47		ovexd	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to P^{k} {(\frac{N}{P})}^{l} \in V$
48	47	ralrimiva	$⊢ (φ \land k \in ℕ_{0}) \to \forall l \in ℕ_{0} P^{k} {(\frac{N}{P})}^{l} \in V$
49	48	ralrimiva	$⊢ φ \to \forall k \in ℕ_{0} \forall l \in ℕ_{0} P^{k} {(\frac{N}{P})}^{l} \in V$
50	12	fnmpo	$⊢ \forall k \in ℕ_{0} \forall l \in ℕ_{0} P^{k} {(\frac{N}{P})}^{l} \in V \to E Fn (ℕ_{0} \times ℕ_{0})$
51	49 50	syl	$⊢ φ \to E Fn (ℕ_{0} \times ℕ_{0})$
52		ssidd	$⊢ φ \to ℕ_{0} \times ℕ_{0} \subseteq ℕ_{0} \times ℕ_{0}$
53		fnimaeq0	$⊢ (E Fn (ℕ_{0} \times ℕ_{0}) \land ℕ_{0} \times ℕ_{0} \subseteq ℕ_{0} \times ℕ_{0}) \to (E [ℕ_{0} \times ℕ_{0}] = \emptyset \leftrightarrow ℕ_{0} \times ℕ_{0} = \emptyset)$
54	51 52 53	syl2anc	$⊢ φ \to (E [ℕ_{0} \times ℕ_{0}] = \emptyset \leftrightarrow ℕ_{0} \times ℕ_{0} = \emptyset)$
55	54	necon3bid	$⊢ φ \to (E [ℕ_{0} \times ℕ_{0}] \neq \emptyset \leftrightarrow ℕ_{0} \times ℕ_{0} \neq \emptyset)$
56	46 55	mpbird	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \neq \emptyset$
57	5	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
58	22	zncrng	$⊢ R \in ℕ_{0} \to ℤ / R ℤ \in CRing$
59	57 58	syl	$⊢ φ \to ℤ / R ℤ \in CRing$
60		crngring	$⊢ ℤ / R ℤ \in CRing \to ℤ / R ℤ \in Ring$
61	13	zrhrhm	$⊢ ℤ / R ℤ \in Ring \to L \in (ℤ_{ring} RingHom ℤ / R ℤ)$
62		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
63		eqid	$⊢ {Base}_{ℤ / R ℤ} = {Base}_{ℤ / R ℤ}$
64	62 63	rhmf	$⊢ L \in (ℤ_{ring} RingHom ℤ / R ℤ) \to L : ℤ ⟶ {Base}_{ℤ / R ℤ}$
65	59 60 61 64	4syl	$⊢ φ \to L : ℤ ⟶ {Base}_{ℤ / R ℤ}$
66	65	ffnd	$⊢ φ \to L Fn ℤ$
67	12	a1i	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
68		simprl	$⊢ (((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \land (k = x \land l = y)) \to k = x$
69	68	oveq2d	$⊢ (((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \land (k = x \land l = y)) \to P^{k} = P^{x}$
70		simprr	$⊢ (((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \land (k = x \land l = y)) \to l = y$
71	70	oveq2d	$⊢ (((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \land (k = x \land l = y)) \to {(\frac{N}{P})}^{l} = {(\frac{N}{P})}^{y}$
72	69 71	oveq12d	$⊢ (((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \land (k = x \land l = y)) \to P^{k} {(\frac{N}{P})}^{l} = P^{x} {(\frac{N}{P})}^{y}$
73		simplr	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to x \in ℕ_{0}$
74		simpr	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to y \in ℕ_{0}$
75		ovexd	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P^{x} {(\frac{N}{P})}^{y} \in V$
76	67 72 73 74 75	ovmpod	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to x E y = P^{x} {(\frac{N}{P})}^{y}$
77	4	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P \in ℙ$
78		prmnn	$⊢ P \in ℙ \to P \in ℕ$
79	77 78	syl	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P \in ℕ$
80	79	nnzd	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P \in ℤ$
81	80 73	zexpcld	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P^{x} \in ℤ$
82	7	ad2antrr	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P ∥ N$
83	79	nnne0d	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P \neq 0$
84	6	nnzd	$⊢ φ \to N \in ℤ$
85	84	adantr	$⊢ (φ \land x \in ℕ_{0}) \to N \in ℤ$
86	85	adantr	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to N \in ℤ$
87		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land N \in ℤ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
88	80 83 86 87	syl3anc	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
89	82 88	mpbid	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to \frac{N}{P} \in ℤ$
90	89 74	zexpcld	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to {(\frac{N}{P})}^{y} \in ℤ$
91	81 90	zmulcld	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to P^{x} {(\frac{N}{P})}^{y} \in ℤ$
92	76 91	eqeltrd	$⊢ ((φ \land x \in ℕ_{0}) \land y \in ℕ_{0}) \to x E y \in ℤ$
93	92	ralrimiva	$⊢ (φ \land x \in ℕ_{0}) \to \forall y \in ℕ_{0} x E y \in ℤ$
94	93	ralrimiva	$⊢ φ \to \forall x \in ℕ_{0} \forall y \in ℕ_{0} x E y \in ℤ$
95	51 94	jca	$⊢ φ \to (E Fn (ℕ_{0} \times ℕ_{0}) \land \forall x \in ℕ_{0} \forall y \in ℕ_{0} x E y \in ℤ)$
96		ffnov	$⊢ E : ℕ_{0} \times ℕ_{0} ⟶ ℤ \leftrightarrow (E Fn (ℕ_{0} \times ℕ_{0}) \land \forall x \in ℕ_{0} \forall y \in ℕ_{0} x E y \in ℤ)$
97	95 96	sylibr	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℤ$
98		frn	$⊢ E : ℕ_{0} \times ℕ_{0} ⟶ ℤ \to ran E \subseteq ℤ$
99	97 98	syl	$⊢ φ \to ran E \subseteq ℤ$
100		fnima	$⊢ E Fn (ℕ_{0} \times ℕ_{0}) \to E [ℕ_{0} \times ℕ_{0}] = ran E$
101	51 100	syl	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] = ran E$
102	101	sseq1d	$⊢ φ \to (E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ \leftrightarrow ran E \subseteq ℤ)$
103	99 102	mpbird	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ$
104		fnimaeq0	$⊢ (L Fn ℤ \land E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ) \to (L [E [ℕ_{0} \times ℕ_{0}]] = \emptyset \leftrightarrow E [ℕ_{0} \times ℕ_{0}] = \emptyset)$
105	66 103 104	syl2anc	$⊢ φ \to (L [E [ℕ_{0} \times ℕ_{0}]] = \emptyset \leftrightarrow E [ℕ_{0} \times ℕ_{0}] = \emptyset)$
106	105	necon3bid	$⊢ φ \to (L [E [ℕ_{0} \times ℕ_{0}]] \neq \emptyset \leftrightarrow E [ℕ_{0} \times ℕ_{0}] \neq \emptyset)$
107	56 106	mpbird	$⊢ φ \to L [E [ℕ_{0} \times ℕ_{0}]] \neq \emptyset$
108		hashge1	$⊢ (L [E [ℕ_{0} \times ℕ_{0}]] \in V \land L [E [ℕ_{0} \times ℕ_{0}]] \neq \emptyset) \to 1 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
109	18	eqcomi	$⊢ \|L [E [ℕ_{0} \times ℕ_{0}]]\| = D$
110	109	a1i	$⊢ (L [E [ℕ_{0} \times ℕ_{0}]] \in V \land L [E [ℕ_{0} \times ℕ_{0}]] \neq \emptyset) \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| = D$
111	108 110	breqtrd	$⊢ (L [E [ℕ_{0} \times ℕ_{0}]] \in V \land L [E [ℕ_{0} \times ℕ_{0}]] \neq \emptyset) \to 1 \leq D$
112	42 107 111	syl2anc	$⊢ φ \to 1 \leq D$
113	39 112	eqbrtrd	$⊢ φ \to 0 + 1 \leq D$
114		0red	$⊢ φ \to 0 \in ℝ$
115		1red	$⊢ φ \to 1 \in ℝ$
116	24	nn0red	$⊢ φ \to D \in ℝ$
117		leaddsub	$⊢ (0 \in ℝ \land 1 \in ℝ \land D \in ℝ) \to (0 + 1 \leq D \leftrightarrow 0 \leq D - 1)$
118	114 115 116 117	syl3anc	$⊢ φ \to (0 + 1 \leq D \leftrightarrow 0 \leq D - 1)$
119	113 118	mpbid	$⊢ φ \to 0 \leq D - 1$
120	37 119	jca	$⊢ φ \to (D - 1 \in ℤ \land 0 \leq D - 1)$
121		elnn0z	$⊢ D - 1 \in ℕ_{0} \leftrightarrow (D - 1 \in ℤ \land 0 \leq D - 1)$
122	120 121	sylibr	$⊢ φ \to D - 1 \in ℕ_{0}$
123		fzfid	$⊢ φ \to (0 \dots A) \in Fin$
124		hashcl	$⊢ (0 \dots A) \in Fin \to \|(0 \dots A)\| \in ℕ_{0}$
125	123 124	syl	$⊢ φ \to \|(0 \dots A)\| \in ℕ_{0}$
126	122 125	nn0addcld	$⊢ φ \to D - 1 + \|(0 \dots A)\| \in ℕ_{0}$
127	35 126	eqeltrd	$⊢ φ \to D + A \in ℕ_{0}$
128		bccl	$⊢ (D + A \in ℕ_{0} \land D - 1 \in ℤ) \to (\binom{D + A}{D - 1}) \in ℕ_{0}$
129	127 37 128	syl2anc	$⊢ φ \to (\binom{D + A}{D - 1}) \in ℕ_{0}$
130	129	nn0red	$⊢ φ \to (\binom{D + A}{D - 1}) \in ℝ$
131	130	rexrd	$⊢ φ \to (\binom{D + A}{D - 1}) \in ℝ^{*}$
132		ovexd	$⊢ φ \to {ℕ_{0}}^{(0 \dots A)} \in V$
133	132	mptexd	$⊢ φ \to (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M)) \in V$
134	17 133	eqeltrid	$⊢ φ \to H \in V$
135	134	imaexd	$⊢ φ \to H [{ℕ_{0}}^{(0 \dots A)}] \in V$
136		simprl	$⊢ (φ \land (w \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} w (t) \leq D - 1)) \to w \in ({ℕ_{0}}^{(0 \dots A)})$
137	136	ex	$⊢ φ \to ((w \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} w (t) \leq D - 1) \to w \in ({ℕ_{0}}^{(0 \dots A)}))$
138		simpl	$⊢ (s = w \land t \in (0 \dots A)) \to s = w$
139	138	fveq1d	$⊢ (s = w \land t \in (0 \dots A)) \to s (t) = w (t)$
140	139	sumeq2dv	$⊢ s = w \to \sum_{t = 0}^{A} s (t) = \sum_{t = 0}^{A} w (t)$
141	140	breq1d	$⊢ s = w \to (\sum_{t = 0}^{A} s (t) \leq D - 1 \leftrightarrow \sum_{t = 0}^{A} w (t) \leq D - 1)$
142	141	elrab	$⊢ w \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \leftrightarrow (w \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} w (t) \leq D - 1)$
143	142	a1i	$⊢ φ \to (w \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \leftrightarrow (w \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} w (t) \leq D - 1))$
144	143	biimpd	$⊢ φ \to (w \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to (w \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} w (t) \leq D - 1))$
145	144	imim1d	$⊢ φ \to (((w \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} w (t) \leq D - 1) \to w \in ({ℕ_{0}}^{(0 \dots A)})) \to (w \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to w \in ({ℕ_{0}}^{(0 \dots A)})))$
146	137 145	mpd	$⊢ φ \to (w \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to w \in ({ℕ_{0}}^{(0 \dots A)}))$
147	146	ssrdv	$⊢ φ \to \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \subseteq {ℕ_{0}}^{(0 \dots A)}$
148	19	a1i	$⊢ φ \to S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
149	148	sseq1d	$⊢ φ \to (S \subseteq {ℕ_{0}}^{(0 \dots A)} \leftrightarrow \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \subseteq {ℕ_{0}}^{(0 \dots A)})$
150	147 149	mpbird	$⊢ φ \to S \subseteq {ℕ_{0}}^{(0 \dots A)}$
151		imass2	$⊢ S \subseteq {ℕ_{0}}^{(0 \dots A)} \to H [S] \subseteq H [{ℕ_{0}}^{(0 \dots A)}]$
152	150 151	syl	$⊢ φ \to H [S] \subseteq H [{ℕ_{0}}^{(0 \dots A)}]$
153	135 152	ssexd	$⊢ φ \to H [S] \in V$
154		hashxnn0	$⊢ H [S] \in V \to \|H [S]\| \in ℕ_{0}^{*}$
155	153 154	syl	$⊢ φ \to \|H [S]\| \in ℕ_{0}^{*}$
156		xnn0xr	$⊢ \|H [S]\| \in ℕ_{0}^{} \to \|H [S]\| \in ℝ^{}$
157	155 156	syl	$⊢ φ \to \|H [S]\| \in ℝ^{*}$
158		hashxnn0	$⊢ H [{ℕ_{0}}^{(0 \dots A)}] \in V \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℕ_{0}^{*}$
159	135 158	syl	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℕ_{0}^{*}$
160		xnn0xr	$⊢ \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℕ_{0}^{} \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℝ^{}$
161	159 160	syl	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℝ^{*}$
162	122	nn0cnd	$⊢ φ \to D - 1 \in ℂ$
163	125	nn0cnd	$⊢ φ \to \|(0 \dots A)\| \in ℂ$
164	162 163	pncand	$⊢ φ \to (D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\| = D - 1$
165	164	eqcomd	$⊢ φ \to D - 1 = (D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\|$
166	35 165	oveq12d	$⊢ φ \to (\binom{D + A}{D - 1}) = (\binom{D - 1 + \|(0 \dots A)\|}{(D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\|})$
167	11	nn0ge0d	$⊢ φ \to 0 \leq A$
168		0zd	$⊢ φ \to 0 \in ℤ$
169	11	nn0zd	$⊢ φ \to A \in ℤ$
170		eluz	$⊢ (0 \in ℤ \land A \in ℤ) \to (A \in ℤ_{\geq 0} \leftrightarrow 0 \leq A)$
171	168 169 170	syl2anc	$⊢ φ \to (A \in ℤ_{\geq 0} \leftrightarrow 0 \leq A)$
172	167 171	mpbird	$⊢ φ \to A \in ℤ_{\geq 0}$
173		fzn0	$⊢ (0 \dots A) \neq \emptyset \leftrightarrow A \in ℤ_{\geq 0}$
174	172 173	sylibr	$⊢ φ \to (0 \dots A) \neq \emptyset$
175	122 123 174 19	sticksstones23	$⊢ φ \to \|S\| = (\binom{D - 1 + \|(0 \dots A)\|}{\|(0 \dots A)\|})$
176	125	nn0zd	$⊢ φ \to \|(0 \dots A)\| \in ℤ$
177		bccmpl	$⊢ (D - 1 + \|(0 \dots A)\| \in ℕ_{0} \land \|(0 \dots A)\| \in ℤ) \to (\binom{D - 1 + \|(0 \dots A)\|}{\|(0 \dots A)\|}) = (\binom{D - 1 + \|(0 \dots A)\|}{(D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\|})$
178	126 176 177	syl2anc	$⊢ φ \to (\binom{D - 1 + \|(0 \dots A)\|}{\|(0 \dots A)\|}) = (\binom{D - 1 + \|(0 \dots A)\|}{(D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\|})$
179	175 178	eqtrd	$⊢ φ \to \|S\| = (\binom{D - 1 + \|(0 \dots A)\|}{(D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\|})$
180	179	eqcomd	$⊢ φ \to (\binom{D - 1 + \|(0 \dots A)\|}{(D - 1) + \|(0 \dots A)\| - \|(0 \dots A)\|}) = \|S\|$
181	166 180	eqtrd	$⊢ φ \to (\binom{D + A}{D - 1}) = \|S\|$
182	181	adantr	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to (\binom{D + A}{D - 1}) = \|S\|$
183	17	a1i	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
184		ovexd	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to {ℕ_{0}}^{(0 \dots A)} \in V$
185	184	mptexd	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M)) \in V$
186	183 185	eqeltrd	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to H \in V$
187	186	resexd	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to {H ↾}_{S} \in V$
188	186	imaexd	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to H [S] \in V$
189		simpr	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]$
190		hashf1dmcdm	$⊢ ({H ↾}_{S} \in V \land H [S] \in V \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to \|S\| \leq \|H [S]\|$
191	187 188 189 190	syl3anc	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to \|S\| \leq \|H [S]\|$
192	182 191	eqbrtrd	$⊢ (φ \land ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|$
193	17	a1i	$⊢ (φ \land j \in S) \to H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
194		simpr	$⊢ ((φ \land j \in S) \land h = j) \to h = j$
195	194	fveq2d	$⊢ ((φ \land j \in S) \land h = j) \to G (h) = G (j)$
196	195	fveq2d	$⊢ ((φ \land j \in S) \land h = j) \to {eval}_{1} (K) (G (h)) = {eval}_{1} (K) (G (j))$
197	196	fveq1d	$⊢ ((φ \land j \in S) \land h = j) \to {eval}_{1} (K) (G (h)) (M) = {eval}_{1} (K) (G (j)) (M)$
198		simp2	$⊢ (φ \land s \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} s (t) \leq D - 1) \to s \in ({ℕ_{0}}^{(0 \dots A)})$
199	198	rabssdv	$⊢ φ \to \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \subseteq {ℕ_{0}}^{(0 \dots A)}$
200	19 199	eqsstrid	$⊢ φ \to S \subseteq {ℕ_{0}}^{(0 \dots A)}$
201	200	sselda	$⊢ (φ \land j \in S) \to j \in ({ℕ_{0}}^{(0 \dots A)})$
202		fvexd	$⊢ (φ \land j \in S) \to {eval}_{1} (K) (G (j)) (M) \in V$
203	193 197 201 202	fvmptd	$⊢ (φ \land j \in S) \to H (j) = {eval}_{1} (K) (G (j)) (M)$
204		eqid	$⊢ {eval}_{1} (K) = {eval}_{1} (K)$
205		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
206		eqid	$⊢ {Base}_{K} = {Base}_{K}$
207		eqid	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{Poly}_{1} (K)}$
208	3	fldcrngd	$⊢ φ \to K \in CRing$
209	208	adantr	$⊢ (φ \land j \in S) \to K \in CRing$
210		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
211	210	crngmgp	$⊢ K \in CRing \to {mulGrp}_{K} \in CMnd$
212	208 211	syl	$⊢ φ \to {mulGrp}_{K} \in CMnd$
213		eqid	$⊢ \cdot_{{mulGrp}_{K}} = \cdot_{{mulGrp}_{K}}$
214	212 57 213	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)))$
215	214	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)))$
216	16 215	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))$
217	216	simp1d	$⊢ φ \to M \in {Base}_{{mulGrp}_{K}}$
218	210 206	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
219	218	eqcomi	$⊢ {Base}_{{mulGrp}_{K}} = {Base}_{K}$
220	217 219	eleqtrdi	$⊢ φ \to M \in {Base}_{K}$
221	220	adantr	$⊢ (φ \land j \in S) \to M \in {Base}_{K}$
222		eqid	$⊢ {var}_{1} (K) = {var}_{1} (K)$
223		eqid	$⊢ \cdot_{{mulGrp}_{{Poly}_{1} (K)}} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
224	3 4 2 11 9 222 223 10	aks6d1c5lem0	$⊢ φ \to G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)}$
225	224	adantr	$⊢ (φ \land j \in S) \to G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)}$
226	225 201	ffvelcdmd	$⊢ (φ \land j \in S) \to G (j) \in {Base}_{{Poly}_{1} (K)}$
227	204 205 206 207 209 221 226	fveval1fvcl	$⊢ (φ \land j \in S) \to {eval}_{1} (K) (G (j)) (M) \in {Base}_{K}$
228	203 227	eqeltrd	$⊢ (φ \land j \in S) \to H (j) \in {Base}_{K}$
229		eqid	$⊢ (j \in S ⟼ H (j)) = (j \in S ⟼ H (j))$
230	228 229	fmptd	$⊢ φ \to (j \in S ⟼ H (j)) : S ⟶ {Base}_{K}$
231		fvexd	$⊢ (φ \land h \in ({ℕ_{0}}^{(0 \dots A)})) \to {eval}_{1} (K) (G (h)) (M) \in V$
232	231 17	fmptd	$⊢ φ \to H : {ℕ_{0}}^{(0 \dots A)} ⟶ V$
233	232 200	feqresmpt	$⊢ φ \to {H ↾}_{S} = (j \in S ⟼ H (j))$
234	233	feq1d	$⊢ φ \to (({H ↾}_{S}) : S ⟶ {Base}_{K} \leftrightarrow (j \in S ⟼ H (j)) : S ⟶ {Base}_{K})$
235	230 234	mpbird	$⊢ φ \to ({H ↾}_{S}) : S ⟶ {Base}_{K}$
236		ffrn	$⊢ ({H ↾}_{S}) : S ⟶ {Base}_{K} \to ({H ↾}_{S}) : S ⟶ ran ({H ↾}_{S})$
237	235 236	syl	$⊢ φ \to ({H ↾}_{S}) : S ⟶ ran ({H ↾}_{S})$
238		df-ima	$⊢ H [S] = ran ({H ↾}_{S})$
239	238	a1i	$⊢ φ \to H [S] = ran ({H ↾}_{S})$
240	239	feq3d	$⊢ φ \to (({H ↾}_{S}) : S ⟶ H [S] \leftrightarrow ({H ↾}_{S}) : S ⟶ ran ({H ↾}_{S}))$
241	237 240	mpbird	$⊢ φ \to ({H ↾}_{S}) : S ⟶ H [S]$
242	241	notnotd	$⊢ φ \to \neg \neg ({H ↾}_{S}) : S ⟶ H [S]$
243	242	a1d	$⊢ φ \to (\neg (\binom{D + A}{D - 1}) \leq \|H [S]\| \to \neg \neg ({H ↾}_{S}) : S ⟶ H [S])$
244	243	con4d	$⊢ φ \to (\neg ({H ↾}_{S}) : S ⟶ H [S] \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
245		df-an	$⊢ (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v) \leftrightarrow \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v)$
246	245	a1i	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to ((({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v) \leftrightarrow \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v))$
247		eqid	$⊢ \deg_{1} (K) = \deg_{1} (K)$
248		eqid	$⊢ 0_{K} = 0_{K}$
249		eqid	$⊢ 0_{{Poly}_{1} (K)} = 0_{{Poly}_{1} (K)}$
250		fldidom	$⊢ K \in Field \to K \in IDomn$
251	3 250	syl	$⊢ φ \to K \in IDomn$
252	251	ad4antr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to K \in IDomn$
253	205	ply1crng	$⊢ K \in CRing \to {Poly}_{1} (K) \in CRing$
254		crngring	$⊢ {Poly}_{1} (K) \in CRing \to {Poly}_{1} (K) \in Ring$
255		ringgrp	$⊢ {Poly}_{1} (K) \in Ring \to {Poly}_{1} (K) \in Grp$
256	208 253 254 255	4syl	$⊢ φ \to {Poly}_{1} (K) \in Grp$
257	256	ad4antr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to {Poly}_{1} (K) \in Grp$
258	3 4 2 11 9 222 223 10	aks6d1c5	$⊢ φ \to G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)}$
259	258	ad4antr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)}$
260		f1f	$⊢ G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)} \to G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)}$
261	259 260	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)}$
262	19	eleq2i	$⊢ u \in S \leftrightarrow u \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
263		simpl	$⊢ (s = u \land t \in (0 \dots A)) \to s = u$
264	263	fveq1d	$⊢ (s = u \land t \in (0 \dots A)) \to s (t) = u (t)$
265	264	sumeq2dv	$⊢ s = u \to \sum_{t = 0}^{A} s (t) = \sum_{t = 0}^{A} u (t)$
266	265	breq1d	$⊢ s = u \to (\sum_{t = 0}^{A} s (t) \leq D - 1 \leftrightarrow \sum_{t = 0}^{A} u (t) \leq D - 1)$
267	266	elrab	$⊢ u \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \leftrightarrow (u \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} u (t) \leq D - 1)$
268	267	simplbi	$⊢ u \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to u \in ({ℕ_{0}}^{(0 \dots A)})$
269	262 268	sylbi	$⊢ u \in S \to u \in ({ℕ_{0}}^{(0 \dots A)})$
270	269	adantl	$⊢ ((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \to u \in ({ℕ_{0}}^{(0 \dots A)})$
271	270	adantr	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to u \in ({ℕ_{0}}^{(0 \dots A)})$
272	271	adantr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to u \in ({ℕ_{0}}^{(0 \dots A)})$
273	261 272	ffvelcdmd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G (u) \in {Base}_{{Poly}_{1} (K)}$
274	19	eleq2i	$⊢ v \in S \leftrightarrow v \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
275		elrabi	$⊢ v \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to v \in ({ℕ_{0}}^{(0 \dots A)})$
276	274 275	sylbi	$⊢ v \in S \to v \in ({ℕ_{0}}^{(0 \dots A)})$
277	276	adantl	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to v \in ({ℕ_{0}}^{(0 \dots A)})$
278	277	adantr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to v \in ({ℕ_{0}}^{(0 \dots A)})$
279	261 278	ffvelcdmd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G (v) \in {Base}_{{Poly}_{1} (K)}$
280		eqid	$⊢ -_{{Poly}_{1} (K)} = -_{{Poly}_{1} (K)}$
281	207 280	grpsubcl	$⊢ ({Poly}_{1} (K) \in Grp \land G (u) \in {Base}_{{Poly}_{1} (K)} \land G (v) \in {Base}_{{Poly}_{1} (K)}) \to G (u) -_{{Poly}_{1} (K)} G (v) \in {Base}_{{Poly}_{1} (K)}$
282	257 273 279 281	syl3anc	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G (u) -_{{Poly}_{1} (K)} G (v) \in {Base}_{{Poly}_{1} (K)}$
283		neqne	$⊢ \neg u = v \to u \neq v$
284	283	adantl	$⊢ (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v) \to u \neq v$
285	284	adantl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to u \neq v$
286	272 278	jca	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (u \in ({ℕ_{0}}^{(0 \dots A)}) \land v \in ({ℕ_{0}}^{(0 \dots A)}))$
287		f1fveq	$⊢ (G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)} \land (u \in ({ℕ_{0}}^{(0 \dots A)}) \land v \in ({ℕ_{0}}^{(0 \dots A)}))) \to (G (u) = G (v) \leftrightarrow u = v)$
288	259 286 287	syl2anc	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (G (u) = G (v) \leftrightarrow u = v)$
289	288	bicomd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (u = v \leftrightarrow G (u) = G (v))$
290	289	necon3bid	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (u \neq v \leftrightarrow G (u) \neq G (v))$
291	290	biimpd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (u \neq v \to G (u) \neq G (v))$
292	285 291	mpd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G (u) \neq G (v)$
293	207 249 280	grpsubeq0	$⊢ ({Poly}_{1} (K) \in Grp \land G (u) \in {Base}_{{Poly}_{1} (K)} \land G (v) \in {Base}_{{Poly}_{1} (K)}) \to (G (u) -_{{Poly}_{1} (K)} G (v) = 0_{{Poly}_{1} (K)} \leftrightarrow G (u) = G (v))$
294	293	necon3bid	$⊢ ({Poly}_{1} (K) \in Grp \land G (u) \in {Base}_{{Poly}_{1} (K)} \land G (v) \in {Base}_{{Poly}_{1} (K)}) \to (G (u) -_{{Poly}_{1} (K)} G (v) \neq 0_{{Poly}_{1} (K)} \leftrightarrow G (u) \neq G (v))$
295	257 273 279 294	syl3anc	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (G (u) -_{{Poly}_{1} (K)} G (v) \neq 0_{{Poly}_{1} (K)} \leftrightarrow G (u) \neq G (v))$
296	292 295	mpbird	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to G (u) -_{{Poly}_{1} (K)} G (v) \neq 0_{{Poly}_{1} (K)}$
297	205 207 247 204 248 249 252 282 296	fta1g	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \leq \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))$
298	247 205 207	deg1xrcl	$⊢ G (u) -_{{Poly}_{1} (K)} G (v) \in {Base}_{{Poly}_{1} (K)} \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℝ^{*}$
299	282 298	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℝ^{*}$
300	116	ad4antr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D \in ℝ$
301		1red	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to 1 \in ℝ$
302	300 301	resubcld	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D - 1 \in ℝ$
303	302	rexrd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D - 1 \in ℝ^{*}$
304		simp-4l	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to φ$
305		fvexd	$⊢ φ \to {eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in V$
306		cnvexg	$⊢ {eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in V \to {{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} \in V$
307	305 306	syl	$⊢ φ \to {{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} \in V$
308	307	imaexd	$⊢ φ \to {{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}] \in V$
309		hashxnn0	$⊢ {{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}] \in V \to \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℕ_{0}^{*}$
310		xnn0xr	$⊢ \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℕ_{0}^{} \to \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℝ^{}$
311	304 308 309 310	4syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℝ^{*}$
312	247 205 207	deg1xrcl	$⊢ G (v) \in {Base}_{{Poly}_{1} (K)} \to \deg_{1} (K) (G (v)) \in ℝ^{*}$
313	279 312	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (v)) \in ℝ^{*}$
314	247 205 207	deg1xrcl	$⊢ G (u) \in {Base}_{{Poly}_{1} (K)} \to \deg_{1} (K) (G (u)) \in ℝ^{*}$
315	273 314	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u)) \in ℝ^{*}$
316	313 315	ifcld	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \in ℝ^{*}$
317	252	idomringd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to K \in Ring$
318	205 247 317 207 280 273 279	deg1suble	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \leq if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u)))$
319		id	$⊢ \deg_{1} (K) (G (v)) = if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \to \deg_{1} (K) (G (v)) = if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u)))$
320	319	breq1d	$⊢ \deg_{1} (K) (G (v)) = if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \to (\deg_{1} (K) (G (v)) \leq D - 1 \leftrightarrow if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \leq D - 1)$
321		id	$⊢ \deg_{1} (K) (G (u)) = if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \to \deg_{1} (K) (G (u)) = if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u)))$
322	321	breq1d	$⊢ \deg_{1} (K) (G (u)) = if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \to (\deg_{1} (K) (G (u)) \leq D - 1 \leftrightarrow if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \leq D - 1)$
323	3	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to K \in Field$
324	4	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to P \in ℙ$
325	5	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to R \in ℕ$
326	6	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to N \in ℕ$
327	7	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to P ∥ N$
328	8	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to N \gcd R = 1$
329	9	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to A < P$
330	11	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to A \in ℕ_{0}$
331	14	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
332	15	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
333	16	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to M \in ({mulGrp}_{K} PrimRoots R)$
334		simpllr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to v \in S$
335	334 276	syl	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to v \in ({ℕ_{0}}^{(0 \dots A)})$
336	1 2 323 324 325 326 327 328 329 10 330 12 13 331 332 333 17 18 19 335	aks6d1c6lem1	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \deg_{1} (K) (G (v)) = \sum_{t = 0}^{A} v (t)$
337		simpl	$⊢ (s = v \land t \in (0 \dots A)) \to s = v$
338	337	fveq1d	$⊢ (s = v \land t \in (0 \dots A)) \to s (t) = v (t)$
339	338	sumeq2dv	$⊢ s = v \to \sum_{t = 0}^{A} s (t) = \sum_{t = 0}^{A} v (t)$
340	339	breq1d	$⊢ s = v \to (\sum_{t = 0}^{A} s (t) \leq D - 1 \leftrightarrow \sum_{t = 0}^{A} v (t) \leq D - 1)$
341	340	elrab	$⊢ v \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \leftrightarrow (v \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} v (t) \leq D - 1)$
342	274 341	bitri	$⊢ v \in S \leftrightarrow (v \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} v (t) \leq D - 1)$
343	334 342	sylib	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to (v \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} v (t) \leq D - 1)$
344	343	simprd	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \sum_{t = 0}^{A} v (t) \leq D - 1$
345	336 344	eqbrtrd	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \deg_{1} (K) (G (v)) \leq D - 1$
346	3	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to K \in Field$
347	4	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to P \in ℙ$
348	5	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to R \in ℕ$
349	6	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to N \in ℕ$
350	7	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to P ∥ N$
351	8	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to N \gcd R = 1$
352	9	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to A < P$
353	11	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to A \in ℕ_{0}$
354	14	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
355	15	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
356	16	ad5antr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to M \in ({mulGrp}_{K} PrimRoots R)$
357	272	adantr	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to u \in ({ℕ_{0}}^{(0 \dots A)})$
358	1 2 346 347 348 349 350 351 352 10 353 12 13 354 355 356 17 18 19 357	aks6d1c6lem1	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \deg_{1} (K) (G (u)) = \sum_{t = 0}^{A} u (t)$
359		simp-4r	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to u \in S$
360	262 267	bitri	$⊢ u \in S \leftrightarrow (u \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} u (t) \leq D - 1)$
361	359 360	sylib	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to (u \in ({ℕ_{0}}^{(0 \dots A)}) \land \sum_{t = 0}^{A} u (t) \leq D - 1)$
362	361	simprd	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \sum_{t = 0}^{A} u (t) \leq D - 1$
363	358 362	eqbrtrd	$⊢ (((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \land \neg \deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v))) \to \deg_{1} (K) (G (u)) \leq D - 1$
364	320 322 345 363	ifbothda	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to if (\deg_{1} (K) (G (u)) \leq \deg_{1} (K) (G (v)), \deg_{1} (K) (G (v)), \deg_{1} (K) (G (u))) \leq D - 1$
365	299 316 303 318 364	xrletrd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \leq D - 1$
366	300	rexrd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D \in ℝ^{*}$
367	300	ltm1d	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D - 1 < D$
368		simpllr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to u \in S$
369		simplr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to v \in S$
370	304 368 369	jca31	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to ((φ \land u \in S) \land v \in S)$
371		simpr	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)$
372	370 371	jca	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v))$
373	3	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to K \in Field$
374	4	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to P \in ℙ$
375	5	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to R \in ℕ$
376	6	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to N \in ℕ$
377	7	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to P ∥ N$
378	8	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to N \gcd R = 1$
379	9	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to A < P$
380	11	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to A \in ℕ_{0}$
381	14	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
382	15	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
383	16	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to M \in ({mulGrp}_{K} PrimRoots R)$
384		simpllr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to u \in S$
385		simplr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to v \in S$
386		simprl	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to ({H ↾}_{S}) (u) = ({H ↾}_{S}) (v)$
387	284	adantl	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to u \neq v$
388	21	ad3antrrr	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [ℕ_{0} \times ℕ_{0}]\|$
389	1 2 373 374 375 376 377 378 379 10 380 12 13 381 382 383 17 18 19 384 385 386 387 20 388	aks6d1c6lem2	$⊢ (((φ \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D \leq \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\|$
390	372 389	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D \leq \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\|$
391	303 366 311 367 390	xrltletrd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to D - 1 < \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\|$
392	299 303 311 365 391	xrlelttrd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) < \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\|$
393	247 205 249 207	deg1nn0clb	$⊢ (K \in Ring \land G (u) -_{{Poly}_{1} (K)} G (v) \in {Base}_{{Poly}_{1} (K)}) \to (G (u) -_{{Poly}_{1} (K)} G (v) \neq 0_{{Poly}_{1} (K)} \leftrightarrow \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℕ_{0})$
394	317 282 393	syl2anc	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (G (u) -_{{Poly}_{1} (K)} G (v) \neq 0_{{Poly}_{1} (K)} \leftrightarrow \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℕ_{0})$
395	296 394	mpbid	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℕ_{0}$
396	395	nn0red	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℝ$
397	396	rexrd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℝ^{*}$
398		fvexd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to {eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in V$
399	398 306	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to {{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} \in V$
400	399	imaexd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to {{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}] \in V$
401	400 309	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℕ_{0}^{*}$
402	401 310	syl	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℝ^{*}$
403		xrltnle	$⊢ (\deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) \in ℝ^{} \land \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \in ℝ^{}) \to (\deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) < \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \leftrightarrow \neg \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \leq \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)))$
404	397 402 403	syl2anc	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (\deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)) < \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \leftrightarrow \neg \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \leq \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v)))$
405	392 404	mpbid	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to \neg \|{{eval}_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))}^{-1} [\{0_{K}\}]\| \leq \deg_{1} (K) (G (u) -_{{Poly}_{1} (K)} G (v))$
406	297 405	pm2.21dd	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|$
407	406	ex	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to ((({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \land \neg u = v) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
408	246 407	sylbird	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to (\neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
409		biidd	$⊢ ({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to (u = v \leftrightarrow u = v)$
410	409	necon3abid	$⊢ ({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to (u \neq v \leftrightarrow \neg u = v)$
411	410	necon1bbid	$⊢ ({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to (\neg \neg u = v \leftrightarrow u = v)$
412	411	pm5.74i	$⊢ (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v) \leftrightarrow (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v)$
413	412	notbii	$⊢ \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v) \leftrightarrow \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v)$
414	413	a1i	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to (\neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v) \leftrightarrow \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v))$
415	414	imbi1d	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to ((\neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to \neg \neg u = v) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|) \leftrightarrow (\neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|))$
416	408 415	mpbid	$⊢ (((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \to (\neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
417	416	imp	$⊢ ((((φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \land u \in S) \land v \in S) \land \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|$
418		fveqeq2	$⊢ x = u \to (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \leftrightarrow ({H ↾}_{S}) (u) = ({H ↾}_{S}) (y))$
419		equequ1	$⊢ x = u \to (x = y \leftrightarrow u = y)$
420	418 419	imbi12d	$⊢ x = u \to ((({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \leftrightarrow (({H ↾}_{S}) (u) = ({H ↾}_{S}) (y) \to u = y))$
421	420	notbid	$⊢ x = u \to (\neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \leftrightarrow \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (y) \to u = y))$
422		fveq2	$⊢ y = v \to ({H ↾}_{S}) (y) = ({H ↾}_{S}) (v)$
423	422	eqeq2d	$⊢ y = v \to (({H ↾}_{S}) (u) = ({H ↾}_{S}) (y) \leftrightarrow ({H ↾}_{S}) (u) = ({H ↾}_{S}) (v))$
424		equequ2	$⊢ y = v \to (u = y \leftrightarrow u = v)$
425	423 424	imbi12d	$⊢ y = v \to ((({H ↾}_{S}) (u) = ({H ↾}_{S}) (y) \to u = y) \leftrightarrow (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v))$
426	425	notbid	$⊢ y = v \to (\neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (y) \to u = y) \leftrightarrow \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v))$
427	421 426	cbvrex2vw	$⊢ \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \leftrightarrow \exists u \in S \exists v \in S \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v)$
428	427	bilani	$⊢ (φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to \exists u \in S \exists v \in S \neg (({H ↾}_{S}) (u) = ({H ↾}_{S}) (v) \to u = v)$
429	417 428	r19.29vva	$⊢ (φ \land \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|$
430	429	ex	$⊢ φ \to (\exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
431		rexnal2	$⊢ \exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \leftrightarrow \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)$
432	431	a1i	$⊢ φ \to (\exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \leftrightarrow \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y))$
433	432	imbi1d	$⊢ φ \to ((\exists x \in S \exists y \in S \neg (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|) \leftrightarrow (\neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|))$
434	430 433	mpbid	$⊢ φ \to (\neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
435	244 434	jaod	$⊢ φ \to ((\neg ({H ↾}_{S}) : S ⟶ H [S] \lor \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
436		ianor	$⊢ \neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \leftrightarrow (\neg ({H ↾}_{S}) : S ⟶ H [S] \lor \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y))$
437	436	a1i	$⊢ φ \to (\neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \leftrightarrow (\neg ({H ↾}_{S}) : S ⟶ H [S] \lor \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)))$
438	437	biimpd	$⊢ φ \to (\neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\neg ({H ↾}_{S}) : S ⟶ H [S] \lor \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)))$
439	438	imim1d	$⊢ φ \to (((\neg ({H ↾}_{S}) : S ⟶ H [S] \lor \neg \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|) \to (\neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|))$
440	435 439	mpd	$⊢ φ \to (\neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
441		dff13	$⊢ ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S] \leftrightarrow (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y))$
442	441	a1i	$⊢ φ \to (({H ↾}_{S}) : S \underset{1-1}{⟶} H [S] \leftrightarrow (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)))$
443	442	notbid	$⊢ φ \to (\neg ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S] \leftrightarrow \neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)))$
444	443	biimpd	$⊢ φ \to (\neg ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S] \to \neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)))$
445	444	imim1d	$⊢ φ \to ((\neg (({H ↾}_{S}) : S ⟶ H [S] \land \forall x \in S \forall y \in S (({H ↾}_{S}) (x) = ({H ↾}_{S}) (y) \to x = y)) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|) \to (\neg ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S] \to (\binom{D + A}{D - 1}) \leq \|H [S]\|))$
446	440 445	mpd	$⊢ φ \to (\neg ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S] \to (\binom{D + A}{D - 1}) \leq \|H [S]\|)$
447	446	imp	$⊢ (φ \land \neg ({H ↾}_{S}) : S \underset{1-1}{⟶} H [S]) \to (\binom{D + A}{D - 1}) \leq \|H [S]\|$
448	192 447	pm2.61dan	$⊢ φ \to (\binom{D + A}{D - 1}) \leq \|H [S]\|$
449		hashss	$⊢ (H [{ℕ_{0}}^{(0 \dots A)}] \in V \land H [S] \subseteq H [{ℕ_{0}}^{(0 \dots A)}]) \to \|H [S]\| \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$
450	135 152 449	syl2anc	$⊢ φ \to \|H [S]\| \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$
451	131 157 161 448 450	xrletrd	$⊢ φ \to (\binom{D + A}{D - 1}) \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$

Metamath Proof Explorer

Theorem aks6d1c6lem3

Proof