Metamath Proof Explorer


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 𝑁 ) )