Step | Hyp | Ref
| Expression |
1 | | eluzelz 12327 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) |
2 | | peano2zm 12099 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∈ ℤ) |
4 | | 0z 12066 |
. . . . 5
⊢ 0 ∈
ℤ |
5 | | congid 40349 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℤ ∧
0 ∈ ℤ) → (𝐴
− 1) ∥ (0 − 0)) |
6 | 3, 4, 5 | sylancl 589 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ (0 −
0)) |
7 | | rmy0 40307 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
8 | 7 | oveq1d 7179 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 Yrm 0) − 0) = (0 −
0)) |
9 | 6, 8 | breqtrrd 5055 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm 0) −
0)) |
10 | | 1z 12086 |
. . . . 5
⊢ 1 ∈
ℤ |
11 | | congid 40349 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℤ ∧
1 ∈ ℤ) → (𝐴
− 1) ∥ (1 − 1)) |
12 | 3, 10, 11 | sylancl 589 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ (1 −
1)) |
13 | | rmy1 40308 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 1) = 1) |
14 | 13 | oveq1d 7179 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 Yrm 1) − 1) = (1 −
1)) |
15 | 12, 14 | breqtrrd 5055 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm 1) −
1)) |
16 | | pm3.43 477 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1))) ∧ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑏) − 𝑏))) → (𝐴 ∈ (ℤ≥‘2)
→ ((𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 − 1)) −
(𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏)))) |
17 | 1 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℤ) |
18 | 17, 2 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 − 1) ∈ ℤ) |
19 | | eluzel2 12322 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → 2 ∈ ℤ) |
20 | 19 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 2 ∈ ℤ) |
21 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈
(ℤ≥‘2)) |
22 | | nnz 12078 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℤ) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ∈ ℤ) |
24 | | frmy 40292 |
. . . . . . . . . . . . . 14
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
25 | 24 | fovcl 7288 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) |
26 | 21, 23, 25 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm 𝑏) ∈ ℤ) |
27 | 26, 17 | zmulcld 12167 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ) |
28 | 20, 27 | zmulcld 12167 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (2 · ((𝐴 Yrm 𝑏) · 𝐴)) ∈ ℤ) |
29 | | zmulcl 12105 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑏 ·
1) ∈ ℤ) |
30 | 23, 10, 29 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 · 1) ∈ ℤ) |
31 | 20, 30 | zmulcld 12167 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (2 · (𝑏 · 1)) ∈
ℤ) |
32 | 18, 28, 31 | 3jca 1129 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 − 1) ∈ ℤ ∧ (2 ·
((𝐴 Yrm 𝑏) · 𝐴)) ∈ ℤ ∧ (2 · (𝑏 · 1)) ∈
ℤ)) |
33 | 32 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → ((𝐴 − 1) ∈ ℤ ∧ (2 ·
((𝐴 Yrm 𝑏) · 𝐴)) ∈ ℤ ∧ (2 · (𝑏 · 1)) ∈
ℤ)) |
34 | | peano2zm 12099 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℤ → (𝑏 − 1) ∈
ℤ) |
35 | 23, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 − 1) ∈ ℤ) |
36 | 24 | fovcl 7288 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℤ) |
37 | 21, 35, 36 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm (𝑏 − 1)) ∈ ℤ) |
38 | 37, 35 | jca 515 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 − 1)) ∈ ℤ ∧ (𝑏 − 1) ∈
ℤ)) |
39 | 38 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → ((𝐴 Yrm (𝑏 − 1)) ∈ ℤ ∧ (𝑏 − 1) ∈
ℤ)) |
40 | 18, 20, 20 | 3jca 1129 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 − 1) ∈ ℤ ∧ 2 ∈
ℤ ∧ 2 ∈ ℤ)) |
41 | 40 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → ((𝐴 − 1) ∈ ℤ ∧ 2 ∈
ℤ ∧ 2 ∈ ℤ)) |
42 | 27, 30 | jca 515 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ (𝑏 · 1) ∈
ℤ)) |
43 | 42 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ (𝑏 · 1) ∈
ℤ)) |
44 | | congid 40349 |
. . . . . . . . . . 11
⊢ (((𝐴 − 1) ∈ ℤ ∧
2 ∈ ℤ) → (𝐴
− 1) ∥ (2 − 2)) |
45 | 18, 20, 44 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 − 1) ∥ (2 −
2)) |
46 | 45 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ (2 −
2)) |
47 | 18, 26, 23 | 3jca 1129 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 − 1) ∈ ℤ ∧ (𝐴 Yrm 𝑏) ∈ ℤ ∧ 𝑏 ∈
ℤ)) |
48 | 47 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → ((𝐴 − 1) ∈ ℤ ∧ (𝐴 Yrm 𝑏) ∈ ℤ ∧ 𝑏 ∈
ℤ)) |
49 | 17, 10 | jctir 524 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 ∈ ℤ ∧ 1 ∈
ℤ)) |
50 | 49 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 ∈ ℤ ∧ 1 ∈
ℤ)) |
51 | | simp3r 1203 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏)) |
52 | | iddvds 15708 |
. . . . . . . . . . . 12
⊢ ((𝐴 − 1) ∈ ℤ
→ (𝐴 − 1)
∥ (𝐴 −
1)) |
53 | 18, 52 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 − 1) ∥ (𝐴 − 1)) |
54 | 53 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ (𝐴 − 1)) |
55 | | congmul 40345 |
. . . . . . . . . 10
⊢ ((((𝐴 − 1) ∈ ℤ ∧
(𝐴 Yrm 𝑏) ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 1 ∈
ℤ) ∧ ((𝐴 −
1) ∥ ((𝐴
Yrm 𝑏) −
𝑏) ∧ (𝐴 − 1) ∥ (𝐴 − 1))) → (𝐴 − 1) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − (𝑏 · 1))) |
56 | 48, 50, 51, 54, 55 | syl112anc 1375 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − (𝑏 · 1))) |
57 | | congmul 40345 |
. . . . . . . . 9
⊢ ((((𝐴 − 1) ∈ ℤ ∧
2 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ (𝑏 · 1) ∈ ℤ) ∧ ((𝐴 − 1) ∥ (2 −
2) ∧ (𝐴 − 1)
∥ (((𝐴 Yrm
𝑏) · 𝐴) − (𝑏 · 1)))) → (𝐴 − 1) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · (𝑏 · 1)))) |
58 | 41, 43, 46, 56, 57 | syl112anc 1375 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · (𝑏 · 1)))) |
59 | | simp3l 1202 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1))) |
60 | | congsub 40348 |
. . . . . . . 8
⊢ ((((𝐴 − 1) ∈ ℤ ∧
(2 · ((𝐴
Yrm 𝑏) ·
𝐴)) ∈ ℤ ∧ (2
· (𝑏 · 1))
∈ ℤ) ∧ ((𝐴
Yrm (𝑏 −
1)) ∈ ℤ ∧ (𝑏
− 1) ∈ ℤ) ∧ ((𝐴 − 1) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · (𝑏 · 1))) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)))) → (𝐴 − 1) ∥ (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · (𝑏 · 1)) − (𝑏 − 1)))) |
61 | 33, 39, 58, 59, 60 | syl112anc 1375 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · (𝑏 · 1)) − (𝑏 − 1)))) |
62 | | rmyluc 40315 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) |
63 | 21, 23, 62 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) |
64 | | nncn 11717 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℂ) |
65 | 64 | mulid1d 10729 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ℕ → (𝑏 · 1) = 𝑏) |
66 | 65 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → (2
· (𝑏 · 1)) =
(2 · 𝑏)) |
67 | 64 | 2timesd 11952 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → (2
· 𝑏) = (𝑏 + 𝑏)) |
68 | 66, 67 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ → (2
· (𝑏 · 1)) =
(𝑏 + 𝑏)) |
69 | 68 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℕ → ((2
· (𝑏 · 1))
− (𝑏 − 1)) =
((𝑏 + 𝑏) − (𝑏 − 1))) |
70 | | 1cnd 10707 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ → 1 ∈
ℂ) |
71 | 64, 64, 70 | pnncand 11107 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℕ → ((𝑏 + 𝑏) − (𝑏 − 1)) = (𝑏 + 1)) |
72 | 69, 71 | eqtr2d 2774 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℕ → (𝑏 + 1) = ((2 · (𝑏 · 1)) − (𝑏 − 1))) |
73 | 72 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 + 1) = ((2 · (𝑏 · 1)) − (𝑏 − 1))) |
74 | 63, 73 | oveq12d 7182 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1)) = (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · (𝑏 · 1)) − (𝑏 − 1)))) |
75 | 74 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1)) = (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · (𝑏 · 1)) − (𝑏 − 1)))) |
76 | 61, 75 | breqtrrd 5055 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1))) |
77 | 76 | 3exp 1120 |
. . . . 5
⊢ (𝑏 ∈ ℕ → (𝐴 ∈
(ℤ≥‘2) → (((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏)) → (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1))))) |
78 | 77 | a2d 29 |
. . . 4
⊢ (𝑏 ∈ ℕ → ((𝐴 ∈
(ℤ≥‘2) → ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 + 1)) − (𝑏 + 1))))) |
79 | 16, 78 | syl5 34 |
. . 3
⊢ (𝑏 ∈ ℕ → (((𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1))) ∧ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑏) − 𝑏))) → (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 + 1)) − (𝑏 + 1))))) |
80 | | oveq2 7172 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 0)) |
81 | | id 22 |
. . . . . 6
⊢ (𝑎 = 0 → 𝑎 = 0) |
82 | 80, 81 | oveq12d 7182 |
. . . . 5
⊢ (𝑎 = 0 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 0) −
0)) |
83 | 82 | breq2d 5039 |
. . . 4
⊢ (𝑎 = 0 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 0) −
0))) |
84 | 83 | imbi2d 344 |
. . 3
⊢ (𝑎 = 0 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
0) − 0)))) |
85 | | oveq2 7172 |
. . . . . 6
⊢ (𝑎 = 1 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 1)) |
86 | | id 22 |
. . . . . 6
⊢ (𝑎 = 1 → 𝑎 = 1) |
87 | 85, 86 | oveq12d 7182 |
. . . . 5
⊢ (𝑎 = 1 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 1) −
1)) |
88 | 87 | breq2d 5039 |
. . . 4
⊢ (𝑎 = 1 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 1) −
1))) |
89 | 88 | imbi2d 344 |
. . 3
⊢ (𝑎 = 1 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
1) − 1)))) |
90 | | oveq2 7172 |
. . . . . 6
⊢ (𝑎 = (𝑏 − 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 − 1))) |
91 | | id 22 |
. . . . . 6
⊢ (𝑎 = (𝑏 − 1) → 𝑎 = (𝑏 − 1)) |
92 | 90, 91 | oveq12d 7182 |
. . . . 5
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1))) |
93 | 92 | breq2d 5039 |
. . . 4
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)))) |
94 | 93 | imbi2d 344 |
. . 3
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 − 1)) −
(𝑏 −
1))))) |
95 | | oveq2 7172 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑏)) |
96 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
97 | 95, 96 | oveq12d 7182 |
. . . . 5
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 𝑏) − 𝑏)) |
98 | 97 | breq2d 5039 |
. . . 4
⊢ (𝑎 = 𝑏 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) |
99 | 98 | imbi2d 344 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑏) − 𝑏)))) |
100 | | oveq2 7172 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 + 1))) |
101 | | id 22 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → 𝑎 = (𝑏 + 1)) |
102 | 100, 101 | oveq12d 7182 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1))) |
103 | 102 | breq2d 5039 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1)))) |
104 | 103 | imbi2d 344 |
. . 3
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 + 1)) − (𝑏 + 1))))) |
105 | | oveq2 7172 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑁)) |
106 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝑁 → 𝑎 = 𝑁) |
107 | 105, 106 | oveq12d 7182 |
. . . . 5
⊢ (𝑎 = 𝑁 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 𝑁) − 𝑁)) |
108 | 107 | breq2d 5039 |
. . . 4
⊢ (𝑎 = 𝑁 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))) |
109 | 108 | imbi2d 344 |
. . 3
⊢ (𝑎 = 𝑁 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑁) − 𝑁)))) |
110 | 9, 15, 79, 84, 89, 94, 99, 104, 109 | 2nn0ind 40323 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))) |
111 | 110 | impcom 411 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁)) |