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	syl5bb	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 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 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) )