Theorem rmxyadd

Description: Addition formula for X and Y sequences. See rmxadd and rmyadd for most uses. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	rmxyadd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∧ ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
3	2	3adant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
4		rmxyval	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑀 + 𝑁 ) ) )
5	1 3 4	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑀 + 𝑁 ) ) )
6		eluzelz	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
7	6	3ad2ant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℤ )
8	7	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
9		zq	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℚ )
10		qsqcl	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) ∈ ℚ )
11	7 9 10	3syl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 2 ) ∈ ℚ )
12		zssq	⊢ ℤ ⊆ ℚ
13		1z	⊢ 1 ∈ ℤ
14	12 13	sselii	⊢ 1 ∈ ℚ
15	14	a1i	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 1 ∈ ℚ )
16		qsubcl	⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℚ ∧ 1 ∈ ℚ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℚ )
17	11 15 16	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℚ )
18		qcn	⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℚ → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
19	17 18	syl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
20	19	sqrtcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℂ )
21	8 20	addcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℂ )
22		rmbaserp	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℝ+ )
23	22	rpne0d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≠ 0 )
24	23	3ad2ant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≠ 0 )
25		simp2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
26		simp3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
27		expaddz	⊢ ( ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℂ ∧ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≠ 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑀 ) · ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) )
28	21 24 25 26 27	syl22anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑀 ) · ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) )
29		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
30	29	a1i	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0 )
31	30 1 25	fovcdmd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℕ0 )
32	31	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℂ )
33		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
34	33	a1i	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ )
35	34 1 25	fovcdmd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
36	35	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
37	20 36	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
38	30 1 26	fovcdmd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
39	38	nn0cnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
40	34 1 26	fovcdmd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
41	40	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
42	20 41	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ )
43	32 37 39 42	muladdd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) · ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) + ( ( ( 𝐴 Xrm 𝑀 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) ) )
44		rmxyval	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑀 ) )
45	1 25 44	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑀 ) )
46		rmxyval	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )
47	1 26 46	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )
48	45 47	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) · ( ( 𝐴 Xrm 𝑁 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑀 ) · ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) )
49	43 48	eqtr3d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) + ( ( ( 𝐴 Xrm 𝑀 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) ) = ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑀 ) · ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) )
50	20 41 20 36	mul4d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
51	19	msqsqrtd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) = ( ( 𝐴 ↑ 2 ) − 1 ) )
52	41 36	mulcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) = ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) )
53	51 52	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
54	50 53	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
55	54	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
56	32 20 41	mul12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
57	39 20 36	mul12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) )
58	56 57	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) )
59	32 41	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ )
60	39 36	mulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
61	20 59 60	adddid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) )
62	59 60	addcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
63	39 36	mulcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) = ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) )
64	63	oveq1d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
65	62 64	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
66	65	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
67	58 61 66	3eqtr2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
68	55 67	oveq12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) + ( ( ( 𝐴 Xrm 𝑀 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) + ( ( 𝐴 Xrm 𝑁 ) · ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑀 ) ) ) ) ) = ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
69	28 49 68	3eqtr2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ ( 𝑀 + 𝑁 ) ) = ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
70	5 69	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ) ) = ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
71		rmspecsqrtnq	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
72	71	3ad2ant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
73		nn0ssq	⊢ ℕ0 ⊆ ℚ
74	30 1 3	fovcdmd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) ∈ ℕ0 )
75	73 74	sselid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) ∈ ℚ )
76	34 1 3	fovcdmd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ∈ ℤ )
77	12 76	sselid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ∈ ℚ )
78	73 31	sselid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑀 ) ∈ ℚ )
79	73 38	sselid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℚ )
80		qmulcl	⊢ ( ( ( 𝐴 Xrm 𝑀 ) ∈ ℚ ∧ ( 𝐴 Xrm 𝑁 ) ∈ ℚ ) → ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℚ )
81	78 79 80	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℚ )
82	12 35	sselid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℚ )
83	12 40	sselid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℚ )
84		qmulcl	⊢ ( ( ( 𝐴 Yrm 𝑀 ) ∈ ℚ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℚ ) → ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℚ )
85	82 83 84	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℚ )
86		qmulcl	⊢ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℚ ∧ ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℚ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℚ )
87	17 85 86	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℚ )
88		qaddcl	⊢ ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℚ ∧ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℚ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℚ )
89	81 87 88	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℚ )
90		qmulcl	⊢ ( ( ( 𝐴 Yrm 𝑀 ) ∈ ℚ ∧ ( 𝐴 Xrm 𝑁 ) ∈ ℚ ) → ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℚ )
91	82 79 90	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℚ )
92		qmulcl	⊢ ( ( ( 𝐴 Xrm 𝑀 ) ∈ ℚ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℚ ) → ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℚ )
93	78 83 92	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℚ )
94		qaddcl	⊢ ( ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) ∈ ℚ ∧ ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℚ ) → ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℚ )
95	91 93 94	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℚ )
96		qirropth	⊢ ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) ∧ ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) ∈ ℚ ∧ ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ∈ ℚ ) ∧ ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℚ ∧ ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℚ ) ) → ( ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ) ) = ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) ↔ ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∧ ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
97	72 75 77 89 95 96	syl122anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) ) ) = ( ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) ↔ ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∧ ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
98	70 97	mpbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∧ ( 𝐴 Yrm ( 𝑀 + 𝑁 ) ) = ( ( ( 𝐴 Yrm 𝑀 ) · ( 𝐴 Xrm 𝑁 ) ) + ( ( 𝐴 Xrm 𝑀 ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )