Theorem knoppndvlem19

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 17-Aug-2021)

	Ref	Expression
Hypotheses	knoppndvlem19.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)m$$
	knoppndvlem19.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(m+1\right)$$
	knoppndvlem19.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	knoppndvlem19.h	$$⊢\phi \to H\in ℝ$$
	knoppndvlem19.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	knoppndvlem19	$$⊢\phi \to \exists m\in \mathbb{Z}\left(A\le H\wedge H\le B\right)$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem19.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)m$$
2		knoppndvlem19.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(m+1\right)$$
3		knoppndvlem19.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
4		knoppndvlem19.h	$$⊢\phi \to H\in ℝ$$
5		knoppndvlem19.n	$$⊢\phi \to N\in \mathbb{N}$$
6		2re	$$⊢2\in ℝ$$
7	6	a1i	$$⊢\phi \to 2\in ℝ$$
8	5	nnred	$$⊢\phi \to N\in ℝ$$
9	7 8	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
10		2pos	$$⊢0<2$$
11	10	a1i	$$⊢\phi \to 0<2$$
12	5	nngt0d	$$⊢\phi \to 0<N$$
13	7 8 11 12	mulgt0d	$$⊢\phi \to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
14	13	gt0ne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
15	3	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
16	15	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
17	9 14 16	reexpclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℝ$$
18	7	recnd	$$⊢\phi \to 2\in ℂ$$
19	8	recnd	$$⊢\phi \to N\in ℂ$$
20	18 19 14	mulne0bad	$$⊢\phi \to 2\ne 0$$
21	17 7 20	redivcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℝ$$
22	9 16 13	3jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge -J\in \mathbb{Z}\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
23		expgt0	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge -J\in \mathbb{Z}\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to 0<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
24	22 23	syl	$$⊢\phi \to 0<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
25	17 7 24 11	divgt0d	$$⊢\phi \to 0<\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
26	25	gt0ne0d	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\ne 0$$
27	4 21 26	redivcld	$$⊢\phi \to \frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\in ℝ$$
28	27	flcld	$$⊢\phi \to ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\in \mathbb{Z}$$
29	1	a1i	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)m$$
30		id	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋$$
31	30	oveq2d	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)m=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋$$
32	29 31	eqtrd	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋$$
33	32	breq1d	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to \left(A\le H\leftrightarrow \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le H\right)$$
34	2	a1i	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(m+1\right)$$
35	30	oveq1d	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to m+1=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1$$
36	35	oveq2d	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(m+1\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)$$
37	34 36	eqtrd	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)$$
38	37	breq2d	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to \left(H\le B\leftrightarrow H\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)\right)$$
39	33 38	anbi12d	$$⊢m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\to \left(\left(A\le H\wedge H\le B\right)\leftrightarrow \left(\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le H\wedge H\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)\right)\right)$$
40	39	adantl	$$⊢\left(\phi \wedge m=⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\right)\to \left(\left(A\le H\wedge H\le B\right)\leftrightarrow \left(\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le H\wedge H\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)\right)\right)$$
41	28	zred	$$⊢\phi \to ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\in ℝ$$
42		0red	$$⊢\phi \to 0\in ℝ$$
43	42 21 25	ltled	$$⊢\phi \to 0\le \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
44		flle	$$⊢\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\in ℝ\to ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le \frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}$$
45	27 44	syl	$$⊢\phi \to ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le \frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}$$
46	41 27 21 43 45	lemul2ad	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)$$
47	4	recnd	$$⊢\phi \to H\in ℂ$$
48	21	recnd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℂ$$
49	47 48 26	divcan2d	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)=H$$
50	46 49	breqtrd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le H$$
51	49	eqcomd	$$⊢\phi \to H=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)$$
52		peano2re	$$⊢⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\in ℝ\to ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\in ℝ$$
53	41 52	syl	$$⊢\phi \to ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\in ℝ$$
54		fllep1	$$⊢\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\in ℝ\to \frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\le ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1$$
55	27 54	syl	$$⊢\phi \to \frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\le ⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1$$
56	27 53 21 43 55	lemul2ad	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)$$
57	51 56	eqbrtrd	$$⊢\phi \to H\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)$$
58	50 57	jca	$$⊢\phi \to \left(\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋\le H\wedge H\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(⌊\frac{H}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}⌋+1\right)\right)$$
59	28 40 58	rspcedvd	$$⊢\phi \to \exists m\in \mathbb{Z}\left(A\le H\wedge H\le B\right)$$