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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑎 = 0 → 𝑎 = 0 )
2		oveq2	⊢ ( 𝑎 = 0 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 0 ) )
3	1 2	breq12d	⊢ ( 𝑎 = 0 → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 0 ≤ ( 𝐴 Yrm 0 ) ) )
4	3	imbi2d	⊢ ( 𝑎 = 0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ ( 𝐴 Yrm 0 ) ) ) )
5		id	⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
6		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
7	5 6	breq12d	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) )
8	7	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) ) )
9		id	⊢ ( 𝑎 = ( 𝑏 + 1 ) → 𝑎 = ( 𝑏 + 1 ) )
10		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
11	9 10	breq12d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
12	11	imbi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) )
13		id	⊢ ( 𝑎 = 𝑁 → 𝑎 = 𝑁 )
14		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
15	13 14	breq12d	⊢ ( 𝑎 = 𝑁 → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) )
16	15	imbi2d	⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) ) )
17		0le0	⊢ 0 ≤ 0
18		rmy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
19	17 18	breqtrrid	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ ( 𝐴 Yrm 0 ) )
20		nn0z	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
21	20	3ad2ant1	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 ∈ ℤ )
22	21	peano2zd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ∈ ℤ )
23	22	zred	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ∈ ℝ )
24		simp2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
25		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
26	25	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
27	24 21 26	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
28	27	peano2zd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) + 1 ) ∈ ℤ )
29	28	zred	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) + 1 ) ∈ ℝ )
30	25	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ )
31	24 22 30	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ )
32	31	zred	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ )
33		nn0re	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ )
34	33	3ad2ant1	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 ∈ ℝ )
35	27	zred	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
36		1red	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 1 ∈ ℝ )
37		simp3	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) )
38	34 35 36 37	leadd1dd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ≤ ( ( 𝐴 Yrm 𝑏 ) + 1 ) )
39	34	ltp1d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 < ( 𝑏 + 1 ) )
40		ltrmy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝑏 < ( 𝑏 + 1 ) ↔ ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
41	24 21 22 40	syl3anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 < ( 𝑏 + 1 ) ↔ ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
42	39 41	mpbid	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
43		zltp1le	⊢ ( ( ( 𝐴 Yrm 𝑏 ) ∈ ℤ ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ ) → ( ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ↔ ( ( 𝐴 Yrm 𝑏 ) + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
44	27 31 43	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ↔ ( ( 𝐴 Yrm 𝑏 ) + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
45	42 44	mpbid	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
46	23 29 32 38 45	letrd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
47	46	3exp	⊢ ( 𝑏 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) )
48	47	a2d	⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) )
49	4 8 12 16 19 48	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) )
50	49	impcom	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) )