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 eqtrid ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝑃 ) = ( 𝐴 ( 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 eqtrid ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 𝑃 ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( 𝑆 ↑ 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 ⊒ ( πœ‘ β†’ βˆƒ π‘₯ ∈ π‘Œ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )