Metamath Proof Explorer

Theorem minvecolem4

Description: Lemma for minveco . 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 AV, 4-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x ⊒ 𝑋 = ( BaseSet β€˜ π‘ˆ )
minveco.m ⊒ 𝑀 = ( βˆ’π‘£ β€˜ π‘ˆ )
minveco.n ⊒ 𝑁 = ( normCV β€˜ π‘ˆ )
minveco.y ⊒ π‘Œ = ( BaseSet β€˜ π‘Š )
minveco.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ CPreHilOLD )
minveco.w ⊒ ( πœ‘ β†’ π‘Š ∈ ( ( SubSp β€˜ π‘ˆ ) ∩ CBan ) )
minveco.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
minveco.d ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
minveco.j ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
minveco.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
minveco.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
minveco.f ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ π‘Œ )
minveco.1 ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
minveco.t ⊒ 𝑇 = ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) )
Assertion minvecolem4 ( πœ‘ β†’ βˆƒ π‘₯ ∈ π‘Œ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 minveco.x ⊒ 𝑋 = ( BaseSet β€˜ π‘ˆ )
2 minveco.m ⊒ 𝑀 = ( βˆ’π‘£ β€˜ π‘ˆ )
3 minveco.n ⊒ 𝑁 = ( normCV β€˜ π‘ˆ )
4 minveco.y ⊒ π‘Œ = ( BaseSet β€˜ π‘Š )
5 minveco.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ CPreHilOLD )
6 minveco.w ⊒ ( πœ‘ β†’ π‘Š ∈ ( ( SubSp β€˜ π‘ˆ ) ∩ CBan ) )
7 minveco.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
8 minveco.d ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
9 minveco.j ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
10 minveco.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
11 minveco.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
12 minveco.f ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ π‘Œ )
13 minveco.1 ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
14 minveco.t ⊒ 𝑇 = ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) )
15 phnv ⊒ ( π‘ˆ ∈ CPreHilOLD β†’ π‘ˆ ∈ NrmCVec )
16 1 8 imsxmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
17 5 15 16 3syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
18 9 methaus ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ Haus )
19 lmfun ⊒ ( 𝐽 ∈ Haus β†’ Fun ( ⇝𝑑 β€˜ 𝐽 ) )
20 17 18 19 3syl ⊒ ( πœ‘ β†’ Fun ( ⇝𝑑 β€˜ 𝐽 ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4a ⊒ ( πœ‘ β†’ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) )
22 eqid ⊒ ( 𝐽 β†Ύt π‘Œ ) = ( 𝐽 β†Ύt π‘Œ )
23 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
24 4 fvexi ⊒ π‘Œ ∈ V
25 24 a1i ⊒ ( πœ‘ β†’ π‘Œ ∈ V )
26 5 15 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ NrmCVec )
27 9 mopntop ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ Top )
28 26 16 27 3syl ⊒ ( πœ‘ β†’ 𝐽 ∈ Top )
29 elin ⊒ ( π‘Š ∈ ( ( SubSp β€˜ π‘ˆ ) ∩ CBan ) ↔ ( π‘Š ∈ ( SubSp β€˜ π‘ˆ ) ∧ π‘Š ∈ CBan ) )
30 6 29 sylib ⊒ ( πœ‘ β†’ ( π‘Š ∈ ( SubSp β€˜ π‘ˆ ) ∧ π‘Š ∈ CBan ) )
31 30 simpld ⊒ ( πœ‘ β†’ π‘Š ∈ ( SubSp β€˜ π‘ˆ ) )
32 eqid ⊒ ( SubSp β€˜ π‘ˆ ) = ( SubSp β€˜ π‘ˆ )
33 1 4 32 sspba ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ ( SubSp β€˜ π‘ˆ ) ) β†’ π‘Œ βŠ† 𝑋 )
34 26 31 33 syl2anc ⊒ ( πœ‘ β†’ π‘Œ βŠ† 𝑋 )
35 xmetres2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ π‘Œ ) )
36 17 34 35 syl2anc ⊒ ( πœ‘ β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ π‘Œ ) )
37 eqid ⊒ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) )
38 37 mopntopon ⊒ ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ π‘Œ ) β†’ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ∈ ( TopOn β€˜ π‘Œ ) )
39 36 38 syl ⊒ ( πœ‘ β†’ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ∈ ( TopOn β€˜ π‘Œ ) )
40 lmcl ⊒ ( ( ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ∈ ( TopOn β€˜ π‘Œ ) ∧ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) β†’ ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ∈ π‘Œ )
41 39 21 40 syl2anc ⊒ ( πœ‘ β†’ ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ∈ π‘Œ )
42 1zzd ⊒ ( πœ‘ β†’ 1 ∈ β„€ )
43 22 23 25 28 41 42 12 lmss ⊒ ( πœ‘ β†’ ( 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ↔ 𝐹 ( ⇝𝑑 β€˜ ( 𝐽 β†Ύt π‘Œ ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) )
44 eqid ⊒ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) = ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) )
45 44 9 37 metrest ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘Œ βŠ† 𝑋 ) β†’ ( 𝐽 β†Ύt π‘Œ ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )
46 17 34 45 syl2anc ⊒ ( πœ‘ β†’ ( 𝐽 β†Ύt π‘Œ ) = ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )
47 46 fveq2d ⊒ ( πœ‘ β†’ ( ⇝𝑑 β€˜ ( 𝐽 β†Ύt π‘Œ ) ) = ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) )
48 47 breqd ⊒ ( πœ‘ β†’ ( 𝐹 ( ⇝𝑑 β€˜ ( 𝐽 β†Ύt π‘Œ ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ↔ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) )
49 43 48 bitrd ⊒ ( πœ‘ β†’ ( 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ↔ 𝐹 ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) )
50 21 49 mpbird ⊒ ( πœ‘ β†’ 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) )
51 funbrfv ⊒ ( Fun ( ⇝𝑑 β€˜ 𝐽 ) β†’ ( 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) β†’ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) = ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) ) )
52 20 50 51 sylc ⊒ ( πœ‘ β†’ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) = ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β€˜ 𝐹 ) )
53 52 41 eqeltrd ⊒ ( πœ‘ β†’ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ π‘Œ )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4b ⊒ ( πœ‘ β†’ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ 𝑋 )
55 1 2 3 8 imsdval ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ 𝑋 ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) = ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) )
56 26 7 54 55 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) = ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) )
57 56 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) = ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) )
58 1 8 imsmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
59 5 15 58 3syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
60 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ 𝑋 ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ∈ ℝ )
61 59 7 54 60 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ∈ ℝ )
62 61 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ∈ ℝ )
63 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4c ⊒ ( πœ‘ β†’ 𝑆 ∈ ℝ )
64 63 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑆 ∈ ℝ )
65 26 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ π‘ˆ ∈ NrmCVec )
66 7 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝐴 ∈ 𝑋 )
67 34 sselda ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ 𝑋 )
68 1 2 nvmcl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) β†’ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
69 65 66 67 68 syl3anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
70 1 3 nvcl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
71 65 69 70 syl2anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
72 63 61 ltnled ⊒ ( πœ‘ β†’ ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ↔ Β¬ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 ) )
73 eqid ⊒ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) = ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) )
74 17 adantr ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
75 61 63 readdcld ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ∈ ℝ )
76 75 rehalfcld ⊒ ( πœ‘ β†’ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ )
77 76 resqcld ⊒ ( πœ‘ β†’ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℝ )
78 63 resqcld ⊒ ( πœ‘ β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
79 77 78 resubcld ⊒ ( πœ‘ β†’ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ )
80 79 adantr ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ )
81 63 61 63 ltadd1d ⊒ ( πœ‘ β†’ ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ↔ ( 𝑆 + 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ) )
82 63 recnd ⊒ ( πœ‘ β†’ 𝑆 ∈ β„‚ )
83 82 2timesd ⊒ ( πœ‘ β†’ ( 2 Β· 𝑆 ) = ( 𝑆 + 𝑆 ) )
84 83 breq1d ⊒ ( πœ‘ β†’ ( ( 2 Β· 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ ( 𝑆 + 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ) )
85 2re ⊒ 2 ∈ ℝ
86 2pos ⊒ 0 < 2
87 85 86 pm3.2i ⊒ ( 2 ∈ ℝ ∧ 0 < 2 )
88 87 a1i ⊒ ( πœ‘ β†’ ( 2 ∈ ℝ ∧ 0 < 2 ) )
89 ltmuldiv2 ⊒ ( ( 𝑆 ∈ ℝ ∧ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) β†’ ( ( 2 Β· 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
90 63 75 88 89 syl3anc ⊒ ( πœ‘ β†’ ( ( 2 Β· 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
91 81 84 90 3bitr2d ⊒ ( πœ‘ β†’ ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
92 1 2 3 4 5 6 7 8 9 10 minvecolem1 ⊒ ( πœ‘ β†’ ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
93 92 simp3d ⊒ ( πœ‘ β†’ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 )
94 92 simp1d ⊒ ( πœ‘ β†’ 𝑅 βŠ† ℝ )
95 92 simp2d ⊒ ( πœ‘ β†’ 𝑅 β‰  βˆ… )
96 0re ⊒ 0 ∈ ℝ
97 breq1 ⊒ ( π‘₯ = 0 β†’ ( π‘₯ ≀ 𝑀 ↔ 0 ≀ 𝑀 ) )
98 97 ralbidv ⊒ ( π‘₯ = 0 β†’ ( βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
99 98 rspcev ⊒ ( ( 0 ∈ ℝ ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) β†’ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 )
100 96 93 99 sylancr ⊒ ( πœ‘ β†’ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 )
101 96 a1i ⊒ ( πœ‘ β†’ 0 ∈ ℝ )
102 infregelb ⊒ ( ( ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 ) ∧ 0 ∈ ℝ ) β†’ ( 0 ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
103 94 95 100 101 102 syl31anc ⊒ ( πœ‘ β†’ ( 0 ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
104 93 103 mpbird ⊒ ( πœ‘ β†’ 0 ≀ inf ( 𝑅 , ℝ , < ) )
105 104 11 breqtrrdi ⊒ ( πœ‘ β†’ 0 ≀ 𝑆 )
106 metge0 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ 𝑋 ) β†’ 0 ≀ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) )
107 59 7 54 106 syl3anc ⊒ ( πœ‘ β†’ 0 ≀ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) )
108 61 63 107 105 addge0d ⊒ ( πœ‘ β†’ 0 ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) )
109 divge0 ⊒ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ∈ ℝ ∧ 0 ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) β†’ 0 ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) )
110 75 108 88 109 syl21anc ⊒ ( πœ‘ β†’ 0 ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) )
111 63 76 105 110 lt2sqd ⊒ ( πœ‘ β†’ ( 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↔ ( 𝑆 ↑ 2 ) < ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
112 78 77 posdifd ⊒ ( πœ‘ β†’ ( ( 𝑆 ↑ 2 ) < ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ↔ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) )
113 91 111 112 3bitrd ⊒ ( πœ‘ β†’ ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ↔ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) )
114 113 biimpa ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) )
115 80 114 elrpd ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ+ )
116 115 rpreccld ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) ∈ ℝ+ )
117 14 116 eqeltrid ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ 𝑇 ∈ ℝ+ )
118 117 rprege0d ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( 𝑇 ∈ ℝ ∧ 0 ≀ 𝑇 ) )
119 flge0nn0 ⊒ ( ( 𝑇 ∈ ℝ ∧ 0 ≀ 𝑇 ) β†’ ( ⌊ β€˜ 𝑇 ) ∈ β„•0 )
120 nn0p1nn ⊒ ( ( ⌊ β€˜ 𝑇 ) ∈ β„•0 β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ∈ β„• )
121 118 119 120 3syl ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ∈ β„• )
122 121 nnzd ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ∈ β„€ )
123 50 52 breqtrrd ⊒ ( πœ‘ β†’ 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) )
124 123 adantr ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) )
125 7 adantr ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ 𝐴 ∈ 𝑋 )
126 76 adantr ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ )
127 126 rexrd ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ* )
128 simpll ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ πœ‘ )
129 eluznn ⊒ ( ( ( ( ⌊ β€˜ 𝑇 ) + 1 ) ∈ β„• ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑛 ∈ β„• )
130 121 129 sylan ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑛 ∈ β„• )
131 59 adantr ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
132 7 adantr ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ 𝐴 ∈ 𝑋 )
133 12 34 fssd ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ 𝑋 )
134 133 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ ( 𝐹 β€˜ 𝑛 ) ∈ 𝑋 )
135 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 β€˜ 𝑛 ) ∈ 𝑋 ) β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ∈ ℝ )
136 131 132 134 135 syl3anc ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ∈ ℝ )
137 128 130 136 syl2anc ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ∈ ℝ )
138 137 resqcld ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ↑ 2 ) ∈ ℝ )
139 63 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑆 ∈ ℝ )
140 139 resqcld ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
141 130 nnrecred ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( 1 / 𝑛 ) ∈ ℝ )
142 140 141 readdcld ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
143 77 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℝ )
144 128 130 13 syl2anc ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
145 117 adantr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑇 ∈ ℝ+ )
146 145 rpred ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑇 ∈ ℝ )
147 reflcl ⊒ ( 𝑇 ∈ ℝ β†’ ( ⌊ β€˜ 𝑇 ) ∈ ℝ )
148 peano2re ⊒ ( ( ⌊ β€˜ 𝑇 ) ∈ ℝ β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ∈ ℝ )
149 146 147 148 3syl ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ∈ ℝ )
150 130 nnred ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑛 ∈ ℝ )
151 fllep1 ⊒ ( 𝑇 ∈ ℝ β†’ 𝑇 ≀ ( ( ⌊ β€˜ 𝑇 ) + 1 ) )
152 146 151 syl ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑇 ≀ ( ( ⌊ β€˜ 𝑇 ) + 1 ) )
153 eluzle ⊒ ( 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ≀ 𝑛 )
154 153 adantl ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ≀ 𝑛 )
155 146 149 150 152 154 letrd ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 𝑇 ≀ 𝑛 )
156 14 155 eqbrtrrid ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) ≀ 𝑛 )
157 1red ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 1 ∈ ℝ )
158 79 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ )
159 114 adantr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) )
160 130 nngt0d ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 0 < 𝑛 )
161 lediv23 ⊒ ( ( 1 ∈ ℝ ∧ ( ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ ∧ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) β†’ ( ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) ≀ 𝑛 ↔ ( 1 / 𝑛 ) ≀ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) )
162 157 158 159 150 160 161 syl122anc ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) ≀ 𝑛 ↔ ( 1 / 𝑛 ) ≀ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) )
163 156 162 mpbid ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( 1 / 𝑛 ) ≀ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) )
164 140 141 143 leaddsub2d ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≀ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ↔ ( 1 / 𝑛 ) ≀ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ) )
165 163 164 mpbird ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≀ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) )
166 138 142 143 144 165 letrd ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ↑ 2 ) ≀ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) )
167 76 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ )
168 metge0 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 β€˜ 𝑛 ) ∈ 𝑋 ) β†’ 0 ≀ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) )
169 131 132 134 168 syl3anc ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„• ) β†’ 0 ≀ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) )
170 128 130 169 syl2anc ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 0 ≀ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) )
171 110 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ 0 ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) )
172 137 167 170 171 le2sqd ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↔ ( ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ↑ 2 ) ≀ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
173 166 172 mpbird ⊒ ( ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ ( ( ⌊ β€˜ 𝑇 ) + 1 ) ) ) β†’ ( 𝐴 𝐷 ( 𝐹 β€˜ 𝑛 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) )
174 73 9 74 122 124 125 127 173 lmle ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) )
175 61 63 61 leadd2d ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 ↔ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ) )
176 61 recnd ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ∈ β„‚ )
177 176 2timesd ⊒ ( πœ‘ β†’ ( 2 Β· ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) = ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) )
178 177 breq1d ⊒ ( πœ‘ β†’ ( ( 2 Β· ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ) )
179 lemuldiv2 ⊒ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ∈ ℝ ∧ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) β†’ ( ( 2 Β· ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
180 87 179 mp3an3 ⊒ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ∈ ℝ ∧ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ∈ ℝ ) β†’ ( ( 2 Β· ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
181 61 75 180 syl2anc ⊒ ( πœ‘ β†’ ( ( 2 Β· ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) ↔ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
182 175 178 181 3bitr2d ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 ↔ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
183 182 biimpar ⊒ ( ( πœ‘ ∧ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( ( ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) + 𝑆 ) / 2 ) ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 )
184 174 183 syldan ⊒ ( ( πœ‘ ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 )
185 184 ex ⊒ ( πœ‘ β†’ ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 ) )
186 72 185 sylbird ⊒ ( πœ‘ β†’ ( Β¬ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 ) )
187 186 pm2.18d ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 )
188 187 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ 𝑆 )
189 94 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑅 βŠ† ℝ )
190 100 adantr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 )
191 simpr ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ π‘Œ )
192 fvex ⊒ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ V
193 eqid ⊒ ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
194 193 elrnmpt1 ⊒ ( ( 𝑦 ∈ π‘Œ ∧ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ V ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ) )
195 191 192 194 sylancl ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ) )
196 195 10 eleqtrrdi ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ 𝑅 )
197 infrelb ⊒ ( ( 𝑅 βŠ† ℝ ∧ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 ∧ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ∈ 𝑅 ) β†’ inf ( 𝑅 , ℝ , < ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
198 189 190 196 197 syl3anc ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ inf ( 𝑅 , ℝ , < ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
199 11 198 eqbrtrid ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑆 ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
200 62 64 71 188 199 letrd ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
201 57 200 eqbrtrrd ⊒ ( ( πœ‘ ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
202 201 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
203 oveq2 ⊒ ( π‘₯ = ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) β†’ ( 𝐴 𝑀 π‘₯ ) = ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) )
204 203 fveq2d ⊒ ( π‘₯ = ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) β†’ ( 𝑁 β€˜ ( 𝐴 𝑀 π‘₯ ) ) = ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) )
205 204 breq1d ⊒ ( π‘₯ = ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) β†’ ( ( 𝑁 β€˜ ( 𝐴 𝑀 π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ↔ ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ) )
206 205 ralbidv ⊒ ( π‘₯ = ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) β†’ ( βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ↔ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ) )
207 206 rspcev ⊒ ( ( ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ∈ π‘Œ ∧ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 ( ( ⇝𝑑 β€˜ 𝐽 ) β€˜ 𝐹 ) ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) ) β†’ βˆƒ π‘₯ ∈ π‘Œ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )
208 53 202 207 syl2anc ⊒ ( πœ‘ β†’ βˆƒ π‘₯ ∈ π‘Œ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 𝑀 π‘₯ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 𝑀 𝑦 ) ) )