| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eluzelz 12888 | . . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) | 
| 2 |  | eluzelz 12888 | . . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℤ) | 
| 3 |  | zsubcl 12659 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∈
ℤ) | 
| 5 |  | 0z 12624 | . . . . . 6
⊢ 0 ∈
ℤ | 
| 6 |  | congid 42983 | . . . . . 6
⊢ (((𝐴 − 𝐵) ∈ ℤ ∧ 0 ∈ ℤ)
→ (𝐴 − 𝐵) ∥ (0 −
0)) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ (0 −
0)) | 
| 8 |  | rmy0 42941 | . . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) | 
| 9 |  | rmy0 42941 | . . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵 Yrm 0) = 0) | 
| 10 | 8, 9 | oveqan12d 7450 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ ((𝐴 Yrm
0) − (𝐵
Yrm 0)) = (0 − 0)) | 
| 11 | 7, 10 | breqtrrd 5171 | . . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 0) − (𝐵 Yrm
0))) | 
| 12 |  | 1z 12647 | . . . . . 6
⊢ 1 ∈
ℤ | 
| 13 |  | congid 42983 | . . . . . 6
⊢ (((𝐴 − 𝐵) ∈ ℤ ∧ 1 ∈ ℤ)
→ (𝐴 − 𝐵) ∥ (1 −
1)) | 
| 14 | 4, 12, 13 | sylancl 586 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ (1 −
1)) | 
| 15 |  | rmy1 42942 | . . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 1) = 1) | 
| 16 |  | rmy1 42942 | . . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵 Yrm 1) = 1) | 
| 17 | 15, 16 | oveqan12d 7450 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ ((𝐴 Yrm
1) − (𝐵
Yrm 1)) = (1 − 1)) | 
| 18 | 14, 17 | breqtrrd 5171 | . . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 1) − (𝐵 Yrm
1))) | 
| 19 |  | pm3.43 473 | . . . . 5
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1)))) ∧ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏))))) | 
| 20 | 4 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∈ ℤ) | 
| 21 |  | 2z 12649 | . . . . . . . . . . 11
⊢ 2 ∈
ℤ | 
| 22 | 21 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → 2 ∈
ℤ) | 
| 23 |  | simp2l 1200 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → 𝐴 ∈
(ℤ≥‘2)) | 
| 24 |  | nnz 12634 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℤ) | 
| 25 | 24 | 3ad2ant1 1134 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → 𝑏 ∈ ℤ) | 
| 26 |  | frmy 42926 | . . . . . . . . . . . . 13
⊢ 
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ | 
| 27 | 26 | fovcl 7561 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) | 
| 28 | 23, 25, 27 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 Yrm 𝑏) ∈ ℤ) | 
| 29 | 1 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝐴 ∈
ℤ) | 
| 30 | 29 | 3ad2ant2 1135 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → 𝐴 ∈ ℤ) | 
| 31 | 28, 30 | zmulcld 12728 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → ((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ) | 
| 32 | 22, 31 | zmulcld 12728 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (2 · ((𝐴 Yrm 𝑏) · 𝐴)) ∈ ℤ) | 
| 33 |  | simp2r 1201 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → 𝐵 ∈
(ℤ≥‘2)) | 
| 34 | 26 | fovcl 7561 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐵 Yrm 𝑏) ∈ ℤ) | 
| 35 | 33, 25, 34 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐵 Yrm 𝑏) ∈ ℤ) | 
| 36 | 2 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝐵 ∈
ℤ) | 
| 37 | 36 | 3ad2ant2 1135 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → 𝐵 ∈ ℤ) | 
| 38 | 35, 37 | zmulcld 12728 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → ((𝐵 Yrm 𝑏) · 𝐵) ∈ ℤ) | 
| 39 | 22, 38 | zmulcld 12728 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (2 · ((𝐵 Yrm 𝑏) · 𝐵)) ∈ ℤ) | 
| 40 |  | peano2zm 12660 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ ℤ → (𝑏 − 1) ∈
ℤ) | 
| 41 | 24, 40 | syl 17 | . . . . . . . . . . 11
⊢ (𝑏 ∈ ℕ → (𝑏 − 1) ∈
ℤ) | 
| 42 | 41 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝑏 − 1) ∈ ℤ) | 
| 43 | 26 | fovcl 7561 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℤ) | 
| 44 | 23, 42, 43 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 Yrm (𝑏 − 1)) ∈ ℤ) | 
| 45 | 26 | fovcl 7561 | . . . . . . . . . 10
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐵 Yrm (𝑏 − 1)) ∈
ℤ) | 
| 46 | 33, 42, 45 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐵 Yrm (𝑏 − 1)) ∈ ℤ) | 
| 47 |  | congid 42983 | . . . . . . . . . . 11
⊢ (((𝐴 − 𝐵) ∈ ℤ ∧ 2 ∈ ℤ)
→ (𝐴 − 𝐵) ∥ (2 −
2)) | 
| 48 | 20, 21, 47 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ (2 − 2)) | 
| 49 |  | simp3r 1203 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏))) | 
| 50 |  | iddvds 16307 | . . . . . . . . . . . 12
⊢ ((𝐴 − 𝐵) ∈ ℤ → (𝐴 − 𝐵) ∥ (𝐴 − 𝐵)) | 
| 51 | 20, 50 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ (𝐴 − 𝐵)) | 
| 52 |  | congmul 42979 | . . . . . . . . . . 11
⊢ ((((𝐴 − 𝐵) ∈ ℤ ∧ (𝐴 Yrm 𝑏) ∈ ℤ ∧ (𝐵 Yrm 𝑏) ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)) ∧ (𝐴 − 𝐵) ∥ (𝐴 − 𝐵))) → (𝐴 − 𝐵) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − ((𝐵 Yrm 𝑏) · 𝐵))) | 
| 53 | 20, 28, 35, 30, 37, 49, 51, 52 | syl322anc 1400 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − ((𝐵 Yrm 𝑏) · 𝐵))) | 
| 54 |  | congmul 42979 | . . . . . . . . . 10
⊢ ((((𝐴 − 𝐵) ∈ ℤ ∧ 2 ∈ ℤ
∧ 2 ∈ ℤ) ∧ (((𝐴 Yrm 𝑏) · 𝐴) ∈ ℤ ∧ ((𝐵 Yrm 𝑏) · 𝐵) ∈ ℤ) ∧ ((𝐴 − 𝐵) ∥ (2 − 2) ∧ (𝐴 − 𝐵) ∥ (((𝐴 Yrm 𝑏) · 𝐴) − ((𝐵 Yrm 𝑏) · 𝐵)))) → (𝐴 − 𝐵) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · ((𝐵 Yrm 𝑏) · 𝐵)))) | 
| 55 | 20, 22, 22, 31, 38, 48, 53, 54 | syl322anc 1400 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · ((𝐵 Yrm 𝑏) · 𝐵)))) | 
| 56 |  | simp3l 1202 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1)))) | 
| 57 |  | congsub 42982 | . . . . . . . . 9
⊢ ((((𝐴 − 𝐵) ∈ ℤ ∧ (2 · ((𝐴 Yrm 𝑏) · 𝐴)) ∈ ℤ ∧ (2 · ((𝐵 Yrm 𝑏) · 𝐵)) ∈ ℤ) ∧ ((𝐴 Yrm (𝑏 − 1)) ∈ ℤ ∧ (𝐵 Yrm (𝑏 − 1)) ∈ ℤ)
∧ ((𝐴 − 𝐵) ∥ ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (2 · ((𝐵 Yrm 𝑏) · 𝐵))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))))) → (𝐴 − 𝐵) ∥ (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · ((𝐵 Yrm 𝑏) · 𝐵)) − (𝐵 Yrm (𝑏 − 1))))) | 
| 58 | 20, 32, 39, 44, 46, 55, 56, 57 | syl322anc 1400 | . . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · ((𝐵 Yrm 𝑏) · 𝐵)) − (𝐵 Yrm (𝑏 − 1))))) | 
| 59 |  | rmyluc 42949 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) | 
| 60 | 23, 25, 59 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) | 
| 61 |  | rmyluc 42949 | . . . . . . . . . 10
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐵 Yrm (𝑏 + 1)) = ((2 · ((𝐵 Yrm 𝑏) · 𝐵)) − (𝐵 Yrm (𝑏 − 1)))) | 
| 62 | 33, 25, 61 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐵 Yrm (𝑏 + 1)) = ((2 · ((𝐵 Yrm 𝑏) · 𝐵)) − (𝐵 Yrm (𝑏 − 1)))) | 
| 63 | 60, 62 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1))) = (((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))) − ((2 · ((𝐵 Yrm 𝑏) · 𝐵)) − (𝐵 Yrm (𝑏 − 1))))) | 
| 64 | 58, 63 | breqtrrd 5171 | . . . . . . 7
⊢ ((𝑏 ∈ ℕ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1)))) | 
| 65 | 64 | 3exp 1120 | . . . . . 6
⊢ (𝑏 ∈ ℕ → ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏))) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1)))))) | 
| 66 | 65 | a2d 29 | . . . . 5
⊢ (𝑏 ∈ ℕ → (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ ((𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))) ∧ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1)))))) | 
| 67 | 19, 66 | syl5 34 | . . . 4
⊢ (𝑏 ∈ ℕ → ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1)))) ∧ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) → ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1)))))) | 
| 68 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 0 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 0)) | 
| 69 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 0 → (𝐵 Yrm 𝑎) = (𝐵 Yrm 0)) | 
| 70 | 68, 69 | oveq12d 7449 | . . . . . 6
⊢ (𝑎 = 0 → ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) = ((𝐴 Yrm 0) − (𝐵 Yrm
0))) | 
| 71 | 70 | breq2d 5155 | . . . . 5
⊢ (𝑎 = 0 → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) ↔ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 0) − (𝐵 Yrm
0)))) | 
| 72 | 71 | imbi2d 340 | . . . 4
⊢ (𝑎 = 0 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 0) − (𝐵 Yrm
0))))) | 
| 73 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 1 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 1)) | 
| 74 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 1 → (𝐵 Yrm 𝑎) = (𝐵 Yrm 1)) | 
| 75 | 73, 74 | oveq12d 7449 | . . . . . 6
⊢ (𝑎 = 1 → ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) = ((𝐴 Yrm 1) − (𝐵 Yrm
1))) | 
| 76 | 75 | breq2d 5155 | . . . . 5
⊢ (𝑎 = 1 → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) ↔ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 1) − (𝐵 Yrm
1)))) | 
| 77 | 76 | imbi2d 340 | . . . 4
⊢ (𝑎 = 1 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 1) − (𝐵 Yrm
1))))) | 
| 78 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = (𝑏 − 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 − 1))) | 
| 79 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = (𝑏 − 1) → (𝐵 Yrm 𝑎) = (𝐵 Yrm (𝑏 − 1))) | 
| 80 | 78, 79 | oveq12d 7449 | . . . . . 6
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) = ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1)))) | 
| 81 | 80 | breq2d 5155 | . . . . 5
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) ↔ (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1))))) | 
| 82 | 81 | imbi2d 340 | . . . 4
⊢ (𝑎 = (𝑏 − 1) → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 − 1)) − (𝐵 Yrm (𝑏 − 1)))))) | 
| 83 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 𝑏 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑏)) | 
| 84 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 𝑏 → (𝐵 Yrm 𝑎) = (𝐵 Yrm 𝑏)) | 
| 85 | 83, 84 | oveq12d 7449 | . . . . . 6
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) = ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏))) | 
| 86 | 85 | breq2d 5155 | . . . . 5
⊢ (𝑎 = 𝑏 → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) ↔ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏)))) | 
| 87 | 86 | imbi2d 340 | . . . 4
⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑏) − (𝐵 Yrm 𝑏))))) | 
| 88 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 + 1))) | 
| 89 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → (𝐵 Yrm 𝑎) = (𝐵 Yrm (𝑏 + 1))) | 
| 90 | 88, 89 | oveq12d 7449 | . . . . . 6
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) = ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1)))) | 
| 91 | 90 | breq2d 5155 | . . . . 5
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) ↔ (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1))))) | 
| 92 | 91 | imbi2d 340 | . . . 4
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm (𝑏 + 1)) − (𝐵 Yrm (𝑏 + 1)))))) | 
| 93 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 𝑁 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑁)) | 
| 94 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑎 = 𝑁 → (𝐵 Yrm 𝑎) = (𝐵 Yrm 𝑁)) | 
| 95 | 93, 94 | oveq12d 7449 | . . . . . 6
⊢ (𝑎 = 𝑁 → ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) = ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁))) | 
| 96 | 95 | breq2d 5155 | . . . . 5
⊢ (𝑎 = 𝑁 → ((𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎)) ↔ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁)))) | 
| 97 | 96 | imbi2d 340 | . . . 4
⊢ (𝑎 = 𝑁 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑎) − (𝐵 Yrm 𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
(ℤ≥‘2)) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁))))) | 
| 98 | 11, 18, 67, 72, 77, 82, 87, 92, 97 | 2nn0ind 42957 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁)))) | 
| 99 | 98 | impcom 407 | . 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
ℕ0) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁))) | 
| 100 | 99 | 3impa 1110 | 1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ 𝑁 ∈
ℕ0) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁))) |