Theorem aks6d1c7lem1

Description: The last set of inequalities of Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . (Contributed by metakunt, 12-May-2025)

	Ref	Expression
Hypotheses	aks6d1c7lem1.1	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c7lem1.2	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c7lem1.3	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks6d1c7lem1.4	$$⊢\phi \to P\parallel N$$
	aks6d1c7lem1.5	$$⊢\phi \to N\gcd R=1$$
	aks6d1c7lem1.6	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
	aks6d1c7lem1.7	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
	aks6d1c7lem1.8	$$⊢D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
	aks6d1c7lem1.9	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
	aks6d1c7lem1.10	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
Assertion	aks6d1c7lem1	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{D+A}{D-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7lem1.1	$$⊢\phi \to P\in \mathbb{P}$$
2		aks6d1c7lem1.2	$$⊢\phi \to R\in \mathbb{N}$$
3		aks6d1c7lem1.3	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
4		aks6d1c7lem1.4	$$⊢\phi \to P\parallel N$$
5		aks6d1c7lem1.5	$$⊢\phi \to N\gcd R=1$$
6		aks6d1c7lem1.6	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
7		aks6d1c7lem1.7	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
8		aks6d1c7lem1.8	$$⊢D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
9		aks6d1c7lem1.9	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
10		aks6d1c7lem1.10	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
11		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
12	3 11	syl	$$⊢\phi \to N\in \mathbb{Z}$$
13		0red	$$⊢\phi \to 0\in ℝ$$
14		3re	$$⊢3\in ℝ$$
15	14	a1i	$$⊢\phi \to 3\in ℝ$$
16	12	zred	$$⊢\phi \to N\in ℝ$$
17		3pos	$$⊢0<3$$
18	17	a1i	$$⊢\phi \to 0<3$$
19		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
20	3 19	syl	$$⊢\phi \to 3\le N$$
21	13 15 16 18 20	ltletrd	$$⊢\phi \to 0<N$$
22	12 21	jca	$$⊢\phi \to \left(N\in \mathbb{Z}\wedge 0<N\right)$$
23		elnnz	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in \mathbb{Z}\wedge 0<N\right)$$
24	22 23	sylibr	$$⊢\phi \to N\in \mathbb{N}$$
25	24	nnred	$$⊢\phi \to N\in ℝ$$
26	8	a1i	$$⊢\phi \to D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
27		eqid	$$⊢\mathbb{Z}/R\mathbb{Z}=\mathbb{Z}/R\mathbb{Z}$$
28	24 1 4 2 5 6 7 27	hashscontpowcl	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0$$
29	26 28	eqeltrd	$$⊢\phi \to D\in {\mathbb{N}}_0$$
30	29	nn0red	$$⊢\phi \to D\in ℝ$$
31	29	nn0ge0d	$$⊢\phi \to 0\le D$$
32	30 31	resqrtcld	$$⊢\phi \to \sqrt{D}\in ℝ$$
33	32	flcld	$$⊢\phi \to ⌊\sqrt{D}⌋\in \mathbb{Z}$$
34	30 31	sqrtge0d	$$⊢\phi \to 0\le \sqrt{D}$$
35		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
36		flge	$$⊢\left(\sqrt{D}\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le \sqrt{D}\leftrightarrow 0\le ⌊\sqrt{D}⌋\right)$$
37	32 35 36	syl2anc	$$⊢\phi \to \left(0\le \sqrt{D}\leftrightarrow 0\le ⌊\sqrt{D}⌋\right)$$
38	34 37	mpbid	$$⊢\phi \to 0\le ⌊\sqrt{D}⌋$$
39	33 38	jca	$$⊢\phi \to \left(⌊\sqrt{D}⌋\in \mathbb{Z}\wedge 0\le ⌊\sqrt{D}⌋\right)$$
40		elnn0z	$$⊢⌊\sqrt{D}⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊\sqrt{D}⌋\in \mathbb{Z}\wedge 0\le ⌊\sqrt{D}⌋\right)$$
41	39 40	sylibr	$$⊢\phi \to ⌊\sqrt{D}⌋\in {\mathbb{N}}_0$$
42	25 41	reexpcld	$$⊢\phi \to N^{⌊\sqrt{D}⌋}\in ℝ$$
43		2re	$$⊢2\in ℝ$$
44	43	a1i	$$⊢\phi \to 2\in ℝ$$
45		2pos	$$⊢0<2$$
46	45	a1i	$$⊢\phi \to 0<2$$
47	24	nngt0d	$$⊢\phi \to 0<N$$
48		1ne2	$$⊢1\ne 2$$
49	48	necomi	$$⊢2\ne 1$$
50	49	a1i	$$⊢\phi \to 2\ne 1$$
51	44 46 25 47 50	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
52	26 30	eqeltrrd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in ℝ$$
53	31 26	breqtrd	$$⊢\phi \to 0\le \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
54	52 53	resqrtcld	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ$$
55	51 54	remulcld	$$⊢\phi \to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ$$
56	55	flcld	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in \mathbb{Z}$$
57		1red	$$⊢\phi \to 1\in ℝ$$
58		0le1	$$⊢0\le 1$$
59	58	a1i	$$⊢\phi \to 0\le 1$$
60	44	recnd	$$⊢\phi \to 2\in ℂ$$
61	13 46	gtned	$$⊢\phi \to 2\ne 0$$
62		logbid1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}2=1$$
63	60 61 50 62	syl3anc	$$⊢\phi \to {\log }_{2}2=1$$
64	63	eqcomd	$$⊢\phi \to 1={\log }_{2}2$$
65		2z	$$⊢2\in \mathbb{Z}$$
66	65	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
67	44	leidd	$$⊢\phi \to 2\le 2$$
68		1nn0	$$⊢1\in {\mathbb{N}}_0$$
69	43 68	nn0addge1i	$$⊢2\le 2+1$$
70		2p1e3	$$⊢2+1=3$$
71	69 70	breqtri	$$⊢2\le 3$$
72	71	a1i	$$⊢\phi \to 2\le 3$$
73	44 15 16 72 20	letrd	$$⊢\phi \to 2\le N$$
74	66 67 44 46 16 21 73	logblebd	$$⊢\phi \to {\log }_{2}2\le {\log }_{2}N$$
75	64 74	eqbrtrd	$$⊢\phi \to 1\le {\log }_{2}N$$
76	13 57 51 59 75	letrd	$$⊢\phi \to 0\le {\log }_{2}N$$
77	52 53	sqrtge0d	$$⊢\phi \to 0\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
78	51 54 76 77	mulge0d	$$⊢\phi \to 0\le {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
79		flge	$$⊢\left({\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\leftrightarrow 0\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)$$
80	55 35 79	syl2anc	$$⊢\phi \to \left(0\le {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\leftrightarrow 0\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)$$
81	78 80	mpbid	$$⊢\phi \to 0\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
82	56 81	jca	$$⊢\phi \to \left(⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)$$
83		elnn0z	$$⊢⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)$$
84	82 83	sylibr	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in {\mathbb{N}}_0$$
85	68	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
86	84 85	nn0addcld	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in {\mathbb{N}}_0$$
87	2	phicld	$$⊢\phi \to \mathrm{\varphi }\left(R\right)\in \mathbb{N}$$
88	87	nnred	$$⊢\phi \to \mathrm{\varphi }\left(R\right)\in ℝ$$
89	87	nnnn0d	$$⊢\phi \to \mathrm{\varphi }\left(R\right)\in {\mathbb{N}}_0$$
90	89	nn0ge0d	$$⊢\phi \to 0\le \mathrm{\varphi }\left(R\right)$$
91	88 90	resqrtcld	$$⊢\phi \to \sqrt{\mathrm{\varphi }\left(R\right)}\in ℝ$$
92	91 51	remulcld	$$⊢\phi \to \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N\in ℝ$$
93	92	flcld	$$⊢\phi \to ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in \mathbb{Z}$$
94	88 90	sqrtge0d	$$⊢\phi \to 0\le \sqrt{\mathrm{\varphi }\left(R\right)}$$
95	91 51 94 76	mulge0d	$$⊢\phi \to 0\le \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N$$
96		flge	$$⊢\left(\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N\leftrightarrow 0\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\right)$$
97	92 35 96	syl2anc	$$⊢\phi \to \left(0\le \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N\leftrightarrow 0\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\right)$$
98	95 97	mpbid	$$⊢\phi \to 0\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
99	93 98	jca	$$⊢\phi \to \left(⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in \mathbb{Z}\wedge 0\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\right)$$
100		elnn0z	$$⊢⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in \mathbb{Z}\wedge 0\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\right)$$
101	99 100	sylibr	$$⊢\phi \to ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0$$
102	86 101	nn0addcld	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0$$
103	56	peano2zd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in \mathbb{Z}$$
104		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
105	104	znegcld	$$⊢\phi \to -1\in \mathbb{Z}$$
106	103 105	zaddcld	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1\in \mathbb{Z}$$
107		bccl	$$⊢\left(⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0\wedge ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1\in \mathbb{Z}\right)\to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1}\right)\in {\mathbb{N}}_0$$
108	102 106 107	syl2anc	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1}\right)\in {\mathbb{N}}_0$$
109	108	nn0red	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1}\right)\in ℝ$$
110	28 101	nn0addcld	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0$$
111	28	nn0zd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in \mathbb{Z}$$
112	111 105	zaddcld	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1\in \mathbb{Z}$$
113		bccl	$$⊢\left(\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0\wedge \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1\in \mathbb{Z}\right)\to \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1}\right)\in {\mathbb{N}}_0$$
114	110 112 113	syl2anc	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1}\right)\in {\mathbb{N}}_0$$
115	114	nn0red	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1}\right)\in ℝ$$
116	54 51	remulcld	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\in ℝ$$
117	116	flcld	$$⊢\phi \to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in \mathbb{Z}$$
118	54 51 77 76	mulge0d	$$⊢\phi \to 0\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N$$
119		flge	$$⊢\left(\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\leftrightarrow 0\le ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\right)$$
120	116 35 119	syl2anc	$$⊢\phi \to \left(0\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\leftrightarrow 0\le ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\right)$$
121	118 120	mpbid	$$⊢\phi \to 0\le ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋$$
122	117 121	jca	$$⊢\phi \to \left(⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in \mathbb{Z}\wedge 0\le ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\right)$$
123		elnn0z	$$⊢⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in \mathbb{Z}\wedge 0\le ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\right)$$
124	122 123	sylibr	$$⊢\phi \to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in {\mathbb{N}}_0$$
125	86 124	nn0addcld	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in {\mathbb{N}}_0$$
126		bccl	$$⊢\left(⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in {\mathbb{N}}_0\wedge ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in \mathbb{Z}\right)\to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in {\mathbb{N}}_0$$
127	125 56 126	syl2anc	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in {\mathbb{N}}_0$$
128	127	nn0red	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in ℝ$$
129		bccl	$$⊢\left(⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in {\mathbb{N}}_0\wedge ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in \mathbb{Z}\right)\to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in {\mathbb{N}}_0$$
130	102 56 129	syl2anc	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in {\mathbb{N}}_0$$
131	130	nn0red	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in ℝ$$
132	44 86	reexpcld	$$⊢\phi \to 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}\in ℝ$$
133		2nn0	$$⊢2\in {\mathbb{N}}_0$$
134	133	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
135	134 84	nn0mulcld	$$⊢\phi \to 2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in {\mathbb{N}}_0$$
136	135 85	nn0addcld	$$⊢\phi \to 2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in {\mathbb{N}}_0$$
137		bccl	$$⊢\left(2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in {\mathbb{N}}_0\wedge ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in \mathbb{Z}\right)\to \left(\genfrac{}{}{0ex}{}{2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in {\mathbb{N}}_0$$
138	136 56 137	syl2anc	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in {\mathbb{N}}_0$$
139	138	nn0red	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\in ℝ$$
140	13 44 46	ltled	$$⊢\phi \to 0\le 2$$
141	44 140 55	recxpcld	$$⊢\phi \to 2^{{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}\in ℝ$$
142		reflcl	$$⊢{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ\to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in ℝ$$
143	55 142	syl	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in ℝ$$
144	143 57	readdcld	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in ℝ$$
145	44 140 144	recxpcld	$$⊢\phi \to 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}\in ℝ$$
146		1le2	$$⊢1\le 2$$
147	146	a1i	$$⊢\phi \to 1\le 2$$
148	57 44 16 147 73	letrd	$$⊢\phi \to 1\le N$$
149		reflcl	$$⊢\sqrt{D}\in ℝ\to ⌊\sqrt{D}⌋\in ℝ$$
150	32 149	syl	$$⊢\phi \to ⌊\sqrt{D}⌋\in ℝ$$
151	26	fveq2d	$$⊢\phi \to \sqrt{D}=\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
152	151	fveq2d	$$⊢\phi \to ⌊\sqrt{D}⌋=⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
153		flle	$$⊢\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ\to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
154	54 153	syl	$$⊢\phi \to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
155	152 154	eqbrtrd	$$⊢\phi \to ⌊\sqrt{D}⌋\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
156	16 148 150 54 155	cxplead	$$⊢\phi \to N^{⌊\sqrt{D}⌋}\le N^{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}$$
157	16	recnd	$$⊢\phi \to N\in ℂ$$
158	13 21	gtned	$$⊢\phi \to N\ne 0$$
159	157 158 33	cxpexpzd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}=N^{⌊\sqrt{D}⌋}$$
160	61 50	nelprd	$$⊢\phi \to \neg 2\in \left\{0,1\right\}$$
161	60 160	eldifd	$$⊢\phi \to 2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
162	158	neneqd	$$⊢\phi \to \neg N=0$$
163		elsng	$$⊢N\in \mathbb{N}\to \left(N\in \left\{0\right\}\leftrightarrow N=0\right)$$
164	24 163	syl	$$⊢\phi \to \left(N\in \left\{0\right\}\leftrightarrow N=0\right)$$
165	162 164	mtbird	$$⊢\phi \to \neg N\in \left\{0\right\}$$
166	157 165	eldifd	$$⊢\phi \to N\in \left(ℂ\setminus \left\{0\right\}\right)$$
167		cxplogb	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge N\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 2^{{\log }_{2}N}=N$$
168	161 166 167	syl2anc	$$⊢\phi \to 2^{{\log }_{2}N}=N$$
169	168	eqcomd	$$⊢\phi \to N=2^{{\log }_{2}N}$$
170	169	oveq1d	$$⊢\phi \to N^{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}={\left(2^{{\log }_{2}N}\right)}^{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}$$
171	156 159 170	3brtr3d	$$⊢\phi \to N^{⌊\sqrt{D}⌋}\le {\left(2^{{\log }_{2}N}\right)}^{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}$$
172	44 46	elrpd	$$⊢\phi \to 2\in {ℝ}^{+}$$
173	54	recnd	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℂ$$
174		cxpmul	$$⊢\left(2\in {ℝ}^{+}\wedge {\log }_{2}N\in ℝ\wedge \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℂ\right)\to 2^{{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}={\left(2^{{\log }_{2}N}\right)}^{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}$$
175	172 51 173 174	syl3anc	$$⊢\phi \to 2^{{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}={\left(2^{{\log }_{2}N}\right)}^{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}$$
176	171 175	breqtrrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}\le 2^{{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}$$
177		fllep1	$$⊢{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ\to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1$$
178	55 177	syl	$$⊢\phi \to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1$$
179	57 44 147 50	leneltd	$$⊢\phi \to 1<2$$
180	86	nn0red	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in ℝ$$
181	44 179 55 180	cxpled	$$⊢\phi \to \left({\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\leftrightarrow 2^{{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}\le 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}\right)$$
182	178 181	mpbid	$$⊢\phi \to 2^{{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}\le 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}$$
183	42 141 145 176 182	letrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}\le 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}$$
184		cxpexpz	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in \mathbb{Z}\right)\to 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}=2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}$$
185	60 61 103 184	syl3anc	$$⊢\phi \to 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}=2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}$$
186	183 185	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}\le 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}$$
187	51 51	jca	$$⊢\phi \to \left({\log }_{2}N\in ℝ\wedge {\log }_{2}N\in ℝ\right)$$
188		remulcl	$$⊢\left({\log }_{2}N\in ℝ\wedge {\log }_{2}N\in ℝ\right)\to {\log }_{2}N{\log }_{2}N\in ℝ$$
189	187 188	syl	$$⊢\phi \to {\log }_{2}N{\log }_{2}N\in ℝ$$
190		reflcl	$$⊢{\log }_{2}N{\log }_{2}N\in ℝ\to ⌊{\log }_{2}N{\log }_{2}N⌋\in ℝ$$
191	189 190	syl	$$⊢\phi \to ⌊{\log }_{2}N{\log }_{2}N⌋\in ℝ$$
192	84	nn0red	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in ℝ$$
193	44 46 15 18 50	relogbcld	$$⊢\phi \to {\log }_{2}3\in ℝ$$
194	193	resqcld	$$⊢\phi \to {{\log }_{2}3}^2\in ℝ$$
195	51	recnd	$$⊢\phi \to {\log }_{2}N\in ℂ$$
196	195	sqvald	$$⊢\phi \to {{\log }_{2}N}^2={\log }_{2}N{\log }_{2}N$$
197	196 189	eqeltrd	$$⊢\phi \to {{\log }_{2}N}^2\in ℝ$$
198		3lexlogpow2ineq2	$$⊢\left(2<{{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<3\right)$$
199	198	simpli	$$⊢2<{{\log }_{2}3}^2$$
200	199	a1i	$$⊢\phi \to 2<{{\log }_{2}3}^2$$
201	44 194 200	ltled	$$⊢\phi \to 2\le {{\log }_{2}3}^2$$
202	15 44 61	redivcld	$$⊢\phi \to \frac{3}{2}\in ℝ$$
203		2rp	$$⊢2\in {ℝ}^{+}$$
204	203	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
205	13 15 18	ltled	$$⊢\phi \to 0\le 3$$
206	15 204 205	divge0d	$$⊢\phi \to 0\le \frac{3}{2}$$
207		3lexlogpow2ineq1	$$⊢\left(\frac{3}{2}<{\log }_{2}3\wedge {\log }_{2}3<\frac{5}{3}\right)$$
208	207	simpli	$$⊢\frac{3}{2}<{\log }_{2}3$$
209	208	a1i	$$⊢\phi \to \frac{3}{2}<{\log }_{2}3$$
210	202 193 209	ltled	$$⊢\phi \to \frac{3}{2}\le {\log }_{2}3$$
211	13 202 193 206 210	letrd	$$⊢\phi \to 0\le {\log }_{2}3$$
212	66 67 15 18 16 21 20	logblebd	$$⊢\phi \to {\log }_{2}3\le {\log }_{2}N$$
213	193 51 134 211 212	leexp1ad	$$⊢\phi \to {{\log }_{2}3}^2\le {{\log }_{2}N}^2$$
214	44 194 197 201 213	letrd	$$⊢\phi \to 2\le {{\log }_{2}N}^2$$
215	214 196	breqtrd	$$⊢\phi \to 2\le {\log }_{2}N{\log }_{2}N$$
216		flge	$$⊢\left({\log }_{2}N{\log }_{2}N\in ℝ\wedge 2\in \mathbb{Z}\right)\to \left(2\le {\log }_{2}N{\log }_{2}N\leftrightarrow 2\le ⌊{\log }_{2}N{\log }_{2}N⌋\right)$$
217	189 66 216	syl2anc	$$⊢\phi \to \left(2\le {\log }_{2}N{\log }_{2}N\leftrightarrow 2\le ⌊{\log }_{2}N{\log }_{2}N⌋\right)$$
218	215 217	mpbid	$$⊢\phi \to 2\le ⌊{\log }_{2}N{\log }_{2}N⌋$$
219	51 51	remulcld	$$⊢\phi \to {\log }_{2}N{\log }_{2}N\in ℝ$$
220	24 1 4 2 5 6 7 27 10	aks6d1c3	$$⊢\phi \to {{\log }_{2}N}^2<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
221	173	sqvald	$$⊢\phi \to {\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}^2=\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
222	28	nn0cnd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in ℂ$$
223	222	msqsqrtd	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
224	221 223	eqtr2d	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|={\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}^2$$
225	220 224	breqtrd	$$⊢\phi \to {{\log }_{2}N}^2<{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}^2$$
226	51 54 76 77	lt2sqd	$$⊢\phi \to \left({\log }_{2}N<\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\leftrightarrow {{\log }_{2}N}^2<{\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}}^2\right)$$
227	225 226	mpbird	$$⊢\phi \to {\log }_{2}N<\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
228	51 54 227	ltled	$$⊢\phi \to {\log }_{2}N\le \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
229	51 54 51 76 228	lemul2ad	$$⊢\phi \to {\log }_{2}N{\log }_{2}N\le {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
230		flwordi	$$⊢\left({\log }_{2}N{\log }_{2}N\in ℝ\wedge {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ\wedge {\log }_{2}N{\log }_{2}N\le {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\right)\to ⌊{\log }_{2}N{\log }_{2}N⌋\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
231	219 55 229 230	syl3anc	$$⊢\phi \to ⌊{\log }_{2}N{\log }_{2}N⌋\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
232	44 191 192 218 231	letrd	$$⊢\phi \to 2\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
233	56 232	2ap1caineq	$$⊢\phi \to 2^{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}<\left(\genfrac{}{}{0ex}{}{2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
234	42 132 139 186 233	lelttrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
235	84	nn0cnd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\in ℂ$$
236	235	2timesd	$$⊢\phi \to 2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
237	236	oveq1d	$$⊢\phi \to 2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1$$
238	237	oveq1d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)=\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
239	234 238	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
240		1cnd	$$⊢\phi \to 1\in ℂ$$
241	235 235 240	addassd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1$$
242	86	nn0cnd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\in ℂ$$
243	235 242	addcomd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
244	241 243	eqtrd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
245	244	oveq1d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)=\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
246	239 245	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
247	195 173	mulcomd	$$⊢\phi \to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}=\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N$$
248	247	fveq2d	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋=⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋$$
249	248	oveq2d	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋$$
250	249	oveq1d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)=\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
251	246 250	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
252	124	nn0red	$$⊢\phi \to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\in ℝ$$
253	101	nn0red	$$⊢\phi \to ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋\in ℝ$$
254	8 29	eqeltrrid	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0$$
255	254	nn0red	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in ℝ$$
256	254	nn0ge0d	$$⊢\phi \to 0\le \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
257	255 256	resqrtcld	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ$$
258	257 51	remulcld	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\in ℝ$$
259	24 1 4 2 5 6 7	aks6d1c4	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\le \mathrm{\varphi }\left(R\right)$$
260	52 53 88 90	sqrtled	$$⊢\phi \to \left(\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\le \mathrm{\varphi }\left(R\right)\leftrightarrow \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\le \sqrt{\mathrm{\varphi }\left(R\right)}\right)$$
261	259 260	mpbid	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\le \sqrt{\mathrm{\varphi }\left(R\right)}$$
262	257 91 51 76 261	lemul1ad	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\le \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N$$
263		flwordi	$$⊢\left(\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\in ℝ\wedge \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N\in ℝ\wedge \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N\le \sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N\right)\to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
264	258 92 262 263	syl3anc	$$⊢\phi \to ⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
265	252 253 144 264	leadd2dd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋\le ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
266	125 102 56 265	bcled	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)\le \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
267	42 128 131 251 266	ltletrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)$$
268	235 240	pncand	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1-1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
269	268	eqcomd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1-1$$
270	242 240	negsubd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1-1$$
271	270	eqcomd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1-1=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1$$
272	269 271	eqtrd	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋=⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1$$
273	272	oveq2d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋}\right)=\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1}\right)$$
274	267 273	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1}\right)$$
275	2	nnnn0d	$$⊢\phi \to R\in {\mathbb{N}}_0$$
276	27	zncrng	$$⊢R\in {\mathbb{N}}_0\to \mathbb{Z}/R\mathbb{Z}\in \mathrm{CRing}$$
277	275 276	syl	$$⊢\phi \to \mathbb{Z}/R\mathbb{Z}\in \mathrm{CRing}$$
278		crngring	$$⊢\mathbb{Z}/R\mathbb{Z}\in \mathrm{CRing}\to \mathbb{Z}/R\mathbb{Z}\in \mathrm{Ring}$$
279	7	zrhrhm	$$⊢\mathbb{Z}/R\mathbb{Z}\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\mathbb{Z}/R\mathbb{Z}\right)$$
280		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
281		eqid	$$⊢{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}={\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
282	280 281	rhmf	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\mathbb{Z}/R\mathbb{Z}\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
283	277 278 279 282	4syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
284	283	ffnd	$$⊢\phi \to LFn\mathbb{Z}$$
285	24 1 4 6	aks6d1c2p1	$$⊢\phi \to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{N}$$
286		nnssz	$$⊢\mathbb{N}\subseteq \mathbb{Z}$$
287	286	a1i	$$⊢\phi \to \mathbb{N}\subseteq \mathbb{Z}$$
288	285 287	fssd	$$⊢\phi \to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{Z}$$
289		frn	$$⊢E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{Z}\to \mathrm{ran}E\subseteq \mathbb{Z}$$
290	288 289	syl	$$⊢\phi \to \mathrm{ran}E\subseteq \mathbb{Z}$$
291	285	ffnd	$$⊢\phi \to EFn\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
292		fnima	$$⊢EFn\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]=\mathrm{ran}E$$
293	291 292	syl	$$⊢\phi \to E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]=\mathrm{ran}E$$
294	293	sseq1d	$$⊢\phi \to \left(E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\subseteq \mathbb{Z}\leftrightarrow \mathrm{ran}E\subseteq \mathbb{Z}\right)$$
295	290 294	mpbird	$$⊢\phi \to E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\subseteq \mathbb{Z}$$
296		vex	$$⊢k\in \mathrm{V}$$
297		vex	$$⊢l\in \mathrm{V}$$
298	296 297	op1std	$$⊢v=⟨k,l⟩\to 1^{st}\left(v\right)=k$$
299	298	oveq2d	$$⊢v=⟨k,l⟩\to P^{1^{st}\left(v\right)}=P^k$$
300	296 297	op2ndd	$$⊢v=⟨k,l⟩\to 2^{nd}\left(v\right)=l$$
301	300	oveq2d	$$⊢v=⟨k,l⟩\to {\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}={\left(\frac{N}{P}\right)}^l$$
302	299 301	oveq12d	$$⊢v=⟨k,l⟩\to P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}=P^k{\left(\frac{N}{P}\right)}^l$$
303	302	mpompt	$$⊢\left(v\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}\right)=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
304	303	eqcomi	$$⊢\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)=\left(v\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}\right)$$
305	6 304	eqtri	$$⊢E=\left(v\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}\right)$$
306	305	a1i	$$⊢\phi \to E=\left(v\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}\right)$$
307		c0ex	$$⊢0\in \mathrm{V}$$
308	307 307	op1std	$$⊢v=⟨0,0⟩\to 1^{st}\left(v\right)=0$$
309	308	adantl	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to 1^{st}\left(v\right)=0$$
310	309	oveq2d	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to P^{1^{st}\left(v\right)}=P^0$$
311	307 307	op2ndd	$$⊢v=⟨0,0⟩\to 2^{nd}\left(v\right)=0$$
312	311	adantl	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to 2^{nd}\left(v\right)=0$$
313	312	oveq2d	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to {\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}={\left(\frac{N}{P}\right)}^0$$
314	310 313	oveq12d	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}=P^0{\left(\frac{N}{P}\right)}^0$$
315		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
316	1 315	syl	$$⊢\phi \to P\in \mathbb{N}$$
317	316	nncnd	$$⊢\phi \to P\in ℂ$$
318	317	exp0d	$$⊢\phi \to P^0=1$$
319	316	nnne0d	$$⊢\phi \to P\ne 0$$
320	157 317 319	divcld	$$⊢\phi \to \frac{N}{P}\in ℂ$$
321	320	exp0d	$$⊢\phi \to {\left(\frac{N}{P}\right)}^0=1$$
322	318 321	oveq12d	$$⊢\phi \to P^0{\left(\frac{N}{P}\right)}^0=1\cdot 1$$
323	240	mulridd	$$⊢\phi \to 1\cdot 1=1$$
324	322 323	eqtrd	$$⊢\phi \to P^0{\left(\frac{N}{P}\right)}^0=1$$
325	324	adantr	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to P^0{\left(\frac{N}{P}\right)}^0=1$$
326	314 325	eqtrd	$$⊢\left(\phi \wedge v=⟨0,0⟩\right)\to P^{1^{st}\left(v\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(v\right)}=1$$
327		0nn0	$$⊢0\in {\mathbb{N}}_0$$
328	327	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
329	328 328	opelxpd	$$⊢\phi \to ⟨0,0⟩\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
330		1nn	$$⊢1\in \mathbb{N}$$
331	330	a1i	$$⊢\phi \to 1\in \mathbb{N}$$
332	306 326 329 331	fvmptd	$$⊢\phi \to E\left(⟨0,0⟩\right)=1$$
333		ssidd	$$⊢\phi \to {\mathbb{N}}_0\times {\mathbb{N}}_0\subseteq {\mathbb{N}}_0\times {\mathbb{N}}_0$$
334		fnfvima	$$⊢\left(EFn\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\wedge {\mathbb{N}}_0\times {\mathbb{N}}_0\subseteq {\mathbb{N}}_0\times {\mathbb{N}}_0\wedge ⟨0,0⟩\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to E\left(⟨0,0⟩\right)\in E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]$$
335	291 333 329 334	syl3anc	$$⊢\phi \to E\left(⟨0,0⟩\right)\in E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]$$
336	332 335	eqeltrrd	$$⊢\phi \to 1\in E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]$$
337		fnfvima	$$⊢\left(LFn\mathbb{Z}\wedge E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\subseteq \mathbb{Z}\wedge 1\in E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right)\to L\left(1\right)\in L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]$$
338	284 295 336 337	syl3anc	$$⊢\phi \to L\left(1\right)\in L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]$$
339	7	a1i	$$⊢\phi \to L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
340		fvexd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\in \mathrm{V}$$
341	339 340	eqeltrd	$$⊢\phi \to L\in \mathrm{V}$$
342	341	imaexd	$$⊢\phi \to L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\in \mathrm{V}$$
343	338 342	hashelne0d	$$⊢\phi \to \neg \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|=0$$
344	343	neqned	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\ne 0$$
345	28 344	jca	$$⊢\phi \to \left(\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0\wedge \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\ne 0\right)$$
346		elnnne0	$$⊢\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in \mathbb{N}\leftrightarrow \left(\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0\wedge \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\ne 0\right)$$
347	345 346	sylibr	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in \mathbb{N}$$
348	347	nnrpd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {ℝ}^{+}$$
349	348	rpsqrtcld	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in {ℝ}^{+}$$
350	51 54 349 227	ltmul1dd	$$⊢\phi \to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}<\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
351	52 53 52 53	sqrtmuld	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}=\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
352	351	eqcomd	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}=\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
353	350 352	breqtrd	$$⊢\phi \to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}<\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}$$
354	351 223	eqtrd	$$⊢\phi \to \sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
355	353 354	breqtrd	$$⊢\phi \to {\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
356		fllt	$$⊢\left({\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}\in ℝ\wedge \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in \mathbb{Z}\right)\to \left({\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\leftrightarrow ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\right)$$
357	55 111 356	syl2anc	$$⊢\phi \to \left({\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\leftrightarrow ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\right)$$
358	355 357	mpbid	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
359	56 111	zltp1led	$$⊢\phi \to \left(⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋<\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\leftrightarrow ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\le \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\right)$$
360	358 359	mpbid	$$⊢\phi \to ⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1\le \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
361	57	renegcld	$$⊢\phi \to -1\in ℝ$$
362		df-neg	$$⊢-1=0-1$$
363	362	a1i	$$⊢\phi \to -1=0-1$$
364	13	lem1d	$$⊢\phi \to 0-1\le 0$$
365	363 364	eqbrtrd	$$⊢\phi \to -1\le 0$$
366	361 13 253 365 98	letrd	$$⊢\phi \to -1\le ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
367	86 28 101 105 360 366	bcle2d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{⌊{\log }_{2}N\sqrt{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋+1+-1}\right)\le \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1}\right)$$
368	42 109 115 274 367	ltletrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1}\right)$$
369	222 240	negsubd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1$$
370	369	oveq2d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+-1}\right)=\left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1}\right)$$
371	368 370	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1}\right)$$
372	9	eqcomi	$$⊢⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋=A$$
373	372	a1i	$$⊢\phi \to ⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋=A$$
374	373	oveq2d	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+A$$
375	374	oveq1d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1}\right)=\left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+A}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1}\right)$$
376	371 375	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+A}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1}\right)$$
377	26	eqcomd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|=D$$
378	377	oveq1d	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+A=D+A$$
379	377	oveq1d	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1=D-1$$
380	378 379	oveq12d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|+A}{\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1}\right)=\left(\genfrac{}{}{0ex}{}{D+A}{D-1}\right)$$
381	376 380	breqtrd	$$⊢\phi \to N^{⌊\sqrt{D}⌋}<\left(\genfrac{}{}{0ex}{}{D+A}{D-1}\right)$$