Theorem ltrmynn0

Description: The Y-sequence is strictly monotonic on NN0 . Strengthened by ltrmy . (Contributed by Stefan O'Rear, 24-Sep-2014)

	Ref	Expression
Assertion	ltrmynn0	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) < ( 𝐴 Yrm 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
2		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
3	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
5	4	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
6		eluzelre	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
8	5 7	remulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ∈ ℝ )
9		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
10	9	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Xrm 𝑏 ) ∈ ℕ0 )
11	1 10	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑏 ) ∈ ℕ0 )
12	11	nn0red	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑏 ) ∈ ℝ )
13	8 12	readdcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) ∈ ℝ )
14		rmxypos	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) )
15	14	simprd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 ≤ ( 𝐴 Yrm 𝑏 ) )
16		eluz2nn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
17	16	nnge1d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ 𝐴 )
18	17	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 1 ≤ 𝐴 )
19	5 7 15 18	lemulge11d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) ≤ ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) )
20	14	simpld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 < ( 𝐴 Xrm 𝑏 ) )
21	12 8	ltaddposd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑏 ) ↔ ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) < ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) ) )
22	20 21	mpbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) < ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
23	5 8 13 19 22	lelttrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) < ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
24		rmyp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
25	1 24	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
26	23 25	breqtrrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
27		nn0z	⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℤ )
28	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ )
29	27 28	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑎 ) ∈ ℤ )
30	29	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑎 ) ∈ ℝ )
31		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
32		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
33		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
34		oveq2	⊢ ( 𝑎 = 𝑀 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑀 ) )
35		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
36	26 30 31 32 33 34 35	monotuz	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) < ( 𝐴 Yrm 𝑁 ) ) )
37	36	3impb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) < ( 𝐴 Yrm 𝑁 ) ) )