Theorem dchrisumlem3

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-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 )
	dchrisum.2	⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
	dchrisum.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	dchrisum.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
	dchrisum.5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
	dchrisum.6	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
	dchrisum.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
	dchrisum.9	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
	dchrisum.10	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
Assertion	dchrisumlem3	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 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		dchrisum.2	⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
10		dchrisum.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11		dchrisum.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
12		dchrisum.5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
13		dchrisum.6	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
14		dchrisum.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
15		dchrisum.9	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
16		dchrisum.10	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
17		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
18		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
20	7	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
21	19	nnzd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℤ )
22	4 1 5 2 20 21	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ∈ ℂ )
23	11	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
24		nnrp	⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ+ )
25		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴
26	25	nfel1	⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ
27		csbeq1a	⊢ ( 𝑛 = 𝑖 → 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
28	27	eleq1d	⊢ ( 𝑛 = 𝑖 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
29	26 28	rspc	⊢ ( 𝑖 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
30	29	impcom	⊢ ( ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
31	23 24 30	syl2an	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
32	31	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℂ )
33	22 32	mulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
34		nfcv	⊢ Ⅎ 𝑛 𝑖
35		nfcv	⊢ Ⅎ 𝑛 ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) )
36		nfcv	⊢ Ⅎ 𝑛 ·
37	35 36 25	nfov	⊢ Ⅎ 𝑛 ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
38		2fveq3	⊢ ( 𝑛 = 𝑖 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
39	38 27	oveq12d	⊢ ( 𝑛 = 𝑖 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
40	34 37 39 14	fvmptf	⊢ ( ( 𝑖 ∈ ℕ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
41	19 33 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
42	41 33	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
43	17 18 42	serf	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
44	43	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
45	11	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
46	45	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℂ )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℂ )
48		id	⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ+ )
49		2re	⊢ 2 ∈ ℝ
50		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 2 · 𝑅 ) ∈ ℝ )
51	49 15 50	sylancr	⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ℝ )
52		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
53	3 52	sylibr	⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑁 ) )
54		oveq2	⊢ ( 𝑢 = 0 → ( 0 ..^ 𝑢 ) = ( 0 ..^ 0 ) )
55		fzo0	⊢ ( 0 ..^ 0 ) = ∅
56	54 55	eqtrdi	⊢ ( 𝑢 = 0 → ( 0 ..^ 𝑢 ) = ∅ )
57	56	sumeq1d	⊢ ( 𝑢 = 0 → Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ∅ ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
58		sum0	⊢ Σ 𝑛 ∈ ∅ ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0
59	57 58	eqtrdi	⊢ ( 𝑢 = 0 → Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
60	59	abs00bd	⊢ ( 𝑢 = 0 → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = 0 )
61	60	breq1d	⊢ ( 𝑢 = 0 → ( ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 ↔ 0 ≤ 𝑅 ) )
62	61	rspcv	⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 → 0 ≤ 𝑅 ) )
63	53 16 62	sylc	⊢ ( 𝜑 → 0 ≤ 𝑅 )
64		0le2	⊢ 0 ≤ 2
65		mulge0	⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ) → 0 ≤ ( 2 · 𝑅 ) )
66	49 64 65	mpanl12	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 0 ≤ ( 2 · 𝑅 ) )
67	15 63 66	syl2anc	⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑅 ) )
68	51 67	ge0p1rpd	⊢ ( 𝜑 → ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ+ )
69		rpdivcl	⊢ ( ( 𝑒 ∈ ℝ+ ∧ ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ+ ) → ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ∈ ℝ+ )
70	48 68 69	syl2anr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ∈ ℝ+ )
71	13	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
72	47 70 71	rlimi	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑚 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
73		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑚 ∈ ℝ )
74	10	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℝ )
76	73 75	ifcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ )
77		0red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 0 ∈ ℝ )
78	10	nngt0d	⊢ ( 𝜑 → 0 < 𝑀 )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 0 < 𝑀 )
80		max1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
81	74 80	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
82	77 75 76 79 81	ltletrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 0 < if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
83	76 82	elrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ )
84	83	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ )
85		nfv	⊢ Ⅎ 𝑛 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 )
86		nfcv	⊢ Ⅎ 𝑛 abs
87		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴
88		nfcv	⊢ Ⅎ 𝑛 −
89		nfcv	⊢ Ⅎ 𝑛 0
90	87 88 89	nfov	⊢ Ⅎ 𝑛 ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 )
91	86 90	nffv	⊢ Ⅎ 𝑛 ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) )
92		nfcv	⊢ Ⅎ 𝑛 <
93		nfcv	⊢ Ⅎ 𝑛 ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) )
94	91 92 93	nfbr	⊢ Ⅎ 𝑛 ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) )
95	85 94	nfim	⊢ Ⅎ 𝑛 ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) )
96		breq2	⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( 𝑚 ≤ 𝑛 ↔ 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) )
97		csbeq1a	⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → 𝐴 = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
98	97	fvoveq1d	⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( 𝐴 − 0 ) ) = ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) )
99	98	breq1d	⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ↔ ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
100	96 99	imbi12d	⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ↔ ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ) )
101	95 100	rspc	⊢ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ) )
102	84 101	syl	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ) )
103	74	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℝ )
104		max2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
105	103 104	sylancom	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
106	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
107	87	nfel1	⊢ Ⅎ 𝑛 ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ
108	97	eleq1d	⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( 𝐴 ∈ ℝ ↔ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
109	107 108	rspc	⊢ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
110	84 106 109	sylc	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
111	110	recnd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℂ )
112	111	subid1d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
113	112	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) = ( abs ‘ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
114	76	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ )
115	103 80	sylancom	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
116		elicopnf	⊢ ( 𝑀 ∈ ℝ → ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) ↔ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
117	103 116	syl	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) ↔ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
118	114 115 117	mpbir2and	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) )
119	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑁 ∈ ℕ )
120	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑋 ∈ 𝐷 )
121	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑋 ≠ 1 )
122	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℕ )
123	11	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
124		simpll	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝜑 )
125	124 12	syl3an1	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
126	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
127	1 2 119 4 5 6 120 121 9 122 123 125 126 14	dchrisumlema	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ) )
128	127	simprd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
129	118 128	mpd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 0 ≤ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
130	110 129	absidd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( abs ‘ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
131	113 130	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
132	131	breq1d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ↔ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
133		rpre	⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ )
134	133	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑒 ∈ ℝ )
135	68	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ+ )
136	110 134 135	ltmuldiv2d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ↔ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
137	132 136	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ↔ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
138	51	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( 2 · 𝑅 ) ∈ ℝ )
139	135	rpred	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ )
140	138	lep1d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( 2 · 𝑅 ) ≤ ( ( 2 · 𝑅 ) + 1 ) )
141	138 139 110 129 140	lemul1ad	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
142	138 110	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
143	139 110	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
144		lelttr	⊢ ( ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
145	142 143 134 144	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
146	141 145	mpand	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
147	137 146	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
148		1red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 1 ∈ ℝ )
149	10	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℕ )
150	149	nnge1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 1 ≤ 𝑀 )
151	148 75 76 150 81	letrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 1 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
152		flge1nn	⊢ ( ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ ∧ 1 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
153	76 151 152	syl2anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
154	153	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
155	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑁 ∈ ℕ )
156	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑋 ∈ 𝐷 )
157	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑋 ≠ 1 )
158	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑀 ∈ ℕ )
159	11	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
160	12	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
161	160	3adant1r	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
162	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
163	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑅 ∈ ℝ )
164	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
165	83	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ )
166	81	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
167	76	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ )
168		fllep1	⊢ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ≤ ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) + 1 ) )
169	167 168	syl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ≤ ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) + 1 ) )
170	153	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
171		simpr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
172	1 2 155 4 5 6 156 157 9 158 159 161 162 14 163 164 165 166 169 170 171	dchrisumlem2	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
173	172	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
174	43	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
175		eluznn	⊢ ( ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑘 ∈ ℕ )
176	154 175	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑘 ∈ ℕ )
177	174 176	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
178	154	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
179	174 178	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ∈ ℂ )
180	177 179	subcld	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ∈ ℂ )
181	180	abscld	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ∈ ℝ )
182	142	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
183	134	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑒 ∈ ℝ )
184		lelttr	⊢ ( ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ∈ ℝ ∧ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
185	181 182 183 184	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
186	173 185	mpand	⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
187	186	ralrimdva	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
188		fveq2	⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
189		fveq2	⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
190	189	oveq2d	⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) )
191	190	fveq2d	⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) )
192	191	breq1d	⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
193	188 192	raleqbidv	⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
194	193	rspcev	⊢ ( ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 )
195	154 187 194	syl6an	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
196	147 195	syld	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
197	105 196	embantd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
198	102 197	syld	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
199	198	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
200	72 199	mpd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 )
201	200	ralrimiva	⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 )
202		seqex	⊢ seq 1 ( + , 𝐹 ) ∈ V
203	202	a1i	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ V )
204	17 44 201 203	caucvg	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
205	202	eldm	⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ ∃ 𝑡 seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
206	204 205	sylib	⊢ ( 𝜑 → ∃ 𝑡 seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
207		simpr	⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
208		elrege0	⊢ ( ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 2 · 𝑅 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑅 ) ) )
209	51 67 208	sylanbrc	⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) )
210	209	adantr	⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) )
211		eqid	⊢ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) = ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) )
212		pnfxr	⊢ +∞ ∈ ℝ*
213		icossre	⊢ ( ( 𝑀 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑀 [,) +∞ ) ⊆ ℝ )
214	74 212 213	sylancl	⊢ ( 𝜑 → ( 𝑀 [,) +∞ ) ⊆ ℝ )
215	214	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ )
216	215	adantlr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ )
217	216	flcld	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℤ )
218		simplr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
219	43	ad2antrr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
220		1red	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 1 ∈ ℝ )
221	74	ad2antrr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℝ )
222	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℕ )
223	222	nnge1d	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 1 ≤ 𝑀 )
224		elicopnf	⊢ ( 𝑀 ∈ ℝ → ( 𝑚 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚 ) ) )
225	74 224	syl	⊢ ( 𝜑 → ( 𝑚 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚 ) ) )
226	225	simplbda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝑚 )
227	226	adantlr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝑚 )
228	220 221 216 223 227	letrd	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 1 ≤ 𝑚 )
229		flge1nn	⊢ ( ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
230	216 228 229	syl2anc	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
231	219 230	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ ℂ )
232		nnex	⊢ ℕ ∈ V
233	232	mptex	⊢ ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ∈ V
234	233	a1i	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ∈ V )
235	219	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
236		eluznn	⊢ ( ( ( ⌊ ‘ 𝑚 ) ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑖 ∈ ℕ )
237	230 236	sylan	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑖 ∈ ℕ )
238	235 237	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ∈ ℂ )
239		fveq2	⊢ ( 𝑘 = 𝑖 → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) )
240	239	oveq2d	⊢ ( 𝑘 = 𝑖 → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
241		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) )
242		ovex	⊢ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ∈ V
243	240 241 242	fvmpt3i	⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
244	237 243	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
245	211 217 218 231 234 238 244	climsubc2	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ⇝ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) )
246	232	mptex	⊢ ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ∈ V
247	246	a1i	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ∈ V )
248		fvex	⊢ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ V
249	248	fvconst2	⊢ ( 𝑖 ∈ ℕ → ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
250	237 249	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
251	250	oveq1d	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
252	244 251	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
253	231	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ ℂ )
254	250 253	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) ∈ ℂ )
255	254 238	subcld	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ∈ ℂ )
256	252 255	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
257	240	fveq2d	⊢ ( 𝑘 = 𝑖 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
258		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) )
259		fvex	⊢ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ∈ V
260	257 258 259	fvmpt3i	⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
261	237 260	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
262	244	fveq2d	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
263	261 262	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) ) )
264	211 245 247 217 256 263	climabs	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ⇝ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) )
265	51	ad2antrr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 2 · 𝑅 ) ∈ ℝ )
266		0red	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 0 ∈ ℝ )
267	74	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℝ )
268	78	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 0 < 𝑀 )
269	266 267 215 268 226	ltletrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 0 < 𝑚 )
270	215 269	elrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ+ )
271		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
272	271	nfel1	⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ
273		csbeq1a	⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
274	273	eleq1d	⊢ ( 𝑛 = 𝑚 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
275	272 274	rspc	⊢ ( 𝑚 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
276	23 275	mpan9	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ )
277	270 276	syldan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ )
278	277	adantlr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ )
279	265 278	remulcld	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
280	279	recnd	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
281		1z	⊢ 1 ∈ ℤ
282	17	eqimss2i	⊢ ( ℤ≥ ‘ 1 ) ⊆ ℕ
283	282 232	climconst2	⊢ ( ( ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ⇝ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
284	280 281 283	sylancl	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ⇝ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
285	253 238	subcld	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ∈ ℂ )
286	285	abscld	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) ∈ ℝ )
287	261 286	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ∈ ℝ )
288		ovex	⊢ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V
289	288	fvconst2	⊢ ( 𝑖 ∈ ℕ → ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) = ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
290	237 289	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) = ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
291	279	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
292	290 291	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) ∈ ℝ )
293		simplll	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝜑 )
294	293 3	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑁 ∈ ℕ )
295	293 7	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑋 ∈ 𝐷 )
296	293 8	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑋 ≠ 1 )
297	222	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑀 ∈ ℕ )
298	293 11	sylan	⊢ ( ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
299	293 12	syl3an1	⊢ ( ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
300	293 13	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
301	293 15	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑅 ∈ ℝ )
302	293 16	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
303	270	adantlr	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ+ )
304	303	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 ∈ ℝ+ )
305	227	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑀 ≤ 𝑚 )
306	216	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 ∈ ℝ )
307		reflcl	⊢ ( 𝑚 ∈ ℝ → ( ⌊ ‘ 𝑚 ) ∈ ℝ )
308		peano2re	⊢ ( ( ⌊ ‘ 𝑚 ) ∈ ℝ → ( ( ⌊ ‘ 𝑚 ) + 1 ) ∈ ℝ )
309	306 307 308	3syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ⌊ ‘ 𝑚 ) + 1 ) ∈ ℝ )
310		flltp1	⊢ ( 𝑚 ∈ ℝ → 𝑚 < ( ( ⌊ ‘ 𝑚 ) + 1 ) )
311	306 310	syl	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 < ( ( ⌊ ‘ 𝑚 ) + 1 ) )
312	306 309 311	ltled	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 ≤ ( ( ⌊ ‘ 𝑚 ) + 1 ) )
313	230	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
314		simpr	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) )
315	1 2 294 4 5 6 295 296 9 297 298 299 300 14 301 302 304 305 312 313 314	dchrisumlem2	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
316	253 238	abssubd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
317	261 316	eqtrd	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
318	315 317 290	3brtr4d	⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ≤ ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) )
319	211 217 264 284 287 292 318	climle	⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
320	319	ralrimiva	⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
321		oveq1	⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( 𝑐 · 𝐵 ) = ( ( 2 · 𝑅 ) · 𝐵 ) )
322	321	breq2d	⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) ) )
323	322	ralbidv	⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) ) )
324		2fveq3	⊢ ( 𝑚 = 𝑥 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
325	324	fvoveq1d	⊢ ( 𝑚 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
326		vex	⊢ 𝑚 ∈ V
327	326	a1i	⊢ ( 𝑚 = 𝑥 → 𝑚 ∈ V )
328		equequ2	⊢ ( 𝑚 = 𝑥 → ( 𝑛 = 𝑚 ↔ 𝑛 = 𝑥 ) )
329	328	biimpa	⊢ ( ( 𝑚 = 𝑥 ∧ 𝑛 = 𝑚 ) → 𝑛 = 𝑥 )
330	329 9	syl	⊢ ( ( 𝑚 = 𝑥 ∧ 𝑛 = 𝑚 ) → 𝐴 = 𝐵 )
331	327 330	csbied	⊢ ( 𝑚 = 𝑥 → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 = 𝐵 )
332	331	oveq2d	⊢ ( 𝑚 = 𝑥 → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( ( 2 · 𝑅 ) · 𝐵 ) )
333	325 332	breq12d	⊢ ( 𝑚 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) ) )
334	333	cbvralvw	⊢ ( ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ↔ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) )
335	323 334	bitr4di	⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ↔ ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) )
336	335	rspcev	⊢ ( ( ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) )
337	210 320 336	syl2anc	⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) )
338		r19.42v	⊢ ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) ↔ ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∃ 𝑐 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )
339	207 337 338	sylanbrc	⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )
340	339	ex	⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) ) )
341	340	eximdv	⊢ ( 𝜑 → ( ∃ 𝑡 seq 1 ( + , 𝐹 ) ⇝ 𝑡 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) ) )
342	206 341	mpd	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )