rmxnn

Description: The X-sequence is defined to range over NN0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	rmxnn	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
2		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
3	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
4	1 3	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to A X_{rm} N \in ℕ_{0}$
5		rmxypos	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (0 < A X_{rm} N \land 0 \leq A Y_{rm} N)$
6	5	simpld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to 0 < A X_{rm} N$
7		elnnnn0b	$⊢ A X_{rm} N \in ℕ \leftrightarrow (A X_{rm} N \in ℕ_{0} \land 0 < A X_{rm} N)$
8	4 6 7	sylanbrc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to A X_{rm} N \in ℕ$
9	8	adantlr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \in ℕ_{0}) \to A X_{rm} N \in ℕ$
10		rmxneg	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} -N = A X_{rm} N$
11	10	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land - N \in ℕ_{0}) \to A X_{rm} -N = A X_{rm} N$
12		nn0z	$⊢ - N \in ℕ_{0} \to - N \in ℤ$
13	2	fovcl	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℤ) \to A X_{rm} -N \in ℕ_{0}$
14	12 13	sylan2	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℕ_{0}) \to A X_{rm} -N \in ℕ_{0}$
15		rmxypos	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℕ_{0}) \to (0 < A X_{rm} -N \land 0 \leq A Y_{rm} -N)$
16	15	simpld	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℕ_{0}) \to 0 < A X_{rm} -N$
17		elnnnn0b	$⊢ A X_{rm} -N \in ℕ \leftrightarrow (A X_{rm} -N \in ℕ_{0} \land 0 < A X_{rm} -N)$
18	14 16 17	sylanbrc	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℕ_{0}) \to A X_{rm} -N \in ℕ$
19	18	adantlr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land - N \in ℕ_{0}) \to A X_{rm} -N \in ℕ$
20	11 19	eqeltrrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land - N \in ℕ_{0}) \to A X_{rm} N \in ℕ$
21		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
22	21	simprbi	$⊢ N \in ℤ \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
23	22	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
24	9 20 23	mpjaodan	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ$

Metamath Proof Explorer

Theorem rmxnn

Proof