Proof of Theorem jm2.27a
Step | Hyp | Ref
| Expression |
1 | | jm2.27a23 |
. 2
⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝑃)) |
2 | | 2z 11761 |
. . . . . 6
⊢ 2 ∈
ℤ |
3 | | jm2.27a3 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℕ) |
4 | 3 | nnzd 11833 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℤ) |
5 | | zmulcl 11778 |
. . . . . 6
⊢ ((2
∈ ℤ ∧ 𝐶
∈ ℤ) → (2 · 𝐶) ∈ ℤ) |
6 | 2, 4, 5 | sylancr 581 |
. . . . 5
⊢ (𝜑 → (2 · 𝐶) ∈
ℤ) |
7 | | jm2.27a2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℕ) |
8 | 7 | nnzd 11833 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℤ) |
9 | | jm2.27a27 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℤ) |
10 | | jm2.27a21 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℤ) |
11 | | jm2.27a8 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈
ℕ0) |
12 | 11 | nn0zd 11832 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℤ) |
13 | | jm2.27a19 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵)) |
14 | | congsym 38476 |
. . . . . . . 8
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐻 ∈ ℤ)
∧ (𝐵 ∈ ℤ
∧ (2 · 𝐶)
∥ (𝐻 − 𝐵))) → (2 · 𝐶) ∥ (𝐵 − 𝐻)) |
15 | 6, 12, 8, 13, 14 | syl22anc 829 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐵 − 𝐻)) |
16 | | jm2.27a17 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1)) |
17 | | jm2.27a13 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
(ℤ≥‘2)) |
18 | 11 | nn0ge0d 11705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ 𝐻) |
19 | | rmy0 38435 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈
(ℤ≥‘2) → (𝐺 Yrm 0) = 0) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 Yrm 0) = 0) |
21 | | jm2.27a29 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 = (𝐺 Yrm 𝑅)) |
22 | 21 | eqcomd 2783 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 Yrm 𝑅) = 𝐻) |
23 | 18, 20, 22 | 3brtr4d 4918 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝑅)) |
24 | | 0zd 11740 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℤ) |
25 | | lermy 38463 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (0 ≤ 𝑅 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝑅))) |
26 | 17, 24, 9, 25 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ 𝑅 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝑅))) |
27 | 23, 26 | mpbird 249 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝑅) |
28 | | elnn0z 11741 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
↔ (𝑅 ∈ ℤ
∧ 0 ≤ 𝑅)) |
29 | 9, 27, 28 | sylanbrc 578 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
30 | | jm2.16nn0 38512 |
. . . . . . . . . 10
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝑅 ∈ ℕ0) → (𝐺 − 1) ∥ ((𝐺 Yrm 𝑅) − 𝑅)) |
31 | 17, 29, 30 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 − 1) ∥ ((𝐺 Yrm 𝑅) − 𝑅)) |
32 | 21 | oveq1d 6937 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 − 𝑅) = ((𝐺 Yrm 𝑅) − 𝑅)) |
33 | 31, 32 | breqtrrd 4914 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 − 1) ∥ (𝐻 − 𝑅)) |
34 | | jm2.27a7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈
ℕ0) |
35 | 34 | nn0zd 11832 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ ℤ) |
36 | | peano2zm 11772 |
. . . . . . . . . 10
⊢ (𝐺 ∈ ℤ → (𝐺 − 1) ∈
ℤ) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 − 1) ∈ ℤ) |
38 | 12, 9 | zsubcld 11839 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 − 𝑅) ∈ ℤ) |
39 | | dvdstr 15425 |
. . . . . . . . 9
⊢ (((2
· 𝐶) ∈ ℤ
∧ (𝐺 − 1) ∈
ℤ ∧ (𝐻 −
𝑅) ∈ ℤ) →
(((2 · 𝐶) ∥
(𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻 − 𝑅)) → (2 · 𝐶) ∥ (𝐻 − 𝑅))) |
40 | 6, 37, 38, 39 | syl3anc 1439 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻 − 𝑅)) → (2 · 𝐶) ∥ (𝐻 − 𝑅))) |
41 | 16, 33, 40 | mp2and 689 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝑅)) |
42 | | congtr 38473 |
. . . . . . 7
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝐻 ∈ ℤ
∧ 𝑅 ∈ ℤ)
∧ ((2 · 𝐶)
∥ (𝐵 − 𝐻) ∧ (2 · 𝐶) ∥ (𝐻 − 𝑅))) → (2 · 𝐶) ∥ (𝐵 − 𝑅)) |
43 | 6, 8, 12, 9, 15, 41, 42 | syl222anc 1454 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐵 − 𝑅)) |
44 | 43 | orcd 862 |
. . . . 5
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝐵 − 𝑅) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑅))) |
45 | | jm2.27a24 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℤ) |
46 | | zmulcl 11778 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑄
∈ ℤ) → (2 · 𝑄) ∈ ℤ) |
47 | 2, 45, 46 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑄) ∈
ℤ) |
48 | | zsqcl 13253 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) |
49 | 4, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) |
50 | | dvdsmul2 15411 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ (𝐶↑2) ∈ ℤ) → (𝐶↑2) ∥ (2 ·
(𝐶↑2))) |
51 | 2, 49, 50 | sylancr 581 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑2) ∥ (2 · (𝐶↑2))) |
52 | | jm2.27a10 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
53 | 52 | nn0zd 11832 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐽 ∈ ℤ) |
54 | 53 | peano2zd 11837 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) |
55 | | zmulcl 11778 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (𝐶↑2) ∈ ℤ) → (2 ·
(𝐶↑2)) ∈
ℤ) |
56 | 2, 49, 55 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℤ) |
57 | | dvdsmultr2 15428 |
. . . . . . . . . . . . 13
⊢ (((𝐶↑2) ∈ ℤ ∧
(𝐽 + 1) ∈ ℤ
∧ (2 · (𝐶↑2)) ∈ ℤ) → ((𝐶↑2) ∥ (2 ·
(𝐶↑2)) → (𝐶↑2) ∥ ((𝐽 + 1) · (2 ·
(𝐶↑2))))) |
58 | 49, 54, 56, 57 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶↑2) ∥ (2 · (𝐶↑2)) → (𝐶↑2) ∥ ((𝐽 + 1) · (2 ·
(𝐶↑2))))) |
59 | 51, 58 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) ∥ ((𝐽 + 1) · (2 · (𝐶↑2)))) |
60 | 1 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) = ((𝐴 Yrm 𝑃)↑2)) |
61 | | jm2.27a15 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2)))) |
62 | | jm2.27a26 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 = (𝐴 Yrm 𝑄)) |
63 | 61, 62 | eqtr3d 2815 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐽 + 1) · (2 · (𝐶↑2))) = (𝐴 Yrm 𝑄)) |
64 | 59, 60, 63 | 3brtr3d 4917 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 Yrm 𝑃)↑2) ∥ (𝐴 Yrm 𝑄)) |
65 | | jm2.27a1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
66 | 54 | zred 11834 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐽 + 1) ∈ ℝ) |
67 | 56 | zred 11834 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℝ) |
68 | | nn0p1nn 11683 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℕ) |
69 | 52, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐽 + 1) ∈ ℕ) |
70 | 69 | nngt0d 11424 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (𝐽 + 1)) |
71 | | 2nn 11448 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ |
72 | 3 | nnsqcld 13350 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐶↑2) ∈ ℕ) |
73 | | nnmulcl 11399 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℕ ∧ (𝐶↑2) ∈ ℕ) → (2 ·
(𝐶↑2)) ∈
ℕ) |
74 | 71, 72, 73 | sylancr 581 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℕ) |
75 | 74 | nngt0d 11424 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (2 · (𝐶↑2))) |
76 | 66, 67, 70, 75 | mulgt0d 10531 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < ((𝐽 + 1) · (2 · (𝐶↑2)))) |
77 | 76, 61 | breqtrrd 4914 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝐸) |
78 | | rmy0 38435 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
79 | 65, 78 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 Yrm 0) = 0) |
80 | 62 | eqcomd 2783 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 Yrm 𝑄) = 𝐸) |
81 | 77, 79, 80 | 3brtr4d 4918 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm 𝑄)) |
82 | | ltrmy 38460 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑄 ∈ ℤ) → (0 < 𝑄 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑄))) |
83 | 65, 24, 45, 82 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝑄 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑄))) |
84 | 81, 83 | mpbird 249 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑄) |
85 | | elnnz 11738 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ ℕ ↔ (𝑄 ∈ ℤ ∧ 0 <
𝑄)) |
86 | 45, 84, 85 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) |
87 | 3 | nngt0d 11424 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝐶) |
88 | 1 | eqcomd 2783 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 Yrm 𝑃) = 𝐶) |
89 | 87, 79, 88 | 3brtr4d 4918 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm 𝑃)) |
90 | | ltrmy 38460 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (0 < 𝑃 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑃))) |
91 | 65, 24, 10, 90 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝑃 ↔ (𝐴 Yrm 0) < (𝐴 Yrm 𝑃))) |
92 | 89, 91 | mpbird 249 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑃) |
93 | | elnnz 11738 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℕ ↔ (𝑃 ∈ ℤ ∧ 0 <
𝑃)) |
94 | 10, 92, 93 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) |
95 | | jm2.20nn 38505 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (((𝐴 Yrm 𝑃)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄)) |
96 | 65, 86, 94, 95 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 Yrm 𝑃)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄)) |
97 | 64, 96 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄) |
98 | 1, 4 | eqeltrrd 2859 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 Yrm 𝑃) ∈ ℤ) |
99 | | muldvds2 15414 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 Yrm 𝑃) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄 → (𝐴 Yrm 𝑃) ∥ 𝑄)) |
100 | 10, 98, 45, 99 | syl3anc 1439 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 · (𝐴 Yrm 𝑃)) ∥ 𝑄 → (𝐴 Yrm 𝑃) ∥ 𝑄)) |
101 | 97, 100 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 Yrm 𝑃) ∥ 𝑄) |
102 | 1, 101 | eqbrtrd 4908 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∥ 𝑄) |
103 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) |
104 | | dvdscmul 15415 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ 2 ∈
ℤ) → (𝐶 ∥
𝑄 → (2 · 𝐶) ∥ (2 · 𝑄))) |
105 | 4, 45, 103, 104 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∥ 𝑄 → (2 · 𝐶) ∥ (2 · 𝑄))) |
106 | 102, 105 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐶) ∥ (2 · 𝑄)) |
107 | | jm2.27a25 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝐴 Xrm 𝑄)) |
108 | | jm2.27a6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
ℕ0) |
109 | 108 | nn0zd 11832 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℤ) |
110 | 107, 109 | eqeltrrd 2859 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∈ ℤ) |
111 | | frmy 38420 |
. . . . . . . . . . 11
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
112 | 111 | fovcl 7042 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑅 ∈ ℤ) → (𝐴 Yrm 𝑅) ∈ ℤ) |
113 | 65, 9, 112 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Yrm 𝑅) ∈ ℤ) |
114 | 21, 12 | eqeltrrd 2859 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 Yrm 𝑅) ∈ ℤ) |
115 | | eluzelz 12002 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) |
116 | 65, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
117 | | jm2.27a16 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴)) |
118 | | congsym 38476 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℤ ∧ 𝐺 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐹 ∥ (𝐺 − 𝐴))) → 𝐹 ∥ (𝐴 − 𝐺)) |
119 | 109, 35, 116, 117, 118 | syl22anc 829 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∥ (𝐴 − 𝐺)) |
120 | 107, 119 | eqbrtrrd 4910 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ (𝐴 − 𝐺)) |
121 | | jm2.15nn0 38511 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)
∧ 𝑅 ∈
ℕ0) → (𝐴 − 𝐺) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) |
122 | 65, 17, 29, 121 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝐺) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) |
123 | 116, 35 | zsubcld 11839 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 𝐺) ∈ ℤ) |
124 | 113, 114 | zsubcld 11839 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)) ∈ ℤ) |
125 | | dvdstr 15425 |
. . . . . . . . . . 11
⊢ (((𝐴 Xrm 𝑄) ∈ ℤ ∧ (𝐴 − 𝐺) ∈ ℤ ∧ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)) ∈ ℤ) → (((𝐴 Xrm 𝑄) ∥ (𝐴 − 𝐺) ∧ (𝐴 − 𝐺) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)))) |
126 | 110, 123,
124, 125 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 Xrm 𝑄) ∥ (𝐴 − 𝐺) ∧ (𝐴 − 𝐺) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)))) |
127 | 120, 122,
126 | mp2and 689 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅))) |
128 | | jm2.27a18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶)) |
129 | 21, 1 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 − 𝐶) = ((𝐺 Yrm 𝑅) − (𝐴 Yrm 𝑃))) |
130 | 128, 107,
129 | 3brtr3d 4917 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ ((𝐺 Yrm 𝑅) − (𝐴 Yrm 𝑃))) |
131 | | congtr 38473 |
. . . . . . . . 9
⊢ ((((𝐴 Xrm 𝑄) ∈ ℤ ∧ (𝐴 Yrm 𝑅) ∈ ℤ) ∧ ((𝐺 Yrm 𝑅) ∈ ℤ ∧ (𝐴 Yrm 𝑃) ∈ ℤ) ∧ ((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐺 Yrm 𝑅)) ∧ (𝐴 Xrm 𝑄) ∥ ((𝐺 Yrm 𝑅) − (𝐴 Yrm 𝑃)))) → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃))) |
132 | 110, 113,
114, 98, 127, 130, 131 | syl222anc 1454 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃))) |
133 | 132 | orcd 862 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃)) ∨ (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − -(𝐴 Yrm 𝑃)))) |
134 | | jm2.26 38510 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℕ) ∧ (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → (((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃)) ∨ (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − -(𝐴 Yrm 𝑃))) ↔ ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃)))) |
135 | 65, 86, 9, 10, 134 | syl22anc 829 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − (𝐴 Yrm 𝑃)) ∨ (𝐴 Xrm 𝑄) ∥ ((𝐴 Yrm 𝑅) − -(𝐴 Yrm 𝑃))) ↔ ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃)))) |
136 | 133, 135 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃))) |
137 | | dvdsacongtr 38492 |
. . . . . 6
⊢ ((((2
· 𝑄) ∈ ℤ
∧ 𝑅 ∈ ℤ)
∧ (𝑃 ∈ ℤ
∧ (2 · 𝐶) ∈
ℤ) ∧ ((2 · 𝐶) ∥ (2 · 𝑄) ∧ ((2 · 𝑄) ∥ (𝑅 − 𝑃) ∨ (2 · 𝑄) ∥ (𝑅 − -𝑃)))) → ((2 · 𝐶) ∥ (𝑅 − 𝑃) ∨ (2 · 𝐶) ∥ (𝑅 − -𝑃))) |
138 | 47, 9, 10, 6, 106, 136, 137 | syl222anc 1454 |
. . . . 5
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝑅 − 𝑃) ∨ (2 · 𝐶) ∥ (𝑅 − -𝑃))) |
139 | | acongtr 38486 |
. . . . 5
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝑅 ∈ ℤ
∧ 𝑃 ∈ ℤ)
∧ (((2 · 𝐶)
∥ (𝐵 − 𝑅) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑅)) ∧ ((2 · 𝐶) ∥ (𝑅 − 𝑃) ∨ (2 · 𝐶) ∥ (𝑅 − -𝑃)))) → ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃))) |
140 | 6, 8, 9, 10, 44, 138, 139 | syl222anc 1454 |
. . . 4
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃))) |
141 | 7 | nnnn0d 11702 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
142 | 3 | nnnn0d 11702 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℕ0) |
143 | | jm2.27a20 |
. . . . . 6
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
144 | | elfz2nn0 12749 |
. . . . . 6
⊢ (𝐵 ∈ (0...𝐶) ↔ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0
∧ 𝐵 ≤ 𝐶)) |
145 | 141, 142,
143, 144 | syl3anbrc 1400 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (0...𝐶)) |
146 | 94 | nnnn0d 11702 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
147 | | rmygeid 38472 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℕ0) → 𝑃 ≤ (𝐴 Yrm 𝑃)) |
148 | 65, 146, 147 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ≤ (𝐴 Yrm 𝑃)) |
149 | 148, 1 | breqtrrd 4914 |
. . . . . 6
⊢ (𝜑 → 𝑃 ≤ 𝐶) |
150 | | elfz2nn0 12749 |
. . . . . 6
⊢ (𝑃 ∈ (0...𝐶) ↔ (𝑃 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0
∧ 𝑃 ≤ 𝐶)) |
151 | 146, 142,
149, 150 | syl3anbrc 1400 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (0...𝐶)) |
152 | | acongeq 38491 |
. . . . 5
⊢ ((𝐶 ∈ ℕ ∧ 𝐵 ∈ (0...𝐶) ∧ 𝑃 ∈ (0...𝐶)) → (𝐵 = 𝑃 ↔ ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃)))) |
153 | 3, 145, 151, 152 | syl3anc 1439 |
. . . 4
⊢ (𝜑 → (𝐵 = 𝑃 ↔ ((2 · 𝐶) ∥ (𝐵 − 𝑃) ∨ (2 · 𝐶) ∥ (𝐵 − -𝑃)))) |
154 | 140, 153 | mpbird 249 |
. . 3
⊢ (𝜑 → 𝐵 = 𝑃) |
155 | 154 | oveq2d 6938 |
. 2
⊢ (𝜑 → (𝐴 Yrm 𝐵) = (𝐴 Yrm 𝑃)) |
156 | 1, 155 | eqtr4d 2816 |
1
⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) |