aks6d1c7lem2

Description: Contradiction to Claim 2 and Claim 7. We assumed in Claim 2 that there are two different prime numbers P and Q . (Contributed by metakunt, 16-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7lem2.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		aks6d1c7lem2.2	$⊢ P = chr (K)$
3		aks6d1c7lem2.3	$⊢ φ \to K \in Field$
4		aks6d1c7lem2.4	$⊢ φ \to P \in ℙ$
5		aks6d1c7lem2.5	$⊢ φ \to R \in ℕ$
6		aks6d1c7lem2.6	$⊢ φ \to N \in ℤ_{\geq 3}$
7		aks6d1c7lem2.7	$⊢ φ \to P ∥ N$
8		aks6d1c7lem2.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c7lem2.9	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
10		aks6d1c7lem2.10	$⊢ L = ℤRHom (ℤ / R ℤ)$
11		aks6d1c7lem2.11	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
12		aks6d1c7lem2.12	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
13		aks6d1c7lem2.13	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
14		aks6d1c7lem2.14	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
15		aks6d1c7lem2.15	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
16		aks6d1c7lem2.16	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
17		aks6d1c7lem2.17	$⊢ B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
18		aks6d1c7lem2.18	$⊢ C = E [(0 \dots B) \times (0 \dots B)]$
19		aks6d1c7lem2.19	$⊢ φ \to (Q \in ℙ \land Q ∥ N)$
20		aks6d1c7lem2.20	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
21		aks6d1c7lem2.21	$⊢ 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)))))$
22		aks6d1c7lem2.22	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
23		aks6d1c7lem2.23	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
24		simpr	$⊢ (φ \land P = Q) \to P = Q$
25	3	adantr	$⊢ (φ \land P \neq Q) \to K \in Field$
26	4	adantr	$⊢ (φ \land P \neq Q) \to P \in ℙ$
27	5	adantr	$⊢ (φ \land P \neq Q) \to R \in ℕ$
28		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
29	6 28	syl	$⊢ φ \to N \in ℤ$
30		0red	$⊢ φ \to 0 \in ℝ$
31		3re	$⊢ 3 \in ℝ$
32	31	a1i	$⊢ φ \to 3 \in ℝ$
33	29	zred	$⊢ φ \to N \in ℝ$
34		3pos	$⊢ 0 < 3$
35	34	a1i	$⊢ φ \to 0 < 3$
36		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
37	6 36	syl	$⊢ φ \to 3 \leq N$
38	30 32 33 35 37	ltletrd	$⊢ φ \to 0 < N$
39	29 38	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
40		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
41	39 40	sylibr	$⊢ φ \to N \in ℕ$
42	41	adantr	$⊢ (φ \land P \neq Q) \to N \in ℕ$
43	7	adantr	$⊢ (φ \land P \neq Q) \to P ∥ N$
44	8	adantr	$⊢ (φ \land P \neq Q) \to N \gcd R = 1$
45	5	phicld	$⊢ φ \to ϕ (R) \in ℕ$
46	45	nnred	$⊢ φ \to ϕ (R) \in ℝ$
47		1red	$⊢ φ \to 1 \in ℝ$
48		0le1	$⊢ 0 \leq 1$
49	48	a1i	$⊢ φ \to 0 \leq 1$
50	45	nnge1d	$⊢ φ \to 1 \leq ϕ (R)$
51	30 47 46 49 50	letrd	$⊢ φ \to 0 \leq ϕ (R)$
52	46 51	resqrtcld	$⊢ φ \to \sqrt{ϕ (R)} \in ℝ$
53		2re	$⊢ 2 \in ℝ$
54	53	a1i	$⊢ φ \to 2 \in ℝ$
55		2pos	$⊢ 0 < 2$
56	55	a1i	$⊢ φ \to 0 < 2$
57		1lt2	$⊢ 1 < 2$
58	57	a1i	$⊢ φ \to 1 < 2$
59	47 58	ltned	$⊢ φ \to 1 \neq 2$
60	59	necomd	$⊢ φ \to 2 \neq 1$
61	54 56 33 38 60	relogbcld	$⊢ φ \to \log_{2} N \in ℝ$
62	52 61	remulcld	$⊢ φ \to \sqrt{ϕ (R)} \log_{2} N \in ℝ$
63	62	flcld	$⊢ φ \to ⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℤ$
64	46 51	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{ϕ (R)}$
65	54	recnd	$⊢ φ \to 2 \in ℂ$
66	30 56	gtned	$⊢ φ \to 2 \neq 0$
67		logb1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 1 = 0$
68	65 66 60 67	syl3anc	$⊢ φ \to \log_{2} 1 = 0$
69	68	eqcomd	$⊢ φ \to 0 = \log_{2} 1$
70		2z	$⊢ 2 \in ℤ$
71	70	a1i	$⊢ φ \to 2 \in ℤ$
72	54	leidd	$⊢ φ \to 2 \leq 2$
73		0lt1	$⊢ 0 < 1$
74	73	a1i	$⊢ φ \to 0 < 1$
75	41	nnge1d	$⊢ φ \to 1 \leq N$
76	71 72 47 74 33 38 75	logblebd	$⊢ φ \to \log_{2} 1 \leq \log_{2} N$
77	69 76	eqbrtrd	$⊢ φ \to 0 \leq \log_{2} N$
78	52 61 64 77	mulge0d	$⊢ φ \to 0 \leq \sqrt{ϕ (R)} \log_{2} N$
79		0zd	$⊢ φ \to 0 \in ℤ$
80		flge	$⊢ (\sqrt{ϕ (R)} \log_{2} N \in ℝ \land 0 \in ℤ) \to (0 \leq \sqrt{ϕ (R)} \log_{2} N \leftrightarrow 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
81	62 79 80	syl2anc	$⊢ φ \to (0 \leq \sqrt{ϕ (R)} \log_{2} N \leftrightarrow 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
82	78 81	mpbid	$⊢ φ \to 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
83	63 82	jca	$⊢ φ \to (⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℤ \land 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
84		elnn0z	$⊢ ⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℕ_{0} \leftrightarrow (⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℤ \land 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
85	83 84	sylibr	$⊢ φ \to ⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℕ_{0}$
86	12 85	eqeltrid	$⊢ φ \to A \in ℕ_{0}$
87	86	adantr	$⊢ (φ \land P \neq Q) \to A \in ℕ_{0}$
88	22	adantr	$⊢ (φ \land P \neq Q) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
89	14	adantr	$⊢ (φ \land P \neq Q) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
90	15	adantr	$⊢ (φ \land P \neq Q) \to M \in ({mulGrp}_{K} PrimRoots R)$
91	19	simpld	$⊢ φ \to Q \in ℙ$
92	91	adantr	$⊢ (φ \land P \neq Q) \to Q \in ℙ$
93	19	simprd	$⊢ φ \to Q ∥ N$
94	93	adantr	$⊢ (φ \land P \neq Q) \to Q ∥ N$
95		simpr	$⊢ (φ \land P \neq Q) \to P \neq Q$
96	92 94 95	3jca	$⊢ (φ \land P \neq Q) \to (Q \in ℙ \land Q ∥ N \land P \neq Q)$
97	1 2 25 26 27 42 43 44 21 87 9 10 88 89 90 16 17 18 96	aks6d1c2	$⊢ (φ \land P \neq Q) \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$
98	41	nnzd	$⊢ φ \to N \in ℤ$
99		eqid	$⊢ ℤ / R ℤ = ℤ / R ℤ$
100	41 4 7 5 8 9 10 99	hashscontpowcl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
101	100	nn0red	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ$
102	100	nn0ge0d	$⊢ φ \to 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
103	101 102	resqrtcld	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \in ℝ$
104	103	flcld	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ$
105	101 102	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
106		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}]]\|}⌋)$
107	103 79 106	syl2anc	$⊢ φ \to (0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \leftrightarrow 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
108	105 107	mpbid	$⊢ φ \to 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
109	104 108	jca	$⊢ φ \to (⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ \land 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
110		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}]]\|}⌋)$
111	109 110	sylibr	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℕ_{0}$
112	17 111	eqeltrid	$⊢ φ \to B \in ℕ_{0}$
113	98 112	zexpcld	$⊢ φ \to N^{B} \in ℤ$
114	113	zred	$⊢ φ \to N^{B} \in ℝ$
115	114	adantr	$⊢ (φ \land P \neq Q) \to N^{B} \in ℝ$
116	115	rexrd	$⊢ (φ \land P \neq Q) \to N^{B} \in ℝ^{*}$
117	100	adantr	$⊢ (φ \land P \neq Q) \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
118	11 117	eqeltrid	$⊢ (φ \land P \neq Q) \to D \in ℕ_{0}$
119	118 87	nn0addcld	$⊢ (φ \land P \neq Q) \to D + A \in ℕ_{0}$
120	118	nn0zd	$⊢ (φ \land P \neq Q) \to D \in ℤ$
121		1zzd	$⊢ (φ \land P \neq Q) \to 1 \in ℤ$
122	120 121	zsubcld	$⊢ (φ \land P \neq Q) \to D - 1 \in ℤ$
123		bccl	$⊢ (D + A \in ℕ_{0} \land D - 1 \in ℤ) \to (\binom{D + A}{D - 1}) \in ℕ_{0}$
124	119 122 123	syl2anc	$⊢ (φ \land P \neq Q) \to (\binom{D + A}{D - 1}) \in ℕ_{0}$
125	124	nn0red	$⊢ (φ \land P \neq Q) \to (\binom{D + A}{D - 1}) \in ℝ$
126	125	rexrd	$⊢ (φ \land P \neq Q) \to (\binom{D + A}{D - 1}) \in ℝ^{*}$
127		ovexd	$⊢ (φ \land P \neq Q) \to {ℕ_{0}}^{(0 \dots A)} \in V$
128	127	mptexd	$⊢ (φ \land P \neq Q) \to (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M)) \in V$
129	16 128	eqeltrid	$⊢ (φ \land P \neq Q) \to H \in V$
130	129	imaexd	$⊢ (φ \land P \neq Q) \to H [{ℕ_{0}}^{(0 \dots A)}] \in V$
131		hashxrcl	$⊢ H [{ℕ_{0}}^{(0 \dots A)}] \in V \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℝ^{*}$
132	130 131	syl	$⊢ (φ \land P \neq Q) \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℝ^{*}$
133		eqcom	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leftrightarrow \|L [E [ℕ_{0} \times ℕ_{0}]]\| = D$
134	11 133	mpbi	$⊢ \|L [E [ℕ_{0} \times ℕ_{0}]]\| = D$
135	134	fveq2i	$⊢ \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} = \sqrt{D}$
136	135	fveq2i	$⊢ ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ = ⌊\sqrt{D}⌋$
137	17 136	eqtri	$⊢ B = ⌊\sqrt{D}⌋$
138	137	a1i	$⊢ (φ \land P \neq Q) \to B = ⌊\sqrt{D}⌋$
139	138	oveq2d	$⊢ (φ \land P \neq Q) \to N^{B} = N^{⌊\sqrt{D}⌋}$
140	6	adantr	$⊢ (φ \land P \neq Q) \to N \in ℤ_{\geq 3}$
141	13	adantr	$⊢ (φ \land P \neq Q) \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
142	26 27 140 43 44 9 10 11 12 141	aks6d1c7lem1	$⊢ (φ \land P \neq Q) \to N^{⌊\sqrt{D}⌋} < (\binom{D + A}{D - 1})$
143	139 142	eqbrtrd	$⊢ (φ \land P \neq Q) \to N^{B} < (\binom{D + A}{D - 1})$
144	20	adantr	$⊢ (φ \land P \neq Q) \to \forall b \in (1 \dots A) b \gcd N = 1$
145		eqid	$⊢ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) = (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M)$
146		eqid	$⊢ \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\} = \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\}$
147		nfcv	$⊢ \underline{Ⅎ} b ⋃ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [h]$
148		nfcv	$⊢ \underline{Ⅎ} h ⋃ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [b]$
149		imaeq2	$⊢ h = b \to (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [h] = (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [b]$
150	149	unieqd	$⊢ h = b \to ⋃ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [h] = ⋃ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [b]$
151	147 148 150	cbvmpt	$⊢ (h \in {Base}_{(ℤ_{ring} /_{𝑠} (ℤ_{ring} ~_{QG} {(c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M)}^{-1} [\{0_{(({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\}) ↾_{𝑠} ran (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M))}\}]))} ⟼ ⋃ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [h]) = (b \in {Base}_{(ℤ_{ring} /_{𝑠} (ℤ_{ring} ~_{QG} {(c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M)}^{-1} [\{0_{(({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\}) ↾_{𝑠} ran (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M))}\}]))} ⟼ ⋃ (c \in ℤ ⟼ c \cdot_{({mulGrp}_{K} ↾_{𝑠} \{j \in {Base}_{{mulGrp}_{K}} \| \exists m \in {Base}_{{mulGrp}_{K}} m +_{{mulGrp}_{K}} j = 0_{{mulGrp}_{K}}\})} M) [b])$
152	1 2 25 26 27 42 43 44 144 21 12 9 10 88 89 90 16 11 23 145 146 151	aks6d1c6lem5	$⊢ (φ \land P \neq Q) \to (\binom{D + A}{D - 1}) \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$
153	116 126 132 143 152	xrltletrd	$⊢ (φ \land P \neq Q) \to N^{B} < \|H [{ℕ_{0}}^{(0 \dots A)}]\|$
154		xrltnle	$⊢ (N^{B} \in ℝ^{} \land \|H [{ℕ_{0}}^{(0 \dots A)}]\| \in ℝ^{}) \to (N^{B} < \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leftrightarrow \neg \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B})$
155	116 132 154	syl2anc	$⊢ (φ \land P \neq Q) \to (N^{B} < \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leftrightarrow \neg \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B})$
156	153 155	mpbid	$⊢ (φ \land P \neq Q) \to \neg \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$
157	97 156	pm2.21dd	$⊢ (φ \land P \neq Q) \to P = Q$
158	24 157	pm2.61dane	$⊢ φ \to P = Q$

Metamath Proof Explorer

Theorem aks6d1c7lem2

Proof