Theorem jm2.20nn

Description: Lemma 2.20 of JonesMatijasevic p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014)

	Ref	Expression
Assertion	jm2.20nn	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ↔ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3	2	3ad2ant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
4		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
5	4	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
6	1 3 5	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
7	6	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
8	7	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
9	8	sqvald	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) = ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
10		zsqcl	⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ )
11	6 10	syl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ )
12	11	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ )
13		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
14	13	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
15	1 3 14	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
16	15	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
17	16	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
18	7	sqvald	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) = ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
19	18	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) = ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
20		simpr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) )
21	19 20	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝐴 Yrm 𝑀 ) )
22		nnz	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
23	22	3ad2ant2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℤ )
24	4	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
25	1 23 24	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
26		muldvds1	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝐴 Yrm 𝑀 ) → ( 𝐴 Yrm 𝑁 ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
27	6 6 25 26	syl3anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝐴 Yrm 𝑀 ) → ( 𝐴 Yrm 𝑁 ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
28	27	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝐴 Yrm 𝑀 ) → ( 𝐴 Yrm 𝑁 ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
29	21 28	mpd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑁 ) ∥ ( 𝐴 Yrm 𝑀 ) )
30		simpl1	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
31	3	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝑁 ∈ ℤ )
32	23	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝑀 ∈ ℤ )
33		jm2.19	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∥ 𝑀 ↔ ( 𝐴 Yrm 𝑁 ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
34	30 31 32 33	syl3anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑁 ∥ 𝑀 ↔ ( 𝐴 Yrm 𝑁 ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
35	29 34	mpbird	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝑁 ∥ 𝑀 )
36		simpl2	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝑀 ∈ ℕ )
37		simpl3	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝑁 ∈ ℕ )
38		nndivdvds	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ 𝑀 ↔ ( 𝑀 / 𝑁 ) ∈ ℕ ) )
39	36 37 38	syl2anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑁 ∥ 𝑀 ↔ ( 𝑀 / 𝑁 ) ∈ ℕ ) )
40	35 39	mpbid	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑀 / 𝑁 ) ∈ ℕ )
41		nnm1nn0	⊢ ( ( 𝑀 / 𝑁 ) ∈ ℕ → ( ( 𝑀 / 𝑁 ) − 1 ) ∈ ℕ0 )
42	40 41	syl	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝑀 / 𝑁 ) − 1 ) ∈ ℕ0 )
43		zexpcl	⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( ( 𝑀 / 𝑁 ) − 1 ) ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ∈ ℤ )
44	17 42 43	syl2anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ∈ ℤ )
45	40	nnzd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑀 / 𝑁 ) ∈ ℤ )
46	6	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
47	45 46	zmulcld	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ )
48	25	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
49		nncn	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
50	49	3ad2ant2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℂ )
51		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
52	51	3ad2ant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
53		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
54	53	3ad2ant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
55	50 52 54	divcan2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( 𝑀 / 𝑁 ) ) = 𝑀 )
56	55	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) = ( 𝐴 Yrm 𝑀 ) )
57	56 25	eqeltrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) ∈ ℤ )
58	57	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) ∈ ℤ )
59	44 46	zmulcld	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ )
60	45 59	zmulcld	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
61	58 60	zsubcld	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℤ )
62		3nn0	⊢ 3 ∈ ℕ0
63	62	a1i	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 3 ∈ ℕ0 )
64		zexpcl	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ 3 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℤ )
65	6 63 64	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℤ )
66	65	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∈ ℤ )
67		2nn0	⊢ 2 ∈ ℕ0
68	67	a1i	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 2 ∈ ℕ0 )
69		3z	⊢ 3 ∈ ℤ
70		2re	⊢ 2 ∈ ℝ
71		3re	⊢ 3 ∈ ℝ
72		2lt3	⊢ 2 < 3
73	70 71 72	ltleii	⊢ 2 ≤ 3
74		2z	⊢ 2 ∈ ℤ
75	74	eluz1i	⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 2 ≤ 3 ) )
76	69 73 75	mpbir2an	⊢ 3 ∈ ( ℤ≥ ‘ 2 )
77	76	a1i	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 3 ∈ ( ℤ≥ ‘ 2 ) )
78		dvdsexp	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) )
79	6 68 77 78	syl3anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) )
80	79	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) )
81		jm2.23	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 / 𝑁 ) ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
82	30 31 40 81	syl3anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
83	12 66 61 80 82	dvdstrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
84		dvds2sub	⊢ ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ∧ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℤ ) → ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) ) )
85	84	imp	⊢ ( ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ∧ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℤ ) ∧ ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
86	12 48 61 20 83 85	syl32anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
87	55	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑁 · ( 𝑀 / 𝑁 ) ) = 𝑀 )
88	87	oveq2d	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) = ( 𝐴 Yrm 𝑀 ) )
89	88	oveq1d	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) = ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
90	89	oveq2d	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) = ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) )
91	25	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
92	91	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
93	60	zcnd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℂ )
94	92 93	nncand	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) = ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) )
95	45	zcnd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑀 / 𝑁 ) ∈ ℂ )
96	44	zcnd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ∈ ℂ )
97	95 96 8	mul12d	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
98	94 97	eqtrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
99	90 98	eqtrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑀 ) − ( ( 𝐴 Yrm ( 𝑁 · ( 𝑀 / 𝑁 ) ) ) − ( ( 𝑀 / 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
100	86 99	breqtrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
101	6 16	gcdcomd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) gcd ( 𝐴 Xrm 𝑁 ) ) = ( ( 𝐴 Xrm 𝑁 ) gcd ( 𝐴 Yrm 𝑁 ) ) )
102		jm2.19lem1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) gcd ( 𝐴 Yrm 𝑁 ) ) = 1 )
103	1 3 102	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Xrm 𝑁 ) gcd ( 𝐴 Yrm 𝑁 ) ) = 1 )
104	101 103	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) gcd ( 𝐴 Xrm 𝑁 ) ) = 1 )
105	104	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) gcd ( 𝐴 Xrm 𝑁 ) ) = 1 )
106	67	a1i	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 2 ∈ ℕ0 )
107		rpexp12i	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( 2 ∈ ℕ0 ∧ ( ( 𝑀 / 𝑁 ) − 1 ) ∈ ℕ0 ) ) → ( ( ( 𝐴 Yrm 𝑁 ) gcd ( 𝐴 Xrm 𝑁 ) ) = 1 → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) gcd ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ) = 1 ) )
108	46 17 106 42 107	syl112anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( ( 𝐴 Yrm 𝑁 ) gcd ( 𝐴 Xrm 𝑁 ) ) = 1 → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) gcd ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ) = 1 ) )
109	105 108	mpd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) gcd ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ) = 1 )
110		coprmdvds	⊢ ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ ) → ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∧ ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) gcd ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ) = 1 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
111	110	imp	⊢ ( ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ ) ∧ ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) · ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∧ ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) gcd ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝑀 / 𝑁 ) − 1 ) ) ) = 1 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
112	12 44 47 100 109 111	syl32anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
113	9 112	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) )
114		rmy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
115	114	3ad2ant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) = 0 )
116		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
117	116	3ad2ant3	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
118		0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℤ )
119		ltrmy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
120	1 118 3 119	syl3anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
121	117 120	mpbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) )
122	115 121	eqbrtrrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐴 Yrm 𝑁 ) )
123		elnnz	⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ ↔ ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ 0 < ( 𝐴 Yrm 𝑁 ) ) )
124	6 122 123	sylanbrc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℕ )
125		nnne0	⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ → ( 𝐴 Yrm 𝑁 ) ≠ 0 )
126	124 125	syl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ≠ 0 )
127	126	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑁 ) ≠ 0 )
128		dvdsmulcr	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝑀 / 𝑁 ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑁 ) ≠ 0 ) ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ↔ ( 𝐴 Yrm 𝑁 ) ∥ ( 𝑀 / 𝑁 ) ) )
129	46 45 46 127 128	syl112anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ∥ ( ( 𝑀 / 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ↔ ( 𝐴 Yrm 𝑁 ) ∥ ( 𝑀 / 𝑁 ) ) )
130	113 129	mpbid	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Yrm 𝑁 ) ∥ ( 𝑀 / 𝑁 ) )
131	54	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → 𝑁 ≠ 0 )
132		dvdscmulr	⊢ ( ( ( 𝐴 Yrm 𝑁 ) ∈ ℤ ∧ ( 𝑀 / 𝑁 ) ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝑁 · ( 𝑀 / 𝑁 ) ) ↔ ( 𝐴 Yrm 𝑁 ) ∥ ( 𝑀 / 𝑁 ) ) )
133	46 45 31 131 132	syl112anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝑁 · ( 𝑀 / 𝑁 ) ) ↔ ( 𝐴 Yrm 𝑁 ) ∥ ( 𝑀 / 𝑁 ) ) )
134	130 133	mpbird	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ ( 𝑁 · ( 𝑀 / 𝑁 ) ) )
135	134 87	breqtrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ) → ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 )
136	11	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ )
137	3 6	zmulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ )
138	4	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
139	1 137 138	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
140	139	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
141	25	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
142		nnm1nn0	⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ → ( ( 𝐴 Yrm 𝑁 ) − 1 ) ∈ ℕ0 )
143	124 142	syl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) − 1 ) ∈ ℕ0 )
144		zexpcl	⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) ∈ ℤ )
145	16 143 144	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) ∈ ℤ )
146		dvdsmul2	⊢ ( ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) )
147	145 11 146	syl2anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) )
148	18	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) )
149	145	zcnd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) ∈ ℂ )
150	149 7 7	mul12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( ( 𝐴 Yrm 𝑁 ) · ( 𝐴 Yrm 𝑁 ) ) ) = ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) )
151	148 150	eqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) = ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) )
152	147 151	breqtrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) )
153	145 6	zmulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ )
154	6 153	zmulcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
155	139 154	zsubcld	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) − ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ∈ ℤ )
156		jm2.23	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) − ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
157	1 3 124 156	syl3anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 3 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) − ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
158	11 65 155 79 157	dvdstrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) − ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
159		dvdssub2	⊢ ( ( ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ ) ∧ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) − ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ↔ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
160	11 139 154 158 159	syl31anc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ↔ ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( ( 𝐴 Yrm 𝑁 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( ( 𝐴 Yrm 𝑁 ) − 1 ) ) · ( 𝐴 Yrm 𝑁 ) ) ) ) )
161	152 160	mpbird	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) )
162	161	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) )
163		simpr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 )
164		simpl1	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
165	137	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ )
166	23	adantr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → 𝑀 ∈ ℤ )
167		jm2.19	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ↔ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
168	164 165 166 167	syl3anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ↔ ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∥ ( 𝐴 Yrm 𝑀 ) ) )
169	163 168	mpbid	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( 𝐴 Yrm ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ) ∥ ( 𝐴 Yrm 𝑀 ) )
170	136 140 141 162 169	dvdstrd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) )
171	135 170	impbida	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑀 ) ↔ ( 𝑁 · ( 𝐴 Yrm 𝑁 ) ) ∥ 𝑀 ) )