Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.20nn Structured version   Visualization version   GIF version

Theorem jm2.20nn 38990
Description: Lemma 2.20 of [JonesMatijasevic] p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014.)
Assertion
Ref Expression
jm2.20nn ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ↔ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀))

Proof of Theorem jm2.20nn
StepHypRef Expression
1 simp1 1116 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ (ℤ‘2))
2 nnz 11820 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
323ad2ant3 1115 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
4 frmy 38907 . . . . . . . . . . 11 Yrm :((ℤ‘2) × ℤ)⟶ℤ
54fovcl 7097 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ)
61, 3, 5syl2anc 576 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℤ)
76zcnd 11904 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℂ)
87adantr 473 . . . . . . 7 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∈ ℂ)
98sqvald 13325 . . . . . 6 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) = ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)))
10 zsqcl 13312 . . . . . . . . 9 ((𝐴 Yrm 𝑁) ∈ ℤ → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ)
116, 10syl 17 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ)
1211adantr 473 . . . . . . 7 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ)
13 frmx 38906 . . . . . . . . . . . 12 Xrm :((ℤ‘2) × ℤ)⟶ℕ0
1413fovcl 7097 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
151, 3, 14syl2anc 576 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
1615nn0zd 11901 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℤ)
1716adantr 473 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Xrm 𝑁) ∈ ℤ)
187sqvald 13325 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) = ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)))
1918adantr 473 . . . . . . . . . . . . 13 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) = ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)))
20 simpr 477 . . . . . . . . . . . . 13 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀))
2119, 20eqbrtrrd 4954 . . . . . . . . . . . 12 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀))
22 nnz 11820 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
23223ad2ant2 1114 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℤ)
244fovcl 7097 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
251, 23, 24syl2anc 576 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑀) ∈ ℤ)
26 muldvds1 15497 . . . . . . . . . . . . . 14 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀)))
276, 6, 25, 26syl3anc 1351 . . . . . . . . . . . . 13 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀)))
2827adantr 473 . . . . . . . . . . . 12 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀)))
2921, 28mpd 15 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀))
30 simpl1 1171 . . . . . . . . . . . 12 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝐴 ∈ (ℤ‘2))
313adantr 473 . . . . . . . . . . . 12 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ∈ ℤ)
3223adantr 473 . . . . . . . . . . . 12 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑀 ∈ ℤ)
33 jm2.19 38986 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁𝑀 ↔ (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀)))
3430, 31, 32, 33syl3anc 1351 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁𝑀 ↔ (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀)))
3529, 34mpbird 249 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁𝑀)
36 simpl2 1172 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑀 ∈ ℕ)
37 simpl3 1173 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ∈ ℕ)
38 nndivdvds 15479 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ))
3936, 37, 38syl2anc 576 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ))
4035, 39mpbid 224 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑀 / 𝑁) ∈ ℕ)
41 nnm1nn0 11753 . . . . . . . . 9 ((𝑀 / 𝑁) ∈ ℕ → ((𝑀 / 𝑁) − 1) ∈ ℕ0)
4240, 41syl 17 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) − 1) ∈ ℕ0)
43 zexpcl 13262 . . . . . . . 8 (((𝐴 Xrm 𝑁) ∈ ℤ ∧ ((𝑀 / 𝑁) − 1) ∈ ℕ0) → ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈ ℤ)
4417, 42, 43syl2anc 576 . . . . . . 7 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈ ℤ)
4540nnzd 11902 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑀 / 𝑁) ∈ ℤ)
466adantr 473 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∈ ℤ)
4745, 46zmulcld 11909 . . . . . . 7 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ∈ ℤ)
4825adantr 473 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑀) ∈ ℤ)
49 nncn 11450 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
50493ad2ant2 1114 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℂ)
51 nncn 11450 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
52513ad2ant3 1115 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
53 nnne0 11477 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
54533ad2ant3 1115 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0)
5550, 52, 54divcan2d 11221 . . . . . . . . . . . . 13 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝑀 / 𝑁)) = 𝑀)
5655oveq2d 6994 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) = (𝐴 Yrm 𝑀))
5756, 25eqeltrd 2866 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) ∈ ℤ)
5857adantr 473 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) ∈ ℤ)
5944, 46zmulcld 11909 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)) ∈ ℤ)
6045, 59zmulcld 11909 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℤ)
6158, 60zsubcld 11908 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ)
62 3nn0 11730 . . . . . . . . . . . . 13 3 ∈ ℕ0
6362a1i 11 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈ ℕ0)
64 zexpcl 13262 . . . . . . . . . . . 12 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 3 ∈ ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ)
656, 63, 64syl2anc 576 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ)
6665adantr 473 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ)
67 2nn0 11729 . . . . . . . . . . . . 13 2 ∈ ℕ0
6867a1i 11 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 2 ∈ ℕ0)
69 3z 11831 . . . . . . . . . . . . . 14 3 ∈ ℤ
70 2re 11517 . . . . . . . . . . . . . . 15 2 ∈ ℝ
71 3re 11523 . . . . . . . . . . . . . . 15 3 ∈ ℝ
72 2lt3 11622 . . . . . . . . . . . . . . 15 2 < 3
7370, 71, 72ltleii 10565 . . . . . . . . . . . . . 14 2 ≤ 3
74 2z 11830 . . . . . . . . . . . . . . 15 2 ∈ ℤ
7574eluz1i 12069 . . . . . . . . . . . . . 14 (3 ∈ (ℤ‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
7669, 73, 75mpbir2an 698 . . . . . . . . . . . . 13 3 ∈ (ℤ‘2)
7776a1i 11 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈ (ℤ‘2))
78 dvdsexp 15540 . . . . . . . . . . . 12 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 2 ∈ ℕ0 ∧ 3 ∈ (ℤ‘2)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3))
796, 68, 77, 78syl3anc 1351 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3))
8079adantr 473 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3))
81 jm2.23 38989 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
8230, 31, 40, 81syl3anc 1351 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
83 dvdstr 15509 . . . . . . . . . . 11 ((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ ((𝐴 Yrm 𝑁)↑3) ∈ ℤ ∧ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) → ((((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3) ∧ ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))))
8483imp 398 . . . . . . . . . 10 (((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ ((𝐴 Yrm 𝑁)↑3) ∈ ℤ ∧ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) ∧ (((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3) ∧ ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
8512, 66, 61, 80, 82, 84syl32anc 1358 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
86 dvds2sub 15507 . . . . . . . . . 10 ((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ ∧ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) → ((((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))))
8786imp 398 . . . . . . . . 9 (((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ ∧ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) ∧ (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))))
8812, 48, 61, 20, 85, 87syl32anc 1358 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))))
8955adantr 473 . . . . . . . . . . . 12 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 · (𝑀 / 𝑁)) = 𝑀)
9089oveq2d 6994 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) = (𝐴 Yrm 𝑀))
9190oveq1d 6993 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) = ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
9291oveq2d 6994 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = ((𝐴 Yrm 𝑀) − ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))))
9325zcnd 11904 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑀) ∈ ℂ)
9493adantr 473 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑀) ∈ ℂ)
9560zcnd 11904 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℂ)
9694, 95nncand 10805 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))
9745zcnd 11904 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑀 / 𝑁) ∈ ℂ)
9844zcnd 11904 . . . . . . . . . . 11 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈ ℂ)
9997, 98, 8mul12d 10651 . . . . . . . . . 10 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))) = (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))))
10096, 99eqtrd 2814 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))))
10192, 100eqtrd 2814 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))))
10288, 101breqtrd 4956 . . . . . . 7 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))))
103 gcdcom 15725 . . . . . . . . . . 11 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Xrm 𝑁) ∈ ℤ) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁)))
1046, 16, 103syl2anc 576 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁)))
105 jm2.19lem1 38982 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁)) = 1)
1061, 3, 105syl2anc 576 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁)) = 1)
107104, 106eqtrd 2814 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1)
108107adantr 473 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1)
10967a1i 11 . . . . . . . . 9 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 2 ∈ ℕ0)
110 rpexp12i 15925 . . . . . . . . 9 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Xrm 𝑁) ∈ ℤ ∧ (2 ∈ ℕ0 ∧ ((𝑀 / 𝑁) − 1) ∈ ℕ0)) → (((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1 → (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1))
11146, 17, 109, 42, 110syl112anc 1354 . . . . . . . 8 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1 → (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1))
112108, 111mpd 15 . . . . . . 7 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1)
113 coprmdvds 15856 . . . . . . . 8 ((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈ ℤ ∧ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ∈ ℤ) → ((((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))) ∧ (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))))
114113imp 398 . . . . . . 7 (((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈ ℤ ∧ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ∈ ℤ) ∧ (((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))) ∧ (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))
11512, 44, 47, 102, 112, 114syl32anc 1358 . . . . . 6 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))
1169, 115eqbrtrrd 4954 . . . . 5 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))
117 rmy0 38922 . . . . . . . . . . 11 (𝐴 ∈ (ℤ‘2) → (𝐴 Yrm 0) = 0)
1181173ad2ant1 1113 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 0) = 0)
119 nngt0 11474 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 < 𝑁)
1201193ad2ant3 1115 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 < 𝑁)
121 0zd 11808 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ∈ ℤ)
122 ltrmy 38945 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 < 𝑁 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑁)))
1231, 121, 3, 122syl3anc 1351 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0 < 𝑁 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑁)))
124120, 123mpbid 224 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 0) < (𝐴 Yrm 𝑁))
125118, 124eqbrtrrd 4954 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 < (𝐴 Yrm 𝑁))
126 elnnz 11806 . . . . . . . . 9 ((𝐴 Yrm 𝑁) ∈ ℕ ↔ ((𝐴 Yrm 𝑁) ∈ ℤ ∧ 0 < (𝐴 Yrm 𝑁)))
1276, 125, 126sylanbrc 575 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ)
128 nnne0 11477 . . . . . . . 8 ((𝐴 Yrm 𝑁) ∈ ℕ → (𝐴 Yrm 𝑁) ≠ 0)
129127, 128syl 17 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ≠ 0)
130129adantr 473 . . . . . 6 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ≠ 0)
131 dvdsmulcr 15502 . . . . . 6 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℤ ∧ ((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑁) ≠ 0)) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁)))
13246, 45, 46, 130, 131syl112anc 1354 . . . . 5 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁)))
133116, 132mpbid 224 . . . 4 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁))
13454adantr 473 . . . . 5 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ≠ 0)
135 dvdscmulr 15501 . . . . 5 (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ (𝑁 · (𝑀 / 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁)))
13646, 45, 31, 134, 135syl112anc 1354 . . . 4 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ (𝑁 · (𝑀 / 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁)))
137133, 136mpbird 249 . . 3 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 · (𝐴 Yrm 𝑁)) ∥ (𝑁 · (𝑀 / 𝑁)))
138137, 89breqtrd 4956 . 2 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀)
13911adantr 473 . . 3 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ)
1403, 6zmulcld 11909 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ)
1414fovcl 7097 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ)
1421, 140, 141syl2anc 576 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ)
143142adantr 473 . . 3 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ)
14425adantr 473 . . 3 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝐴 Yrm 𝑀) ∈ ℤ)
145 nnm1nn0 11753 . . . . . . . . 9 ((𝐴 Yrm 𝑁) ∈ ℕ → ((𝐴 Yrm 𝑁) − 1) ∈ ℕ0)
146127, 145syl 17 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) − 1) ∈ ℕ0)
147 zexpcl 13262 . . . . . . . 8 (((𝐴 Xrm 𝑁) ∈ ℤ ∧ ((𝐴 Yrm 𝑁) − 1) ∈ ℕ0) → ((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈ ℤ)
14816, 146, 147syl2anc 576 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈ ℤ)
149 dvdsmul2 15495 . . . . . . 7 ((((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈ ℤ ∧ ((𝐴 Yrm 𝑁)↑2) ∈ ℤ) → ((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2)))
150148, 11, 149syl2anc 576 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2)))
15118oveq2d 6994 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2)) = (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁))))
152148zcnd 11904 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈ ℂ)
153152, 7, 7mul12d 10651 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁))) = ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))
154151, 153eqtrd 2814 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2)) = ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))
155150, 154breqtrd 4956 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))
156148, 6zmulcld 11909 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)) ∈ ℤ)
1576, 156zmulcld 11909 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℤ)
158142, 157zsubcld 11908 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ)
159 jm2.23 38989 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ ∧ (𝐴 Yrm 𝑁) ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
1601, 3, 127, 159syl3anc 1351 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
161 dvdstr 15509 . . . . . . . 8 ((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ ((𝐴 Yrm 𝑁)↑3) ∈ ℤ ∧ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) → ((((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3) ∧ ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))))
162161imp 398 . . . . . . 7 (((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ ((𝐴 Yrm 𝑁)↑3) ∈ ℤ ∧ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) ∧ (((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3) ∧ ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
16311, 65, 158, 79, 160, 162syl32anc 1358 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
164 dvdssub2 15514 . . . . . 6 (((((𝐴 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 𝑁)))))
16511, 142, 157, 163, 164syl31anc 1353 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ↔ ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))
166155, 165mpbird 249 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))))
167166adantr 473 . . 3 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))))
168 simpr 477 . . . 4 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀)
169 simpl1 1171 . . . . 5 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → 𝐴 ∈ (ℤ‘2))
170140adantr 473 . . . . 5 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ)
17123adantr 473 . . . . 5 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → 𝑀 ∈ ℤ)
172 jm2.19 38986 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀 ↔ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀)))
173169, 170, 171, 172syl3anc 1351 . . . 4 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀 ↔ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀)))
174168, 173mpbid 224 . . 3 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀))
175 dvdstr 15509 . . . 4 ((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) → ((((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∧ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)))
176175imp 398 . . 3 (((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) ∧ (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∧ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀))) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀))
177139, 143, 144, 167, 174, 176syl32anc 1358 . 2 (((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀))
178138, 177impbida 788 1 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ↔ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2967   class class class wbr 4930  cfv 6190  (class class class)co 6978  cc 10335  0cc0 10337  1c1 10338   · cmul 10342   < clt 10476  cle 10477  cmin 10672   / cdiv 11100  cn 11441  2c2 11498  3c3 11499  0cn0 11710  cz 11796  cuz 12061  cexp 13247  cdvds 15470   gcd cgcd 15706   Xrm crmx 38893   Yrm crmy 38894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5050  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-inf2 8900  ax-cnex 10393  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414  ax-pre-sup 10415  ax-addf 10416  ax-mulf 10417
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-int 4751  df-iun 4795  df-iin 4796  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-se 5368  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-isom 6199  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-of 7229  df-om 7399  df-1st 7503  df-2nd 7504  df-supp 7636  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-1o 7907  df-2o 7908  df-oadd 7911  df-omul 7912  df-er 8091  df-map 8210  df-pm 8211  df-ixp 8262  df-en 8309  df-dom 8310  df-sdom 8311  df-fin 8312  df-fsupp 8631  df-fi 8672  df-sup 8703  df-inf 8704  df-oi 8771  df-card 9164  df-acn 9167  df-cda 9390  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-div 11101  df-nn 11442  df-2 11506  df-3 11507  df-4 11508  df-5 11509  df-6 11510  df-7 11511  df-8 11512  df-9 11513  df-n0 11711  df-xnn0 11783  df-z 11797  df-dec 11915  df-uz 12062  df-q 12166  df-rp 12208  df-xneg 12327  df-xadd 12328  df-xmul 12329  df-ioo 12561  df-ioc 12562  df-ico 12563  df-icc 12564  df-fz 12712  df-fzo 12853  df-fl 12980  df-mod 13056  df-seq 13188  df-exp 13248  df-fac 13452  df-bc 13481  df-hash 13509  df-shft 14290  df-cj 14322  df-re 14323  df-im 14324  df-sqrt 14458  df-abs 14459  df-limsup 14692  df-clim 14709  df-rlim 14710  df-sum 14907  df-ef 15284  df-sin 15286  df-cos 15287  df-pi 15289  df-dvds 15471  df-gcd 15707  df-prm 15875  df-numer 15934  df-denom 15935  df-struct 16344  df-ndx 16345  df-slot 16346  df-base 16348  df-sets 16349  df-ress 16350  df-plusg 16437  df-mulr 16438  df-starv 16439  df-sca 16440  df-vsca 16441  df-ip 16442  df-tset 16443  df-ple 16444  df-ds 16446  df-unif 16447  df-hom 16448  df-cco 16449  df-rest 16555  df-topn 16556  df-0g 16574  df-gsum 16575  df-topgen 16576  df-pt 16577  df-prds 16580  df-xrs 16634  df-qtop 16639  df-imas 16640  df-xps 16642  df-mre 16718  df-mrc 16719  df-acs 16721  df-mgm 17713  df-sgrp 17755  df-mnd 17766  df-submnd 17807  df-mulg 18015  df-cntz 18221  df-cmn 18671  df-psmet 20242  df-xmet 20243  df-met 20244  df-bl 20245  df-mopn 20246  df-fbas 20247  df-fg 20248  df-cnfld 20251  df-top 21209  df-topon 21226  df-topsp 21248  df-bases 21261  df-cld 21334  df-ntr 21335  df-cls 21336  df-nei 21413  df-lp 21451  df-perf 21452  df-cn 21542  df-cnp 21543  df-haus 21630  df-tx 21877  df-hmeo 22070  df-fil 22161  df-fm 22253  df-flim 22254  df-flf 22255  df-xms 22636  df-ms 22637  df-tms 22638  df-cncf 23192  df-limc 24170  df-dv 24171  df-log 24844  df-squarenn 38834  df-pell1qr 38835  df-pell14qr 38836  df-pell1234qr 38837  df-pellfund 38838  df-rmx 38895  df-rmy 38896
This theorem is referenced by:  jm2.27a  38998  jm2.27c  39000
  Copyright terms: Public domain W3C validator