Proof of Theorem jm2.27a
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | jm2.27a23 | . 2
⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝑃)) | 
| 2 |  | 2z 12651 | . . . . . 6
⊢ 2 ∈
ℤ | 
| 3 |  | jm2.27a3 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℕ) | 
| 4 | 3 | nnzd 12642 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℤ) | 
| 5 |  | zmulcl 12668 | . . . . . 6
⊢ ((2
∈ ℤ ∧ 𝐶
∈ ℤ) → (2 · 𝐶) ∈ ℤ) | 
| 6 | 2, 4, 5 | sylancr 587 | . . . . 5
⊢ (𝜑 → (2 · 𝐶) ∈
ℤ) | 
| 7 |  | jm2.27a2 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℕ) | 
| 8 | 7 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 9 |  | jm2.27a27 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ ℤ) | 
| 10 |  | jm2.27a21 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 11 |  | jm2.27a8 | . . . . . . . 8
⊢ (𝜑 → 𝐻 ∈
ℕ0) | 
| 12 | 11 | nn0zd 12641 | . . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℤ) | 
| 13 |  | jm2.27a19 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵)) | 
| 14 |  | congsym 42985 | . . . . . . . 8
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐻 ∈ ℤ)
∧ (𝐵 ∈ ℤ
∧ (2 · 𝐶)
∥ (𝐻 − 𝐵))) → (2 · 𝐶) ∥ (𝐵 − 𝐻)) | 
| 15 | 6, 12, 8, 13, 14 | syl22anc 838 | . . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐵 − 𝐻)) | 
| 16 |  | jm2.27a7 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
ℕ0) | 
| 17 | 16 | nn0zd 12641 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ ℤ) | 
| 18 |  | peano2zm 12662 | . . . . . . . . 9
⊢ (𝐺 ∈ ℤ → (𝐺 − 1) ∈
ℤ) | 
| 19 | 17, 18 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝐺 − 1) ∈ ℤ) | 
| 20 | 12, 9 | zsubcld 12729 | . . . . . . . 8
⊢ (𝜑 → (𝐻 − 𝑅) ∈ ℤ) | 
| 21 |  | jm2.27a17 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1)) | 
| 22 |  | jm2.27a13 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
(ℤ≥‘2)) | 
| 23 | 11 | nn0ge0d 12592 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ 𝐻) | 
| 24 |  | rmy0 42946 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈
(ℤ≥‘2) → (𝐺 Yrm 0) = 0) | 
| 25 | 22, 24 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 Yrm 0) = 0) | 
| 26 |  | jm2.27a29 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 = (𝐺 Yrm 𝑅)) | 
| 27 | 26 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 Yrm 𝑅) = 𝐻) | 
| 28 | 23, 25, 27 | 3brtr4d 5174 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝑅)) | 
| 29 |  | 0zd 12627 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℤ) | 
| 30 |  | lermy 42972 | . . . . . . . . . . . . 13
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (0 ≤ 𝑅 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝑅))) | 
| 31 | 22, 29, 9, 30 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ 𝑅 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝑅))) | 
| 32 | 28, 31 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝑅) | 
| 33 |  | elnn0z 12628 | . . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
↔ (𝑅 ∈ ℤ
∧ 0 ≤ 𝑅)) | 
| 34 | 9, 32, 33 | sylanbrc 583 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈
ℕ0) | 
| 35 |  | jm2.16nn0 43021 | . . . . . . . . . 10
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝑅 ∈ ℕ0) → (𝐺 − 1) ∥ ((𝐺 Yrm 𝑅) − 𝑅)) | 
| 36 | 22, 34, 35 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 − 1) ∥ ((𝐺 Yrm 𝑅) − 𝑅)) | 
| 37 | 26 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → (𝐻 − 𝑅) = ((𝐺 Yrm 𝑅) − 𝑅)) | 
| 38 | 36, 37 | breqtrrd 5170 | . . . . . . . 8
⊢ (𝜑 → (𝐺 − 1) ∥ (𝐻 − 𝑅)) | 
| 39 | 6, 19, 20, 21, 38 | dvdstrd 16333 | . . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝑅)) | 
| 40 |  | congtr 42982 | . . . . . . 7
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝐻 ∈ ℤ
∧ 𝑅 ∈ ℤ)
∧ ((2 · 𝐶)
∥ (𝐵 − 𝐻) ∧ (2 · 𝐶) ∥ (𝐻 − 𝑅))) → (2 · 𝐶) ∥ (𝐵 − 𝑅)) | 
| 41 | 6, 8, 12, 9, 15, 39, 40 | syl222anc 1387 | . . . . . 6
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐵 − 𝑅)) | 
| 42 | 41 | orcd 873 | . . . . 5
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝐵 − 𝑅) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑅))) | 
| 43 |  | jm2.27a24 | . . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℤ) | 
| 44 |  | zmulcl 12668 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑄
∈ ℤ) → (2 · 𝑄) ∈ ℤ) | 
| 45 | 2, 43, 44 | sylancr 587 | . . . . . 6
⊢ (𝜑 → (2 · 𝑄) ∈
ℤ) | 
| 46 |  | zsqcl 14170 | . . . . . . . . . . . . . 14
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) | 
| 47 | 4, 46 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) | 
| 48 |  | dvdsmul2 16317 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ (𝐶↑2) ∈ ℤ) → (𝐶↑2) ∥ (2 ·
(𝐶↑2))) | 
| 49 | 2, 47, 48 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑2) ∥ (2 · (𝐶↑2))) | 
| 50 |  | jm2.27a10 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 51 | 50 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 52 | 51 | peano2zd 12727 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) | 
| 53 |  | zmulcl 12668 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (𝐶↑2) ∈ ℤ) → (2 ·
(𝐶↑2)) ∈
ℤ) | 
| 54 | 2, 47, 53 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℤ) | 
| 55 |  | dvdsmultr2 16336 | . . . . . . . . . . . . 13
⊢ (((𝐶↑2) ∈ ℤ ∧
(𝐽 + 1) ∈ ℤ
∧ (2 · (𝐶↑2)) ∈ ℤ) → ((𝐶↑2) ∥ (2 ·
(𝐶↑2)) → (𝐶↑2) ∥ ((𝐽 + 1) · (2 ·
(𝐶↑2))))) | 
| 56 | 47, 52, 54, 55 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶↑2) ∥ (2 · (𝐶↑2)) → (𝐶↑2) ∥ ((𝐽 + 1) · (2 ·
(𝐶↑2))))) | 
| 57 | 49, 56 | mpd 15 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) ∥ ((𝐽 + 1) · (2 · (𝐶↑2)))) | 
| 58 | 1 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) = ((𝐴 Yrm 𝑃)↑2)) | 
| 59 |  | jm2.27a15 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2)))) | 
| 60 |  | jm2.27a26 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 = (𝐴 Yrm 𝑄)) | 
| 61 | 59, 60 | eqtr3d 2778 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐽 + 1) · (2 · (𝐶↑2))) = (𝐴 Yrm 𝑄)) | 
| 62 | 57, 58, 61 | 3brtr3d 5173 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 Yrm 𝑃)↑2) ∥ (𝐴 Yrm 𝑄)) | 
| 63 |  | jm2.27a1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) | 
| 64 | 52 | zred 12724 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐽 + 1) ∈ ℝ) | 
| 65 | 54 | zred 12724 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℝ) | 
| 66 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℕ) | 
| 67 | 50, 66 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐽 + 1) ∈ ℕ) | 
| 68 | 67 | nngt0d 12316 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (𝐽 + 1)) | 
| 69 |  | 2nn 12340 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ | 
| 70 | 3 | nnsqcld 14284 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐶↑2) ∈ ℕ) | 
| 71 |  | nnmulcl 12291 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℕ ∧ (𝐶↑2) ∈ ℕ) → (2 ·
(𝐶↑2)) ∈
ℕ) | 
| 72 | 69, 70, 71 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℕ) | 
| 73 | 72 | nngt0d 12316 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (2 · (𝐶↑2))) | 
| 74 | 64, 65, 68, 73 | mulgt0d 11417 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < ((𝐽 + 1) · (2 · (𝐶↑2)))) | 
| 75 | 74, 59 | breqtrrd 5170 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝐸) | 
| 76 |  | rmy0 42946 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) | 
| 77 | 63, 76 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 Yrm 0) = 0) | 
| 78 | 60 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 Yrm 𝑄) = 𝐸) | 
| 79 | 75, 77, 78 | 3brtr4d 5174 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm 𝑄)) | 
| 80 |  | ltrmy 42969 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑄 ∈ ℤ) → (0 < 𝑄 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑄))) | 
| 81 | 63, 29, 43, 80 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝑄 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑄))) | 
| 82 | 79, 81 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑄) | 
| 83 |  | elnnz 12625 | . . . . . . . . . . . 12
⊢ (𝑄 ∈ ℕ ↔ (𝑄 ∈ ℤ ∧ 0 <
𝑄)) | 
| 84 | 43, 82, 83 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) | 
| 85 | 3 | nngt0d 12316 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝐶) | 
| 86 | 1 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 Yrm 𝑃) = 𝐶) | 
| 87 | 85, 77, 86 | 3brtr4d 5174 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm 𝑃)) | 
| 88 |  | ltrmy 42969 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (0 < 𝑃 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑃))) | 
| 89 | 63, 29, 10, 88 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝑃 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑃))) | 
| 90 | 87, 89 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑃) | 
| 91 |  | elnnz 12625 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ ℕ ↔ (𝑃 ∈ ℤ ∧ 0 <
𝑃)) | 
| 92 | 10, 90, 91 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 93 |  | jm2.20nn 43014 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (((𝐴 Yrm 𝑃)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄)) | 
| 94 | 63, 84, 92, 93 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴 Yrm 𝑃)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄)) | 
| 95 | 62, 94 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄) | 
| 96 | 1, 4 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 Yrm 𝑃) ∈ ℤ) | 
| 97 |  | muldvds2 16320 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 Yrm 𝑃) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄 → (𝐴 Yrm 𝑃) ∥ 𝑄)) | 
| 98 | 10, 96, 43, 97 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → ((𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄 → (𝐴 Yrm 𝑃) ∥ 𝑄)) | 
| 99 | 95, 98 | mpd 15 | . . . . . . . 8
⊢ (𝜑 → (𝐴 Yrm 𝑃) ∥ 𝑄) | 
| 100 | 1, 99 | eqbrtrd 5164 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∥ 𝑄) | 
| 101 | 2 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) | 
| 102 |  | dvdscmul 16321 | . . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ 2 ∈
ℤ) → (𝐶 ∥
𝑄 → (2 · 𝐶) ∥ (2 · 𝑄))) | 
| 103 | 4, 43, 101, 102 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (𝐶 ∥ 𝑄 → (2 · 𝐶) ∥ (2 · 𝑄))) | 
| 104 | 100, 103 | mpd 15 | . . . . . 6
⊢ (𝜑 → (2 · 𝐶) ∥ (2 · 𝑄)) | 
| 105 |  | jm2.27a25 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝐴 Xrm 𝑄)) | 
| 106 |  | jm2.27a6 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
ℕ0) | 
| 107 | 106 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℤ) | 
| 108 | 105, 107 | eqeltrrd 2841 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∈ ℤ) | 
| 109 |  | frmy 42931 | . . . . . . . . . . 11
⊢ 
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ | 
| 110 | 109 | fovcl 7562 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑅 ∈ ℤ) → (𝐴 Yrm 𝑅) ∈ ℤ) | 
| 111 | 63, 9, 110 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 Yrm 𝑅) ∈ ℤ) | 
| 112 | 26, 12 | eqeltrrd 2841 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 Yrm 𝑅) ∈ ℤ) | 
| 113 |  | eluzelz 12889 | . . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) | 
| 114 | 63, 113 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 115 | 114, 17 | zsubcld 12729 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝐺) ∈ ℤ) | 
| 116 | 111, 112 | zsubcld 12729 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)) ∈ ℤ) | 
| 117 |  | jm2.27a16 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴)) | 
| 118 |  | congsym 42985 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℤ ∧ 𝐺 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐹 ∥ (𝐺 − 𝐴))) → 𝐹 ∥ (𝐴 − 𝐺)) | 
| 119 | 107, 17, 114, 117, 118 | syl22anc 838 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∥ (𝐴 − 𝐺)) | 
| 120 | 105, 119 | eqbrtrrd 5166 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ (𝐴 − 𝐺)) | 
| 121 |  | jm2.15nn0 43020 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)
∧ 𝑅 ∈
ℕ0) → (𝐴 − 𝐺) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) | 
| 122 | 63, 22, 34, 121 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝐺) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) | 
| 123 | 108, 115,
116, 120, 122 | dvdstrd 16333 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) | 
| 124 |  | jm2.27a18 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶)) | 
| 125 | 26, 1 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝜑 → (𝐻 − 𝐶) = ((𝐺 Yrm 𝑅) − (𝐴 Yrm 𝑃))) | 
| 126 | 124, 105,
125 | 3brtr3d 5173 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ ((𝐺 Yrm 𝑅) − (𝐴 Yrm 𝑃))) | 
| 127 |  | congtr 42982 | . . . . . . . . 9
⊢ ((((𝐴 Xrm 𝑄) ∈ ℤ ∧ (𝐴 Yrm 𝑅) ∈ ℤ) ∧ ((𝐺 Yrm 𝑅) ∈ ℤ ∧ (𝐴 Yrm 𝑃) ∈ ℤ) ∧ ((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)) ∧ (𝐴 Xrm 𝑄) ∥ ((𝐺 Yrm 𝑅) − (𝐴 Yrm 𝑃)))) → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃))) | 
| 128 | 108, 111,
112, 96, 123, 126, 127 | syl222anc 1387 | . . . . . . . 8
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃))) | 
| 129 | 128 | orcd 873 | . . . . . . 7
⊢ (𝜑 → ((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃)) ∨ (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − -(𝐴 Yrm 𝑃)))) | 
| 130 |  | jm2.26 43019 | . . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℕ) ∧ (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → (((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃)) ∨ (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − -(𝐴 Yrm 𝑃))) ↔ ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃)))) | 
| 131 | 63, 84, 9, 10, 130 | syl22anc 838 | . . . . . . 7
⊢ (𝜑 → (((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃)) ∨ (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − -(𝐴 Yrm 𝑃))) ↔ ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃)))) | 
| 132 | 129, 131 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃))) | 
| 133 |  | dvdsacongtr 43001 | . . . . . 6
⊢ ((((2
· 𝑄) ∈ ℤ
∧ 𝑅 ∈ ℤ)
∧ (𝑃 ∈ ℤ
∧ (2 · 𝐶) ∈
ℤ) ∧ ((2 · 𝐶) ∥ (2 · 𝑄) ∧ ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃)))) → ((2 · 𝐶) ∥ (𝑅 − 𝑃) ∨ (2 · 𝐶) ∥ (𝑅 − -𝑃))) | 
| 134 | 45, 9, 10, 6, 104, 132, 133 | syl222anc 1387 | . . . . 5
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝑅 − 𝑃) ∨ (2 · 𝐶) ∥ (𝑅 − -𝑃))) | 
| 135 |  | acongtr 42995 | . . . . 5
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝑅 ∈ ℤ
∧ 𝑃 ∈ ℤ)
∧ (((2 · 𝐶)
∥ (𝐵 − 𝑅) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑅)) ∧ ((2 · 𝐶) ∥ (𝑅 − 𝑃) ∨ (2 · 𝐶) ∥ (𝑅 − -𝑃)))) → ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃))) | 
| 136 | 6, 8, 9, 10, 42, 134, 135 | syl222anc 1387 | . . . 4
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃))) | 
| 137 | 7 | nnnn0d 12589 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℕ0) | 
| 138 | 3 | nnnn0d 12589 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℕ0) | 
| 139 |  | jm2.27a20 | . . . . . 6
⊢ (𝜑 → 𝐵 ≤ 𝐶) | 
| 140 |  | elfz2nn0 13659 | . . . . . 6
⊢ (𝐵 ∈ (0...𝐶) ↔ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0
∧ 𝐵 ≤ 𝐶)) | 
| 141 | 137, 138,
139, 140 | syl3anbrc 1343 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ (0...𝐶)) | 
| 142 | 92 | nnnn0d 12589 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) | 
| 143 |  | rmygeid 42981 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℕ0) → 𝑃 ≤ (𝐴 Yrm 𝑃)) | 
| 144 | 63, 142, 143 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝑃 ≤ (𝐴 Yrm 𝑃)) | 
| 145 | 144, 1 | breqtrrd 5170 | . . . . . 6
⊢ (𝜑 → 𝑃 ≤ 𝐶) | 
| 146 |  | elfz2nn0 13659 | . . . . . 6
⊢ (𝑃 ∈ (0...𝐶) ↔ (𝑃 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0
∧ 𝑃 ≤ 𝐶)) | 
| 147 | 142, 138,
145, 146 | syl3anbrc 1343 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ (0...𝐶)) | 
| 148 |  | acongeq 43000 | . . . . 5
⊢ ((𝐶 ∈ ℕ ∧ 𝐵 ∈ (0...𝐶) ∧ 𝑃 ∈ (0...𝐶)) → (𝐵 = 𝑃 ↔ ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃)))) | 
| 149 | 3, 141, 147, 148 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝐵 = 𝑃 ↔ ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃)))) | 
| 150 | 136, 149 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐵 = 𝑃) | 
| 151 | 150 | oveq2d 7448 | . 2
⊢ (𝜑 → (𝐴 Yrm 𝐵) = (𝐴 Yrm 𝑃)) | 
| 152 | 1, 151 | eqtr4d 2779 | 1
⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) |