Theorem rmxypos

Description: For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014)

	Ref	Expression
Assertion	rmxypos	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑁 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑎 = 0 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 0 ) )
2	1	breq2d	⊢ ( 𝑎 = 0 → ( 0 < ( 𝐴 Xrm 𝑎 ) ↔ 0 < ( 𝐴 Xrm 0 ) ) )
3		oveq2	⊢ ( 𝑎 = 0 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 0 ) )
4	3	breq2d	⊢ ( 𝑎 = 0 → ( 0 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 0 ≤ ( 𝐴 Yrm 0 ) ) )
5	2 4	anbi12d	⊢ ( 𝑎 = 0 → ( ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 0 < ( 𝐴 Xrm 0 ) ∧ 0 ≤ ( 𝐴 Yrm 0 ) ) ) )
6	5	imbi2d	⊢ ( 𝑎 = 0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 0 ) ∧ 0 ≤ ( 𝐴 Yrm 0 ) ) ) ) )
7		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑏 ) )
8	7	breq2d	⊢ ( 𝑎 = 𝑏 → ( 0 < ( 𝐴 Xrm 𝑎 ) ↔ 0 < ( 𝐴 Xrm 𝑏 ) ) )
9		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
10	9	breq2d	⊢ ( 𝑎 = 𝑏 → ( 0 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) )
11	8 10	anbi12d	⊢ ( 𝑎 = 𝑏 → ( ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) )
12	11	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) ) )
13		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm ( 𝑏 + 1 ) ) )
14	13	breq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ↔ 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) ) )
15		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
16	15	breq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 0 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
17	14 16	anbi12d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∧ 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) )
18	17	imbi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∧ 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) ) )
19		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Xrm 𝑎 ) = ( 𝐴 Xrm 𝑁 ) )
20	19	breq2d	⊢ ( 𝑎 = 𝑁 → ( 0 < ( 𝐴 Xrm 𝑎 ) ↔ 0 < ( 𝐴 Xrm 𝑁 ) ) )
21		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
22	21	breq2d	⊢ ( 𝑎 = 𝑁 → ( 0 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) )
23	20 22	anbi12d	⊢ ( 𝑎 = 𝑁 → ( ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 0 < ( 𝐴 Xrm 𝑁 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) ) )
24	23	imbi2d	⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑎 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑎 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑁 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) ) ) )
25		0lt1	⊢ 0 < 1
26		rmx0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 0 ) = 1 )
27	25 26	breqtrrid	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( 𝐴 Xrm 0 ) )
28		0le0	⊢ 0 ≤ 0
29		rmy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
30	28 29	breqtrrid	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ ( 𝐴 Yrm 0 ) )
31	27 30	jca	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 0 ) ∧ 0 ≤ ( 𝐴 Yrm 0 ) ) )
32		simp2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
33		nn0z	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
34	33	3ad2ant1	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 𝑏 ∈ ℤ )
35		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
36	35	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Xrm 𝑏 ) ∈ ℕ0 )
37	32 34 36	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 Xrm 𝑏 ) ∈ ℕ0 )
38	37	nn0red	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 Xrm 𝑏 ) ∈ ℝ )
39		eluzelre	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
40	39	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 𝐴 ∈ ℝ )
41	38 40	remulcld	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) ∈ ℝ )
42		rmspecpos	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ+ )
43	42	rpred	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ )
44	43	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ )
45		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
46	45	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
47	32 34 46	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
48	47	zred	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
49	44 48	remulcld	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ∈ ℝ )
50		simp3l	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 < ( 𝐴 Xrm 𝑏 ) )
51		eluz2nn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
52	51	nngt0d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 < 𝐴 )
53	52	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 < 𝐴 )
54	38 40 50 53	mulgt0d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 < ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) )
55	42	rpge0d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ ( ( 𝐴 ↑ 2 ) − 1 ) )
56	55	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( ( 𝐴 ↑ 2 ) − 1 ) )
57		simp3r	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( 𝐴 Yrm 𝑏 ) )
58	44 48 56 57	mulge0d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) )
59	41 49 54 58	addgtge0d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 < ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) )
60		rmxp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) )
61	32 34 60	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 Xrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Xrm 𝑏 ) · 𝐴 ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑏 ) ) ) )
62	59 61	breqtrrd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) )
63	48 40	remulcld	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ∈ ℝ )
64		eluzge2nn0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ0 )
65	64	nn0ge0d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝐴 )
66	65	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ 𝐴 )
67	48 40 57 66	mulge0d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) )
68	37	nn0ge0d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( 𝐴 Xrm 𝑏 ) )
69	63 38 67 68	addge0d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
70		rmyp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
71	32 34 70	syl2anc	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) + ( 𝐴 Xrm 𝑏 ) ) )
72	69 71	breqtrrd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
73	62 72	jca	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∧ 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
74	73	3exp	⊢ ( 𝑏 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∧ 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) ) )
75	74	a2d	⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) ) → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm ( 𝑏 + 1 ) ) ∧ 0 ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) ) )
76	6 12 18 24 31 75	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( 𝐴 Xrm 𝑁 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) ) )
77	76	impcom	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑁 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑁 ) ) )