| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | minveco.u | . . . . . 6
⊢ (𝜑 → 𝑈 ∈
CPreHilOLD) | 
| 2 |  | phnv 30834 | . . . . . 6
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) | 
| 3 |  | minveco.x | . . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 4 |  | minveco.d | . . . . . . 7
⊢ 𝐷 = (IndMet‘𝑈) | 
| 5 | 3, 4 | imsxmet 30712 | . . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋)) | 
| 6 | 1, 2, 5 | 3syl 18 | . . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | 
| 7 |  | minveco.j | . . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 8 | 7 | methaus 24534 | . . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) | 
| 9 |  | lmfun 23390 | . . . . 5
⊢ (𝐽 ∈ Haus → Fun
(⇝𝑡‘𝐽)) | 
| 10 | 6, 8, 9 | 3syl 18 | . . . 4
⊢ (𝜑 → Fun
(⇝𝑡‘𝐽)) | 
| 11 |  | minveco.m | . . . . . 6
⊢ 𝑀 = ( −𝑣
‘𝑈) | 
| 12 |  | minveco.n | . . . . . 6
⊢ 𝑁 =
(normCV‘𝑈) | 
| 13 |  | minveco.y | . . . . . 6
⊢ 𝑌 = (BaseSet‘𝑊) | 
| 14 |  | minveco.w | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) | 
| 15 |  | minveco.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 16 |  | minveco.r | . . . . . 6
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) | 
| 17 |  | minveco.s | . . . . . 6
⊢ 𝑆 = inf(𝑅, ℝ, < ) | 
| 18 |  | minveco.f | . . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶𝑌) | 
| 19 |  | minveco.1 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) | 
| 20 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4a 30897 | . . . . 5
⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) | 
| 21 |  | eqid 2736 | . . . . . . 7
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) | 
| 22 |  | nnuz 12922 | . . . . . . 7
⊢ ℕ =
(ℤ≥‘1) | 
| 23 | 13 | fvexi 6919 | . . . . . . . 8
⊢ 𝑌 ∈ V | 
| 24 | 23 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) | 
| 25 | 1, 2 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ NrmCVec) | 
| 26 | 7 | mopntop 24451 | . . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) | 
| 27 | 25, 5, 26 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 28 |  | elin 3966 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan)) | 
| 29 | 14, 28 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan)) | 
| 30 | 29 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) | 
| 31 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) | 
| 32 | 3, 13, 31 | sspba 30747 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) | 
| 33 | 25, 30, 32 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ⊆ 𝑋) | 
| 34 |  | xmetres2 24372 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) | 
| 35 | 6, 33, 34 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) | 
| 36 |  | eqid 2736 | . . . . . . . . . 10
⊢
(MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) | 
| 37 | 36 | mopntopon 24450 | . . . . . . . . 9
⊢ ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌)) | 
| 38 | 35, 37 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌)) | 
| 39 |  | lmcl 23306 | . . . . . . . 8
⊢
(((MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) →
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌) | 
| 40 | 38, 20, 39 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 →
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌) | 
| 41 |  | 1zzd 12650 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) | 
| 42 | 21, 22, 24, 27, 40, 41, 18 | lmss 23307 | . . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽 ↾t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) | 
| 43 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌)) | 
| 44 | 43, 7, 36 | metrest 24538 | . . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) | 
| 45 | 6, 33, 44 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) | 
| 46 | 45 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 →
(⇝𝑡‘(𝐽 ↾t 𝑌)) =
(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))) | 
| 47 | 46 | breqd 5153 | . . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘(𝐽 ↾t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) | 
| 48 | 42, 47 | bitrd 279 | . . . . 5
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) | 
| 49 | 20, 48 | mpbird 257 | . . . 4
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) | 
| 50 |  | funbrfv 6956 | . . . 4
⊢ (Fun
(⇝𝑡‘𝐽) → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡‘𝐽)‘𝐹) =
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) | 
| 51 | 10, 49, 50 | sylc 65 | . . 3
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) =
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) | 
| 52 | 51, 40 | eqeltrd 2840 | . 2
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑌) | 
| 53 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4b 30898 | . . . . . 6
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) | 
| 54 | 3, 11, 12, 4 | imsdval 30706 | . . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) | 
| 55 | 25, 15, 53, 54 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) | 
| 56 | 55 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) | 
| 57 | 3, 4 | imsmet 30711 | . . . . . . . 8
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋)) | 
| 58 | 1, 2, 57 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 59 |  | metcl 24343 | . . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) | 
| 60 | 58, 15, 53, 59 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) | 
| 61 | 60 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) | 
| 62 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4c 30899 | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 63 | 62 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) | 
| 64 | 25 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmCVec) | 
| 65 | 15 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) | 
| 66 | 33 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) | 
| 67 | 3, 11 | nvmcl 30666 | . . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝑀𝑦) ∈ 𝑋) | 
| 68 | 64, 65, 66, 67 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝑀𝑦) ∈ 𝑋) | 
| 69 | 3, 12 | nvcl 30681 | . . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) | 
| 70 | 64, 68, 69 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) | 
| 71 | 62, 60 | ltnled 11409 | . . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) | 
| 72 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(ℤ≥‘((⌊‘𝑇) + 1)) =
(ℤ≥‘((⌊‘𝑇) + 1)) | 
| 73 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 74 |  | minveco.t | . . . . . . . . . . . . . . 15
⊢ 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) | 
| 75 | 60, 62 | readdcld 11291 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ) | 
| 76 | 75 | rehalfcld 12515 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) | 
| 77 | 76 | resqcld 14166 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈
ℝ) | 
| 78 | 62 | resqcld 14166 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) | 
| 79 | 77, 78 | resubcld 11692 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) | 
| 81 | 62, 60, 62 | ltadd1d 11857 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) | 
| 82 | 62 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑆 ∈ ℂ) | 
| 83 | 82 | 2timesd 12511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆)) | 
| 84 | 83 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) | 
| 85 |  | 2re 12341 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ | 
| 86 |  | 2pos 12370 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 | 
| 87 | 85, 86 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 88 | 87 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) | 
| 89 |  | ltmuldiv2 12143 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 90 | 62, 75, 88, 89 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 91 | 81, 84, 90 | 3bitr2d 307 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 92 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16 | minvecolem1 30894 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 93 | 92 | simp3d 1144 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) | 
| 94 | 92 | simp1d 1142 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ⊆ ℝ) | 
| 95 | 92 | simp2d 1143 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ≠ ∅) | 
| 96 |  | 0re 11264 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ | 
| 97 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) | 
| 98 | 97 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 99 | 98 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) | 
| 100 | 96, 93, 99 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) | 
| 101 | 96 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ∈
ℝ) | 
| 102 |  | infregelb 12253 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) | 
| 103 | 94, 95, 100, 101, 102 | syl31anc 1374 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 104 | 93, 103 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, <
)) | 
| 105 | 104, 17 | breqtrrdi 5184 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ 𝑆) | 
| 106 |  | metge0 24356 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) | 
| 107 | 58, 15, 53, 106 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) | 
| 108 | 60, 62, 107, 105 | addge0d 11840 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆)) | 
| 109 |  | divge0 12138 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) | 
| 110 | 75, 108, 88, 109 | syl21anc 837 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) | 
| 111 | 62, 76, 105, 110 | lt2sqd 14296 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2))) | 
| 112 | 78, 77 | posdifd 11851 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) | 
| 113 | 91, 111, 112 | 3bitrd 305 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) | 
| 114 | 113 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) | 
| 115 | 80, 114 | elrpd 13075 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈
ℝ+) | 
| 116 | 115 | rpreccld 13088 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈
ℝ+) | 
| 117 | 74, 116 | eqeltrid 2844 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝑇 ∈
ℝ+) | 
| 118 | 117 | rprege0d 13085 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇)) | 
| 119 |  | flge0nn0 13861 | . . . . . . . . . . . . 13
⊢ ((𝑇 ∈ ℝ ∧ 0 ≤
𝑇) →
(⌊‘𝑇) ∈
ℕ0) | 
| 120 |  | nn0p1nn 12567 | . . . . . . . . . . . . 13
⊢
((⌊‘𝑇)
∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ) | 
| 121 | 118, 119,
120 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ) | 
| 122 | 121 | nnzd 12642 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ) | 
| 123 | 49, 51 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐹)) | 
| 124 | 123 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐹)) | 
| 125 | 15 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐴 ∈ 𝑋) | 
| 126 | 76 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) | 
| 127 | 126 | rexrd 11312 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈
ℝ*) | 
| 128 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝜑) | 
| 129 |  | eluznn 12961 | . . . . . . . . . . . . . . . 16
⊢
((((⌊‘𝑇)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ) | 
| 130 | 121, 129 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ) | 
| 131 | 58 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋)) | 
| 132 | 15 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝑋) | 
| 133 | 18, 33 | fssd 6752 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) | 
| 134 | 133 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑋) | 
| 135 |  | metcl 24343 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) | 
| 136 | 131, 132,
134, 135 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) | 
| 137 | 128, 130,
136 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) | 
| 138 | 137 | resqcld 14166 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ∈ ℝ) | 
| 139 | 62 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ) | 
| 140 | 139 | resqcld 14166 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ) | 
| 141 | 130 | nnrecred 12318 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ) | 
| 142 | 140, 141 | readdcld 11291 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ) | 
| 143 | 77 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈
ℝ) | 
| 144 | 128, 130,
19 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) | 
| 145 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ∈
ℝ+) | 
| 146 | 145 | rpred 13078 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ) | 
| 147 |  | reflcl 13837 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ →
(⌊‘𝑇) ∈
ℝ) | 
| 148 |  | peano2re 11435 | . . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑇)
∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ) | 
| 149 | 146, 147,
148 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈
ℝ) | 
| 150 | 130 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ) | 
| 151 |  | fllep1 13842 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1)) | 
| 152 | 146, 151 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1)) | 
| 153 |  | eluzle 12892 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛) | 
| 154 | 153 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛) | 
| 155 | 146, 149,
150, 152, 154 | letrd 11419 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ≤ 𝑛) | 
| 156 | 74, 155 | eqbrtrrid 5178 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛) | 
| 157 |  | 1red 11263 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 1 ∈
ℝ) | 
| 158 | 79 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) | 
| 159 | 114 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) | 
| 160 | 130 | nngt0d 12316 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 < 𝑛) | 
| 161 |  | lediv23 12161 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ ((((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ ∧ 0 <
(((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) | 
| 162 | 157, 158,
159, 150, 160, 161 | syl122anc 1380 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) | 
| 163 | 156, 162 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) | 
| 164 | 140, 141,
143 | leaddsub2d 11866 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) | 
| 165 | 163, 164 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2)) | 
| 166 | 138, 142,
143, 144, 165 | letrd 11419 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2)) | 
| 167 | 76 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) | 
| 168 |  | metge0 24356 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) | 
| 169 | 131, 132,
134, 168 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) | 
| 170 | 128, 130,
169 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) | 
| 171 | 110 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) | 
| 172 | 137, 167,
170, 171 | le2sqd 14297 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2))) | 
| 173 | 166, 172 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹‘𝑛)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) | 
| 174 | 72, 7, 73, 122, 124, 125, 127, 173 | lmle 25336 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) | 
| 175 | 60, 62, 60 | leadd2d 11859 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) | 
| 176 | 60 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℂ) | 
| 177 | 176 | 2timesd 12511 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)))) | 
| 178 | 177 | breq1d 5152 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) | 
| 179 |  | lemuldiv2 12150 | . . . . . . . . . . . . . 14
⊢ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 180 | 87, 179 | mp3an3 1451 | . . . . . . . . . . . . 13
⊢ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 181 | 60, 75, 180 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 182 | 175, 178,
181 | 3bitr2d 307 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) | 
| 183 | 182 | biimpar 477 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) | 
| 184 | 174, 183 | syldan 591 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) | 
| 185 | 184 | ex 412 | . . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) | 
| 186 | 71, 185 | sylbird 260 | . . . . . . 7
⊢ (𝜑 → (¬ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) | 
| 187 | 186 | pm2.18d 127 | . . . . . 6
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) | 
| 188 | 187 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) | 
| 189 | 94 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ) | 
| 190 | 100 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) | 
| 191 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) | 
| 192 |  | fvex 6918 | . . . . . . . . 9
⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V | 
| 193 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) | 
| 194 | 193 | elrnmpt1 5970 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))) | 
| 195 | 191, 192,
194 | sylancl 586 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))) | 
| 196 | 195, 16 | eleqtrrdi 2851 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) | 
| 197 |  | infrelb 12254 | . . . . . . 7
⊢ ((𝑅 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 198 | 189, 190,
196, 197 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 199 | 17, 198 | eqbrtrid 5177 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 200 | 61, 63, 70, 188, 199 | letrd 11419 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 201 | 56, 200 | eqbrtrrd 5166 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 202 | 201 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 203 |  | oveq2 7440 | . . . . . 6
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) | 
| 204 | 203 | fveq2d 6909 | . . . . 5
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) | 
| 205 | 204 | breq1d 5152 | . . . 4
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 206 | 205 | ralbidv 3177 | . . 3
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 207 | 206 | rspcev 3621 | . 2
⊢
((((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 208 | 52, 202, 207 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |