MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minveclem4 Structured version   Visualization version   GIF version

Theorem minveclem4 25180
Description: Lemma for minvec 25184. The convergent point of the Cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in π‘Œ. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
Hypotheses
Ref Expression
minvec.x 𝑋 = (Baseβ€˜π‘ˆ)
minvec.m βˆ’ = (-gβ€˜π‘ˆ)
minvec.n 𝑁 = (normβ€˜π‘ˆ)
minvec.u (πœ‘ β†’ π‘ˆ ∈ β„‚PreHil)
minvec.y (πœ‘ β†’ π‘Œ ∈ (LSubSpβ€˜π‘ˆ))
minvec.w (πœ‘ β†’ (π‘ˆ β†Ύs π‘Œ) ∈ CMetSp)
minvec.a (πœ‘ β†’ 𝐴 ∈ 𝑋)
minvec.j 𝐽 = (TopOpenβ€˜π‘ˆ)
minvec.r 𝑅 = ran (𝑦 ∈ π‘Œ ↦ (π‘β€˜(𝐴 βˆ’ 𝑦)))
minvec.s 𝑆 = inf(𝑅, ℝ, < )
minvec.d 𝐷 = ((distβ€˜π‘ˆ) β†Ύ (𝑋 Γ— 𝑋))
minvec.f 𝐹 = ran (π‘Ÿ ∈ ℝ+ ↦ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)})
minvec.p 𝑃 = βˆͺ (𝐽 fLim (𝑋filGen𝐹))
minvec.t 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2))
Assertion
Ref Expression
minveclem4 (πœ‘ β†’ βˆƒπ‘₯ ∈ π‘Œ βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ π‘₯)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
Distinct variable groups:   π‘₯,𝑦, βˆ’   π‘₯,π‘Ÿ,𝑦,𝐴   𝐽,π‘Ÿ,π‘₯,𝑦   π‘₯,𝑃,𝑦   π‘₯,𝐹,𝑦   π‘₯,𝑁,𝑦   πœ‘,π‘Ÿ,π‘₯,𝑦   π‘₯,𝑅,𝑦   π‘₯,π‘ˆ,𝑦   𝑋,π‘Ÿ,π‘₯,𝑦   π‘Œ,π‘Ÿ,π‘₯,𝑦   𝐷,π‘Ÿ,π‘₯,𝑦   𝑆,π‘Ÿ,π‘₯,𝑦   𝑇,π‘Ÿ,𝑦
Allowed substitution hints:   𝑃(π‘Ÿ)   𝑅(π‘Ÿ)   𝑇(π‘₯)   π‘ˆ(π‘Ÿ)   𝐹(π‘Ÿ)   βˆ’ (π‘Ÿ)   𝑁(π‘Ÿ)

