rmxyneg

Description: Negation law for X and Y sequences. JonesMatijasevic is inconsistent on whether the X and Y sequences have domain NN0 or ZZ ; we use ZZ consistently to avoid the need for a separate subtraction law. (Contributed by Stefan O'Rear, 22-Sep-2014)

		Ref	Expression
	Assertion	rmxyneg	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} -N = A X_{rm} N \land A Y_{rm} -N = - (A Y_{rm} N))$

Proof

Step	Hyp	Ref	Expression
1		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
2		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℤ) \to (A X_{rm} -N) + \sqrt{A^{2} - 1} (A Y_{rm} -N) = {(A + \sqrt{A^{2} - 1})}^{- N}$
3	1 2	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} -N) + \sqrt{A^{2} - 1} (A Y_{rm} -N) = {(A + \sqrt{A^{2} - 1})}^{- N}$
4		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) = {(A + \sqrt{A^{2} - 1})}^{N}$
5	4	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \frac{1}{(A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)} = \frac{1}{{(A + \sqrt{A^{2} - 1})}^{N}}$
6		rmbaserp	$⊢ A \in ℤ_{\geq 2} \to A + \sqrt{A^{2} - 1} \in ℝ^{+}$
7	6	rpcnd	$⊢ A \in ℤ_{\geq 2} \to A + \sqrt{A^{2} - 1} \in ℂ$
8	7	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A + \sqrt{A^{2} - 1} \in ℂ$
9	6	rpne0d	$⊢ A \in ℤ_{\geq 2} \to A + \sqrt{A^{2} - 1} \neq 0$
10	9	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A + \sqrt{A^{2} - 1} \neq 0$
11		simpr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℤ$
12	8 10 11	expclzd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \in ℂ$
13	4 12	eqeltrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ$
14		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
15	14	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
16	15	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℂ$
17		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
18	17	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
19	18	nncnd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℂ$
20	19	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A^{2} - 1 \in ℂ$
21	20	sqrtcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \sqrt{A^{2} - 1} \in ℂ$
22		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
23	22	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
24	23	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℂ$
25	24	negcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to - (A Y_{rm} N) \in ℂ$
26	21 25	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \sqrt{A^{2} - 1} (- (A Y_{rm} N)) \in ℂ$
27	16 26	addcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N)) \in ℂ$
28	8 10 11	expne0d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \neq 0$
29	4 28	eqnetrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N) \neq 0$
30	21 24	mulneg2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \sqrt{A^{2} - 1} (- (A Y_{rm} N)) = - \sqrt{A^{2} - 1} (A Y_{rm} N)$
31	30	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N)) = (A X_{rm} N) + (- \sqrt{A^{2} - 1} (A Y_{rm} N))$
32	21 24	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ$
33	16 32	negsubd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + (- \sqrt{A^{2} - 1} (A Y_{rm} N)) = (A X_{rm} N) - \sqrt{A^{2} - 1} (A Y_{rm} N)$
34	31 33	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N)) = (A X_{rm} N) - \sqrt{A^{2} - 1} (A Y_{rm} N)$
35	34	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) ((A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N))) = ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) ((A X_{rm} N) - \sqrt{A^{2} - 1} (A Y_{rm} N))$
36		subsq	$⊢ (A X_{rm} N \in ℂ \land \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ) \to {(A X_{rm} N)}^{2} - {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{2} = ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) ((A X_{rm} N) - \sqrt{A^{2} - 1} (A Y_{rm} N))$
37	16 32 36	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} - {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{2} = ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) ((A X_{rm} N) - \sqrt{A^{2} - 1} (A Y_{rm} N))$
38	21 24	sqmuld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{2} = {\sqrt{A^{2} - 1}}^{2} {(A Y_{rm} N)}^{2}$
39	20	sqsqrtd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {\sqrt{A^{2} - 1}}^{2} = A^{2} - 1$
40	39	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {\sqrt{A^{2} - 1}}^{2} {(A Y_{rm} N)}^{2} = (A^{2} - 1) {(A Y_{rm} N)}^{2}$
41	38 40	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{2} = (A^{2} - 1) {(A Y_{rm} N)}^{2}$
42	41	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} - {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{2} = {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2}$
43		rmxynorm	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} - (A^{2} - 1) {(A Y_{rm} N)}^{2} = 1$
44	42 43	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A X_{rm} N)}^{2} - {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{2} = 1$
45	35 37 44	3eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to ((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)) ((A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N))) = 1$
46	13 27 29 45	mvllmuld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N)) = \frac{1}{(A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N)}$
47	8 10 11	expnegd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{- N} = \frac{1}{{(A + \sqrt{A^{2} - 1})}^{N}}$
48	5 46 47	3eqtr4rd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{- N} = (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N))$
49	3 48	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} -N) + \sqrt{A^{2} - 1} (A Y_{rm} -N) = (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N))$
50		rmspecsqrtnq	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
51	50	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
52		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
53	14	fovcl	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℤ) \to A X_{rm} -N \in ℕ_{0}$
54	1 53	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} -N \in ℕ_{0}$
55	52 54	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} -N \in ℚ$
56		zssq	$⊢ ℤ \subseteq ℚ$
57	22	fovcl	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℤ) \to A Y_{rm} -N \in ℤ$
58	1 57	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} -N \in ℤ$
59	56 58	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} -N \in ℚ$
60	52 15	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℚ$
61	56 23	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℚ$
62		qnegcl	$⊢ A Y_{rm} N \in ℚ \to - (A Y_{rm} N) \in ℚ$
63	61 62	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to - (A Y_{rm} N) \in ℚ$
64		qirropth	$⊢ (\sqrt{A^{2} - 1} \in (ℂ ∖ ℚ) \land (A X_{rm} -N \in ℚ \land A Y_{rm} -N \in ℚ) \land (A X_{rm} N \in ℚ \land - (A Y_{rm} N) \in ℚ)) \to ((A X_{rm} -N) + \sqrt{A^{2} - 1} (A Y_{rm} -N) = (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N)) \leftrightarrow (A X_{rm} -N = A X_{rm} N \land A Y_{rm} -N = - (A Y_{rm} N)))$
65	51 55 59 60 63 64	syl122anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to ((A X_{rm} -N) + \sqrt{A^{2} - 1} (A Y_{rm} -N) = (A X_{rm} N) + \sqrt{A^{2} - 1} (- (A Y_{rm} N)) \leftrightarrow (A X_{rm} -N = A X_{rm} N \land A Y_{rm} -N = - (A Y_{rm} N)))$
66	49 65	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} -N = A X_{rm} N \land A Y_{rm} -N = - (A Y_{rm} N))$

Metamath Proof Explorer

Theorem rmxyneg

Proof