aks6d1c2

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

Proof

Step	Hyp	Ref	Expression
1		aks6d1c2a.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		aks6d1c2a.2	$⊢ P = chr (K)$
3		aks6d1c2a.3	$⊢ φ \to K \in Field$
4		aks6d1c2a.4	$⊢ φ \to P \in ℙ$
5		aks6d1c2a.5	$⊢ φ \to R \in ℕ$
6		aks6d1c2a.6	$⊢ φ \to N \in ℕ$
7		aks6d1c2a.7	$⊢ φ \to P ∥ N$
8		aks6d1c2a.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c2a.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)))))$
10		aks6d1c2a.11	$⊢ φ \to A \in ℕ_{0}$
11		aks6d1c2a.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
12		aks6d1c2a.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
13		aks6d1c2a.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
14		aks6d1c2a.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
15		aks6d1c2a.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
16		aks6d1c2a.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
17		aks6d1c2a.18	$⊢ B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
18		aks6d1c2a.19	$⊢ C = E [(0 \dots B) \times (0 \dots B)]$
19		aks6d1c2a.20	$⊢ φ \to (Q \in ℙ \land Q ∥ N \land P \neq Q)$
20		simpl	$⊢ (((φ \land b \in C) \land c \in C) \land (b < c \land \exists d \in ℕ c = b + d R)) \to ((φ \land b \in C) \land c \in C)$
21		simprl	$⊢ (((φ \land b \in C) \land c \in C) \land (b < c \land \exists d \in ℕ c = b + d R)) \to b < c$
22	20 21	jca	$⊢ (((φ \land b \in C) \land c \in C) \land (b < c \land \exists d \in ℕ c = b + d R)) \to (((φ \land b \in C) \land c \in C) \land b < c)$
23		simprr	$⊢ (((φ \land b \in C) \land c \in C) \land (b < c \land \exists d \in ℕ c = b + d R)) \to \exists d \in ℕ c = b + d R$
24	22 23	jca	$⊢ (((φ \land b \in C) \land c \in C) \land (b < c \land \exists d \in ℕ c = b + d R)) \to ((((φ \land b \in C) \land c \in C) \land b < c) \land \exists d \in ℕ c = b + d R)$
25	3	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to K \in Field$
26	4	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to P \in ℙ$
27	5	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to R \in ℕ$
28	6	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to N \in ℕ$
29	7	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to P ∥ N$
30	8	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to N \gcd R = 1$
31		0nn0	$⊢ 0 \in ℕ_{0}$
32	31	a1i	$⊢ ((((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \land j \in (0 \dots A)) \to 0 \in ℕ_{0}$
33		eqid	$⊢ (j \in (0 \dots A) ⟼ 0) = (j \in (0 \dots A) ⟼ 0)$
34	32 33	fmptd	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to (j \in (0 \dots A) ⟼ 0) : (0 \dots A) ⟶ ℕ_{0}$
35	10	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to A \in ℕ_{0}$
36	13	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
37	14	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
38	15	ad5antr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to M \in ({mulGrp}_{K} PrimRoots R)$
39		simp-5r	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to b \in C$
40		simp-4r	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to c \in C$
41		simpllr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to b < c$
42		eqid	$⊢ \cdot_{{mulGrp}_{{Poly}_{1} (K)}} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
43		eqid	$⊢ {var}_{1} (K) = {var}_{1} (K)$
44		eqid	$⊢ (c \cdot_{{mulGrp}_{{Poly}_{1} (K)}} {var}_{1} (K)) -_{{Poly}_{1} (K)} (b \cdot_{{mulGrp}_{{Poly}_{1} (K)}} {var}_{1} (K)) = (c \cdot_{{mulGrp}_{{Poly}_{1} (K)}} {var}_{1} (K)) -_{{Poly}_{1} (K)} (b \cdot_{{mulGrp}_{{Poly}_{1} (K)}} {var}_{1} (K))$
45		simplr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to d \in ℕ$
46		simpr	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to c = b + d R$
47	1 2 25 26 27 28 29 30 34 9 35 11 12 36 37 38 16 17 18 39 40 41 42 43 44 45 46	aks6d1c2lem4	$⊢ (((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \land c = b + d R) \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$
48	47	ex	$⊢ ((((φ \land b \in C) \land c \in C) \land b < c) \land d \in ℕ) \to (c = b + d R \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B})$
49	48	rexlimdva	$⊢ (((φ \land b \in C) \land c \in C) \land b < c) \to (\exists d \in ℕ c = b + d R \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B})$
50	49	imp	$⊢ ((((φ \land b \in C) \land c \in C) \land b < c) \land \exists d \in ℕ c = b + d R) \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$
51	24 50	syl	$⊢ (((φ \land b \in C) \land c \in C) \land (b < c \land \exists d \in ℕ c = b + d R)) \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$
52		simprr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to b < c$
53		nfcv	$⊢ \underline{Ⅎ} s L (t)$
54		nfcv	$⊢ \underline{Ⅎ} t L (s)$
55		fveq2	$⊢ t = s \to L (t) = L (s)$
56	53 54 55	cbvmpt	$⊢ (t \in C ⟼ L (t)) = (s \in C ⟼ L (s))$
57	56	a1i	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (t \in C ⟼ L (t)) = (s \in C ⟼ L (s))$
58		simpr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land s = b) \to s = b$
59	58	fveq2d	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land s = b) \to L (s) = L (b)$
60		simpllr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to b \in C$
61		fvexd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to L (b) \in V$
62	57 59 60 61	fvmptd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (t \in C ⟼ L (t)) (b) = L (b)$
63	62	eqcomd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to L (b) = (t \in C ⟼ L (t)) (b)$
64		simprl	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c)$
65		simpr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land s = c) \to s = c$
66	65	fveq2d	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land s = c) \to L (s) = L (c)$
67		simplr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to c \in C$
68		fvexd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to L (c) \in V$
69	57 66 67 68	fvmptd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (t \in C ⟼ L (t)) (c) = L (c)$
70	64 69	eqtrd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (t \in C ⟼ L (t)) (b) = L (c)$
71	63 70	eqtrd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to L (b) = L (c)$
72	71	eqcomd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to L (c) = L (b)$
73	5	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
74	73	adantr	$⊢ (φ \land b \in C) \to R \in ℕ_{0}$
75	74	adantr	$⊢ ((φ \land b \in C) \land c \in C) \to R \in ℕ_{0}$
76	75	adantr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to R \in ℕ_{0}$
77		fz0ssnn0	$⊢ (0 \dots B) \subseteq ℕ_{0}$
78	77	a1i	$⊢ φ \to (0 \dots B) \subseteq ℕ_{0}$
79	78 78	jca	$⊢ φ \to ((0 \dots B) \subseteq ℕ_{0} \land (0 \dots B) \subseteq ℕ_{0})$
80		eqid	$⊢ ℤ / R ℤ = ℤ / R ℤ$
81	6 4 7 5 8 11 12 80	hashscontpowcl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
82	81	nn0red	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ$
83	81	nn0ge0d	$⊢ φ \to 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
84	82 83	resqrtcld	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \in ℝ$
85	84	flcld	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ$
86	82 83	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
87		0zd	$⊢ φ \to 0 \in ℤ$
88		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}]]\|}⌋)$
89	84 87 88	syl2anc	$⊢ φ \to (0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \leftrightarrow 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
90	86 89	mpbid	$⊢ φ \to 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
91	85 90	jca	$⊢ φ \to (⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ \land 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
92		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}]]\|}⌋)$
93	91 92	sylibr	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℕ_{0}$
94	17	a1i	$⊢ φ \to B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
95	94	eleq1d	$⊢ φ \to (B \in ℕ_{0} \leftrightarrow ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℕ_{0})$
96	93 95	mpbird	$⊢ φ \to B \in ℕ_{0}$
97	96	nn0ge0d	$⊢ φ \to 0 \leq B$
98	96	nn0zd	$⊢ φ \to B \in ℤ$
99		eluz	$⊢ (0 \in ℤ \land B \in ℤ) \to (B \in ℤ_{\geq 0} \leftrightarrow 0 \leq B)$
100	87 98 99	syl2anc	$⊢ φ \to (B \in ℤ_{\geq 0} \leftrightarrow 0 \leq B)$
101	97 100	mpbird	$⊢ φ \to B \in ℤ_{\geq 0}$
102		fzn0	$⊢ (0 \dots B) \neq \emptyset \leftrightarrow B \in ℤ_{\geq 0}$
103	101 102	sylibr	$⊢ φ \to (0 \dots B) \neq \emptyset$
104	103 103	jca	$⊢ φ \to ((0 \dots B) \neq \emptyset \land (0 \dots B) \neq \emptyset)$
105		xpnz	$⊢ ((0 \dots B) \neq \emptyset \land (0 \dots B) \neq \emptyset) \leftrightarrow (0 \dots B) \times (0 \dots B) \neq \emptyset$
106	105	biimpi	$⊢ ((0 \dots B) \neq \emptyset \land (0 \dots B) \neq \emptyset) \to (0 \dots B) \times (0 \dots B) \neq \emptyset$
107	104 106	syl	$⊢ φ \to (0 \dots B) \times (0 \dots B) \neq \emptyset$
108		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}))$
109	107 108	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}))$
110	79 109	mpbird	$⊢ φ \to (0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0}$
111		imass2	$⊢ (0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0} \to E [(0 \dots B) \times (0 \dots B)] \subseteq E [ℕ_{0} \times ℕ_{0}]$
112	110 111	syl	$⊢ φ \to E [(0 \dots B) \times (0 \dots B)] \subseteq E [ℕ_{0} \times ℕ_{0}]$
113		nfv	$⊢ Ⅎ o φ$
114	19	simp1d	$⊢ φ \to Q \in ℙ$
115	19	simp2d	$⊢ φ \to Q ∥ N$
116	19	simp3d	$⊢ φ \to P \neq Q$
117	6 4 7 11 114 115 116	aks6d1c2p2	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} \underset{1-1}{⟶} ℕ$
118		f1f	$⊢ E : ℕ_{0} \times ℕ_{0} \underset{1-1}{⟶} ℕ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ$
119	117 118	syl	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ$
120	119	ffnd	$⊢ φ \to E Fn (ℕ_{0} \times ℕ_{0})$
121	120	fnfund	$⊢ φ \to Fun E$
122	119	ffvelcdmda	$⊢ (φ \land o \in (ℕ_{0} \times ℕ_{0})) \to E (o) \in ℕ$
123	113 121 122	funimassd	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \subseteq ℕ$
124	112 123	sstrd	$⊢ φ \to E [(0 \dots B) \times (0 \dots B)] \subseteq ℕ$
125	18	a1i	$⊢ φ \to C = E [(0 \dots B) \times (0 \dots B)]$
126	125	sseq1d	$⊢ φ \to (C \subseteq ℕ \leftrightarrow E [(0 \dots B) \times (0 \dots B)] \subseteq ℕ)$
127	124 126	mpbird	$⊢ φ \to C \subseteq ℕ$
128	127	ad2antrr	$⊢ ((φ \land b \in C) \land c \in C) \to C \subseteq ℕ$
129		simpr	$⊢ ((φ \land b \in C) \land c \in C) \to c \in C$
130	128 129	sseldd	$⊢ ((φ \land b \in C) \land c \in C) \to c \in ℕ$
131	130	nnzd	$⊢ ((φ \land b \in C) \land c \in C) \to c \in ℤ$
132	131	adantr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to c \in ℤ$
133		simplr	$⊢ ((φ \land b \in C) \land c \in C) \to b \in C$
134	128 133	sseldd	$⊢ ((φ \land b \in C) \land c \in C) \to b \in ℕ$
135	134	nnzd	$⊢ ((φ \land b \in C) \land c \in C) \to b \in ℤ$
136	135	adantr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to b \in ℤ$
137	80 12	zndvds	$⊢ (R \in ℕ_{0} \land c \in ℤ \land b \in ℤ) \to (L (c) = L (b) \leftrightarrow R ∥ (c - b))$
138	76 132 136 137	syl3anc	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (L (c) = L (b) \leftrightarrow R ∥ (c - b))$
139	72 138	mpbid	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to R ∥ (c - b)$
140	76	nn0zd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to R \in ℤ$
141	132 136	zsubcld	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to c - b \in ℤ$
142		divides	$⊢ (R \in ℤ \land c - b \in ℤ) \to (R ∥ (c - b) \leftrightarrow \exists d \in ℤ d R = c - b)$
143	140 141 142	syl2anc	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (R ∥ (c - b) \leftrightarrow \exists d \in ℤ d R = c - b)$
144	143	biimpd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (R ∥ (c - b) \to \exists d \in ℤ d R = c - b)$
145	139 144	mpd	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to \exists d \in ℤ d R = c - b$
146		simprl	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to d \in ℤ$
147	130	ad2antrr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c \in ℕ$
148	147	nnred	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c \in ℝ$
149	134	ad2antrr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to b \in ℕ$
150	149	nnred	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to b \in ℝ$
151	148 150	resubcld	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c - b \in ℝ$
152	5	nnrpd	$⊢ φ \to R \in ℝ^{+}$
153	152	adantr	$⊢ (φ \land b \in C) \to R \in ℝ^{+}$
154	153	adantr	$⊢ ((φ \land b \in C) \land c \in C) \to R \in ℝ^{+}$
155	154	adantr	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to R \in ℝ^{+}$
156	155	adantr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to R \in ℝ^{+}$
157	156	rpred	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to R \in ℝ$
158	52	adantr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to b < c$
159	150 148	posdifd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to (b < c \leftrightarrow 0 < c - b)$
160	158 159	mpbid	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to 0 < c - b$
161	156	rpgt0d	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to 0 < R$
162	151 157 160 161	divgt0d	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to 0 < \frac{c - b}{R}$
163	157	recnd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to R \in ℂ$
164	146	zred	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to d \in ℝ$
165	164	recnd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to d \in ℂ$
166	163 165	mulcomd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to R d = d R$
167		simprr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to d R = c - b$
168	166 167	eqtrd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to R d = c - b$
169	151	recnd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c - b \in ℂ$
170	161	gt0ne0d	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to R \neq 0$
171	169 163 165 170	divmuld	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to (\frac{c - b}{R} = d \leftrightarrow R d = c - b)$
172	168 171	mpbird	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to \frac{c - b}{R} = d$
173	162 172	breqtrd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to 0 < d$
174	146 173	jca	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to (d \in ℤ \land 0 < d)$
175		elnnz	$⊢ d \in ℕ \leftrightarrow (d \in ℤ \land 0 < d)$
176	174 175	sylibr	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to d \in ℕ$
177	167	eqcomd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c - b = d R$
178	148	recnd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c \in ℂ$
179	150	recnd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to b \in ℂ$
180	167 169	eqeltrd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to d R \in ℂ$
181	178 179 180	subaddd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to (c - b = d R \leftrightarrow b + d R = c)$
182	177 181	mpbid	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to b + d R = c$
183	182	eqcomd	$⊢ ((((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \land (d \in ℤ \land d R = c - b)) \to c = b + d R$
184	145 176 183	reximssdv	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to \exists d \in ℕ c = b + d R$
185	52 184	jca	$⊢ (((φ \land b \in C) \land c \in C) \land ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)) \to (b < c \land \exists d \in ℕ c = b + d R)$
186		fzfid	$⊢ φ \to (0 \dots B) \in Fin$
187		xpfi	$⊢ ((0 \dots B) \in Fin \land (0 \dots B) \in Fin) \to (0 \dots B) \times (0 \dots B) \in Fin$
188	186 186 187	syl2anc	$⊢ φ \to (0 \dots B) \times (0 \dots B) \in Fin$
189		imafi	$⊢ (Fun E \land (0 \dots B) \times (0 \dots B) \in Fin) \to E [(0 \dots B) \times (0 \dots B)] \in Fin$
190	121 188 189	syl2anc	$⊢ φ \to E [(0 \dots B) \times (0 \dots B)] \in Fin$
191	125	eleq1d	$⊢ φ \to (C \in Fin \leftrightarrow E [(0 \dots B) \times (0 \dots B)] \in Fin)$
192	190 191	mpbird	$⊢ φ \to C \in Fin$
193	80	zncrng	$⊢ R \in ℕ_{0} \to ℤ / R ℤ \in CRing$
194	73 193	syl	$⊢ φ \to ℤ / R ℤ \in CRing$
195		crngring	$⊢ ℤ / R ℤ \in CRing \to ℤ / R ℤ \in Ring$
196	194 195	syl	$⊢ φ \to ℤ / R ℤ \in Ring$
197	12	zrhrhm	$⊢ ℤ / R ℤ \in Ring \to L \in (ℤ_{ring} RingHom ℤ / R ℤ)$
198	196 197	syl	$⊢ φ \to L \in (ℤ_{ring} RingHom ℤ / R ℤ)$
199	198	imaexd	$⊢ φ \to L [E [ℕ_{0} \times ℕ_{0}]] \in V$
200		hashclb	$⊢ L [E [ℕ_{0} \times ℕ_{0}]] \in V \to (L [E [ℕ_{0} \times ℕ_{0}]] \in Fin \leftrightarrow \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0})$
201	199 200	syl	$⊢ φ \to (L [E [ℕ_{0} \times ℕ_{0}]] \in Fin \leftrightarrow \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0})$
202	81 201	mpbird	$⊢ φ \to L [E [ℕ_{0} \times ℕ_{0}]] \in Fin$
203		hashcl	$⊢ L [E [ℕ_{0} \times ℕ_{0}]] \in Fin \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
204	202 203	syl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
205	204	nn0red	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ$
206	204	nn0ge0d	$⊢ φ \to 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
207		sqrtmsq	$⊢ (\|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ \land 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|) \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\| \|L [E [ℕ_{0} \times ℕ_{0}]]\|} = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
208	205 206 207	syl2anc	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\| \|L [E [ℕ_{0} \times ℕ_{0}]]\|} = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
209	208	eqcomd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| = \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\| \|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
210	205 206	jca	$⊢ φ \to (\|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ \land 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|)$
211		sqrtmul	$⊢ ((\|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ \land 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|) \land (\|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ \land 0 \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|)) \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\| \|L [E [ℕ_{0} \times ℕ_{0}]]\|} = \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
212	210 210 211	syl2anc	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\| \|L [E [ℕ_{0} \times ℕ_{0}]]\|} = \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
213	205 206	resqrtcld	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \in ℝ$
214	213	flcld	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ$
215	205 206	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}$
216	213 87 88	syl2anc	$⊢ φ \to (0 \leq \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \leftrightarrow 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
217	215 216	mpbid	$⊢ φ \to 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
218	214 217	jca	$⊢ φ \to (⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℤ \land 0 \leq ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋)$
219	218 92	sylibr	$⊢ φ \to ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ \in ℕ_{0}$
220	219 95	mpbird	$⊢ φ \to B \in ℕ_{0}$
221	220	nn0red	$⊢ φ \to B \in ℝ$
222		1red	$⊢ φ \to 1 \in ℝ$
223	221 222	readdcld	$⊢ φ \to B + 1 \in ℝ$
224		flltp1	$⊢ \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \in ℝ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} < ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ + 1$
225	213 224	syl	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} < ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ + 1$
226	94	oveq1d	$⊢ φ \to B + 1 = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋ + 1$
227	225 226	breqtrrd	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} < B + 1$
228	213 223 213 223 215 227 215 227	ltmul12ad	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|} < (B + 1) (B + 1)$
229	212 228	eqbrtrd	$⊢ φ \to \sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\| \|L [E [ℕ_{0} \times ℕ_{0}]]\|} < (B + 1) (B + 1)$
230	209 229	eqbrtrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| < (B + 1) (B + 1)$
231		hashfz0	$⊢ B \in ℕ_{0} \to \|(0 \dots B)\| = B + 1$
232	220 231	syl	$⊢ φ \to \|(0 \dots B)\| = B + 1$
233	232 232	oveq12d	$⊢ φ \to \|(0 \dots B)\| \|(0 \dots B)\| = (B + 1) (B + 1)$
234	230 233	breqtrrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| < \|(0 \dots B)\| \|(0 \dots B)\|$
235	186 186	jca	$⊢ φ \to ((0 \dots B) \in Fin \land (0 \dots B) \in Fin)$
236		hashxp	$⊢ ((0 \dots B) \in Fin \land (0 \dots B) \in Fin) \to \|(0 \dots B) \times (0 \dots B)\| = \|(0 \dots B)\| \|(0 \dots B)\|$
237	235 236	syl	$⊢ φ \to \|(0 \dots B) \times (0 \dots B)\| = \|(0 \dots B)\| \|(0 \dots B)\|$
238	234 237	breqtrrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| < \|(0 \dots B) \times (0 \dots B)\|$
239		ovexd	$⊢ φ \to (0 \dots B) \in V$
240	239 239	jca	$⊢ φ \to ((0 \dots B) \in V \land (0 \dots B) \in V)$
241		xpexg	$⊢ ((0 \dots B) \in V \land (0 \dots B) \in V) \to (0 \dots B) \times (0 \dots B) \in V$
242	240 241	syl	$⊢ φ \to (0 \dots B) \times (0 \dots B) \in V$
243	242	mptexd	$⊢ φ \to (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) \in V$
244	120	adantr	$⊢ (φ \land w \in ((0 \dots B) \times (0 \dots B))) \to E Fn (ℕ_{0} \times ℕ_{0})$
245	110	sselda	$⊢ (φ \land w \in ((0 \dots B) \times (0 \dots B))) \to w \in (ℕ_{0} \times ℕ_{0})$
246		simpr	$⊢ (φ \land w \in ((0 \dots B) \times (0 \dots B))) \to w \in ((0 \dots B) \times (0 \dots B))$
247	244 245 246	fnfvimad	$⊢ (φ \land w \in ((0 \dots B) \times (0 \dots B))) \to E (w) \in E [(0 \dots B) \times (0 \dots B)]$
248		eqid	$⊢ (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) = (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w))$
249	247 248	fmptd	$⊢ φ \to (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) ⟶ E [(0 \dots B) \times (0 \dots B)]$
250	119 110	feqresmpt	$⊢ φ \to {E ↾}_{((0 \dots B) \times (0 \dots B))} = (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w))$
251	250	feq1d	$⊢ φ \to (({E ↾}_{((0 \dots B) \times (0 \dots B))}) : (0 \dots B) \times (0 \dots B) ⟶ E [(0 \dots B) \times (0 \dots B)] \leftrightarrow (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) ⟶ E [(0 \dots B) \times (0 \dots B)])$
252	249 251	mpbird	$⊢ φ \to ({E ↾}_{((0 \dots B) \times (0 \dots B))}) : (0 \dots B) \times (0 \dots B) ⟶ E [(0 \dots B) \times (0 \dots B)]$
253		f1resf1	$⊢ (E : ℕ_{0} \times ℕ_{0} \underset{1-1}{⟶} ℕ \land (0 \dots B) \times (0 \dots B) \subseteq ℕ_{0} \times ℕ_{0} \land ({E ↾}_{((0 \dots B) \times (0 \dots B))}) : (0 \dots B) \times (0 \dots B) ⟶ E [(0 \dots B) \times (0 \dots B)]) \to ({E ↾}_{((0 \dots B) \times (0 \dots B))}) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)]$
254	117 110 252 253	syl3anc	$⊢ φ \to ({E ↾}_{((0 \dots B) \times (0 \dots B))}) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)]$
255		eqidd	$⊢ φ \to (0 \dots B) \times (0 \dots B) = (0 \dots B) \times (0 \dots B)$
256		eqidd	$⊢ φ \to E [(0 \dots B) \times (0 \dots B)] = E [(0 \dots B) \times (0 \dots B)]$
257	250 255 256	f1eq123d	$⊢ φ \to (({E ↾}_{((0 \dots B) \times (0 \dots B))}) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)] \leftrightarrow (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)])$
258	254 257	mpbid	$⊢ φ \to (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)]$
259		df-ima	$⊢ E [(0 \dots B) \times (0 \dots B)] = ran ({E ↾}_{((0 \dots B) \times (0 \dots B))})$
260	259	a1i	$⊢ φ \to E [(0 \dots B) \times (0 \dots B)] = ran ({E ↾}_{((0 \dots B) \times (0 \dots B))})$
261	250	rneqd	$⊢ φ \to ran ({E ↾}_{((0 \dots B) \times (0 \dots B))}) = ran (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w))$
262	260 261	eqtr2d	$⊢ φ \to ran (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) = E [(0 \dots B) \times (0 \dots B)]$
263	258 262	jca	$⊢ φ \to ((w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)] \land ran (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) = E [(0 \dots B) \times (0 \dots B)])$
264		dff1o5	$⊢ (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)] \leftrightarrow ((w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1}{⟶} E [(0 \dots B) \times (0 \dots B)] \land ran (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) = E [(0 \dots B) \times (0 \dots B)])$
265	263 264	sylibr	$⊢ φ \to (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)]$
266		f1oeq1	$⊢ u = (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) \to (u : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)] \leftrightarrow (w \in ((0 \dots B) \times (0 \dots B)) ⟼ E (w)) : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)])$
267	243 265 266	spcedv	$⊢ φ \to \exists u u : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)]$
268		hasheqf1oi	$⊢ (0 \dots B) \times (0 \dots B) \in V \to (\exists u u : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)] \to \|(0 \dots B) \times (0 \dots B)\| = \|E [(0 \dots B) \times (0 \dots B)]\|)$
269	242 268	syl	$⊢ φ \to (\exists u u : (0 \dots B) \times (0 \dots B) \underset{1-1 onto}{⟶} E [(0 \dots B) \times (0 \dots B)] \to \|(0 \dots B) \times (0 \dots B)\| = \|E [(0 \dots B) \times (0 \dots B)]\|)$
270	267 269	mpd	$⊢ φ \to \|(0 \dots B) \times (0 \dots B)\| = \|E [(0 \dots B) \times (0 \dots B)]\|$
271	238 270	breqtrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| < \|E [(0 \dots B) \times (0 \dots B)]\|$
272	125	fveq2d	$⊢ φ \to \|C\| = \|E [(0 \dots B) \times (0 \dots B)]\|$
273	271 272	breqtrrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| < \|C\|$
274		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
275		eqid	$⊢ {Base}_{ℤ / R ℤ} = {Base}_{ℤ / R ℤ}$
276	274 275	rhmf	$⊢ L \in (ℤ_{ring} RingHom ℤ / R ℤ) \to L : ℤ ⟶ {Base}_{ℤ / R ℤ}$
277	198 276	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{ℤ / R ℤ}$
278	277	ffnd	$⊢ φ \to L Fn ℤ$
279	278	adantr	$⊢ (φ \land t \in C) \to L Fn ℤ$
280		resss	$⊢ {E ↾}_{(ℕ_{0} \times ℕ_{0})} \subseteq E$
281	280	a1i	$⊢ φ \to {E ↾}_{(ℕ_{0} \times ℕ_{0})} \subseteq E$
282		rnss	$⊢ {E ↾}_{(ℕ_{0} \times ℕ_{0})} \subseteq E \to ran ({E ↾}_{(ℕ_{0} \times ℕ_{0})}) \subseteq ran E$
283	281 282	syl	$⊢ φ \to ran ({E ↾}_{(ℕ_{0} \times ℕ_{0})}) \subseteq ran E$
284		df-ima	$⊢ E [ℕ_{0} \times ℕ_{0}] = ran ({E ↾}_{(ℕ_{0} \times ℕ_{0})})$
285	284	a1i	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] = ran ({E ↾}_{(ℕ_{0} \times ℕ_{0})})$
286	285	sseq1d	$⊢ φ \to (E [ℕ_{0} \times ℕ_{0}] \subseteq ran E \leftrightarrow ran ({E ↾}_{(ℕ_{0} \times ℕ_{0})}) \subseteq ran E)$
287	283 286	mpbird	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \subseteq ran E$
288		frn	$⊢ E : ℕ_{0} \times ℕ_{0} ⟶ ℕ \to ran E \subseteq ℕ$
289	119 288	syl	$⊢ φ \to ran E \subseteq ℕ$
290	287 289	sstrd	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \subseteq ℕ$
291		nnssz	$⊢ ℕ \subseteq ℤ$
292	291	a1i	$⊢ φ \to ℕ \subseteq ℤ$
293	290 292	sstrd	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ$
294	293	adantr	$⊢ (φ \land t \in C) \to E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ$
295	125	sseq1d	$⊢ φ \to (C \subseteq E [ℕ_{0} \times ℕ_{0}] \leftrightarrow E [(0 \dots B) \times (0 \dots B)] \subseteq E [ℕ_{0} \times ℕ_{0}])$
296	112 295	mpbird	$⊢ φ \to C \subseteq E [ℕ_{0} \times ℕ_{0}]$
297	296	sseld	$⊢ φ \to (t \in C \to t \in E [ℕ_{0} \times ℕ_{0}])$
298	297	imp	$⊢ (φ \land t \in C) \to t \in E [ℕ_{0} \times ℕ_{0}]$
299		fnfvima	$⊢ (L Fn ℤ \land E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ \land t \in E [ℕ_{0} \times ℕ_{0}]) \to L (t) \in L [E [ℕ_{0} \times ℕ_{0}]]$
300	279 294 298 299	syl3anc	$⊢ (φ \land t \in C) \to L (t) \in L [E [ℕ_{0} \times ℕ_{0}]]$
301		eqid	$⊢ (t \in C ⟼ L (t)) = (t \in C ⟼ L (t))$
302	300 301	fmptd	$⊢ φ \to (t \in C ⟼ L (t)) : C ⟶ L [E [ℕ_{0} \times ℕ_{0}]]$
303		nnssre	$⊢ ℕ \subseteq ℝ$
304	303	a1i	$⊢ φ \to ℕ \subseteq ℝ$
305	127 304	sstrd	$⊢ φ \to C \subseteq ℝ$
306	192 202 273 302 305	hashnexinjle	$⊢ φ \to \exists b \in C \exists c \in C ((t \in C ⟼ L (t)) (b) = (t \in C ⟼ L (t)) (c) \land b < c)$
307	185 306	reximddv2	$⊢ φ \to \exists b \in C \exists c \in C (b < c \land \exists d \in ℕ c = b + d R)$
308	51 307	r19.29vva	$⊢ φ \to \|H [{ℕ_{0}}^{(0 \dots A)}]\| \leq N^{B}$

Metamath Proof Explorer

Theorem aks6d1c2

Proof