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		2re	$⊢ 2 \in ℝ$
71		3re	$⊢ 3 \in ℝ$
72		2lt3	$⊢ 2 < 3$
73	70 71 72	ltleii	$⊢ 2 \leq 3$
74		2z	$⊢ 2 \in ℤ$
75	74	eluz1i	$⊢ 3 \in ℤ_{\geq 2} \leftrightarrow (3 \in ℤ \land 2 \leq 3)$
76	69 73 75	mpbir2an	$⊢ 3 \in ℤ_{\geq 2}$
77	76	a1i	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to 3 \in ℤ_{\geq 2}$
78		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}$
79	6 68 77 78	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to {(A Y_{rm} N)}^{2} ∥ {(A Y_{rm} N)}^{3}$
80	79	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}$
81		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))$
82	30 31 40 81	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))$
83	12 66 61 80 82	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))$
84		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))))$
85	84	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)))$
86	12 48 61 20 83 85	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)))$
87	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$
88	87	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$
89	88	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)$
90	89	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))$
91	25	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to A Y_{rm} M \in ℂ$
92	91	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 ℂ$
93	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 ℂ$
94	92 93	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)$
95	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 ℂ$
96	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 ℂ$
97	95 96 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)$
98	94 97	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)$
99	90 98	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)$
100	86 99	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)$
101	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)$
102		jm2.19lem1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A X_{rm} N) \gcd (A Y_{rm} N) = 1$
103	1 3 102	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to (A X_{rm} N) \gcd (A Y_{rm} N) = 1$
104	101 103	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to (A Y_{rm} N) \gcd (A X_{rm} N) = 1$
105	104	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$
106	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}$
107		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)$
108	46 17 106 42 107	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)$
109	105 108	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$
110		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))$
111	110	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)$
112	12 44 47 100 109 111	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)$
113	9 112	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)$
114		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
115	114	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to A Y_{rm} 0 = 0$
116		nngt0	$⊢ N \in ℕ \to 0 < N$
117	116	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to 0 < N$
118		0zd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to 0 \in ℤ$
119		ltrmy	$⊢ (A \in ℤ_{\geq 2} \land 0 \in ℤ \land N \in ℤ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
120	1 118 3 119	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
121	117 120	mpbid	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to A Y_{rm} 0 < A Y_{rm} N$
122	115 121	eqbrtrrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to 0 < A Y_{rm} N$
123		elnnz	$⊢ A Y_{rm} N \in ℕ \leftrightarrow (A Y_{rm} N \in ℤ \land 0 < A Y_{rm} N)$
124	6 122 123	sylanbrc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to A Y_{rm} N \in ℕ$
125		nnne0	$⊢ A Y_{rm} N \in ℕ \to A Y_{rm} N \neq 0$
126	124 125	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to A Y_{rm} N \neq 0$
127	126	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$
128		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}))$
129	46 45 46 127 128	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}))$
130	113 129	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})$
131	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$
132		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}))$
133	46 45 31 131 132	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}))$
134	130 133	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})$
135	134 87	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$
136	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 ℤ$
137	3 6	zmulcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to N (A Y_{rm} N) \in ℤ$
138	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N (A Y_{rm} N) \in ℤ) \to A Y_{rm} N (A Y_{rm} N) \in ℤ$
139	1 137 138	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to A Y_{rm} N (A Y_{rm} N) \in ℤ$
140	139	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 ℤ$
141	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 ℤ$
142		nnm1nn0	$⊢ A Y_{rm} N \in ℕ \to (A Y_{rm} N) - 1 \in ℕ_{0}$
143	124 142	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to (A Y_{rm} N) - 1 \in ℕ_{0}$
144		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 ℤ$
145	16 143 144	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to {(A X_{rm} N)}^{(A Y_{rm} N) - 1} \in ℤ$
146		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}$
147	145 11 146	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}$
148	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)$
149	145	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \to {(A X_{rm} N)}^{(A Y_{rm} N) - 1} \in ℂ$
150	149 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)$
151	148 150	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)$
152	147 151	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)$
153	145 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 ℤ$
154	6 153	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 ℤ$
155	139 154	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 ℤ$
156		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))$
157	1 3 124 156	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))$
158	11 65 155 79 157	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))$
159		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))$
160	11 139 154 158 159	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))$
161	152 160	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))$
162	161	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))$
163		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$
164		simpl1	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \land N (A Y_{rm} N) ∥ M) \to A \in ℤ_{\geq 2}$
165	137	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 ℤ$
166	23	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℕ \land N \in ℕ) \land N (A Y_{rm} N) ∥ M) \to M \in ℤ$
167		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))$
168	164 165 166 167	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))$
169	163 168	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)$
170	136 140 141 162 169	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)$
171	135 170	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