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

Metamath Proof Explorer

Theorem dchrisum0lema

Description: Lemma for dchrisum0 . Apply dchrisum for the function 1 / sqrt y . (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum2.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum2.1 ⊢ 1 = ( 0g ‘ 𝐺 )
rpvmasum2.w ⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
dchrisum0.b ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
dchrisum0lem1.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) )
Assertion dchrisum0lema ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum2.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum2.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 rpvmasum2.w ⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
8 dchrisum0.b ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
9 dchrisum0lem1.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) )
10 7 ssrab3 ⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
11 10 8 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
12 11 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
13 eldifsni ⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → 𝑋 ≠ 1 )
14 11 13 syl ⊢ ( 𝜑 → 𝑋 ≠ 1 )
15 fveq2 ⊢ ( 𝑛 = 𝑥 → ( √ ‘ 𝑛 ) = ( √ ‘ 𝑥 ) )
16 15 oveq2d ⊢ ( 𝑛 = 𝑥 → ( 1 / ( √ ‘ 𝑛 ) ) = ( 1 / ( √ ‘ 𝑥 ) ) )
17 1nn ⊢ 1 ∈ ℕ
18 17 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
19 rpsqrtcl ⊢ ( 𝑛 ∈ ℝ+ → ( √ ‘ 𝑛 ) ∈ ℝ+ )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → ( √ ‘ 𝑛 ) ∈ ℝ+ )
21 20 rprecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → ( 1 / ( √ ‘ 𝑛 ) ) ∈ ℝ )
22 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
23 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
24 23 rprege0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) )
25 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
26 25 rprege0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
27 sqrtle ⊢ ( ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( 𝑛 ≤ 𝑥 ↔ ( √ ‘ 𝑛 ) ≤ ( √ ‘ 𝑥 ) ) )
28 24 26 27 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝑛 ≤ 𝑥 ↔ ( √ ‘ 𝑛 ) ≤ ( √ ‘ 𝑥 ) ) )
29 22 28 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( √ ‘ 𝑛 ) ≤ ( √ ‘ 𝑥 ) )
30 23 rpsqrtcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( √ ‘ 𝑛 ) ∈ ℝ+ )
31 25 rpsqrtcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
32 30 31 lerecd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( ( √ ‘ 𝑛 ) ≤ ( √ ‘ 𝑥 ) ↔ ( 1 / ( √ ‘ 𝑥 ) ) ≤ ( 1 / ( √ ‘ 𝑛 ) ) ) )
33 29 32 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → ( 1 / ( √ ‘ 𝑥 ) ) ≤ ( 1 / ( √ ‘ 𝑛 ) ) )
34 sqrtlim ⊢ ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑛 ) ) ) ⇝𝑟 0
35 34 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑛 ) ) ) ⇝𝑟 0 )
36 2fveq3 ⊢ ( 𝑎 = 𝑛 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
37 fveq2 ⊢ ( 𝑎 = 𝑛 → ( √ ‘ 𝑎 ) = ( √ ‘ 𝑛 ) )
38 37 oveq2d ⊢ ( 𝑎 = 𝑛 → ( 1 / ( √ ‘ 𝑎 ) ) = ( 1 / ( √ ‘ 𝑛 ) ) )
39 36 38 oveq12d ⊢ ( 𝑎 = 𝑛 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / ( √ ‘ 𝑛 ) ) ) )
40 39 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / ( √ ‘ 𝑛 ) ) ) )
41 1 2 3 4 5 6 12 14 16 18 21 33 35 40 dchrisum ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) )
42 12 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
43 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
45 4 1 5 2 42 44 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
47 46 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ+ )
48 47 rpsqrtcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 𝑛 ) ∈ ℝ+ )
49 48 rpcnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 𝑛 ) ∈ ℂ )
50 48 rpne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 𝑛 ) ≠ 0 )
51 45 49 50 divrecd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / ( √ ‘ 𝑛 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / ( √ ‘ 𝑛 ) ) ) )
52 51 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / ( √ ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( 1 / ( √ ‘ 𝑛 ) ) ) ) )
53 36 37 oveq12d ⊢ ( 𝑎 = 𝑛 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / ( √ ‘ 𝑛 ) ) )
54 53 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / ( √ ‘ 𝑛 ) ) )
55 9 54 eqtri ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / ( √ ‘ 𝑛 ) ) )
56 52 55 40 3eqtr4g ⊢ ( 𝜑 → 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) )
57 56 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) = seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) )
58 57 breq1d ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ↔ seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ⇝ 𝑡 ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ↔ seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ⇝ 𝑡 ) )
60 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
61 60 fvoveq1d ⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
62 fveq2 ⊢ ( 𝑦 = 𝑥 → ( √ ‘ 𝑦 ) = ( √ ‘ 𝑥 ) )
63 62 oveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑐 / ( √ ‘ 𝑦 ) ) = ( 𝑐 / ( √ ‘ 𝑥 ) ) )
64 61 63 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑥 ) ) ) )
65 64 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑥 ) ) )
66 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) )
67 66 seqeq3d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) = seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) )
68 67 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) = ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) )
69 68 fvoveq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
70 elrege0 ⊢ ( 𝑐 ∈ ( 0 [,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ 0 ≤ 𝑐 ) )
71 70 simplbi ⊢ ( 𝑐 ∈ ( 0 [,) +∞ ) → 𝑐 ∈ ℝ )
72 71 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑐 ∈ ℝ )
73 72 recnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑐 ∈ ℂ )
74 1re ⊢ 1 ∈ ℝ
75 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
76 74 75 ax-mp ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
77 76 simplbi ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ )
78 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ )
79 0red ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 ∈ ℝ )
80 1red ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ )
81 0lt1 ⊢ 0 < 1
82 81 a1i ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 < 1 )
83 76 simprbi ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑥 )
84 83 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
85 79 80 78 82 84 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 < 𝑥 )
86 78 85 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ+ )
87 86 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
88 87 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ∈ ℂ )
89 87 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ≠ 0 )
90 73 88 89 divrecd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 𝑐 / ( √ ‘ 𝑥 ) ) = ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) )
91 69 90 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑥 ) ) ↔ ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) )
92 91 ralbidva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) )
93 65 92 bitrid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) )
94 59 93 anbi12d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 0 [,) +∞ ) ) → ( ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ↔ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) ) )
95 94 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ↔ ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) ) )
96 95 exbidv ⊢ ( 𝜑 → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ↔ ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 1 / ( √ ‘ 𝑎 ) ) ) ) ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( 1 / ( √ ‘ 𝑥 ) ) ) ) ) )
97 41 96 mpbird ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) )