Proof of Theorem minveclem4
Dummy variable 𝑀 is distinct from all other variables.
StepHypRef Expression
1 minvec.x . . . 4 𝑋 = (Baseβ€˜π‘ˆ)
2 minvec.m . . . 4 βˆ’ = (-gβ€˜π‘ˆ)
3 minvec.n . . . 4 𝑁 = (normβ€˜π‘ˆ)
4 minvec.u . . . 4 (πœ‘ β†’ π‘ˆ ∈ β„‚PreHil)
5 minvec.y . . . 4 (πœ‘ β†’ π‘Œ ∈ (LSubSpβ€˜π‘ˆ))
6 minvec.w . . . 4 (πœ‘ β†’ (π‘ˆ β†Ύs π‘Œ) ∈ CMetSp)
7 minvec.a . . . 4 (πœ‘ β†’ 𝐴 ∈ 𝑋)
8 minvec.j . . . 4 𝐽 = (TopOpenβ€˜π‘ˆ)
9 minvec.r . . . 4 𝑅 = ran (𝑦 ∈ π‘Œ ↦ (π‘β€˜(𝐴 βˆ’ 𝑦)))
10 minvec.s . . . 4 𝑆 = inf(𝑅, ℝ, < )
11 minvec.d . . . 4 𝐷 = ((distβ€˜π‘ˆ) β†Ύ (𝑋 Γ— 𝑋))
12 minvec.f . . . 4 𝐹 = ran (π‘Ÿ ∈ ℝ+ ↦ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)})
13 minvec.p . . . 4 𝑃 = βˆͺ (𝐽 fLim (𝑋filGen𝐹))
141, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13minveclem4a 25178 . . 3 (πœ‘ β†’ 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ π‘Œ))
1514elin2d 4198 . 2 (πœ‘ β†’ 𝑃 ∈ π‘Œ)
1611oveqi 7424 . . . . . . 7 (𝐴𝐷𝑃) = (𝐴((distβ€˜π‘ˆ) β†Ύ (𝑋 Γ— 𝑋))𝑃)
171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13minveclem4b 25179 . . . . . . . 8 (πœ‘ β†’ 𝑃 ∈ 𝑋)
187, 17ovresd 7576 . . . . . . 7 (πœ‘ β†’ (𝐴((distβ€˜π‘ˆ) β†Ύ (𝑋 Γ— 𝑋))𝑃) = (𝐴(distβ€˜π‘ˆ)𝑃))
1916, 18eqtrid 2782 . . . . . 6 (πœ‘ β†’ (𝐴𝐷𝑃) = (𝐴(distβ€˜π‘ˆ)𝑃))
20 cphngp 24921 . . . . . . . 8 (π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ NrmGrp)
214, 20syl 17 . . . . . . 7 (πœ‘ β†’ π‘ˆ ∈ NrmGrp)
22 eqid 2730 . . . . . . . 8 (distβ€˜π‘ˆ) = (distβ€˜π‘ˆ)
233, 1, 2, 22ngpds 24333 . . . . . . 7 ((π‘ˆ ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (𝐴(distβ€˜π‘ˆ)𝑃) = (π‘β€˜(𝐴 βˆ’ 𝑃)))
2421, 7, 17, 23syl3anc 1369 . . . . . 6 (πœ‘ β†’ (𝐴(distβ€˜π‘ˆ)𝑃) = (π‘β€˜(𝐴 βˆ’ 𝑃)))
2519, 24eqtrd 2770 . . . . 5 (πœ‘ β†’ (𝐴𝐷𝑃) = (π‘β€˜(𝐴 βˆ’ 𝑃)))
2625adantr 479 . . . 4 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (𝐴𝐷𝑃) = (π‘β€˜(𝐴 βˆ’ 𝑃)))
27 ngpms 24329 . . . . . . . 8 (π‘ˆ ∈ NrmGrp β†’ π‘ˆ ∈ MetSp)
281, 11msmet 24183 . . . . . . . 8 (π‘ˆ ∈ MetSp β†’ 𝐷 ∈ (Metβ€˜π‘‹))
2921, 27, 283syl 18 . . . . . . 7 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
30 metcl 24058 . . . . . . 7 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (𝐴𝐷𝑃) ∈ ℝ)
3129, 7, 17, 30syl3anc 1369 . . . . . 6 (πœ‘ β†’ (𝐴𝐷𝑃) ∈ ℝ)
3231adantr 479 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (𝐴𝐷𝑃) ∈ ℝ)
331, 2, 3, 4, 5, 6, 7, 8, 9, 10minveclem4c 25173 . . . . . 6 (πœ‘ β†’ 𝑆 ∈ ℝ)
3433adantr 479 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ 𝑆 ∈ ℝ)
3521adantr 479 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ π‘ˆ ∈ NrmGrp)
36 cphlmod 24922 . . . . . . . . 9 (π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ LMod)
374, 36syl 17 . . . . . . . 8 (πœ‘ β†’ π‘ˆ ∈ LMod)
3837adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ π‘ˆ ∈ LMod)
397adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ 𝐴 ∈ 𝑋)
40 eqid 2730 . . . . . . . . . 10 (LSubSpβ€˜π‘ˆ) = (LSubSpβ€˜π‘ˆ)
411, 40lssss 20691 . . . . . . . . 9 (π‘Œ ∈ (LSubSpβ€˜π‘ˆ) β†’ π‘Œ βŠ† 𝑋)
425, 41syl 17 . . . . . . . 8 (πœ‘ β†’ π‘Œ βŠ† 𝑋)
4342sselda 3981 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ 𝑋)
441, 2lmodvsubcl 20661 . . . . . . 7 ((π‘ˆ ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝐴 βˆ’ 𝑦) ∈ 𝑋)
4538, 39, 43, 44syl3anc 1369 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (𝐴 βˆ’ 𝑦) ∈ 𝑋)
461, 3nmcl 24345 . . . . . 6 ((π‘ˆ ∈ NrmGrp ∧ (𝐴 βˆ’ 𝑦) ∈ 𝑋) β†’ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ ℝ)
4735, 45, 46syl2anc 582 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ ℝ)
4833, 31ltnled 11365 . . . . . . . 8 (πœ‘ β†’ (𝑆 < (𝐴𝐷𝑃) ↔ Β¬ (𝐴𝐷𝑃) ≀ 𝑆))
491, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12minveclem3b 25176 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (fBasβ€˜π‘Œ))
50 fbsspw 23556 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ (fBasβ€˜π‘Œ) β†’ 𝐹 βŠ† 𝒫 π‘Œ)
5149, 50syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐹 βŠ† 𝒫 π‘Œ)
5242sspwd 4614 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝒫 π‘Œ βŠ† 𝒫 𝑋)
5351, 52sstrd 3991 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 βŠ† 𝒫 𝑋)
541fvexi 6904 . . . . . . . . . . . . . . . . . . 19 𝑋 ∈ V
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑋 ∈ V)
56 fbasweak 23589 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (fBasβ€˜π‘Œ) ∧ 𝐹 βŠ† 𝒫 𝑋 ∧ 𝑋 ∈ V) β†’ 𝐹 ∈ (fBasβ€˜π‘‹))
5749, 53, 55, 56syl3anc 1369 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ (fBasβ€˜π‘‹))
5857adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝐹 ∈ (fBasβ€˜π‘‹))
59 fgcl 23602 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (fBasβ€˜π‘‹) β†’ (𝑋filGen𝐹) ∈ (Filβ€˜π‘‹))
6058, 59syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (𝑋filGen𝐹) ∈ (Filβ€˜π‘‹))
61 ssfg 23596 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (fBasβ€˜π‘‹) β†’ 𝐹 βŠ† (𝑋filGen𝐹))
6258, 61syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝐹 βŠ† (𝑋filGen𝐹))
63 minvec.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2))
6431, 33readdcld 11247 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ)
6564rehalfcld 12463 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
6665resqcld 14094 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
6733resqcld 14094 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑆↑2) ∈ ℝ)
6866, 67resubcld 11646 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2)) ∈ ℝ)
6968adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2)) ∈ ℝ)
7033, 31, 33ltadd1d 11811 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
7133recnd 11246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑆 ∈ β„‚)
72712timesd 12459 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (2 Β· 𝑆) = (𝑆 + 𝑆))
7372breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((2 Β· 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
74 2re 12290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℝ
75 2pos 12319 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 < 2
7674, 75pm3.2i 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℝ ∧ 0 < 2)
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (2 ∈ ℝ ∧ 0 < 2))
78 ltmuldiv2 12092 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ ((2 Β· 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
7933, 64, 77, 78syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((2 Β· 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
8070, 73, 793bitr2d 306 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
811, 2, 3, 4, 5, 6, 7, 8, 9minveclem1 25172 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆ€π‘€ ∈ 𝑅 0 ≀ 𝑀))
8281simp3d 1142 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ βˆ€π‘€ ∈ 𝑅 0 ≀ 𝑀)
8381simp1d 1140 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝑅 βŠ† ℝ)
8481simp2d 1141 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝑅 β‰  βˆ…)
85 0re 11220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
86 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = 0 β†’ (π‘₯ ≀ 𝑀 ↔ 0 ≀ 𝑀))
8786ralbidv 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ = 0 β†’ (βˆ€π‘€ ∈ 𝑅 π‘₯ ≀ 𝑀 ↔ βˆ€π‘€ ∈ 𝑅 0 ≀ 𝑀))
8887rspcev 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℝ ∧ βˆ€π‘€ ∈ 𝑅 0 ≀ 𝑀) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ 𝑅 π‘₯ ≀ 𝑀)
8985, 82, 88sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ 𝑅 π‘₯ ≀ 𝑀)
9085a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 0 ∈ ℝ)
91 infregelb 12202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ 𝑅 π‘₯ ≀ 𝑀) ∧ 0 ∈ ℝ) β†’ (0 ≀ inf(𝑅, ℝ, < ) ↔ βˆ€π‘€ ∈ 𝑅 0 ≀ 𝑀))
9283, 84, 89, 90, 91syl31anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (0 ≀ inf(𝑅, ℝ, < ) ↔ βˆ€π‘€ ∈ 𝑅 0 ≀ 𝑀))
9382, 92mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 0 ≀ inf(𝑅, ℝ, < ))
9493, 10breqtrrdi 5189 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 0 ≀ 𝑆)
95 metge0 24071 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ 0 ≀ (𝐴𝐷𝑃))
9629, 7, 17, 95syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 0 ≀ (𝐴𝐷𝑃))
9731, 33, 96, 94addge0d 11794 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 0 ≀ ((𝐴𝐷𝑃) + 𝑆))
98 divge0 12087 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≀ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ 0 ≀ (((𝐴𝐷𝑃) + 𝑆) / 2))
9964, 97, 77, 98syl21anc 834 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 0 ≀ (((𝐴𝐷𝑃) + 𝑆) / 2))
10033, 65, 94, 99lt2sqd 14223 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
10167, 66posdifd 11805 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2))))
10280, 100, 1013bitrd 304 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2))))
103102biimpa 475 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2)))
10469, 103elrpd 13017 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2)) ∈ ℝ+)
10563, 104eqeltrid 2835 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝑇 ∈ ℝ+)
1065adantr 479 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ π‘Œ ∈ (LSubSpβ€˜π‘ˆ))
107 rabexg 5330 . . . . . . . . . . . . . . . . . . 19 (π‘Œ ∈ (LSubSpβ€˜π‘ˆ) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ V)
108106, 107syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ V)
109 eqid 2730 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ ∈ ℝ+ ↦ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)}) = (π‘Ÿ ∈ ℝ+ ↦ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)})
110 oveq2 7419 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ÿ = 𝑇 β†’ ((𝑆↑2) + π‘Ÿ) = ((𝑆↑2) + 𝑇))
111110breq2d 5159 . . . . . . . . . . . . . . . . . . . 20 (π‘Ÿ = 𝑇 β†’ (((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ) ↔ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)))
112111rabbidv 3438 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ = 𝑇 β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)} = {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)})
113109, 112elrnmpt1s 5955 . . . . . . . . . . . . . . . . . 18 ((𝑇 ∈ ℝ+ ∧ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ V) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ ran (π‘Ÿ ∈ ℝ+ ↦ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)}))
114105, 108, 113syl2anc 582 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ ran (π‘Ÿ ∈ ℝ+ ↦ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + π‘Ÿ)}))
115114, 12eleqtrrdi 2842 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ 𝐹)
11662, 115sseldd 3982 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹))
117 ssrab2 4076 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} βŠ† 𝑋
118117a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} βŠ† 𝑋)
11963oveq2i 7422 . . . . . . . . . . . . . . . . . . . 20 ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2)))
12067ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ (𝑆↑2) ∈ ℝ)
121120recnd 11246 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ (𝑆↑2) ∈ β„‚)
12265ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
123122resqcld 14094 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
124123recnd 11246 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ β„‚)
125121, 124pncan3d 11578 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) βˆ’ (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
126119, 125eqtrid 2782 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
127126breq2d 5159 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ (((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≀ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
12829ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
1297ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ 𝐴 ∈ 𝑋)
13043adantlr 711 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ 𝑋)
131 metcl 24058 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝐴𝐷𝑦) ∈ ℝ)
132128, 129, 130, 131syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ (𝐴𝐷𝑦) ∈ ℝ)
133 metge0 24071 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ 0 ≀ (𝐴𝐷𝑦))
134128, 129, 130, 133syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ 0 ≀ (𝐴𝐷𝑦))
13599ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ 0 ≀ (((𝐴𝐷𝑃) + 𝑆) / 2))
136132, 122, 134, 135le2sqd 14224 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ ((𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≀ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
137127, 136bitr4d 281 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ π‘Œ) β†’ (((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
138137rabbidva 3437 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ π‘Œ ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
13942adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ π‘Œ βŠ† 𝑋)
140 rabss2 4074 . . . . . . . . . . . . . . . . 17 (π‘Œ βŠ† 𝑋 β†’ {𝑦 ∈ π‘Œ ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} βŠ† {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
141139, 140syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} βŠ† {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
142138, 141eqsstrd 4019 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} βŠ† {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
143 filss 23577 . . . . . . . . . . . . . . 15 (((𝑋filGen𝐹) ∈ (Filβ€˜π‘‹) ∧ ({𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} βŠ† 𝑋 ∧ {𝑦 ∈ π‘Œ ∣ ((𝐴𝐷𝑦)↑2) ≀ ((𝑆↑2) + 𝑇)} βŠ† {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})) β†’ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
14460, 116, 118, 142, 143syl13anc 1370 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
145 flimclsi 23702 . . . . . . . . . . . . . 14 ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) β†’ (𝐽 fLim (𝑋filGen𝐹)) βŠ† ((clsβ€˜π½)β€˜{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
146144, 145syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (𝐽 fLim (𝑋filGen𝐹)) βŠ† ((clsβ€˜π½)β€˜{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
14714elin1d 4197 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
148147adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
149146, 148sseldd 3982 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝑃 ∈ ((clsβ€˜π½)β€˜{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
150 ngpxms 24330 . . . . . . . . . . . . . . . . 17 (π‘ˆ ∈ NrmGrp β†’ π‘ˆ ∈ ∞MetSp)
1511, 11xmsxmet 24182 . . . . . . . . . . . . . . . . 17 (π‘ˆ ∈ ∞MetSp β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
15221, 150, 1513syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
153152adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
1547adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝐴 ∈ 𝑋)
15565adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
156155rexrd 11268 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ*)
157 eqid 2730 . . . . . . . . . . . . . . . 16 (MetOpenβ€˜π·) = (MetOpenβ€˜π·)
158 eqid 2730 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)}
159157, 158blcld 24234 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ*) β†’ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsdβ€˜(MetOpenβ€˜π·)))
160153, 154, 156, 159syl3anc 1369 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsdβ€˜(MetOpenβ€˜π·)))
1618, 1, 11xmstopn 24177 . . . . . . . . . . . . . . . . 17 (π‘ˆ ∈ ∞MetSp β†’ 𝐽 = (MetOpenβ€˜π·))
16221, 150, 1613syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽 = (MetOpenβ€˜π·))
163162adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝐽 = (MetOpenβ€˜π·))
164163fveq2d 6894 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (Clsdβ€˜π½) = (Clsdβ€˜(MetOpenβ€˜π·)))
165160, 164eleqtrrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsdβ€˜π½))
166 cldcls 22766 . . . . . . . . . . . . 13 ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsdβ€˜π½) β†’ ((clsβ€˜π½)β€˜{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
167165, 166syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ ((clsβ€˜π½)β€˜{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
168149, 167eleqtrd 2833 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)})
169 oveq2 7419 . . . . . . . . . . . . . 14 (𝑦 = 𝑃 β†’ (𝐴𝐷𝑦) = (𝐴𝐷𝑃))
170169breq1d 5157 . . . . . . . . . . . . 13 (𝑦 = 𝑃 β†’ ((𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
171170elrab 3682 . . . . . . . . . . . 12 (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
172171simprbi 495 . . . . . . . . . . 11 (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)} β†’ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2))
173168, 172syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2))
17431, 33, 31leadd2d 11813 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐴𝐷𝑃) ≀ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≀ ((𝐴𝐷𝑃) + 𝑆)))
17531recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐴𝐷𝑃) ∈ β„‚)
1761752timesd 12459 . . . . . . . . . . . . 13 (πœ‘ β†’ (2 Β· (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)))
177176breq1d 5157 . . . . . . . . . . . 12 (πœ‘ β†’ ((2 Β· (𝐴𝐷𝑃)) ≀ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≀ ((𝐴𝐷𝑃) + 𝑆)))
178 lemuldiv2 12099 . . . . . . . . . . . . . 14 (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ ((2 Β· (𝐴𝐷𝑃)) ≀ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
17976, 178mp3an3 1448 . . . . . . . . . . . . 13 (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) β†’ ((2 Β· (𝐴𝐷𝑃)) ≀ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
18031, 64, 179syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ ((2 Β· (𝐴𝐷𝑃)) ≀ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
181174, 177, 1803bitr2d 306 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐴𝐷𝑃) ≀ 𝑆 ↔ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)))
182181biimpar 476 . . . . . . . . . 10 ((πœ‘ ∧ (𝐴𝐷𝑃) ≀ (((𝐴𝐷𝑃) + 𝑆) / 2)) β†’ (𝐴𝐷𝑃) ≀ 𝑆)
183173, 182syldan 589 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 < (𝐴𝐷𝑃)) β†’ (𝐴𝐷𝑃) ≀ 𝑆)
184183ex 411 . . . . . . . 8 (πœ‘ β†’ (𝑆 < (𝐴𝐷𝑃) β†’ (𝐴𝐷𝑃) ≀ 𝑆))
18548, 184sylbird 259 . . . . . . 7 (πœ‘ β†’ (Β¬ (𝐴𝐷𝑃) ≀ 𝑆 β†’ (𝐴𝐷𝑃) ≀ 𝑆))
186185pm2.18d 127 . . . . . 6 (πœ‘ β†’ (𝐴𝐷𝑃) ≀ 𝑆)
187186adantr 479 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (𝐴𝐷𝑃) ≀ 𝑆)
18883adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ 𝑅 βŠ† ℝ)
18989adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ 𝑅 π‘₯ ≀ 𝑀)
190 simpr 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ π‘Œ)
191 fvex 6903 . . . . . . . . 9 (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ V
192 eqid 2730 . . . . . . . . . 10 (𝑦 ∈ π‘Œ ↦ (π‘β€˜(𝐴 βˆ’ 𝑦))) = (𝑦 ∈ π‘Œ ↦ (π‘β€˜(𝐴 βˆ’ 𝑦)))
193192elrnmpt1 5956 . . . . . . . . 9 ((𝑦 ∈ π‘Œ ∧ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ V) β†’ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ ran (𝑦 ∈ π‘Œ ↦ (π‘β€˜(𝐴 βˆ’ 𝑦))))
194190, 191, 193sylancl 584 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ ran (𝑦 ∈ π‘Œ ↦ (π‘β€˜(𝐴 βˆ’ 𝑦))))
195194, 9eleqtrrdi 2842 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ 𝑅)
196 infrelb 12203 . . . . . . 7 ((𝑅 βŠ† ℝ ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ 𝑅 π‘₯ ≀ 𝑀 ∧ (π‘β€˜(𝐴 βˆ’ 𝑦)) ∈ 𝑅) β†’ inf(𝑅, ℝ, < ) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
197188, 189, 195, 196syl3anc 1369 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ inf(𝑅, ℝ, < ) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
19810, 197eqbrtrid 5182 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ 𝑆 ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
19932, 34, 47, 187, 198letrd 11375 . . . 4 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (𝐴𝐷𝑃) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
20026, 199eqbrtrrd 5171 . . 3 ((πœ‘ ∧ 𝑦 ∈ π‘Œ) β†’ (π‘β€˜(𝐴 βˆ’ 𝑃)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
201200ralrimiva 3144 . 2 (πœ‘ β†’ βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ 𝑃)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
202 oveq2 7419 . . . . . 6 (π‘₯ = 𝑃 β†’ (𝐴 βˆ’ π‘₯) = (𝐴 βˆ’ 𝑃))
203202fveq2d 6894 . . . . 5 (π‘₯ = 𝑃 β†’ (π‘β€˜(𝐴 βˆ’ π‘₯)) = (π‘β€˜(𝐴 βˆ’ 𝑃)))
204203breq1d 5157 . . . 4 (π‘₯ = 𝑃 β†’ ((π‘β€˜(𝐴 βˆ’ π‘₯)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)) ↔ (π‘β€˜(𝐴 βˆ’ 𝑃)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦))))
205204ralbidv 3175 . . 3 (π‘₯ = 𝑃 β†’ (βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ π‘₯)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)) ↔ βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ 𝑃)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦))))
206205rspcev 3611 . 2 ((𝑃 ∈ π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ 𝑃)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦))) β†’ βˆƒπ‘₯ ∈ π‘Œ βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ π‘₯)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
20715, 201, 206syl2anc 582 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ π‘Œ βˆ€π‘¦ ∈ π‘Œ (π‘β€˜(𝐴 βˆ’ π‘₯)) ≀ (π‘β€˜(𝐴 βˆ’ 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  βˆͺ cuni 4907   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  ran crn 5676   β†Ύ cres 5677  β€˜cfv 6542  (class class class)co 7411  infcinf 9438  β„cr 11111  0cc0 11112   + caddc 11115   Β· cmul 11117  β„*cxr 11251   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448   / cdiv 11875  2c2 12271  β„+crp 12978  β†‘cexp 14031  Basecbs 17148   β†Ύs cress 17177  distcds 17210  TopOpenctopn 17371  -gcsg 18857  LModclmod 20614  LSubSpclss 20686  βˆžMetcxmet 21129  Metcmet 21130  fBascfbas 21132  filGencfg 21133  MetOpencmopn 21134  Clsdccld 22740  clsccl 22742  Filcfil 23569   fLim cflim 23658  βˆžMetSpcxms 24043  MetSpcms 24044  normcnm 24305  NrmGrpcngp 24306  β„‚PreHilccph 24914  CMetSpccms 25080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ico 13334  df-icc 13335  df-fz 13489  df-seq 13971  df-exp 14032  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-rest 17372  df-0g 17391  df-topgen 17393  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-grp 18858  df-minusg 18859  df-sbg 18860  df-mulg 18987  df-subg 19039  df-ghm 19128  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-cring 20130  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-dvr 20292  df-rhm 20363  df-subrg 20459  df-drng 20502  df-staf 20596  df-srng 20597  df-lmod 20616  df-lss 20687  df-lmhm 20777  df-lvec 20858  df-sra 20930  df-rgmod 20931  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-phl 21398  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-haus 23039  df-fil 23570  df-flim 23663  df-xms 24046  df-ms 24047  df-nm 24311  df-ngp 24312  df-nlm 24315  df-clm 24810  df-cph 24916  df-cfil 25003  df-cmet 25005  df-cms 25083
This theorem is referenced by:  minveclem5  25181
  Copyright terms: Public domain W3C validator