Proof of Theorem ipcnlem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ipcn.t | . . . 4
⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) | 
| 2 |  | ipcn.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 3 | 2 | rphalfcld 13089 | . . . . 5
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) | 
| 4 |  | ipcn.w | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ ℂPreHil) | 
| 5 |  | cphnlm 25206 | . . . . . . . . 9
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmMod) | 
| 6 | 4, 5 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ NrmMod) | 
| 7 |  | nlmngp 24698 | . . . . . . . 8
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) | 
| 8 | 6, 7 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ NrmGrp) | 
| 9 |  | ipcn.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 10 |  | ipcn.v | . . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) | 
| 11 |  | ipcn.n | . . . . . . . 8
⊢ 𝑁 = (norm‘𝑊) | 
| 12 | 10, 11 | nmcl 24629 | . . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉) → (𝑁‘𝐴) ∈ ℝ) | 
| 13 | 8, 9, 12 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑁‘𝐴) ∈ ℝ) | 
| 14 | 10, 11 | nmge0 24630 | . . . . . . 7
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉) → 0 ≤ (𝑁‘𝐴)) | 
| 15 | 8, 9, 14 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 0 ≤ (𝑁‘𝐴)) | 
| 16 | 13, 15 | ge0p1rpd 13107 | . . . . 5
⊢ (𝜑 → ((𝑁‘𝐴) + 1) ∈
ℝ+) | 
| 17 | 3, 16 | rpdivcld 13094 | . . . 4
⊢ (𝜑 → ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) ∈
ℝ+) | 
| 18 | 1, 17 | eqeltrid 2845 | . . 3
⊢ (𝜑 → 𝑇 ∈
ℝ+) | 
| 19 |  | ipcn.u | . . . 4
⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) | 
| 20 |  | ipcn.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑉) | 
| 21 | 10, 11 | nmcl 24629 | . . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉) → (𝑁‘𝐵) ∈ ℝ) | 
| 22 | 8, 20, 21 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑁‘𝐵) ∈ ℝ) | 
| 23 | 18 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 24 | 22, 23 | readdcld 11290 | . . . . . 6
⊢ (𝜑 → ((𝑁‘𝐵) + 𝑇) ∈ ℝ) | 
| 25 |  | 0red 11264 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) | 
| 26 | 10, 11 | nmge0 24630 | . . . . . . . 8
⊢ ((𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉) → 0 ≤ (𝑁‘𝐵)) | 
| 27 | 8, 20, 26 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑁‘𝐵)) | 
| 28 | 22, 18 | ltaddrpd 13110 | . . . . . . 7
⊢ (𝜑 → (𝑁‘𝐵) < ((𝑁‘𝐵) + 𝑇)) | 
| 29 | 25, 22, 24, 27, 28 | lelttrd 11419 | . . . . . 6
⊢ (𝜑 → 0 < ((𝑁‘𝐵) + 𝑇)) | 
| 30 | 24, 29 | elrpd 13074 | . . . . 5
⊢ (𝜑 → ((𝑁‘𝐵) + 𝑇) ∈
ℝ+) | 
| 31 | 3, 30 | rpdivcld 13094 | . . . 4
⊢ (𝜑 → ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) ∈
ℝ+) | 
| 32 | 19, 31 | eqeltrid 2845 | . . 3
⊢ (𝜑 → 𝑈 ∈
ℝ+) | 
| 33 | 18, 32 | ifcld 4572 | . 2
⊢ (𝜑 → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈
ℝ+) | 
| 34 |  | ipcn.h | . . . . 5
⊢  , =
(·𝑖‘𝑊) | 
| 35 |  | ipcn.d | . . . . 5
⊢ 𝐷 = (dist‘𝑊) | 
| 36 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ ℂPreHil) | 
| 37 | 9 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐴 ∈ 𝑉) | 
| 38 | 20 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝐵 ∈ 𝑉) | 
| 39 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑅 ∈
ℝ+) | 
| 40 |  | simprll 779 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑥 ∈ 𝑉) | 
| 41 |  | simprlr 780 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑦 ∈ 𝑉) | 
| 42 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ NrmGrp) | 
| 43 |  | ngpms 24613 | . . . . . . . 8
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp) | 
| 44 | 42, 43 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ MetSp) | 
| 45 | 10, 35 | mscl 24471 | . . . . . . 7
⊢ ((𝑊 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝐴𝐷𝑥) ∈ ℝ) | 
| 46 | 44, 37, 40, 45 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐴𝐷𝑥) ∈ ℝ) | 
| 47 | 33 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈
ℝ+) | 
| 48 | 47 | rpred 13077 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈ ℝ) | 
| 49 | 32 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ ℝ) | 
| 50 | 49 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑈 ∈ ℝ) | 
| 51 |  | simprrl 781 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) | 
| 52 | 23 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑇 ∈ ℝ) | 
| 53 |  | min2 13232 | . . . . . . 7
⊢ ((𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑈) | 
| 54 | 52, 50, 53 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑈) | 
| 55 | 46, 48, 50, 51, 54 | ltletrd 11421 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐴𝐷𝑥) < 𝑈) | 
| 56 | 8, 43 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ MetSp) | 
| 57 | 56 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → 𝑊 ∈ MetSp) | 
| 58 | 10, 35 | mscl 24471 | . . . . . . 7
⊢ ((𝑊 ∈ MetSp ∧ 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝐵𝐷𝑦) ∈ ℝ) | 
| 59 | 57, 38, 41, 58 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐷𝑦) ∈ ℝ) | 
| 60 |  | simprrr 782 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) | 
| 61 |  | min1 13231 | . . . . . . 7
⊢ ((𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑇) | 
| 62 | 52, 50, 61 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ≤ 𝑇) | 
| 63 | 59, 48, 52, 60, 62 | ltletrd 11421 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (𝐵𝐷𝑦) < 𝑇) | 
| 64 | 10, 34, 35, 11, 1, 19, 36, 37, 38, 39, 40, 41, 55, 63 | ipcnlem2 25278 | . . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅) | 
| 65 | 64 | expr 456 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) | 
| 66 | 65 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) | 
| 67 |  | breq2 5147 | . . . . . 6
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((𝐴𝐷𝑥) < 𝑟 ↔ (𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈))) | 
| 68 |  | breq2 5147 | . . . . . 6
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((𝐵𝐷𝑦) < 𝑟 ↔ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈))) | 
| 69 | 67, 68 | anbi12d 632 | . . . . 5
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) ↔ ((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)))) | 
| 70 | 69 | imbi1d 341 | . . . 4
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → ((((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅) ↔ (((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅))) | 
| 71 | 70 | 2ralbidv 3221 | . . 3
⊢ (𝑟 = if(𝑇 ≤ 𝑈, 𝑇, 𝑈) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅))) | 
| 72 | 71 | rspcev 3622 | . 2
⊢
((if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∈ ℝ+ ∧
∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈) ∧ (𝐵𝐷𝑦) < if(𝑇 ≤ 𝑈, 𝑇, 𝑈)) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) | 
| 73 | 33, 66, 72 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) |