Theorem rmygeid

Description: Y(n) increases faster than n. Used implicitly without proof or comment in lemma 2.27 of JonesMatijasevic p. 697. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	rmygeid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N\le A{Y}_{\mathrm{rm}}N$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢a=0\to a=0$$
2		oveq2	$$⊢a=0\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}0$$
3	1 2	breq12d	$$⊢a=0\to \left(a\le A{Y}_{\mathrm{rm}}a\leftrightarrow 0\le A{Y}_{\mathrm{rm}}0\right)$$
4	3	imbi2d	$$⊢a=0\to \left(\left(A\in {\mathbb{Z}}_{\ge 2}\to a\le A{Y}_{\mathrm{rm}}a\right)\leftrightarrow \left(A\in {\mathbb{Z}}_{\ge 2}\to 0\le A{Y}_{\mathrm{rm}}0\right)\right)$$
5		id	$$⊢a=b\to a=b$$
6		oveq2	$$⊢a=b\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}b$$
7	5 6	breq12d	$$⊢a=b\to \left(a\le A{Y}_{\mathrm{rm}}a\leftrightarrow b\le A{Y}_{\mathrm{rm}}b\right)$$
8	7	imbi2d	$$⊢a=b\to \left(\left(A\in {\mathbb{Z}}_{\ge 2}\to a\le A{Y}_{\mathrm{rm}}a\right)\leftrightarrow \left(A\in {\mathbb{Z}}_{\ge 2}\to b\le A{Y}_{\mathrm{rm}}b\right)\right)$$
9		id	$$⊢a=b+1\to a=b+1$$
10		oveq2	$$⊢a=b+1\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}\left(b+1\right)$$
11	9 10	breq12d	$$⊢a=b+1\to \left(a\le A{Y}_{\mathrm{rm}}a\leftrightarrow b+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)\right)$$
12	11	imbi2d	$$⊢a=b+1\to \left(\left(A\in {\mathbb{Z}}_{\ge 2}\to a\le A{Y}_{\mathrm{rm}}a\right)\leftrightarrow \left(A\in {\mathbb{Z}}_{\ge 2}\to b+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)\right)\right)$$
13		id	$$⊢a=N\to a=N$$
14		oveq2	$$⊢a=N\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}N$$
15	13 14	breq12d	$$⊢a=N\to \left(a\le A{Y}_{\mathrm{rm}}a\leftrightarrow N\le A{Y}_{\mathrm{rm}}N\right)$$
16	15	imbi2d	$$⊢a=N\to \left(\left(A\in {\mathbb{Z}}_{\ge 2}\to a\le A{Y}_{\mathrm{rm}}a\right)\leftrightarrow \left(A\in {\mathbb{Z}}_{\ge 2}\to N\le A{Y}_{\mathrm{rm}}N\right)\right)$$
17		0le0	$$⊢0\le 0$$
18		rmy0	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}0=0$$
19	17 18	breqtrrid	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 0\le A{Y}_{\mathrm{rm}}0$$
20		nn0z	$$⊢b\in {\mathbb{N}}_0\to b\in \mathbb{Z}$$
21	20	3ad2ant1	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b\in \mathbb{Z}$$
22	21	peano2zd	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b+1\in \mathbb{Z}$$
23	22	zred	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b+1\in ℝ$$
24		simp2	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to A\in {\mathbb{Z}}_{\ge 2}$$
25		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
26	25	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}b\in \mathbb{Z}$$
27	24 21 26	syl2anc	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to A{Y}_{\mathrm{rm}}b\in \mathbb{Z}$$
28	27	peano2zd	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to \left(A{Y}_{\mathrm{rm}}b\right)+1\in \mathbb{Z}$$
29	28	zred	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to \left(A{Y}_{\mathrm{rm}}b\right)+1\in ℝ$$
30	25	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b+1\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}\left(b+1\right)\in \mathbb{Z}$$
31	24 22 30	syl2anc	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to A{Y}_{\mathrm{rm}}\left(b+1\right)\in \mathbb{Z}$$
32	31	zred	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to A{Y}_{\mathrm{rm}}\left(b+1\right)\in ℝ$$
33		nn0re	$$⊢b\in {\mathbb{N}}_0\to b\in ℝ$$
34	33	3ad2ant1	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b\in ℝ$$
35	27	zred	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to A{Y}_{\mathrm{rm}}b\in ℝ$$
36		1red	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to 1\in ℝ$$
37		simp3	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b\le A{Y}_{\mathrm{rm}}b$$
38	34 35 36 37	leadd1dd	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b+1\le \left(A{Y}_{\mathrm{rm}}b\right)+1$$
39	34	ltp1d	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b<b+1$$
40		ltrmy	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\wedge b+1\in \mathbb{Z}\right)\to \left(b<b+1\leftrightarrow A{Y}_{\mathrm{rm}}b<A{Y}_{\mathrm{rm}}\left(b+1\right)\right)$$
41	24 21 22 40	syl3anc	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to \left(b<b+1\leftrightarrow A{Y}_{\mathrm{rm}}b<A{Y}_{\mathrm{rm}}\left(b+1\right)\right)$$
42	39 41	mpbid	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to A{Y}_{\mathrm{rm}}b<A{Y}_{\mathrm{rm}}\left(b+1\right)$$
43		zltp1le	$$⊢\left(A{Y}_{\mathrm{rm}}b\in \mathbb{Z}\wedge A{Y}_{\mathrm{rm}}\left(b+1\right)\in \mathbb{Z}\right)\to \left(A{Y}_{\mathrm{rm}}b<A{Y}_{\mathrm{rm}}\left(b+1\right)\leftrightarrow \left(A{Y}_{\mathrm{rm}}b\right)+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)\right)$$
44	27 31 43	syl2anc	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to \left(A{Y}_{\mathrm{rm}}b<A{Y}_{\mathrm{rm}}\left(b+1\right)\leftrightarrow \left(A{Y}_{\mathrm{rm}}b\right)+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)\right)$$
45	42 44	mpbid	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to \left(A{Y}_{\mathrm{rm}}b\right)+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)$$
46	23 29 32 38 45	letrd	$$⊢\left(b\in {\mathbb{N}}_0\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge b\le A{Y}_{\mathrm{rm}}b\right)\to b+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)$$
47	46	3exp	$$⊢b\in {\mathbb{N}}_0\to \left(A\in {\mathbb{Z}}_{\ge 2}\to \left(b\le A{Y}_{\mathrm{rm}}b\to b+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)\right)\right)$$
48	47	a2d	$$⊢b\in {\mathbb{N}}_0\to \left(\left(A\in {\mathbb{Z}}_{\ge 2}\to b\le A{Y}_{\mathrm{rm}}b\right)\to \left(A\in {\mathbb{Z}}_{\ge 2}\to b+1\le A{Y}_{\mathrm{rm}}\left(b+1\right)\right)\right)$$
49	4 8 12 16 19 48	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(A\in {\mathbb{Z}}_{\ge 2}\to N\le A{Y}_{\mathrm{rm}}N\right)$$
50	49	impcom	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to N\le A{Y}_{\mathrm{rm}}N$$