Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈
CPreHilOLD) |
2 | | phnv 27669 |
. . . . . 6
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
3 | | minveco.x |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
4 | | minveco.d |
. . . . . . 7
⊢ 𝐷 = (IndMet‘𝑈) |
5 | 3, 4 | imsxmet 27547 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋)) |
6 | 1, 2, 5 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
7 | | minveco.j |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
8 | 7 | methaus 22325 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) |
9 | | lmfun 21185 |
. . . . 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 27733 |
. . . . 5
⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) |
21 | | eqid 2622 |
. . . . . . 7
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) |
22 | | nnuz 11723 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
23 | | fvex 6201 |
. . . . . . . . 9
⊢
(BaseSet‘𝑊)
∈ V |
24 | 13, 23 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝑌 ∈ V |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
26 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ NrmCVec) |
27 | 7 | mopntop 22245 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
28 | 26, 5, 27 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) |
29 | | elin 3796 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan)) |
30 | 14, 29 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan)) |
31 | 30 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) |
32 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
33 | 3, 13, 32 | sspba 27582 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) |
34 | 26, 31, 33 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
35 | | xmetres2 22166 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
36 | 6, 34, 35 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
37 | | eqid 2622 |
. . . . . . . . . 10
⊢
(MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) |
38 | 37 | mopntopon 22244 |
. . . . . . . . 9
⊢ ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌)) |
39 | 36, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌)) |
40 | | lmcl 21101 |
. . . . . . . 8
⊢
(((MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) →
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌) |
41 | 39, 20, 40 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 →
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌) |
42 | | 1zzd 11408 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
43 | 21, 22, 25, 28, 41, 42, 18 | lmss 21102 |
. . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽 ↾t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
44 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌)) |
45 | 44, 7, 37 | metrest 22329 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
46 | 6, 34, 45 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
47 | 46 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 →
(⇝𝑡‘(𝐽 ↾t 𝑌)) =
(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))) |
48 | 47 | breqd 4664 |
. . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘(𝐽 ↾t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
49 | 43, 48 | bitrd 268 |
. . . . 5
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
50 | 20, 49 | mpbird 247 |
. . . 4
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) |
51 | | funbrfv 6234 |
. . . 4
⊢ (Fun
(⇝𝑡‘𝐽) → (𝐹(⇝𝑡‘𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡‘𝐽)‘𝐹) =
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))) |
52 | 10, 50, 51 | sylc 65 |
. . 3
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) =
((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) |
53 | 52, 41 | eqeltrd 2701 |
. 2
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑌) |
54 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4b 27734 |
. . . . . 6
⊢ (𝜑 →
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) |
55 | 3, 11, 12, 4 | imsdval 27541 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
56 | 26, 15, 54, 55 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
57 | 56 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
58 | 3, 4 | imsmet 27546 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋)) |
59 | 1, 2, 58 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
60 | | metcl 22137 |
. . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) |
61 | 59, 15, 54, 60 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) |
62 | 61 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ) |
63 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4c 27735 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) |
64 | 63 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) |
65 | 26 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmCVec) |
66 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
67 | 34 | sselda 3603 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
68 | 3, 11 | nvmcl 27501 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝑀𝑦) ∈ 𝑋) |
69 | 65, 66, 67, 68 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝑀𝑦) ∈ 𝑋) |
70 | 3, 12 | nvcl 27516 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) |
71 | 65, 69, 70 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) |
72 | 63, 61 | ltnled 10184 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) |
73 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(ℤ≥‘((⌊‘𝑇) + 1)) =
(ℤ≥‘((⌊‘𝑇) + 1)) |
74 | 6 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋)) |
75 | | minveco.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
76 | 61, 63 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ) |
77 | 76 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) |
78 | 77 | resqcld 13035 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈
ℝ) |
79 | 63 | resqcld 13035 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) |
80 | 78, 79 | resubcld 10458 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
82 | 63, 61, 63 | ltadd1d 10620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
83 | 63 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑆 ∈ ℂ) |
84 | 83 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆)) |
85 | 84 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
86 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
87 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
88 | 86, 87 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
90 | | ltmuldiv2 10897 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
91 | 63, 76, 89, 90 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
92 | 82, 85, 91 | 3bitr2d 296 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
93 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16 | minvecolem1 27730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
94 | 93 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
95 | 93 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ⊆ ℝ) |
96 | 93 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ≠ ∅) |
97 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ |
98 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
99 | 98 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
100 | 99 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
101 | 97, 94, 100 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
102 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ∈
ℝ) |
103 | | infregelb 11007 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
104 | 95, 96, 101, 102, 103 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
105 | 94, 104 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, <
)) |
106 | 105, 17 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ 𝑆) |
107 | | metge0 22150 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧
((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) |
108 | 59, 15, 54, 107 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) |
109 | 61, 63, 108, 106 | addge0d 10603 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆)) |
110 | | divge0 10892 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
111 | 76, 109, 89, 110 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
112 | 63, 77, 106, 111 | lt2sqd 13043 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2))) |
113 | 79, 78 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
114 | 92, 112, 113 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
115 | 114 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
116 | 81, 115 | elrpd 11869 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈
ℝ+) |
117 | 116 | rpreccld 11882 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈
ℝ+) |
118 | 75, 117 | syl5eqel 2705 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝑇 ∈
ℝ+) |
119 | 118 | rprege0d 11879 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇)) |
120 | | flge0nn0 12621 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ ℝ ∧ 0 ≤
𝑇) →
(⌊‘𝑇) ∈
ℕ0) |
121 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝑇)
∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ) |
122 | 119, 120,
121 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ) |
123 | 122 | nnzd 11481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ) |
124 | 50, 52 | breqtrrd 4681 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐹)) |
125 | 124 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐹(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐹)) |
126 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → 𝐴 ∈ 𝑋) |
127 | 77 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) |
128 | 127 | rexrd 10089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈
ℝ*) |
129 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝜑) |
130 | | eluznn 11758 |
. . . . . . . . . . . . . . . 16
⊢
((((⌊‘𝑇)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ) |
131 | 122, 130 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ) |
132 | 59 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋)) |
133 | 15 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝑋) |
134 | 18, 34 | fssd 6057 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
135 | 134 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑋) |
136 | | metcl 22137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) |
137 | 132, 133,
135, 136 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) |
138 | 129, 131,
137 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹‘𝑛)) ∈ ℝ) |
139 | 138 | resqcld 13035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ∈ ℝ) |
140 | 63 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ) |
141 | 140 | resqcld 13035 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ) |
142 | 131 | nnrecred 11066 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ) |
143 | 141, 142 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ) |
144 | 78 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈
ℝ) |
145 | 129, 131,
19 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) |
146 | 118 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ∈
ℝ+) |
147 | 146 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ) |
148 | | reflcl 12597 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ →
(⌊‘𝑇) ∈
ℝ) |
149 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑇)
∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ) |
150 | 147, 148,
149 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈
ℝ) |
151 | 131 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ) |
152 | | fllep1 12602 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1)) |
153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1)) |
154 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛) |
156 | 147, 150,
151, 153, 155 | letrd 10194 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 𝑇 ≤ 𝑛) |
157 | 75, 156 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛) |
158 | | 1red 10055 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 1 ∈
ℝ) |
159 | 80 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
160 | 115 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
161 | 131 | nngt0d 11064 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 < 𝑛) |
162 | | lediv23 10915 |
. . . . . . . . . . . . . . . 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 1335 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
164 | 157, 163 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
165 | 141, 142,
144 | leaddsub2d 10629 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
166 | 164, 165 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2)) |
167 | 139, 143,
144, 145, 166 | letrd 10194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2)) |
168 | 77 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ) |
169 | | metge0 22150 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) |
170 | 132, 133,
135, 169 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) |
171 | 129, 131,
170 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹‘𝑛))) |
172 | 111 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
173 | 138, 168,
171, 172 | le2sqd 13044 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹‘𝑛)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2))) |
174 | 167, 173 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ∧ 𝑛 ∈
(ℤ≥‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹‘𝑛)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
175 | 73, 7, 74, 123, 125, 126, 128, 174 | lmle 23099 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) |
176 | 61, 63, 61 | leadd2d 10622 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
177 | 61 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℂ) |
178 | 177 | 2timesd 11275 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)))) |
179 | 178 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆))) |
180 | | lemuldiv2 10904 |
. . . . . . . . . . . . . 14
⊢ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
181 | 88, 180 | mp3an3 1413 |
. . . . . . . . . . . . 13
⊢ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
182 | 61, 76, 181 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
183 | 176, 179,
182 | 3bitr2d 296 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2))) |
184 | 183 | biimpar 502 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
185 | 175, 184 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
186 | 185 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) |
187 | 72, 186 | sylbird 250 |
. . . . . . 7
⊢ (𝜑 → (¬ (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆)) |
188 | 187 | pm2.18d 124 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
189 | 188 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ 𝑆) |
190 | 95 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ) |
191 | 101 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
192 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
193 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V |
194 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
195 | 194 | elrnmpt1 5374 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))) |
196 | 192, 193,
195 | sylancl 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))) |
197 | 196, 16 | syl6eleqr 2712 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) |
198 | | infrelb 11008 |
. . . . . . 7
⊢ ((𝑅 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦))) |
199 | 190, 191,
197, 198 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦))) |
200 | 17, 199 | syl5eqbr 4688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦))) |
201 | 62, 64, 71, 189, 200 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
202 | 57, 201 | eqbrtrrd 4677 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
203 | 202 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
204 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) |
205 | 204 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹)))) |
206 | 205 | breq1d 4663 |
. . . 4
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
207 | 206 | ralbidv 2986 |
. . 3
⊢ (𝑥 =
((⇝𝑡‘𝐽)‘𝐹) → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
208 | 207 | rspcev 3309 |
. 2
⊢
((((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((⇝𝑡‘𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
209 | 53, 203, 208 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |