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	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (0 < A X_{rm} N \land 0 \leq A Y_{rm} N)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ a = 0 \to A X_{rm} a = A X_{rm} 0$
2	1	breq2d	$⊢ a = 0 \to (0 < A X_{rm} a \leftrightarrow 0 < A X_{rm} 0)$
3		oveq2	$⊢ a = 0 \to A Y_{rm} a = A Y_{rm} 0$
4	3	breq2d	$⊢ a = 0 \to (0 \leq A Y_{rm} a \leftrightarrow 0 \leq A Y_{rm} 0)$
5	2 4	anbi12d	$⊢ a = 0 \to ((0 < A X_{rm} a \land 0 \leq A Y_{rm} a) \leftrightarrow (0 < A X_{rm} 0 \land 0 \leq A Y_{rm} 0))$
6	5	imbi2d	$⊢ a = 0 \to ((A \in ℤ_{\geq 2} \to (0 < A X_{rm} a \land 0 \leq A Y_{rm} a)) \leftrightarrow (A \in ℤ_{\geq 2} \to (0 < A X_{rm} 0 \land 0 \leq A Y_{rm} 0)))$
7		oveq2	$⊢ a = b \to A X_{rm} a = A X_{rm} b$
8	7	breq2d	$⊢ a = b \to (0 < A X_{rm} a \leftrightarrow 0 < A X_{rm} b)$
9		oveq2	$⊢ a = b \to A Y_{rm} a = A Y_{rm} b$
10	9	breq2d	$⊢ a = b \to (0 \leq A Y_{rm} a \leftrightarrow 0 \leq A Y_{rm} b)$
11	8 10	anbi12d	$⊢ a = b \to ((0 < A X_{rm} a \land 0 \leq A Y_{rm} a) \leftrightarrow (0 < A X_{rm} b \land 0 \leq A Y_{rm} b))$
12	11	imbi2d	$⊢ a = b \to ((A \in ℤ_{\geq 2} \to (0 < A X_{rm} a \land 0 \leq A Y_{rm} a)) \leftrightarrow (A \in ℤ_{\geq 2} \to (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)))$
13		oveq2	$⊢ a = b + 1 \to A X_{rm} a = A X_{rm} (b + 1)$
14	13	breq2d	$⊢ a = b + 1 \to (0 < A X_{rm} a \leftrightarrow 0 < A X_{rm} (b + 1))$
15		oveq2	$⊢ a = b + 1 \to A Y_{rm} a = A Y_{rm} (b + 1)$
16	15	breq2d	$⊢ a = b + 1 \to (0 \leq A Y_{rm} a \leftrightarrow 0 \leq A Y_{rm} (b + 1))$
17	14 16	anbi12d	$⊢ a = b + 1 \to ((0 < A X_{rm} a \land 0 \leq A Y_{rm} a) \leftrightarrow (0 < A X_{rm} (b + 1) \land 0 \leq A Y_{rm} (b + 1)))$
18	17	imbi2d	$⊢ a = b + 1 \to ((A \in ℤ_{\geq 2} \to (0 < A X_{rm} a \land 0 \leq A Y_{rm} a)) \leftrightarrow (A \in ℤ_{\geq 2} \to (0 < A X_{rm} (b + 1) \land 0 \leq A Y_{rm} (b + 1))))$
19		oveq2	$⊢ a = N \to A X_{rm} a = A X_{rm} N$
20	19	breq2d	$⊢ a = N \to (0 < A X_{rm} a \leftrightarrow 0 < A X_{rm} N)$
21		oveq2	$⊢ a = N \to A Y_{rm} a = A Y_{rm} N$
22	21	breq2d	$⊢ a = N \to (0 \leq A Y_{rm} a \leftrightarrow 0 \leq A Y_{rm} N)$
23	20 22	anbi12d	$⊢ a = N \to ((0 < A X_{rm} a \land 0 \leq A Y_{rm} a) \leftrightarrow (0 < A X_{rm} N \land 0 \leq A Y_{rm} N))$
24	23	imbi2d	$⊢ a = N \to ((A \in ℤ_{\geq 2} \to (0 < A X_{rm} a \land 0 \leq A Y_{rm} a)) \leftrightarrow (A \in ℤ_{\geq 2} \to (0 < A X_{rm} N \land 0 \leq A Y_{rm} N)))$
25		0lt1	$⊢ 0 < 1$
26		rmx0	$⊢ A \in ℤ_{\geq 2} \to A X_{rm} 0 = 1$
27	25 26	breqtrrid	$⊢ A \in ℤ_{\geq 2} \to 0 < A X_{rm} 0$
28		0le0	$⊢ 0 \leq 0$
29		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
30	28 29	breqtrrid	$⊢ A \in ℤ_{\geq 2} \to 0 \leq A Y_{rm} 0$
31	27 30	jca	$⊢ A \in ℤ_{\geq 2} \to (0 < A X_{rm} 0 \land 0 \leq A Y_{rm} 0)$
32		simp2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A \in ℤ_{\geq 2}$
33		nn0z	$⊢ b \in ℕ_{0} \to b \in ℤ$
34	33	3ad2ant1	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to b \in ℤ$
35		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
36	35	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A X_{rm} b \in ℕ_{0}$
37	32 34 36	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A X_{rm} b \in ℕ_{0}$
38	37	nn0red	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A X_{rm} b \in ℝ$
39		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
40	39	3ad2ant2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A \in ℝ$
41	38 40	remulcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to (A X_{rm} b) A \in ℝ$
42		rmspecpos	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℝ^{+}$
43	42	rpred	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℝ$
44	43	3ad2ant2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A^{2} - 1 \in ℝ$
45		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
46	45	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} b \in ℤ$
47	32 34 46	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A Y_{rm} b \in ℤ$
48	47	zred	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A Y_{rm} b \in ℝ$
49	44 48	remulcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to (A^{2} - 1) (A Y_{rm} b) \in ℝ$
50		simp3l	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 < A X_{rm} b$
51		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
52	51	nngt0d	$⊢ A \in ℤ_{\geq 2} \to 0 < A$
53	52	3ad2ant2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 < A$
54	38 40 50 53	mulgt0d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 < (A X_{rm} b) A$
55	42	rpge0d	$⊢ A \in ℤ_{\geq 2} \to 0 \leq A^{2} - 1$
56	55	3ad2ant2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq A^{2} - 1$
57		simp3r	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq A Y_{rm} b$
58	44 48 56 57	mulge0d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq (A^{2} - 1) (A Y_{rm} b)$
59	41 49 54 58	addgtge0d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 < (A X_{rm} b) A + (A^{2} - 1) (A Y_{rm} b)$
60		rmxp1	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A X_{rm} (b + 1) = (A X_{rm} b) A + (A^{2} - 1) (A Y_{rm} b)$
61	32 34 60	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A X_{rm} (b + 1) = (A X_{rm} b) A + (A^{2} - 1) (A Y_{rm} b)$
62	59 61	breqtrrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 < A X_{rm} (b + 1)$
63	48 40	remulcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to (A Y_{rm} b) A \in ℝ$
64		eluzge2nn0	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ_{0}$
65	64	nn0ge0d	$⊢ A \in ℤ_{\geq 2} \to 0 \leq A$
66	65	3ad2ant2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq A$
67	48 40 57 66	mulge0d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq (A Y_{rm} b) A$
68	37	nn0ge0d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq A X_{rm} b$
69	63 38 67 68	addge0d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq (A Y_{rm} b) A + (A X_{rm} b)$
70		rmyp1	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} (b + 1) = (A Y_{rm} b) A + (A X_{rm} b)$
71	32 34 70	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to A Y_{rm} (b + 1) = (A Y_{rm} b) A + (A X_{rm} b)$
72	69 71	breqtrrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to 0 \leq A Y_{rm} (b + 1)$
73	62 72	jca	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to (0 < A X_{rm} (b + 1) \land 0 \leq A Y_{rm} (b + 1))$
74	73	3exp	$⊢ b \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to ((0 < A X_{rm} b \land 0 \leq A Y_{rm} b) \to (0 < A X_{rm} (b + 1) \land 0 \leq A Y_{rm} (b + 1))))$
75	74	a2d	$⊢ b \in ℕ_{0} \to ((A \in ℤ_{\geq 2} \to (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)) \to (A \in ℤ_{\geq 2} \to (0 < A X_{rm} (b + 1) \land 0 \leq A Y_{rm} (b + 1))))$
76	6 12 18 24 31 75	nn0ind	$⊢ N \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to (0 < A X_{rm} N \land 0 \leq A Y_{rm} N))$
77	76	impcom	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (0 < A X_{rm} N \land 0 \leq A Y_{rm} N)$

Metamath Proof Explorer

Theorem rmxypos

Proof