Metamath Proof Explorer

Theorem minveclem4

Description: Lemma for minvec . The convergent point of the Cauchy sequence F attains the minimum distance, and so is closer to A than any other point in Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses 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 minveclem4 ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊢ 𝑋 = ( Base ‘ 𝑈 )
2 minvec.m ⊢ − = ( -g ‘ 𝑈 )
3 minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
4 minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
5 minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
6 minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
7 minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
9 minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
10 minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
12 minvec.f ⊢ 𝐹 = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
13 minvec.p ⊢ 𝑃 = ∪ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) )
14 minvec.t ⊢ 𝑇 = ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 minveclem4a ⊢ ( 𝜑 → 𝑃 ∈ ( ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ∩ 𝑌 ) )
16 15 elin2d ⊢ ( 𝜑 → 𝑃 ∈ 𝑌 )
17 11 oveqi ⊢ ( 𝐴 𝐷 𝑃 ) = ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝑃 )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 minveclem4b ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
19 7 18 ovresd ⊢ ( 𝜑 → ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝑃 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝑃 ) )
20 17 19 syl5eq ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑃 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝑃 ) )
21 cphngp ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp )
22 4 21 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmGrp )
23 eqid ⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
24 3 1 2 23 ngpds ⊢ ( ( 𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝑃 ) = ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) )
25 22 7 18 24 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝑈 ) 𝑃 ) = ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) )
26 20 25 eqtrd ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑃 ) = ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑃 ) = ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) )
28 ngpms ⊢ ( 𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp )
29 1 11 msmet ⊢ ( 𝑈 ∈ MetSp → 𝐷 ∈ ( Met ‘ 𝑋 ) )
30 22 28 29 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
31 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑃 ) ∈ ℝ )
32 30 7 18 31 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑃 ) ∈ ℝ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑃 ) ∈ ℝ )
34 1 2 3 4 5 6 7 8 9 10 minveclem4c ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑆 ∈ ℝ )
36 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ NrmGrp )
37 cphlmod ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod )
38 4 37 syl ⊢ ( 𝜑 → 𝑈 ∈ LMod )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ LMod )
40 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
41 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
42 1 41 lssss ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
43 5 42 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
44 43 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
45 1 2 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 − 𝑦 ) ∈ 𝑋 )
46 39 40 44 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 − 𝑦 ) ∈ 𝑋 )
47 1 3 nmcl ⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐴 − 𝑦 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ ℝ )
48 36 46 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ ℝ )
49 34 32 ltnled ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 𝑃 ) ↔ ¬ ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3b ⊢ ( 𝜑 → 𝐹 ∈ ( fBas ‘ 𝑌 ) )
51 fbsspw ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → 𝐹 ⊆ 𝒫 𝑌 )
52 50 51 syl ⊢ ( 𝜑 → 𝐹 ⊆ 𝒫 𝑌 )
53 43 sspwd ⊢ ( 𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋 )
54 52 53 sstrd ⊢ ( 𝜑 → 𝐹 ⊆ 𝒫 𝑋 )
55 1 fvexi ⊢ 𝑋 ∈ V
56 55 a1i ⊢ ( 𝜑 → 𝑋 ∈ V )
57 fbasweak ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
58 50 54 56 57 syl3anc ⊢ ( 𝜑 → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
60 fgcl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
61 59 60 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
62 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
63 59 62 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
64 32 34 readdcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ∈ ℝ )
65 64 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ∈ ℝ )
66 65 resqcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℝ )
67 34 resqcld ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℝ )
68 66 67 resubcld ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ )
70 34 32 34 ltadd1d ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 𝑃 ) ↔ ( 𝑆 + 𝑆 ) < ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ) )
71 34 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
72 71 2timesd ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( 𝑆 + 𝑆 ) )
73 72 breq1d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) < ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ ( 𝑆 + 𝑆 ) < ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ) )
74 2re ⊢ 2 ∈ ℝ
75 2pos ⊢ 0 < 2
76 74 75 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
77 76 a1i ⊢ ( 𝜑 → ( 2 ∈ ℝ ∧ 0 < 2 ) )
78 ltmuldiv2 ⊢ ( ( 𝑆 ∈ ℝ ∧ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑆 ) < ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
79 34 64 77 78 syl3anc ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) < ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
80 70 73 79 3bitr2d ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 𝑃 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
81 1 2 3 4 5 6 7 8 9 minveclem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
82 81 simp3d ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
83 81 simp1d ⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
84 81 simp2d ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
85 0re ⊢ 0 ∈ ℝ
86 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
87 86 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
88 87 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
89 85 82 88 sylancr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
90 85 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )
91 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
92 83 84 89 90 91 syl31anc ⊢ ( 𝜑 → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
93 82 92 mpbird ⊢ ( 𝜑 → 0 ≤ inf ( 𝑅 , ℝ , < ) )
94 93 10 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑆 )
95 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝑃 ) )
96 30 7 18 95 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝐴 𝐷 𝑃 ) )
97 32 34 96 94 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) )
98 divge0 ⊢ ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) )
99 64 97 77 98 syl21anc ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) )
100 34 65 94 99 lt2sqd ⊢ ( 𝜑 → ( 𝑆 < ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↔ ( 𝑆 ↑ 2 ) < ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
101 67 66 posdifd ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) < ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ↔ 0 < ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
102 80 100 101 3bitrd ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 𝑃 ) ↔ 0 < ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
103 102 biimpa ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 0 < ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
104 69 103 elrpd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ+ )
105 14 104 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝑇 ∈ ℝ+ )
106 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
107 rabexg ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ V )
108 106 107 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ V )
109 eqid ⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
110 oveq2 ⊢ ( 𝑟 = 𝑇 → ( ( 𝑆 ↑ 2 ) + 𝑟 ) = ( ( 𝑆 ↑ 2 ) + 𝑇 ) )
111 110 breq2d ⊢ ( 𝑟 = 𝑇 → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) ) )
112 111 rabbidv ⊢ ( 𝑟 = 𝑇 → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } )
113 109 112 elrnmpt1s ⊢ ( ( 𝑇 ∈ ℝ+ ∧ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ V ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) )
114 105 108 113 syl2anc ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) )
115 114 12 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ 𝐹 )
116 63 115 sseldd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ ( 𝑋 filGen 𝐹 ) )
117 ssrab2 ⊢ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ⊆ 𝑋
118 117 a1i ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ⊆ 𝑋 )
119 14 oveq2i ⊢ ( ( 𝑆 ↑ 2 ) + 𝑇 ) = ( ( 𝑆 ↑ 2 ) + ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
120 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
121 120 recnd ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
122 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ∈ ℝ )
123 122 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℝ )
124 123 recnd ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℂ )
125 121 124 pncan3d ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + ( ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) = ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) )
126 119 125 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + 𝑇 ) = ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) )
127 126 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
128 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
129 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
130 44 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
131 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑦 ) ∈ ℝ )
132 128 129 130 131 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) ∈ ℝ )
133 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝑦 ) )
134 128 129 130 133 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( 𝐴 𝐷 𝑦 ) )
135 99 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) )
136 132 122 134 135 le2sqd ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
137 127 136 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) ↔ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
138 137 rabbidva ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } = { 𝑦 ∈ 𝑌 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
139 43 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝑌 ⊆ 𝑋 )
140 rabss2 ⊢ ( 𝑌 ⊆ 𝑋 → { 𝑦 ∈ 𝑌 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ⊆ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
141 139 140 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ⊆ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
142 138 141 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ⊆ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
143 filss ⊢ ( ( ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) ∧ ( { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ∈ ( 𝑋 filGen 𝐹 ) ∧ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ⊆ 𝑋 ∧ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑇 ) } ⊆ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( 𝑋 filGen 𝐹 ) )
144 61 116 118 142 143 syl13anc ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( 𝑋 filGen 𝐹 ) )
145 flimclsi ⊢ ( { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( 𝑋 filGen 𝐹 ) → ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ) )
146 144 145 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ) )
147 15 elin1d ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) )
148 147 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝑃 ∈ ( 𝐽 fLim ( 𝑋 filGen 𝐹 ) ) )
149 146 148 sseldd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ) )
150 ngpxms ⊢ ( 𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp )
151 1 11 xmsxmet ⊢ ( 𝑈 ∈ ∞MetSp → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
152 22 150 151 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
154 7 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝐴 ∈ 𝑋 )
155 65 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ∈ ℝ )
156 155 rexrd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ∈ ℝ* )
157 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
158 eqid ⊢ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } = { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) }
159 157 158 blcld ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ∈ ℝ* ) → { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( Clsd ‘ ( MetOpen ‘ 𝐷 ) ) )
160 153 154 156 159 syl3anc ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( Clsd ‘ ( MetOpen ‘ 𝐷 ) ) )
161 8 1 11 xmstopn ⊢ ( 𝑈 ∈ ∞MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )
162 22 150 161 3syl ⊢ ( 𝜑 → 𝐽 = ( MetOpen ‘ 𝐷 ) )
163 162 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝐽 = ( MetOpen ‘ 𝐷 ) )
164 163 fveq2d ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( MetOpen ‘ 𝐷 ) ) )
165 160 164 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( Clsd ‘ 𝐽 ) )
166 cldcls ⊢ ( { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ) = { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
167 165 166 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( ( cls ‘ 𝐽 ) ‘ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ) = { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
168 149 167 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → 𝑃 ∈ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } )
169 oveq2 ⊢ ( 𝑦 = 𝑃 → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑃 ) )
170 169 breq1d ⊢ ( 𝑦 = 𝑃 → ( ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ↔ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
171 170 elrab ⊢ ( 𝑃 ∈ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
172 171 simprbi ⊢ ( 𝑃 ∈ { 𝑦 ∈ 𝑋 ∣ ( 𝐴 𝐷 𝑦 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) } → ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) )
173 168 172 syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) )
174 32 34 32 leadd2d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 ↔ ( ( 𝐴 𝐷 𝑃 ) + ( 𝐴 𝐷 𝑃 ) ) ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ) )
175 32 recnd ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑃 ) ∈ ℂ )
176 175 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝐴 𝐷 𝑃 ) ) = ( ( 𝐴 𝐷 𝑃 ) + ( 𝐴 𝐷 𝑃 ) ) )
177 176 breq1d ⊢ ( 𝜑 → ( ( 2 · ( 𝐴 𝐷 𝑃 ) ) ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ ( ( 𝐴 𝐷 𝑃 ) + ( 𝐴 𝐷 𝑃 ) ) ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ) )
178 lemuldiv2 ⊢ ( ( ( 𝐴 𝐷 𝑃 ) ∈ ℝ ∧ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · ( 𝐴 𝐷 𝑃 ) ) ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
179 76 178 mp3an3 ⊢ ( ( ( 𝐴 𝐷 𝑃 ) ∈ ℝ ∧ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ∈ ℝ ) → ( ( 2 · ( 𝐴 𝐷 𝑃 ) ) ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
180 32 64 179 syl2anc ⊢ ( 𝜑 → ( ( 2 · ( 𝐴 𝐷 𝑃 ) ) ≤ ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) ↔ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
181 174 177 180 3bitr2d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 ↔ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) )
182 181 biimpar ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐷 𝑃 ) ≤ ( ( ( 𝐴 𝐷 𝑃 ) + 𝑆 ) / 2 ) ) → ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 )
183 173 182 syldan ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) → ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 )
184 183 ex ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 𝑃 ) → ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 ) )
185 49 184 sylbird ⊢ ( 𝜑 → ( ¬ ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 → ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 ) )
186 185 pm2.18d ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 )
187 186 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑃 ) ≤ 𝑆 )
188 83 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑅 ⊆ ℝ )
189 89 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
190 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
191 fvex ⊢ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V
192 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
193 192 elrnmpt1 ⊢ ( ( 𝑦 ∈ 𝑌 ∧ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
194 190 191 193 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
195 194 9 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ 𝑅 )
196 infrelb ⊢ ( ( 𝑅 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ 𝑅 ) → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
197 188 189 195 196 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
198 10 197 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑆 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
199 33 35 48 187 198 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑃 ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
200 27 199 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
201 200 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
202 oveq2 ⊢ ( 𝑥 = 𝑃 → ( 𝐴 − 𝑥 ) = ( 𝐴 − 𝑃 ) )
203 202 fveq2d ⊢ ( 𝑥 = 𝑃 → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) = ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) )
204 203 breq1d ⊢ ( 𝑥 = 𝑃 → ( ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
205 204 ralbidv ⊢ ( 𝑥 = 𝑃 → ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
206 205 rspcev ⊢ ( ( 𝑃 ∈ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑃 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
207 16 201 206 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )