Proof of Theorem jm2.20nn
Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈
(ℤ≥‘2)) |
2 | | nnz 12028 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 2 | 3ad2ant3 1133 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ) |
4 | | frmy 40213 |
. . . . . . . . . . 11
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
5 | 4 | fovcl 7267 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
6 | 1, 3, 5 | syl2anc 588 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
7 | 6 | zcnd 12112 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℂ) |
8 | 7 | adantr 485 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∈ ℂ) |
9 | 8 | sqvald 13542 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) = ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁))) |
10 | | zsqcl 13529 |
. . . . . . . . 9
⊢ ((𝐴 Yrm 𝑁) ∈ ℤ → ((𝐴 Yrm 𝑁)↑2) ∈
ℤ) |
11 | 6, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ) |
12 | 11 | adantr 485 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ) |
13 | | frmx 40212 |
. . . . . . . . . . . 12
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
14 | 13 | fovcl 7267 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
15 | 1, 3, 14 | syl2anc 588 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
16 | 15 | nn0zd 12109 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℤ) |
17 | 16 | adantr 485 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Xrm 𝑁) ∈ ℤ) |
18 | 7 | sqvald 13542 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) = ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁))) |
19 | 18 | adantr 485 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) = ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁))) |
20 | | simpr 489 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) |
21 | 19, 20 | eqbrtrrd 5049 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀)) |
22 | | nnz 12028 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
23 | 22 | 3ad2ant2 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℤ) |
24 | 4 | fovcl 7267 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ) |
25 | 1, 23, 24 | syl2anc 588 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑀) ∈ ℤ) |
26 | | muldvds1 15667 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) →
(((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀))) |
27 | 6, 6, 25, 26 | syl3anc 1369 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀))) |
28 | 27 | adantr 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ (𝐴 Yrm 𝑀) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀))) |
29 | 21, 28 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀)) |
30 | | simpl1 1189 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝐴 ∈
(ℤ≥‘2)) |
31 | 3 | adantr 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ∈ ℤ) |
32 | 23 | adantr 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑀 ∈ ℤ) |
33 | | jm2.19 40292 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∥ 𝑀 ↔ (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀))) |
34 | 30, 31, 32, 33 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 ∥ 𝑀 ↔ (𝐴 Yrm 𝑁) ∥ (𝐴 Yrm 𝑀))) |
35 | 29, 34 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ∥ 𝑀) |
36 | | simpl2 1190 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑀 ∈ ℕ) |
37 | | simpl3 1191 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ∈ ℕ) |
38 | | nndivdvds 15649 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ 𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ)) |
39 | 36, 37, 38 | syl2anc 588 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 ∥ 𝑀 ↔ (𝑀 / 𝑁) ∈ ℕ)) |
40 | 35, 39 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑀 / 𝑁) ∈ ℕ) |
41 | | nnm1nn0 11960 |
. . . . . . . . 9
⊢ ((𝑀 / 𝑁) ∈ ℕ → ((𝑀 / 𝑁) − 1) ∈
ℕ0) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) − 1) ∈
ℕ0) |
43 | | zexpcl 13479 |
. . . . . . . 8
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ ((𝑀 / 𝑁) − 1) ∈ ℕ0)
→ ((𝐴 Xrm
𝑁)↑((𝑀 / 𝑁) − 1)) ∈
ℤ) |
44 | 17, 42, 43 | syl2anc 588 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈
ℤ) |
45 | 40 | nnzd 12110 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑀 / 𝑁) ∈ ℤ) |
46 | 6 | adantr 485 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∈ ℤ) |
47 | 45, 46 | zmulcld 12117 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ∈ ℤ) |
48 | 25 | adantr 485 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑀) ∈ ℤ) |
49 | | nncn 11667 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
50 | 49 | 3ad2ant2 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℂ) |
51 | | nncn 11667 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
52 | 51 | 3ad2ant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ) |
53 | | nnne0 11693 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
54 | 53 | 3ad2ant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
55 | 50, 52, 54 | divcan2d 11441 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝑀 / 𝑁)) = 𝑀) |
56 | 55 | oveq2d 7159 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) = (𝐴 Yrm 𝑀)) |
57 | 56, 25 | eqeltrd 2851 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) ∈ ℤ) |
58 | 57 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) ∈ ℤ) |
59 | 44, 46 | zmulcld 12117 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)) ∈ ℤ) |
60 | 45, 59 | zmulcld 12117 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℤ) |
61 | 58, 60 | zsubcld 12116 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) |
62 | | 3nn0 11937 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈
ℕ0) |
64 | | zexpcl 13479 |
. . . . . . . . . . . 12
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 3 ∈
ℕ0) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
65 | 6, 63, 64 | syl2anc 588 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
66 | 65 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑3) ∈ ℤ) |
67 | | 2nn0 11936 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 2 ∈
ℕ0) |
69 | | 3z 12039 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ |
70 | | 2re 11733 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
71 | | 3re 11739 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ |
72 | | 2lt3 11831 |
. . . . . . . . . . . . . . 15
⊢ 2 <
3 |
73 | 70, 71, 72 | ltleii 10786 |
. . . . . . . . . . . . . 14
⊢ 2 ≤
3 |
74 | | 2z 12038 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
75 | 74 | eluz1i 12275 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
(ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤
3)) |
76 | 69, 73, 75 | mpbir2an 711 |
. . . . . . . . . . . . 13
⊢ 3 ∈
(ℤ≥‘2) |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 3 ∈
(ℤ≥‘2)) |
78 | | dvdsexp 15714 |
. . . . . . . . . . . 12
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ 2 ∈
ℕ0 ∧ 3 ∈ (ℤ≥‘2)) →
((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3)) |
79 | 6, 68, 77, 78 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3)) |
80 | 79 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁)↑3)) |
81 | | jm2.23 40295 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
82 | 30, 31, 40, 81 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
83 | 12, 66, 61, 80, 82 | dvdstrd 15681 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
84 | | dvds2sub 15677 |
. . . . . . . . . 10
⊢ ((((𝐴 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 411 |
. . . . . . . . 9
⊢
(((((𝐴
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 1376 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))) |
87 | 55 | adantr 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 · (𝑀 / 𝑁)) = 𝑀) |
88 | 87 | oveq2d 7159 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) = (𝐴 Yrm 𝑀)) |
89 | 88 | oveq1d 7158 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) = ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
90 | 89 | oveq2d 7159 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = ((𝐴 Yrm 𝑀) − ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))))) |
91 | 25 | zcnd 12112 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑀) ∈ ℂ) |
92 | 91 | adantr 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑀) ∈ ℂ) |
93 | 60 | zcnd 12112 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℂ) |
94 | 92, 93 | nncand 11025 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) |
95 | 45 | zcnd 12112 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑀 / 𝑁) ∈ ℂ) |
96 | 44 | zcnd 12112 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈
ℂ) |
97 | 95, 96, 8 | mul12d 10872 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))) = (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))) |
98 | 94, 97 | eqtrd 2794 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm 𝑀) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))) |
99 | 90, 98 | eqtrd 2794 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑀) − ((𝐴 Yrm (𝑁 · (𝑀 / 𝑁))) − ((𝑀 / 𝑁) · (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) = (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))) |
100 | 86, 99 | breqtrd 5051 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))) |
101 | 6, 16 | gcdcomd 15898 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁))) |
102 | | jm2.19lem1 40288 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁)) = 1) |
103 | 1, 3, 102 | syl2anc 588 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁) gcd (𝐴 Yrm 𝑁)) = 1) |
104 | 101, 103 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1) |
105 | 104 | adantr 485 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1) |
106 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 2 ∈
ℕ0) |
107 | | rpexp12i 16105 |
. . . . . . . . 9
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Xrm 𝑁) ∈ ℤ ∧ (2 ∈
ℕ0 ∧ ((𝑀 / 𝑁) − 1) ∈ ℕ0))
→ (((𝐴 Yrm
𝑁) gcd (𝐴 Xrm 𝑁)) = 1 → (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1)) |
108 | 46, 17, 106, 42, 107 | syl112anc 1372 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁) gcd (𝐴 Xrm 𝑁)) = 1 → (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1)) |
109 | 105, 108 | mpd 15 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1) |
110 | | coprmdvds 16034 |
. . . . . . . 8
⊢ ((((𝐴 Yrm 𝑁)↑2) ∈ ℤ ∧
((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) ∈ ℤ ∧ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ∈ ℤ) → ((((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1)) · ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))) ∧ (((𝐴 Yrm 𝑁)↑2) gcd ((𝐴 Xrm 𝑁)↑((𝑀 / 𝑁) − 1))) = 1) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)))) |
111 | 110 | imp 411 |
. . . . . . 7
⊢
(((((𝐴
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 1376 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))) |
113 | 9, 112 | eqbrtrrd 5049 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁))) |
114 | | rmy0 40228 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
115 | 114 | 3ad2ant1 1131 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 0) = 0) |
116 | | nngt0 11690 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
117 | 116 | 3ad2ant3 1133 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 < 𝑁) |
118 | | 0zd 12017 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ∈
ℤ) |
119 | | ltrmy 40251 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 < 𝑁 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑁))) |
120 | 1, 118, 3, 119 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0 < 𝑁 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑁))) |
121 | 117, 120 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 0) < (𝐴 Yrm 𝑁)) |
122 | 115, 121 | eqbrtrrd 5049 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 < (𝐴 Yrm 𝑁)) |
123 | | elnnz 12015 |
. . . . . . . . 9
⊢ ((𝐴 Yrm 𝑁) ∈ ℕ ↔ ((𝐴 Yrm 𝑁) ∈ ℤ ∧ 0 <
(𝐴 Yrm 𝑁))) |
124 | 6, 122, 123 | sylanbrc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ) |
125 | | nnne0 11693 |
. . . . . . . 8
⊢ ((𝐴 Yrm 𝑁) ∈ ℕ → (𝐴 Yrm 𝑁) ≠ 0) |
126 | 124, 125 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ≠ 0) |
127 | 126 | adantr 485 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ≠ 0) |
128 | | dvdsmulcr 15672 |
. . . . . 6
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℤ ∧ ((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑁) ≠ 0)) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁))) |
129 | 46, 45, 46, 127, 128 | syl112anc 1372 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)) ∥ ((𝑀 / 𝑁) · (𝐴 Yrm 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁))) |
130 | 113, 129 | mpbid 235 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁)) |
131 | 54 | adantr 485 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → 𝑁 ≠ 0) |
132 | | dvdscmulr 15671 |
. . . . 5
⊢ (((𝐴 Yrm 𝑁) ∈ ℤ ∧ (𝑀 / 𝑁) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ (𝑁 · (𝑀 / 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁))) |
133 | 46, 45, 31, 131, 132 | syl112anc 1372 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ (𝑁 · (𝑀 / 𝑁)) ↔ (𝐴 Yrm 𝑁) ∥ (𝑀 / 𝑁))) |
134 | 130, 133 | mpbird 260 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 · (𝐴 Yrm 𝑁)) ∥ (𝑁 · (𝑀 / 𝑁))) |
135 | 134, 87 | breqtrd 5051 |
. 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) → (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) |
136 | 11 | adantr 485 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝐴 Yrm 𝑁)↑2) ∈ ℤ) |
137 | 3, 6 | zmulcld 12117 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ) |
138 | 4 | fovcl 7267 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ) |
139 | 1, 137, 138 | syl2anc 588 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ) |
140 | 139 | adantr 485 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∈ ℤ) |
141 | 25 | adantr 485 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝐴 Yrm 𝑀) ∈ ℤ) |
142 | | nnm1nn0 11960 |
. . . . . . . . 9
⊢ ((𝐴 Yrm 𝑁) ∈ ℕ → ((𝐴 Yrm 𝑁) − 1) ∈
ℕ0) |
143 | 124, 142 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) − 1) ∈
ℕ0) |
144 | | zexpcl 13479 |
. . . . . . . 8
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ ((𝐴 Yrm 𝑁) − 1) ∈
ℕ0) → ((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈
ℤ) |
145 | 16, 143, 144 | syl2anc 588 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈
ℤ) |
146 | | dvdsmul2 15665 |
. . . . . . 7
⊢ ((((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈ ℤ ∧ ((𝐴 Yrm 𝑁)↑2) ∈ ℤ) →
((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2))) |
147 | 145, 11, 146 | syl2anc 588 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2))) |
148 | 18 | oveq2d 7159 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2)) = (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁)))) |
149 | 145 | zcnd 12112 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) ∈
ℂ) |
150 | 149, 7, 7 | mul12d 10872 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁) · (𝐴 Yrm 𝑁))) = ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) |
151 | 148, 150 | eqtrd 2794 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · ((𝐴 Yrm 𝑁)↑2)) = ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) |
152 | 147, 151 | breqtrd 5051 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) |
153 | 145, 6 | zmulcld 12117 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)) ∈ ℤ) |
154 | 6, 153 | zmulcld 12117 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℤ) |
155 | 139, 154 | zsubcld 12116 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁)))) ∈ ℤ) |
156 | | jm2.23 40295 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ (𝐴 Yrm 𝑁) ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
157 | 1, 3, 124, 156 | syl3anc 1369 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
158 | 11, 65, 155, 79, 157 | dvdstrd 15681 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) − ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
159 | | dvdssub2 15687 |
. . . . . 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 𝑁))))) |
160 | 11, 139, 154, 158, 159 | syl31anc 1371 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ↔ ((𝐴 Yrm 𝑁)↑2) ∥ ((𝐴 Yrm 𝑁) · (((𝐴 Xrm 𝑁)↑((𝐴 Yrm 𝑁) − 1)) · (𝐴 Yrm 𝑁))))) |
161 | 152, 160 | mpbird 260 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁)))) |
162 | 161 | adantr 485 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁)))) |
163 | | simpr 489 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) |
164 | | simpl1 1189 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → 𝐴 ∈
(ℤ≥‘2)) |
165 | 137 | adantr 485 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ) |
166 | 23 | adantr 485 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → 𝑀 ∈ ℤ) |
167 | | jm2.19 40292 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀 ↔ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀))) |
168 | 164, 165,
166, 167 | syl3anc 1369 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀 ↔ (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀))) |
169 | 163, 168 | mpbid 235 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → (𝐴 Yrm (𝑁 · (𝐴 Yrm 𝑁))) ∥ (𝐴 Yrm 𝑀)) |
170 | 136, 140,
141, 162, 169 | dvdstrd 15681 |
. 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀) → ((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀)) |
171 | 135, 170 | impbida 801 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ↔ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀)) |