Proof of Theorem ipcnlem2
| Step | Hyp | Ref
| Expression |
| 1 | | ipcn.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ ℂPreHil) |
| 2 | | ipcn.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | | ipcn.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 4 | | ipcn.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
| 5 | | ipcn.h |
. . . 4
⊢ , =
(·𝑖‘𝑊) |
| 6 | 4, 5 | cphipcl 25225 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ ℂ) |
| 7 | 1, 2, 3, 6 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝐴 , 𝐵) ∈ ℂ) |
| 8 | | ipcn.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 9 | | ipcn.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 10 | 4, 5 | cphipcl 25225 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 , 𝑌) ∈ ℂ) |
| 11 | 1, 8, 9, 10 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝑋 , 𝑌) ∈ ℂ) |
| 12 | 4, 5 | cphipcl 25225 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐴 , 𝑌) ∈ ℂ) |
| 13 | 1, 2, 9, 12 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝐴 , 𝑌) ∈ ℂ) |
| 14 | | ipcn.r |
. . 3
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
| 15 | 14 | rpred 13077 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℝ) |
| 16 | 7, 13 | subcld 11620 |
. . . 4
⊢ (𝜑 → ((𝐴 , 𝐵) − (𝐴 , 𝑌)) ∈ ℂ) |
| 17 | 16 | abscld 15475 |
. . 3
⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝐴 , 𝑌))) ∈ ℝ) |
| 18 | | cphnlm 25206 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmMod) |
| 19 | 1, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ NrmMod) |
| 20 | | nlmngp 24698 |
. . . . . . . 8
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
| 21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ NrmGrp) |
| 22 | | ipcn.n |
. . . . . . . 8
⊢ 𝑁 = (norm‘𝑊) |
| 23 | 4, 22 | nmcl 24629 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉) → (𝑁‘𝐴) ∈ ℝ) |
| 24 | 21, 2, 23 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝐴) ∈ ℝ) |
| 25 | 4, 22 | nmge0 24630 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉) → 0 ≤ (𝑁‘𝐴)) |
| 26 | 21, 2, 25 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑁‘𝐴)) |
| 27 | 24, 26 | ge0p1rpd 13107 |
. . . . 5
⊢ (𝜑 → ((𝑁‘𝐴) + 1) ∈
ℝ+) |
| 28 | 27 | rpred 13077 |
. . . 4
⊢ (𝜑 → ((𝑁‘𝐴) + 1) ∈ ℝ) |
| 29 | | ngpms 24613 |
. . . . . 6
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp) |
| 30 | 21, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ MetSp) |
| 31 | | ipcn.d |
. . . . . 6
⊢ 𝐷 = (dist‘𝑊) |
| 32 | 4, 31 | mscl 24471 |
. . . . 5
⊢ ((𝑊 ∈ MetSp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐵𝐷𝑌) ∈ ℝ) |
| 33 | 30, 3, 9, 32 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝐵𝐷𝑌) ∈ ℝ) |
| 34 | 28, 33 | remulcld 11291 |
. . 3
⊢ (𝜑 → (((𝑁‘𝐴) + 1) · (𝐵𝐷𝑌)) ∈ ℝ) |
| 35 | 15 | rehalfcld 12513 |
. . 3
⊢ (𝜑 → (𝑅 / 2) ∈ ℝ) |
| 36 | 24, 33 | remulcld 11291 |
. . . 4
⊢ (𝜑 → ((𝑁‘𝐴) · (𝐵𝐷𝑌)) ∈ ℝ) |
| 37 | | eqid 2737 |
. . . . . . . 8
⊢
(-g‘𝑊) = (-g‘𝑊) |
| 38 | 5, 4, 37 | cphsubdi 25243 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐴 , (𝐵(-g‘𝑊)𝑌)) = ((𝐴 , 𝐵) − (𝐴 , 𝑌))) |
| 39 | 1, 2, 3, 9, 38 | syl13anc 1374 |
. . . . . 6
⊢ (𝜑 → (𝐴 , (𝐵(-g‘𝑊)𝑌)) = ((𝐴 , 𝐵) − (𝐴 , 𝑌))) |
| 40 | 39 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐴 , (𝐵(-g‘𝑊)𝑌))) = (abs‘((𝐴 , 𝐵) − (𝐴 , 𝑌)))) |
| 41 | | ngpgrp 24612 |
. . . . . . . . 9
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ Grp) |
| 42 | 21, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Grp) |
| 43 | 4, 37 | grpsubcl 19038 |
. . . . . . . 8
⊢ ((𝑊 ∈ Grp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐵(-g‘𝑊)𝑌) ∈ 𝑉) |
| 44 | 42, 3, 9, 43 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐵(-g‘𝑊)𝑌) ∈ 𝑉) |
| 45 | 4, 5, 22 | ipcau 25272 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝑉 ∧ (𝐵(-g‘𝑊)𝑌) ∈ 𝑉) → (abs‘(𝐴 , (𝐵(-g‘𝑊)𝑌))) ≤ ((𝑁‘𝐴) · (𝑁‘(𝐵(-g‘𝑊)𝑌)))) |
| 46 | 1, 2, 44, 45 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐴 , (𝐵(-g‘𝑊)𝑌))) ≤ ((𝑁‘𝐴) · (𝑁‘(𝐵(-g‘𝑊)𝑌)))) |
| 47 | 22, 4, 37, 31 | ngpds 24617 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐵𝐷𝑌) = (𝑁‘(𝐵(-g‘𝑊)𝑌))) |
| 48 | 21, 3, 9, 47 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐵𝐷𝑌) = (𝑁‘(𝐵(-g‘𝑊)𝑌))) |
| 49 | 48 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘𝐴) · (𝐵𝐷𝑌)) = ((𝑁‘𝐴) · (𝑁‘(𝐵(-g‘𝑊)𝑌)))) |
| 50 | 46, 49 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐴 , (𝐵(-g‘𝑊)𝑌))) ≤ ((𝑁‘𝐴) · (𝐵𝐷𝑌))) |
| 51 | 40, 50 | eqbrtrrd 5167 |
. . . 4
⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝐴 , 𝑌))) ≤ ((𝑁‘𝐴) · (𝐵𝐷𝑌))) |
| 52 | | msxms 24464 |
. . . . . . 7
⊢ (𝑊 ∈ MetSp → 𝑊 ∈
∞MetSp) |
| 53 | 30, 52 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ∞MetSp) |
| 54 | 4, 31 | xmsge0 24473 |
. . . . . 6
⊢ ((𝑊 ∈ ∞MetSp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 0 ≤ (𝐵𝐷𝑌)) |
| 55 | 53, 3, 9, 54 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐵𝐷𝑌)) |
| 56 | 24 | lep1d 12199 |
. . . . 5
⊢ (𝜑 → (𝑁‘𝐴) ≤ ((𝑁‘𝐴) + 1)) |
| 57 | 24, 28, 33, 55, 56 | lemul1ad 12207 |
. . . 4
⊢ (𝜑 → ((𝑁‘𝐴) · (𝐵𝐷𝑌)) ≤ (((𝑁‘𝐴) + 1) · (𝐵𝐷𝑌))) |
| 58 | 17, 36, 34, 51, 57 | letrd 11418 |
. . 3
⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝐴 , 𝑌))) ≤ (((𝑁‘𝐴) + 1) · (𝐵𝐷𝑌))) |
| 59 | | ipcn.2 |
. . . . 5
⊢ (𝜑 → (𝐵𝐷𝑌) < 𝑇) |
| 60 | | ipcn.t |
. . . . 5
⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) |
| 61 | 59, 60 | breqtrdi 5184 |
. . . 4
⊢ (𝜑 → (𝐵𝐷𝑌) < ((𝑅 / 2) / ((𝑁‘𝐴) + 1))) |
| 62 | 33, 35, 27 | ltmuldiv2d 13125 |
. . . 4
⊢ (𝜑 → ((((𝑁‘𝐴) + 1) · (𝐵𝐷𝑌)) < (𝑅 / 2) ↔ (𝐵𝐷𝑌) < ((𝑅 / 2) / ((𝑁‘𝐴) + 1)))) |
| 63 | 61, 62 | mpbird 257 |
. . 3
⊢ (𝜑 → (((𝑁‘𝐴) + 1) · (𝐵𝐷𝑌)) < (𝑅 / 2)) |
| 64 | 17, 34, 35, 58, 63 | lelttrd 11419 |
. 2
⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝐴 , 𝑌))) < (𝑅 / 2)) |
| 65 | 13, 11 | subcld 11620 |
. . . 4
⊢ (𝜑 → ((𝐴 , 𝑌) − (𝑋 , 𝑌)) ∈ ℂ) |
| 66 | 65 | abscld 15475 |
. . 3
⊢ (𝜑 → (abs‘((𝐴 , 𝑌) − (𝑋 , 𝑌))) ∈ ℝ) |
| 67 | 4, 31 | mscl 24471 |
. . . . 5
⊢ ((𝑊 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝐴𝐷𝑋) ∈ ℝ) |
| 68 | 30, 2, 8, 67 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝐴𝐷𝑋) ∈ ℝ) |
| 69 | 4, 22 | nmcl 24629 |
. . . . . 6
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉) → (𝑁‘𝐵) ∈ ℝ) |
| 70 | 21, 3, 69 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘𝐵) ∈ ℝ) |
| 71 | 14 | rphalfcld 13089 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) |
| 72 | 71, 27 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) ∈
ℝ+) |
| 73 | 60, 72 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 74 | 73 | rpred 13077 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 75 | 70, 74 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((𝑁‘𝐵) + 𝑇) ∈ ℝ) |
| 76 | 68, 75 | remulcld 11291 |
. . 3
⊢ (𝜑 → ((𝐴𝐷𝑋) · ((𝑁‘𝐵) + 𝑇)) ∈ ℝ) |
| 77 | 4, 22 | nmcl 24629 |
. . . . . 6
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉) → (𝑁‘𝑌) ∈ ℝ) |
| 78 | 21, 9, 77 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑁‘𝑌) ∈ ℝ) |
| 79 | 68, 78 | remulcld 11291 |
. . . 4
⊢ (𝜑 → ((𝐴𝐷𝑋) · (𝑁‘𝑌)) ∈ ℝ) |
| 80 | 5, 4, 37 | cphsubdir 25242 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝐴(-g‘𝑊)𝑋) , 𝑌) = ((𝐴 , 𝑌) − (𝑋 , 𝑌))) |
| 81 | 1, 2, 8, 9, 80 | syl13anc 1374 |
. . . . . 6
⊢ (𝜑 → ((𝐴(-g‘𝑊)𝑋) , 𝑌) = ((𝐴 , 𝑌) − (𝑋 , 𝑌))) |
| 82 | 81 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (abs‘((𝐴(-g‘𝑊)𝑋) , 𝑌)) = (abs‘((𝐴 , 𝑌) − (𝑋 , 𝑌)))) |
| 83 | 4, 37 | grpsubcl 19038 |
. . . . . . . 8
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝐴(-g‘𝑊)𝑋) ∈ 𝑉) |
| 84 | 42, 2, 8, 83 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐴(-g‘𝑊)𝑋) ∈ 𝑉) |
| 85 | 4, 5, 22 | ipcau 25272 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝐴(-g‘𝑊)𝑋) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (abs‘((𝐴(-g‘𝑊)𝑋) , 𝑌)) ≤ ((𝑁‘(𝐴(-g‘𝑊)𝑋)) · (𝑁‘𝑌))) |
| 86 | 1, 84, 9, 85 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝐴(-g‘𝑊)𝑋) , 𝑌)) ≤ ((𝑁‘(𝐴(-g‘𝑊)𝑋)) · (𝑁‘𝑌))) |
| 87 | 22, 4, 37, 31 | ngpds 24617 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝐴𝐷𝑋) = (𝑁‘(𝐴(-g‘𝑊)𝑋))) |
| 88 | 21, 2, 8, 87 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝐷𝑋) = (𝑁‘(𝐴(-g‘𝑊)𝑋))) |
| 89 | 88 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((𝐴𝐷𝑋) · (𝑁‘𝑌)) = ((𝑁‘(𝐴(-g‘𝑊)𝑋)) · (𝑁‘𝑌))) |
| 90 | 86, 89 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → (abs‘((𝐴(-g‘𝑊)𝑋) , 𝑌)) ≤ ((𝐴𝐷𝑋) · (𝑁‘𝑌))) |
| 91 | 82, 90 | eqbrtrrd 5167 |
. . . 4
⊢ (𝜑 → (abs‘((𝐴 , 𝑌) − (𝑋 , 𝑌))) ≤ ((𝐴𝐷𝑋) · (𝑁‘𝑌))) |
| 92 | 4, 31 | xmsge0 24473 |
. . . . . 6
⊢ ((𝑊 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝐴𝐷𝑋)) |
| 93 | 53, 2, 8, 92 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑋)) |
| 94 | 78, 70 | resubcld 11691 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝐵)) ∈ ℝ) |
| 95 | 4, 22, 37 | nm2dif 24638 |
. . . . . . . . 9
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑁‘𝑌) − (𝑁‘𝐵)) ≤ (𝑁‘(𝑌(-g‘𝑊)𝐵))) |
| 96 | 21, 9, 3, 95 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝐵)) ≤ (𝑁‘(𝑌(-g‘𝑊)𝐵))) |
| 97 | 22, 4, 37, 31 | ngpdsr 24618 |
. . . . . . . . 9
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐵𝐷𝑌) = (𝑁‘(𝑌(-g‘𝑊)𝐵))) |
| 98 | 21, 3, 9, 97 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝐵𝐷𝑌) = (𝑁‘(𝑌(-g‘𝑊)𝐵))) |
| 99 | 96, 98 | breqtrrd 5171 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝐵)) ≤ (𝐵𝐷𝑌)) |
| 100 | 33, 74, 59 | ltled 11409 |
. . . . . . 7
⊢ (𝜑 → (𝐵𝐷𝑌) ≤ 𝑇) |
| 101 | 94, 33, 74, 99, 100 | letrd 11418 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘𝑌) − (𝑁‘𝐵)) ≤ 𝑇) |
| 102 | 78, 70, 74 | lesubadd2d 11862 |
. . . . . 6
⊢ (𝜑 → (((𝑁‘𝑌) − (𝑁‘𝐵)) ≤ 𝑇 ↔ (𝑁‘𝑌) ≤ ((𝑁‘𝐵) + 𝑇))) |
| 103 | 101, 102 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑁‘𝑌) ≤ ((𝑁‘𝐵) + 𝑇)) |
| 104 | 78, 75, 68, 93, 103 | lemul2ad 12208 |
. . . 4
⊢ (𝜑 → ((𝐴𝐷𝑋) · (𝑁‘𝑌)) ≤ ((𝐴𝐷𝑋) · ((𝑁‘𝐵) + 𝑇))) |
| 105 | 66, 79, 76, 91, 104 | letrd 11418 |
. . 3
⊢ (𝜑 → (abs‘((𝐴 , 𝑌) − (𝑋 , 𝑌))) ≤ ((𝐴𝐷𝑋) · ((𝑁‘𝐵) + 𝑇))) |
| 106 | | ipcn.1 |
. . . . 5
⊢ (𝜑 → (𝐴𝐷𝑋) < 𝑈) |
| 107 | | ipcn.u |
. . . . 5
⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) |
| 108 | 106, 107 | breqtrdi 5184 |
. . . 4
⊢ (𝜑 → (𝐴𝐷𝑋) < ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇))) |
| 109 | | 0red 11264 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
| 110 | 4, 22 | nmge0 24630 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉) → 0 ≤ (𝑁‘𝐵)) |
| 111 | 21, 3, 110 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑁‘𝐵)) |
| 112 | 70, 73 | ltaddrpd 13110 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝐵) < ((𝑁‘𝐵) + 𝑇)) |
| 113 | 109, 70, 75, 111, 112 | lelttrd 11419 |
. . . . 5
⊢ (𝜑 → 0 < ((𝑁‘𝐵) + 𝑇)) |
| 114 | | ltmuldiv 12141 |
. . . . 5
⊢ (((𝐴𝐷𝑋) ∈ ℝ ∧ (𝑅 / 2) ∈ ℝ ∧ (((𝑁‘𝐵) + 𝑇) ∈ ℝ ∧ 0 < ((𝑁‘𝐵) + 𝑇))) → (((𝐴𝐷𝑋) · ((𝑁‘𝐵) + 𝑇)) < (𝑅 / 2) ↔ (𝐴𝐷𝑋) < ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)))) |
| 115 | 68, 35, 75, 113, 114 | syl112anc 1376 |
. . . 4
⊢ (𝜑 → (((𝐴𝐷𝑋) · ((𝑁‘𝐵) + 𝑇)) < (𝑅 / 2) ↔ (𝐴𝐷𝑋) < ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)))) |
| 116 | 108, 115 | mpbird 257 |
. . 3
⊢ (𝜑 → ((𝐴𝐷𝑋) · ((𝑁‘𝐵) + 𝑇)) < (𝑅 / 2)) |
| 117 | 66, 76, 35, 105, 116 | lelttrd 11419 |
. 2
⊢ (𝜑 → (abs‘((𝐴 , 𝑌) − (𝑋 , 𝑌))) < (𝑅 / 2)) |
| 118 | 7, 11, 13, 15, 64, 117 | abs3lemd 15500 |
1
⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝑋 , 𝑌))) < 𝑅) |