Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈
CPreHilOLD) |
2 | | phnv 27053 |
. . . . . 6
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
3 | | minveco.x |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
4 | | minveco.d |
. . . . . . 7
⊢ 𝐷 = (IndMet‘𝑈) |
5 | 3, 4 | imsxmet 26931 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋)) |
6 | 1, 2, 5 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
7 | | minveco.j |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
8 | 7 | methaus 22135 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) |
9 | | lmfun 20995 |
. . . . 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 27117 |
. . . . 5
⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) |
21 | | eqid 2610 |
. . . . . . 7
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) |
22 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
23 | | fvex 6113 |
. . . . . . . . 9
⊢
(BaseSet‘𝑊)
∈ V |
24 | 13, 23 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑌 ∈ V |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
26 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ NrmCVec) |
27 | 7 | mopntop 22055 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
28 | 26, 5, 27 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) |
29 | | elin 3758 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan)) |
30 | 14, 29 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan)) |
31 | 30 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) |
32 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
33 | 3, 13, 32 | sspba 26966 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) |
34 | 26, 31, 33 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
35 | | xmetres2 21976 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
36 | 6, 34, 35 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
37 | | eqid 2610 |
. . . . . . . . . 10
⊢
(MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) |
38 | 37 | mopntopon 22054 |
. . . . . . . . 9
⊢ ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌)) |
39 | 36, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌)) |
40 | | lmcl 20911 |
. . . . . . . 8
⊢
(((MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) →
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌) |
41 | 39, 20, 40 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 →
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌) |
42 | | 1zzd 11285 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
43 | 21, 22, 25, 28, 41, 42, 18 | lmss 20912 |
. . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽 ↾t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
44 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌)) |
45 | 44, 7, 37 | metrest 22139 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
46 | 6, 34, 45 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
47 | 46 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 →
(⇝𝑡‘(𝐽 ↾t 𝑌)) =
(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))) |
48 | 47 | breqd 4594 |
. . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘(𝐽 ↾t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
49 | 43, 48 | bitrd 267 |
. . . . 5
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
50 | 20, 49 | mpbird 246 |
. . . 4
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) |
51 | | funbrfv 6144 |
. . . 4
⊢ (Fun
(⇝𝑡‘𝐽) → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡‘𝐽)‘𝐹) =
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
52 | 10, 50, 51 | sylc 63 |
. . 3
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) =
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) |
53 | 52, 41 | eqeltrd 2688 |
. 2
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑌) |
54 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4b 27118 |
. . . . . 6
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) |
55 | 3, 11, 12, 4 | imsdval 26925 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
56 | 26, 15, 54, 55 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
57 | 56 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
58 | 3, 4 | imsmet 26930 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋)) |
59 | 1, 2, 58 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
60 | | metcl 21947 |
. . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) |
61 | 59, 15, 54, 60 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) |
62 | 61 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) |
63 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4c 27119 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) |
64 | 63 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) |
65 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmCVec) |
66 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
67 | 34 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
68 | 3, 11 | nvmcl 26885 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝑀𝑦) ∈ 𝑋) |
69 | 65, 66, 67, 68 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝑀𝑦) ∈ 𝑋) |
70 | 3, 12 | nvcl 26900 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) |
71 | 65, 69, 70 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) |
72 | 63, 61 | ltnled 10063 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) |
73 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(ℤ≥‘((⌊‘𝑇) + 1)) =
(ℤ≥‘((⌊‘𝑇) + 1)) |
74 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋)) |
75 | | minveco.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
76 | 61, 63 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ) |
77 | 76 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) |
78 | 77 | resqcld 12897 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈
ℝ) |
79 | 63 | resqcld 12897 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) |
80 | 78, 79 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
82 | 63, 61, 63 | ltadd1d 10499 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
83 | 63 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑆 ∈ ℂ) |
84 | 83 | 2timesd 11152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆)) |
85 | 84 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
86 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
87 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
88 | 86, 87 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
90 | | ltmuldiv2 10776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
91 | 63, 76, 89, 90 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
92 | 82, 85, 91 | 3bitr2d 295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
93 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16 | minvecolem1 27114 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
94 | 93 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
95 | 93 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ⊆ ℝ) |
96 | 93 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ≠ ∅) |
97 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ |
98 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
99 | 98 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
100 | 99 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
101 | 97, 94, 100 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
102 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ∈
ℝ) |
103 | | infregelb 10884 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
104 | 95, 96, 101, 102, 103 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
105 | 94, 104 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, <
)) |
106 | 105, 17 | syl6breqr 4625 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ 𝑆) |
107 | | metge0 21960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) |
108 | 59, 15, 54, 107 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) |
109 | 61, 63, 108, 106 | addge0d 10482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆)) |
110 | | divge0 10771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
111 | 76, 109, 89, 110 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
112 | 63, 77, 106, 111 | lt2sqd 12905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2))) |
113 | 79, 78 | posdifd 10493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
114 | 92, 112, 113 | 3bitrd 293 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
115 | 114 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
116 | 81, 115 | elrpd 11745 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈
ℝ+) |
117 | 116 | rpreccld 11758 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈
ℝ+) |
118 | 75, 117 | syl5eqel 2692 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝑇 ∈
ℝ+) |
119 | 118 | rprege0d 11755 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇)) |
120 | | flge0nn0 12483 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ ℝ ∧ 0 ≤
𝑇) →
(⌊‘𝑇) ∈
ℕ0) |
121 | | nn0p1nn 11209 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝑇)
∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ) |
122 | 119, 120,
121 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ) |
123 | 122 | nnzd 11357 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ) |
124 | 50, 52 | breqtrrd 4611 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐹)) |
125 | 124 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐹)) |
126 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐴 ∈ 𝑋) |
127 | 77 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) |
128 | 127 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈
ℝ*) |
129 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝜑) |
130 | | eluznn 11634 |
. . . . . . . . . . . . . . . 16
⊢
((((⌊‘𝑇)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ) |
131 | 122, 130 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ) |
132 | 59 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋)) |
133 | 15 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝑋) |
134 | 18, 34 | fssd 5970 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
135 | 134 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑋) |
136 | | metcl 21947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) |
137 | 132, 133,
135, 136 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) |
138 | 129, 131,
137 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) |
139 | 138 | resqcld 12897 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ∈ ℝ) |
140 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ) |
141 | 140 | resqcld 12897 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ) |
142 | 131 | nnrecred 10943 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ) |
143 | 141, 142 | readdcld 9948 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ) |
144 | 78 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈
ℝ) |
145 | 129, 131,
19 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) |
146 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ∈
ℝ+) |
147 | 146 | rpred 11748 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ) |
148 | | reflcl 12459 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ →
(⌊‘𝑇) ∈
ℝ) |
149 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑇)
∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ) |
150 | 147, 148,
149 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈
ℝ) |
151 | 131 | nnred 10912 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ) |
152 | | fllep1 12464 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1)) |
153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1)) |
154 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛) |
156 | 147, 150,
151, 153, 155 | letrd 10073 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ≤ 𝑛) |
157 | 75, 156 | syl5eqbrr 4619 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛) |
158 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 1 ∈
ℝ) |
159 | 80 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
160 | 115 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
161 | 131 | nngt0d 10941 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 < 𝑛) |
162 | | lediv23 10794 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ ((((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ ∧ 0 <
(((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
163 | 158, 159,
160, 151, 161, 162 | syl122anc 1327 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
164 | 157, 163 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
165 | 141, 142,
144 | leaddsub2d 10508 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
166 | 164, 165 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2)) |
167 | 139, 143,
144, 145, 166 | letrd 10073 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2)) |
168 | 77 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) |
169 | | metge0 21960 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) |
170 | 132, 133,
135, 169 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) |
171 | 129, 131,
170 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) |
172 | 111 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
173 | 138, 168,
171, 172 | le2sqd 12906 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2))) |
174 | 167, 173 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹‘𝑛)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
175 | 73, 7, 74, 123, 125, 126, 128, 174 | lmle 22907 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
176 | 61, 63, 61 | leadd2d 10501 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
177 | 61 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℂ) |
178 | 177 | 2timesd 11152 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)))) |
179 | 178 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
180 | | lemuldiv2 10783 |
. . . . . . . . . . . . . 14
⊢ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
181 | 88, 180 | mp3an3 1405 |
. . . . . . . . . . . . 13
⊢ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
182 | 61, 76, 181 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
183 | 176, 179,
182 | 3bitr2d 295 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
184 | 183 | biimpar 501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
185 | 175, 184 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
186 | 185 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) |
187 | 72, 186 | sylbird 249 |
. . . . . . 7
⊢ (𝜑 → (¬ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) |
188 | 187 | pm2.18d 123 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
189 | 188 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
190 | 95 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ) |
191 | 101 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
192 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
193 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V |
194 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
195 | 194 | elrnmpt1 5295 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))) |
196 | 192, 193,
195 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))) |
197 | 196, 16 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) |
198 | | infrelb 10885 |
. . . . . . 7
⊢ ((𝑅 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦))) |
199 | 190, 191,
197, 198 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦))) |
200 | 17, 199 | syl5eqbr 4618 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦))) |
201 | 62, 64, 71, 189, 200 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
202 | 57, 201 | eqbrtrrd 4607 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
203 | 202 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
204 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) |
205 | 204 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
206 | 205 | breq1d 4593 |
. . . 4
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
207 | 206 | ralbidv 2969 |
. . 3
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
208 | 207 | rspcev 3282 |
. 2
⊢
((((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
209 | 53, 203, 208 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |