| Step | Hyp | Ref
| Expression |
| 1 | | eluzelz 12888 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) |
| 2 | | peano2zm 12660 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∈ ℤ) |
| 4 | | 0z 12624 |
. . . . 5
⊢ 0 ∈
ℤ |
| 5 | | congid 42983 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℤ ∧
0 ∈ ℤ) → (𝐴
− 1) ∥ (0 − 0)) |
| 6 | 3, 4, 5 | sylancl 586 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ (0 −
0)) |
| 7 | | rmy0 42941 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
| 8 | 7 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 Yrm 0) − 0) = (0 −
0)) |
| 9 | 6, 8 | breqtrrd 5171 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm 0) −
0)) |
| 10 | | 1z 12647 |
. . . . 5
⊢ 1 ∈
ℤ |
| 11 | | congid 42983 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℤ ∧
1 ∈ ℤ) → (𝐴
− 1) ∥ (1 − 1)) |
| 12 | 3, 10, 11 | sylancl 586 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ (1 −
1)) |
| 13 | | rmy1 42942 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 1) = 1) |
| 14 | 13 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴 Yrm 1) − 1) = (1 −
1)) |
| 15 | 12, 14 | breqtrrd 5171 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm 1) −
1)) |
| 16 | | pm3.43 473 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1))) ∧ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑏) − 𝑏))) → (𝐴 ∈ (ℤ≥‘2)
→ ((𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 − 1)) −
(𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏)))) |
| 17 | 1 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℤ) |
| 18 | 17, 2 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 − 1) ∈ ℤ) |
| 19 | | eluzel2 12883 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → 2 ∈ ℤ) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 2 ∈ ℤ) |
| 21 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈
(ℤ≥‘2)) |
| 22 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℤ) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ∈ ℤ) |
| 24 | | frmy 42926 |
. . . . . . . . . . . . . 14
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 25 | 24 | fovcl 7561 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) |
| 26 | 21, 23, 25 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm 𝑏) ∈ ℤ) |
| 27 | 26, 17 | zmulcld 12728 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ) |
| 28 | 20, 27 | zmulcld 12728 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (2 · ((𝐴 Yrm 𝑏) · 𝐴)) ∈ ℤ) |
| 29 | | zmulcl 12666 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ 1 ∈
ℤ) → (𝑏 ·
1) ∈ ℤ) |
| 30 | 23, 10, 29 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 · 1) ∈ ℤ) |
| 31 | 20, 30 | zmulcld 12728 |
. . . . . . . . . 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 12660 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℤ → (𝑏 − 1) ∈
ℤ) |
| 35 | 23, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 − 1) ∈ ℤ) |
| 36 | 24 | fovcl 7561 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℤ) |
| 37 | 21, 35, 36 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm (𝑏 − 1)) ∈ ℤ) |
| 38 | 37, 35 | jca 511 |
. . . . . . . . 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 511 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ (𝑏 · 1) ∈
ℤ)) |
| 43 | 42 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ (𝑏 · 1) ∈
ℤ)) |
| 44 | | congid 42983 |
. . . . . . . . . . 11
⊢ (((𝐴 − 1) ∈ ℤ ∧
2 ∈ ℤ) → (𝐴
− 1) ∥ (2 − 2)) |
| 45 | 18, 20, 44 | syl2anc 584 |
. . . . . . . . . 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 520 |
. . . . . . . . . . 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 16307 |
. . . . . . . . . . . 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 42979 |
. . . . . . . . . 10
⊢ ((((𝐴 − 1) ∈ ℤ ∧
(𝐴 Yrm 𝑏) ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 1 ∈
ℤ) ∧ ((𝐴 −
1) ∥ ((𝐴
Yrm 𝑏) −
𝑏) ∧ (𝐴 − 1) ∥ (𝐴 − 1))) → (𝐴 − 1) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − (𝑏 · 1))) |
| 56 | 48, 50, 51, 54, 55 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − (𝑏 · 1))) |
| 57 | | congmul 42979 |
. . . . . . . . 9
⊢ ((((𝐴 − 1) ∈ ℤ ∧
2 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ (𝑏 · 1) ∈ ℤ) ∧ ((𝐴 − 1) ∥ (2 −
2) ∧ (𝐴 − 1)
∥ (((𝐴 Yrm
𝑏) · 𝐴) − (𝑏 · 1)))) → (𝐴 − 1) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · (𝑏 · 1)))) |
| 58 | 41, 43, 46, 56, 57 | syl112anc 1376 |
. . . . . . . 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 42982 |
. . . . . . . 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 1376 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2) ∧ ((𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)) ∧ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) → (𝐴 − 1) ∥ (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · (𝑏 · 1)) − (𝑏 − 1)))) |
| 62 | | rmyluc 42949 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) |
| 63 | 21, 23, 62 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) |
| 64 | | nncn 12274 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℂ) |
| 65 | 64 | mulridd 11278 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ℕ → (𝑏 · 1) = 𝑏) |
| 66 | 65 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → (2
· (𝑏 · 1)) =
(2 · 𝑏)) |
| 67 | 64 | 2timesd 12509 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → (2
· 𝑏) = (𝑏 + 𝑏)) |
| 68 | 66, 67 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ → (2
· (𝑏 · 1)) =
(𝑏 + 𝑏)) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℕ → ((2
· (𝑏 · 1))
− (𝑏 − 1)) =
((𝑏 + 𝑏) − (𝑏 − 1))) |
| 70 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ → 1 ∈
ℂ) |
| 71 | 64, 64, 70 | pnncand 11659 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℕ → ((𝑏 + 𝑏) − (𝑏 − 1)) = (𝑏 + 1)) |
| 72 | 69, 71 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℕ → (𝑏 + 1) = ((2 · (𝑏 · 1)) − (𝑏 − 1))) |
| 73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 + 1) = ((2 · (𝑏 · 1)) − (𝑏 − 1))) |
| 74 | 63, 73 | oveq12d 7449 |
. . . . . . . 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 5171 |
. . . . . 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 7439 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 0)) |
| 81 | | id 22 |
. . . . . 6
⊢ (𝑎 = 0 → 𝑎 = 0) |
| 82 | 80, 81 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = 0 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 0) −
0)) |
| 83 | 82 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 0 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 0) −
0))) |
| 84 | 83 | imbi2d 340 |
. . 3
⊢ (𝑎 = 0 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
0) − 0)))) |
| 85 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 1 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 1)) |
| 86 | | id 22 |
. . . . . 6
⊢ (𝑎 = 1 → 𝑎 = 1) |
| 87 | 85, 86 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = 1 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 1) −
1)) |
| 88 | 87 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 1 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 1) −
1))) |
| 89 | 88 | imbi2d 340 |
. . 3
⊢ (𝑎 = 1 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
1) − 1)))) |
| 90 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = (𝑏 − 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 − 1))) |
| 91 | | id 22 |
. . . . . 6
⊢ (𝑎 = (𝑏 − 1) → 𝑎 = (𝑏 − 1)) |
| 92 | 90, 91 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1))) |
| 93 | 92 | breq2d 5155 |
. . . 4
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝑏 − 1)))) |
| 94 | 93 | imbi2d 340 |
. . 3
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 − 1)) −
(𝑏 −
1))))) |
| 95 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑏)) |
| 96 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
| 97 | 95, 96 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 𝑏) − 𝑏)) |
| 98 | 97 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 𝑏 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑏) − 𝑏))) |
| 99 | 98 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑏) − 𝑏)))) |
| 100 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 + 1))) |
| 101 | | id 22 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → 𝑎 = (𝑏 + 1)) |
| 102 | 100, 101 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1))) |
| 103 | 102 | breq2d 5155 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝑏 + 1)))) |
| 104 | 103 | imbi2d 340 |
. . 3
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
(𝑏 + 1)) − (𝑏 + 1))))) |
| 105 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑁)) |
| 106 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝑁 → 𝑎 = 𝑁) |
| 107 | 105, 106 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = 𝑁 → ((𝐴 Yrm 𝑎) − 𝑎) = ((𝐴 Yrm 𝑁) − 𝑁)) |
| 108 | 107 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 𝑁 → ((𝐴 − 1) ∥ ((𝐴 Yrm 𝑎) − 𝑎) ↔ (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))) |
| 109 | 108 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑁 → ((𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑎) − 𝑎)) ↔ (𝐴 ∈ (ℤ≥‘2)
→ (𝐴 − 1)
∥ ((𝐴 Yrm
𝑁) − 𝑁)))) |
| 110 | 9, 15, 79, 84, 89, 94, 99, 104, 109 | 2nn0ind 42957 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))) |
| 111 | 110 | impcom 407 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁)) |