Theorem ltrmxnn0

Description: The X-sequence is strictly monotonic on NN0 . (Contributed by Stefan O'Rear, 4-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
2		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
3	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Xrm 𝑏 ) ∈ ℕ0 )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑏 ) ∈ ℕ0 )
5	4	nn0red	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑏 ) ∈ ℝ )
6		eluzelre	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
8	5 7	remulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ∈ ℝ )
9	1	peano2zd	⊢ ( 𝑏 ∈ ℕ0 → ( 𝑏 + 1 ) ∈ ℤ )
10	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∈ ℕ0 )
11	9 10	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∈ ℕ0 )
12	11	nn0red	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∈ ℝ )
13		eluz2b2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 ∈ ℕ ∧ 1 < 𝐴 ) )
14	13	simprbi	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐴 )
15	14	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 1 < 𝐴 )
16		rmxypos	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) )
17	16	simpld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 < ( 𝐴 Xrm 𝑏 ) )
18		ltmulgt11	⊢ ( ( ( 𝐴 Xrm 𝑏 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 0 < ( 𝐴 Xrm 𝑏 ) ) → ( 1 < 𝐴 ↔ ( 𝐴 Xrm 𝑏 ) < ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ) )
19	5 7 17 18	syl3anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 1 < 𝐴 ↔ ( 𝐴 Xrm 𝑏 ) < ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ) )
20	15 19	mpbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑏 ) < ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) )
21		rmspecnonsq	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
22	21	eldifad	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
23	22	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
24	23	nnred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ )
25		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
26	25	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
27	1 26	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
28	27	zred	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
29	23	nnnn0d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ0 )
30	29	nn0ge0d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 ≤ ( ( 𝐴 ↑ 2 ) − 1 ) )
31	16	simprd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 ≤ ( 𝐴 Yrm 𝑏 ) )
32	24 28 30 31	mulge0d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 ≤ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) )
33	24 28	remulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ∈ ℝ )
34	8 33	addge01d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 0 ≤ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ↔ ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ≤ ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) ) )
35	32 34	mpbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ≤ ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) )
36		rmxp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) )
37	1 36	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) )
38	35 37	breqtrrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ≤ ( 𝐴 Xrm ( 𝑏 + 1 ) ) )
39	5 8 12 20 38	ltletrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑏 ) < ( 𝐴 Xrm ( 𝑏 + 1 ) ) )
40		nn0z	⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℤ )
41	2	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Xrm 𝑎 ) ∈ ℕ0 )
42	40 41	sylan2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑎 ) ∈ ℕ0 )
43	42	nn0red	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑎 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑎 ) ∈ ℝ )
44		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
45		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm ( 𝑏 + 1 ) ) )
46		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑏 ) )
47		oveq2	⊢ ( 𝑎 = 𝑀 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑀 ) )
48		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑁 ) )
49	39 43 44 45 46 47 48	monotuz	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 Xrm 𝑀 ) < ( 𝐴 Xrm 𝑁 ) ) )
50	49	3impb	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 Xrm 𝑀 ) < ( 𝐴 Xrm 𝑁 ) ) )