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	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to ({(A Y_{rm} N)}^{2} ∥ (A Y_{rm} M) \leftrightarrow N (A Y_{rm} N) ∥ M)$

Proof

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

Metamath Proof Explorer

Theorem jm2.20nn

Proof