jm2.19lem1

Description: Lemma for jm2.19 . X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014)

		Ref	Expression
	Assertion	jm2.19lem1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (A X_{rm} M) \gcd (A Y_{rm} M) = 1$

Proof

Step	Hyp	Ref	Expression
1		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
2	1	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A X_{rm} M \in ℕ_{0}$
3	2	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A X_{rm} M \in ℂ$
4	3	sqcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A X_{rm} M)}^{2} \in ℂ$
5		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
6	5	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
7	6	adantr	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A^{2} - 1 \in ℕ$
8	7	nncnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A^{2} - 1 \in ℂ$
9		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
10	9	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
11	10	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℂ$
12	11	sqcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A Y_{rm} M)}^{2} \in ℂ$
13	8 12	mulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (A^{2} - 1) {(A Y_{rm} M)}^{2} \in ℂ$
14	4 13	negsubd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A X_{rm} M)}^{2} + (- (A^{2} - 1) {(A Y_{rm} M)}^{2}) = {(A X_{rm} M)}^{2} - (A^{2} - 1) {(A Y_{rm} M)}^{2}$
15	3	sqvald	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A X_{rm} M)}^{2} = (A X_{rm} M) (A X_{rm} M)$
16	11	sqvald	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A Y_{rm} M)}^{2} = (A Y_{rm} M) (A Y_{rm} M)$
17	16	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (- (A^{2} - 1)) {(A Y_{rm} M)}^{2} = (- (A^{2} - 1)) (A Y_{rm} M) (A Y_{rm} M)$
18	8 12	mulneg1d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (- (A^{2} - 1)) {(A Y_{rm} M)}^{2} = - (A^{2} - 1) {(A Y_{rm} M)}^{2}$
19		nnnegz	$⊢ A^{2} - 1 \in ℕ \to - (A^{2} - 1) \in ℤ$
20	7 19	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to - (A^{2} - 1) \in ℤ$
21	20	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to - (A^{2} - 1) \in ℂ$
22	21 11 11	mul12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (- (A^{2} - 1)) (A Y_{rm} M) (A Y_{rm} M) = (A Y_{rm} M) (- (A^{2} - 1)) (A Y_{rm} M)$
23	17 18 22	3eqtr3d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to - (A^{2} - 1) {(A Y_{rm} M)}^{2} = (A Y_{rm} M) (- (A^{2} - 1)) (A Y_{rm} M)$
24	15 23	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A X_{rm} M)}^{2} + (- (A^{2} - 1) {(A Y_{rm} M)}^{2}) = (A X_{rm} M) (A X_{rm} M) + (A Y_{rm} M) (- (A^{2} - 1)) (A Y_{rm} M)$
25		rmxynorm	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to {(A X_{rm} M)}^{2} - (A^{2} - 1) {(A Y_{rm} M)}^{2} = 1$
26	14 24 25	3eqtr3d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (A X_{rm} M) (A X_{rm} M) + (A Y_{rm} M) (- (A^{2} - 1)) (A Y_{rm} M) = 1$
27	2	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A X_{rm} M \in ℤ$
28	20 10	zmulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (- (A^{2} - 1)) (A Y_{rm} M) \in ℤ$
29		bezoutr1	$⊢ ((A X_{rm} M \in ℤ \land A Y_{rm} M \in ℤ) \land (A X_{rm} M \in ℤ \land (- (A^{2} - 1)) (A Y_{rm} M) \in ℤ)) \to ((A X_{rm} M) (A X_{rm} M) + (A Y_{rm} M) (- (A^{2} - 1)) (A Y_{rm} M) = 1 \to (A X_{rm} M) \gcd (A Y_{rm} M) = 1)$
30	27 10 27 28 29	syl22anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to ((A X_{rm} M) (A X_{rm} M) + (A Y_{rm} M) (- (A^{2} - 1)) (A Y_{rm} M) = 1 \to (A X_{rm} M) \gcd (A Y_{rm} M) = 1)$
31	26 30	mpd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to (A X_{rm} M) \gcd (A Y_{rm} M) = 1$

Metamath Proof Explorer

Theorem jm2.19lem1

Proof