rmxdiophlem

Description: X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014)

		Ref	Expression
	Assertion	rmxdiophlem	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X = A X_{rm} N \leftrightarrow \exists y \in ℕ_{0} (y = A Y_{rm} N \land X^{2} - (A^{2} - 1) y^{2} = 1))$

Proof

Step	Hyp	Ref	Expression
1		nn0sqcl	$⊢ X \in ℕ_{0} \to X^{2} \in ℕ_{0}$
2	1	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to X^{2} \in ℕ_{0}$
3	2	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to X^{2} \in ℂ$
4		simp1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to A \in ℤ_{\geq 2}$
5		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
6	5	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to N \in ℤ$
7		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
8	7	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
9	4 6 8	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to A X_{rm} N \in ℕ_{0}$
10		nn0sqcl	$⊢ A X_{rm} N \in ℕ_{0} \to {(A X_{rm} N)}^{2} \in ℕ_{0}$
11	9 10	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to {(A X_{rm} N)}^{2} \in ℕ_{0}$
12	11	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to {(A X_{rm} N)}^{2} \in ℂ$
13		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
14	13	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
15	14	nnnn0d	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ_{0}$
16	15	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to A^{2} - 1 \in ℕ_{0}$
17		rmynn0	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to A Y_{rm} N \in ℕ_{0}$
18	17	3adant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to A Y_{rm} N \in ℕ_{0}$
19		nn0sqcl	$⊢ A Y_{rm} N \in ℕ_{0} \to {(A Y_{rm} N)}^{2} \in ℕ_{0}$
20	18 19	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to {(A Y_{rm} N)}^{2} \in ℕ_{0}$
21	16 20	nn0mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (A^{2} - 1) {(A Y_{rm} N)}^{2} \in ℕ_{0}$
22	21	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (A^{2} - 1) {(A Y_{rm} N)}^{2} \in ℂ$
23	3 12 22	subcan2ad	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} \leftrightarrow X^{2} = {(A X_{rm} N)}^{2})$
24		rmxynorm	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1$
25	4 6 24	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1$
26	25	eqeq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} \leftrightarrow X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1)$
27		nn0re	$⊢ X \in ℕ_{0} \to X \in ℝ$
28		nn0ge0	$⊢ X \in ℕ_{0} \to 0 \leq X$
29	27 28	jca	$⊢ X \in ℕ_{0} \to (X \in ℝ \land 0 \leq X)$
30	29	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X \in ℝ \land 0 \leq X)$
31		nn0re	$⊢ A X_{rm} N \in ℕ_{0} \to A X_{rm} N \in ℝ$
32		nn0ge0	$⊢ A X_{rm} N \in ℕ_{0} \to 0 \leq A X_{rm} N$
33	31 32	jca	$⊢ A X_{rm} N \in ℕ_{0} \to (A X_{rm} N \in ℝ \land 0 \leq A X_{rm} N)$
34	9 33	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (A X_{rm} N \in ℝ \land 0 \leq A X_{rm} N)$
35		sq11	$⊢ ((X \in ℝ \land 0 \leq X) \land (A X_{rm} N \in ℝ \land 0 \leq A X_{rm} N)) \to (X^{2} = {(A X_{rm} N)}^{2} \leftrightarrow X = A X_{rm} N)$
36	30 34 35	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X^{2} = {(A X_{rm} N)}^{2} \leftrightarrow X = A X_{rm} N)$
37	23 26 36	3bitr3rd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X = A X_{rm} N \leftrightarrow X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1)$
38		oveq1	$⊢ y = A Y_{rm} N \to y^{2} = {(A Y_{rm} N)}^{2}$
39	38	oveq2d	$⊢ y = A Y_{rm} N \to (A^{2} - 1) y^{2} = (A^{2} - 1) {(A Y_{rm} N)}^{2}$
40	39	oveq2d	$⊢ y = A Y_{rm} N \to X^{2} - (A^{2} - 1) y^{2} = X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2}$
41	40	eqeq1d	$⊢ y = A Y_{rm} N \to (X^{2} - (A^{2} - 1) y^{2} = 1 \leftrightarrow X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1)$
42	41	ceqsrexv	$⊢ A Y_{rm} N \in ℕ_{0} \to (\exists y \in ℕ_{0} (y = A Y_{rm} N \land X^{2} - (A^{2} - 1) y^{2} = 1) \leftrightarrow X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1)$
43	18 42	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (\exists y \in ℕ_{0} (y = A Y_{rm} N \land X^{2} - (A^{2} - 1) y^{2} = 1) \leftrightarrow X^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1)$
44	37 43	bitr4d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0} \land X \in ℕ_{0}) \to (X = A X_{rm} N \leftrightarrow \exists y \in ℕ_{0} (y = A Y_{rm} N \land X^{2} - (A^{2} - 1) y^{2} = 1))$

Metamath Proof Explorer

Theorem rmxdiophlem

Proof