Theorem 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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
2	1	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℕ0 )
3	2	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℂ )
4	3	sqcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) ↑ 2 ) ∈ ℂ )
5		rmspecnonsq	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
6	5	eldifad	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
8	7	nncnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
9		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
10	9	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
11	10	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
12	11	sqcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ∈ ℂ )
13	8 12	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) ∈ ℂ )
14	4 13	negsubd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) ↑ 2 ) + - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm 𝑀 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) ) )
15	3	sqvald	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) ↑ 2 ) = ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑀 ) ) )
16	11	sqvald	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) = ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑀 ) ) )
17	16	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) = ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
18	8 12	mulneg1d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) = - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) )
19		nnnegz	⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ → - ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
20	7 19	syl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → - ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
21	20	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → - ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
22	21 11 11	mul12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( 𝐴 Yrm 𝑀 ) · ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
23	17 18 22	3eqtr3d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) = ( ( 𝐴 Yrm 𝑀 ) · ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
24	15 23	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) ↑ 2 ) + - ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑀 ) · ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) )
25		rmxynorm	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) ↑ 2 ) ) ) = 1 )
26	14 24 25	3eqtr3d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑀 ) · ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = 1 )
27	2	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℤ )
28	20 10	zmulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ )
29		bezoutr1	⊢ ( ( ( ( 𝐴 Xrm 𝑀 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ) ∧ ( ( 𝐴 Xrm 𝑀 ) ∈ ℤ ∧ ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ ) ) → ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑀 ) · ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = 1 → ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) = 1 ) )
30	27 10 27 28 29	syl22anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑀 ) ) + ( ( 𝐴 Yrm 𝑀 ) · ( - ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = 1 → ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) = 1 ) )
31	26 30	mpd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) gcd ( 𝐴 Yrm 𝑀 ) ) = 1 )