This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrmusumlema

Description: Lemma for dchrmusum and dchrisumn0 . Apply dchrisum for the function 1 / y . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrisumn0.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
Assertion dchrmusumlema ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrisumn0.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 1 / 𝑛 ) = ( 1 / 𝑥 ) )
11 1nn ⊢ 1 ∈ ℕ
12 11 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
13 rpreccl ⊢ ( 𝑛 ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ+ )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
15 14 rpred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → ( 1 / 𝑛 ) ∈ ℝ )
16 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
17 rpregt0 ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
18 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
19 lerec ⊢ ( ( ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( 𝑛 ≤ 𝑥 ↔ ( 1 / 𝑥 ) ≤ ( 1 / 𝑛 ) ) )
20 17 18 19 syl2an ⊢ ( ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑛 ≤ 𝑥 ↔ ( 1 / 𝑥 ) ≤ ( 1 / 𝑛 ) ) )
21 20 3ad2ant2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑛 ≤ 𝑥 ↔ ( 1 / 𝑥 ) ≤ ( 1 / 𝑛 ) ) )
22 16 21 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 1 / 𝑥 ) ≤ ( 1 / 𝑛 ) )
23 ax-1cn ⊢ 1 ∈ ℂ
24 divrcnv ⊢ ( 1 ∈ ℂ → ( 𝑛 ∈ ℝ+ ↦ ( 1 / 𝑛 ) ) ⇝𝑟 0 )
25 23 24 mp1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ ( 1 / 𝑛 ) ) ⇝𝑟 0 )
26 2fveq3 ⊢ ( 𝑎 = 𝑛 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
27 oveq2 ⊢ ( 𝑎 = 𝑛 → ( 1 / 𝑎 ) = ( 1 / 𝑛 ) )
28 26 27 oveq12d ⊢ ( 𝑎 = 𝑛 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / 𝑛 ) ) )
29 28 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / 𝑛 ) ) )
30 1 2 3 4 5 6 7 8 10 12 15 22 25 29 dchrisum ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) )
31 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
32 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
34 4 1 5 2 31 33 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
35 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
37 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
39 34 36 38 divrecd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / 𝑛 ) ) )
40 39 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / 𝑛 ) ) ) )
41 id ⊢ ( 𝑎 = 𝑛 → 𝑎 = 𝑛 )
42 26 41 oveq12d ⊢ ( 𝑎 = 𝑛 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) )
43 42 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) )
44 9 43 eqtri ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) )
45 40 44 29 3eqtr4g ⊢ ( 𝜑 → 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) )
47 46 seqeq3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) = seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) )
48 47 breq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ↔ seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ⇝ 𝑡 ) )
49 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
50 49 fvoveq1d ⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
51 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑐 / 𝑦 ) = ( 𝑐 / 𝑥 ) )
52 50 51 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑥 ) ) )
53 52 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑥 ) )
54 45 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) = seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) )
55 54 fveq1d ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) = ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) )
56 55 fvoveq1d ⊢ ( 𝜑 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
58 elrege0 ⊢ ( 𝑐 ∈ ( 0 [,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ 0 ≤ 𝑐 ) )
59 58 simplbi ⊢ ( 𝑐 ∈ ( 0 [,) +∞ ) → 𝑐 ∈ ℝ )
60 59 recnd ⊢ ( 𝑐 ∈ ( 0 [,) +∞ ) → 𝑐 ∈ ℂ )
61 60 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑐 ∈ ℂ )
62 1re ⊢ 1 ∈ ℝ
63 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
64 62 63 ax-mp ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
65 64 simplbi ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ )
66 65 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ )
67 66 recnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℂ )
68 0red ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 ∈ ℝ )
69 1red ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ )
70 0lt1 ⊢ 0 < 1
71 70 a1i ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 < 1 )
72 64 simprbi ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑥 )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
74 68 69 66 71 73 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 < 𝑥 )
75 74 gt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ≠ 0 )
76 61 67 75 divrecd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 𝑐 / 𝑥 ) = ( 𝑐 · ( 1 / 𝑥 ) ) )
77 57 76 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑥 ) ↔ ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) )
78 77 ralbidva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑥 ) ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) )
79 53 78 bitrid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) )
80 48 79 anbi12d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ↔ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) ) )
81 80 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ↔ ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) ) )
82 81 exbidv ⊢ ( 𝜑 → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ↔ ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / 𝑥 ) ) ) ) )
83 30 82 mpbird ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) )