o1fsum

Description: If A ( k ) is O(1), then sum_ k <_ x , A ( k ) is O( x ). (Contributed by Mario Carneiro, 23-May-2016)

	Ref	Expression
Hypotheses	o1fsum.1	$⊢ (φ \land k \in ℕ) \to A \in V$
	o1fsum.2	$⊢ φ \to (k \in ℕ ⟼ A) \in 𝑂 (1)$
Assertion	o1fsum	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{\sum_{k = 1}^{⌊x⌋} A}{x}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		o1fsum.1	$⊢ (φ \land k \in ℕ) \to A \in V$
2		o1fsum.2	$⊢ φ \to (k \in ℕ ⟼ A) \in 𝑂 (1)$
3		nnssre	$⊢ ℕ \subseteq ℝ$
4	3	a1i	$⊢ φ \to ℕ \subseteq ℝ$
5	1 2	o1mptrcl	$⊢ (φ \land k \in ℕ) \to A \in ℂ$
6		1red	$⊢ φ \to 1 \in ℝ$
7	4 5 6	elo1mpt2	$⊢ φ \to ((k \in ℕ ⟼ A) \in 𝑂 (1) \leftrightarrow \exists c \in [1, +∞) \exists m \in ℝ \forall k \in ℕ (c \leq k \to \|A\| \leq m))$
8	2 7	mpbid	$⊢ φ \to \exists c \in [1, +∞) \exists m \in ℝ \forall k \in ℕ (c \leq k \to \|A\| \leq m)$
9		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
10	9	a1i	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to ℝ^{+} \subseteq ℝ$
11		nfcv	$⊢ \underline{Ⅎ} n A$
12		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ A$
13		csbeq1a	$⊢ k = n \to A = ⦋ n / k ⦌ A$
14	11 12 13	cbvsumi	$⊢ \sum_{k = 1}^{⌊x⌋} A = \sum_{n = 1}^{⌊x⌋} ⦋ n / k ⦌ A$
15		fzfid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
16		o1f	$⊢ (k \in ℕ ⟼ A) \in 𝑂 (1) \to (k \in ℕ ⟼ A) : dom (k \in ℕ ⟼ A) ⟶ ℂ$
17	2 16	syl	$⊢ φ \to (k \in ℕ ⟼ A) : dom (k \in ℕ ⟼ A) ⟶ ℂ$
18	1	ralrimiva	$⊢ φ \to \forall k \in ℕ A \in V$
19		dmmptg	$⊢ \forall k \in ℕ A \in V \to dom (k \in ℕ ⟼ A) = ℕ$
20	18 19	syl	$⊢ φ \to dom (k \in ℕ ⟼ A) = ℕ$
21	20	feq2d	$⊢ φ \to ((k \in ℕ ⟼ A) : dom (k \in ℕ ⟼ A) ⟶ ℂ \leftrightarrow (k \in ℕ ⟼ A) : ℕ ⟶ ℂ)$
22	17 21	mpbid	$⊢ φ \to (k \in ℕ ⟼ A) : ℕ ⟶ ℂ$
23		eqid	$⊢ (k \in ℕ ⟼ A) = (k \in ℕ ⟼ A)$
24	23	fmpt	$⊢ \forall k \in ℕ A \in ℂ \leftrightarrow (k \in ℕ ⟼ A) : ℕ ⟶ ℂ$
25	22 24	sylibr	$⊢ φ \to \forall k \in ℕ A \in ℂ$
26	25	ad3antrrr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to \forall k \in ℕ A \in ℂ$
27		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
28	12	nfel1	$⊢ Ⅎ k ⦋ n / k ⦌ A \in ℂ$
29	13	eleq1d	$⊢ k = n \to (A \in ℂ \leftrightarrow ⦋ n / k ⦌ A \in ℂ)$
30	28 29	rspc	$⊢ n \in ℕ \to (\forall k \in ℕ A \in ℂ \to ⦋ n / k ⦌ A \in ℂ)$
31	30	impcom	$⊢ (\forall k \in ℕ A \in ℂ \land n \in ℕ) \to ⦋ n / k ⦌ A \in ℂ$
32	26 27 31	syl2an	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to ⦋ n / k ⦌ A \in ℂ$
33	15 32	fsumcl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ⦋ n / k ⦌ A \in ℂ$
34	14 33	eqeltrid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to \sum_{k = 1}^{⌊x⌋} A \in ℂ$
35		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
36	35	adantl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to x \in ℂ$
37		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
38	37	adantl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to x \neq 0$
39	34 36 38	divcld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to \frac{\sum_{k = 1}^{⌊x⌋} A}{x} \in ℂ$
40		simplrl	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to c \in [1, +∞)$
41		1re	$⊢ 1 \in ℝ$
42		elicopnf	$⊢ 1 \in ℝ \to (c \in [1, +∞) \leftrightarrow (c \in ℝ \land 1 \leq c))$
43	41 42	ax-mp	$⊢ c \in [1, +∞) \leftrightarrow (c \in ℝ \land 1 \leq c)$
44	40 43	sylib	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to (c \in ℝ \land 1 \leq c)$
45	44	simpld	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to c \in ℝ$
46		fzfid	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to (1 \dots ⌊c⌋) \in Fin$
47	25	ad2antrr	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to \forall k \in ℕ A \in ℂ$
48		elfznn	$⊢ n \in (1 \dots ⌊c⌋) \to n \in ℕ$
49	47 48 31	syl2an	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land n \in (1 \dots ⌊c⌋)) \to ⦋ n / k ⦌ A \in ℂ$
50	49	abscld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land n \in (1 \dots ⌊c⌋)) \to \|⦋ n / k ⦌ A\| \in ℝ$
51	46 50	fsumrecl	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℝ$
52		simplrr	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to m \in ℝ$
53	51 52	readdcld	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m \in ℝ$
54	34 36 38	absdivd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land x \in ℝ^{+}) \to \|\frac{\sum_{k = 1}^{⌊x⌋} A}{x}\| = \frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{\|x\|}$
55	54	adantrr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\frac{\sum_{k = 1}^{⌊x⌋} A}{x}\| = \frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{\|x\|}$
56		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
57	56	ad2antrl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (x \in ℝ \land 0 \leq x)$
58		absid	$⊢ (x \in ℝ \land 0 \leq x) \to \|x\| = x$
59	57 58	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|x\| = x$
60	59	oveq2d	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{\|x\|} = \frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{x}$
61	55 60	eqtrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\frac{\sum_{k = 1}^{⌊x⌋} A}{x}\| = \frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{x}$
62	34	adantrr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{k = 1}^{⌊x⌋} A \in ℂ$
63	62	abscld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\sum_{k = 1}^{⌊x⌋} A\| \in ℝ$
64		fzfid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
65	47 27 31	syl2an	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land n \in (1 \dots ⌊x⌋)) \to ⦋ n / k ⦌ A \in ℂ$
66	65	adantlr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (1 \dots ⌊x⌋)) \to ⦋ n / k ⦌ A \in ℂ$
67	66	abscld	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \|⦋ n / k ⦌ A\| \in ℝ$
68	64 67	fsumrecl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \in ℝ$
69	57	simpld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to x \in ℝ$
70	51	adantr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℝ$
71	52	adantr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to m \in ℝ$
72	70 71	readdcld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m \in ℝ$
73	69 72	remulcld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to x (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m) \in ℝ$
74	14	fveq2i	$⊢ \|\sum_{k = 1}^{⌊x⌋} A\| = \|\sum_{n = 1}^{⌊x⌋} ⦋ n / k ⦌ A\|$
75	64 66	fsumabs	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} ⦋ n / k ⦌ A\| \leq \sum_{n = 1}^{⌊x⌋} \|⦋ n / k ⦌ A\|$
76	74 75	eqbrtrid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\sum_{k = 1}^{⌊x⌋} A\| \leq \sum_{n = 1}^{⌊x⌋} \|⦋ n / k ⦌ A\|$
77		fzfid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (⌊c⌋ + 1 \dots ⌊x⌋) \in Fin$
78		ssun2	$⊢ (⌊c⌋ + 1 \dots ⌊x⌋) \subseteq (1 \dots ⌊c⌋) \cup (⌊c⌋ + 1 \dots ⌊x⌋)$
79		flge1nn	$⊢ (c \in ℝ \land 1 \leq c) \to ⌊c⌋ \in ℕ$
80	44 79	syl	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to ⌊c⌋ \in ℕ$
81	80	adantr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ \in ℕ$
82	81	nnred	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ \in ℝ$
83	45	adantr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to c \in ℝ$
84		flle	$⊢ c \in ℝ \to ⌊c⌋ \leq c$
85	83 84	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ \leq c$
86		simprr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to c \leq x$
87	82 83 69 85 86	letrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ \leq x$
88		fznnfl	$⊢ x \in ℝ \to (⌊c⌋ \in (1 \dots ⌊x⌋) \leftrightarrow (⌊c⌋ \in ℕ \land ⌊c⌋ \leq x))$
89	69 88	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (⌊c⌋ \in (1 \dots ⌊x⌋) \leftrightarrow (⌊c⌋ \in ℕ \land ⌊c⌋ \leq x))$
90	81 87 89	mpbir2and	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ \in (1 \dots ⌊x⌋)$
91		fzsplit	$⊢ ⌊c⌋ \in (1 \dots ⌊x⌋) \to (1 \dots ⌊x⌋) = (1 \dots ⌊c⌋) \cup (⌊c⌋ + 1 \dots ⌊x⌋)$
92	90 91	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (1 \dots ⌊x⌋) = (1 \dots ⌊c⌋) \cup (⌊c⌋ + 1 \dots ⌊x⌋)$
93	78 92	sseqtrrid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (⌊c⌋ + 1 \dots ⌊x⌋) \subseteq (1 \dots ⌊x⌋)$
94	93	sselda	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (⌊c⌋ + 1 \dots ⌊x⌋)) \to n \in (1 \dots ⌊x⌋)$
95	65	abscld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land n \in (1 \dots ⌊x⌋)) \to \|⦋ n / k ⦌ A\| \in ℝ$
96	95	adantlr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \|⦋ n / k ⦌ A\| \in ℝ$
97	94 96	syldan	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (⌊c⌋ + 1 \dots ⌊x⌋)) \to \|⦋ n / k ⦌ A\| \in ℝ$
98	77 97	fsumrecl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \in ℝ$
99	69 70	remulcld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to x \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℝ$
100	69 71	remulcld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to x m \in ℝ$
101	70	recnd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℂ$
102	101	mulid2d	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to 1 \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| = \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|$
103		1red	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to 1 \in ℝ$
104	49	absge0d	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land n \in (1 \dots ⌊c⌋)) \to 0 \leq \|⦋ n / k ⦌ A\|$
105	46 50 104	fsumge0	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to 0 \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|$
106	51 105	jca	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℝ \land 0 \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|)$
107	106	adantr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℝ \land 0 \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|)$
108	44	simprd	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to 1 \leq c$
109	108	adantr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to 1 \leq c$
110	103 83 69 109 86	letrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to 1 \leq x$
111		lemul1a	$⊢ ((1 \in ℝ \land x \in ℝ \land (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \in ℝ \land 0 \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|)) \land 1 \leq x) \to 1 \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \leq x \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|$
112	103 69 107 110 111	syl31anc	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to 1 \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \leq x \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|$
113	102 112	eqbrtrrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| \leq x \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\|$
114		hashcl	$⊢ (⌊c⌋ + 1 \dots ⌊x⌋) \in Fin \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \in ℕ_{0}$
115		nn0re	$⊢ \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \in ℕ_{0} \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \in ℝ$
116	77 114 115	3syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \in ℝ$
117	116 71	remulcld	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| m \in ℝ$
118	71	adantr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (⌊c⌋ + 1 \dots ⌊x⌋)) \to m \in ℝ$
119		elfzuz	$⊢ n \in (⌊c⌋ + 1 \dots ⌊x⌋) \to n \in ℤ_{\geq (⌊c⌋ + 1)}$
120	81	peano2nnd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ + 1 \in ℕ$
121		eluznn	$⊢ (⌊c⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to n \in ℕ$
122	120 121	sylan	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to n \in ℕ$
123		simpllr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to \forall k \in ℕ (c \leq k \to \|A\| \leq m)$
124	83	adantr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to c \in ℝ$
125		reflcl	$⊢ c \in ℝ \to ⌊c⌋ \in ℝ$
126		peano2re	$⊢ ⌊c⌋ \in ℝ \to ⌊c⌋ + 1 \in ℝ$
127	124 125 126	3syl	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to ⌊c⌋ + 1 \in ℝ$
128	122	nnred	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to n \in ℝ$
129		fllep1	$⊢ c \in ℝ \to c \leq ⌊c⌋ + 1$
130	124 129	syl	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to c \leq ⌊c⌋ + 1$
131		eluzle	$⊢ n \in ℤ_{\geq (⌊c⌋ + 1)} \to ⌊c⌋ + 1 \leq n$
132	131	adantl	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to ⌊c⌋ + 1 \leq n$
133	124 127 128 130 132	letrd	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to c \leq n$
134		nfv	$⊢ Ⅎ k c \leq n$
135		nfcv	$⊢ \underline{Ⅎ} k abs$
136	135 12	nffv	$⊢ \underline{Ⅎ} k \|⦋ n / k ⦌ A\|$
137		nfcv	$⊢ \underline{Ⅎ} k \leq$
138		nfcv	$⊢ \underline{Ⅎ} k m$
139	136 137 138	nfbr	$⊢ Ⅎ k \|⦋ n / k ⦌ A\| \leq m$
140	134 139	nfim	$⊢ Ⅎ k (c \leq n \to \|⦋ n / k ⦌ A\| \leq m)$
141		breq2	$⊢ k = n \to (c \leq k \leftrightarrow c \leq n)$
142	13	fveq2d	$⊢ k = n \to \|A\| = \|⦋ n / k ⦌ A\|$
143	142	breq1d	$⊢ k = n \to (\|A\| \leq m \leftrightarrow \|⦋ n / k ⦌ A\| \leq m)$
144	141 143	imbi12d	$⊢ k = n \to ((c \leq k \to \|A\| \leq m) \leftrightarrow (c \leq n \to \|⦋ n / k ⦌ A\| \leq m))$
145	140 144	rspc	$⊢ n \in ℕ \to (\forall k \in ℕ (c \leq k \to \|A\| \leq m) \to (c \leq n \to \|⦋ n / k ⦌ A\| \leq m))$
146	122 123 133 145	syl3c	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to \|⦋ n / k ⦌ A\| \leq m$
147	119 146	sylan2	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (⌊c⌋ + 1 \dots ⌊x⌋)) \to \|⦋ n / k ⦌ A\| \leq m$
148	77 97 118 147	fsumle	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \leq \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} m$
149	71	recnd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to m \in ℂ$
150		fsumconst	$⊢ ((⌊c⌋ + 1 \dots ⌊x⌋) \in Fin \land m \in ℂ) \to \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} m = \|(⌊c⌋ + 1 \dots ⌊x⌋)\| m$
151	77 149 150	syl2anc	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} m = \|(⌊c⌋ + 1 \dots ⌊x⌋)\| m$
152	148 151	breqtrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \leq \|(⌊c⌋ + 1 \dots ⌊x⌋)\| m$
153		biidd	$⊢ n = ⌊c⌋ + 1 \to (0 \leq m \leftrightarrow 0 \leq m)$
154		0red	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to 0 \in ℝ$
155	47 30	mpan9	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land n \in ℕ) \to ⦋ n / k ⦌ A \in ℂ$
156	155	adantlr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℕ) \to ⦋ n / k ⦌ A \in ℂ$
157	122 156	syldan	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to ⦋ n / k ⦌ A \in ℂ$
158	157	abscld	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to \|⦋ n / k ⦌ A\| \in ℝ$
159	71	adantr	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to m \in ℝ$
160	157	absge0d	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to 0 \leq \|⦋ n / k ⦌ A\|$
161	154 158 159 160 146	letrd	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in ℤ_{\geq (⌊c⌋ + 1)}) \to 0 \leq m$
162	161	ralrimiva	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \forall n \in ℤ_{\geq (⌊c⌋ + 1)} 0 \leq m$
163	120	nnzd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ + 1 \in ℤ$
164		uzid	$⊢ ⌊c⌋ + 1 \in ℤ \to ⌊c⌋ + 1 \in ℤ_{\geq (⌊c⌋ + 1)}$
165	163 164	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊c⌋ + 1 \in ℤ_{\geq (⌊c⌋ + 1)}$
166	153 162 165	rspcdva	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to 0 \leq m$
167		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
168	69 167	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊x⌋ \in ℝ$
169		ssdomg	$⊢ (1 \dots ⌊x⌋) \in Fin \to ((⌊c⌋ + 1 \dots ⌊x⌋) \subseteq (1 \dots ⌊x⌋) \to (⌊c⌋ + 1 \dots ⌊x⌋) ≼ (1 \dots ⌊x⌋))$
170	64 93 169	sylc	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (⌊c⌋ + 1 \dots ⌊x⌋) ≼ (1 \dots ⌊x⌋)$
171		hashdomi	$⊢ (⌊c⌋ + 1 \dots ⌊x⌋) ≼ (1 \dots ⌊x⌋) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \leq \|(1 \dots ⌊x⌋)\|$
172	170 171	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \leq \|(1 \dots ⌊x⌋)\|$
173		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
174		hashfz1	$⊢ ⌊x⌋ \in ℕ_{0} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
175	57 173 174	3syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
176	172 175	breqtrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \leq ⌊x⌋$
177		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
178	69 177	syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to ⌊x⌋ \leq x$
179	116 168 69 176 178	letrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| \leq x$
180	116 69 71 166 179	lemul1ad	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|(⌊c⌋ + 1 \dots ⌊x⌋)\| m \leq x m$
181	98 117 100 152 180	letrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \leq x m$
182	70 98 99 100 113 181	le2addd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \leq x \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + x m$
183		ltp1	$⊢ ⌊c⌋ \in ℝ \to ⌊c⌋ < ⌊c⌋ + 1$
184		fzdisj	$⊢ ⌊c⌋ < ⌊c⌋ + 1 \to (1 \dots ⌊c⌋) \cap (⌊c⌋ + 1 \dots ⌊x⌋) = \emptyset$
185	82 183 184	3syl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (1 \dots ⌊c⌋) \cap (⌊c⌋ + 1 \dots ⌊x⌋) = \emptyset$
186	96	recnd	$⊢ ((((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \|⦋ n / k ⦌ A\| \in ℂ$
187	185 92 64 186	fsumsplit	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| = \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + \sum_{n = ⌊c⌋ + 1}^{⌊x⌋} \|⦋ n / k ⦌ A\|$
188	36	adantrr	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to x \in ℂ$
189	188 101 149	adddid	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to x (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m) = x \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + x m$
190	182 187 189	3brtr4d	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \sum_{n = 1}^{⌊x⌋} \|⦋ n / k ⦌ A\| \leq x (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m)$
191	63 68 73 76 190	letrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\sum_{k = 1}^{⌊x⌋} A\| \leq x (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m)$
192		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
193	192	ad2antrl	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (x \in ℝ \land 0 < x)$
194		ledivmul	$⊢ (\|\sum_{k = 1}^{⌊x⌋} A\| \in ℝ \land \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m \in ℝ \land (x \in ℝ \land 0 < x)) \to (\frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{x} \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m \leftrightarrow \|\sum_{k = 1}^{⌊x⌋} A\| \leq x (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m))$
195	63 72 193 194	syl3anc	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to (\frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{x} \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m \leftrightarrow \|\sum_{k = 1}^{⌊x⌋} A\| \leq x (\sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m))$
196	191 195	mpbird	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \frac{\|\sum_{k = 1}^{⌊x⌋} A\|}{x} \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m$
197	61 196	eqbrtrd	$⊢ (((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \land (x \in ℝ^{+} \land c \leq x)) \to \|\frac{\sum_{k = 1}^{⌊x⌋} A}{x}\| \leq \sum_{n = 1}^{⌊c⌋} \|⦋ n / k ⦌ A\| + m$
198	10 39 45 53 197	elo1d	$⊢ ((φ \land (c \in [1, +∞) \land m \in ℝ)) \land \forall k \in ℕ (c \leq k \to \|A\| \leq m)) \to (x \in ℝ^{+} ⟼ \frac{\sum_{k = 1}^{⌊x⌋} A}{x}) \in 𝑂 (1)$
199	198	ex	$⊢ (φ \land (c \in [1, +∞) \land m \in ℝ)) \to (\forall k \in ℕ (c \leq k \to \|A\| \leq m) \to (x \in ℝ^{+} ⟼ \frac{\sum_{k = 1}^{⌊x⌋} A}{x}) \in 𝑂 (1))$
200	199	rexlimdvva	$⊢ φ \to (\exists c \in [1, +∞) \exists m \in ℝ \forall k \in ℕ (c \leq k \to \|A\| \leq m) \to (x \in ℝ^{+} ⟼ \frac{\sum_{k = 1}^{⌊x⌋} A}{x}) \in 𝑂 (1))$
201	8 200	mpd	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{\sum_{k = 1}^{⌊x⌋} A}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem o1fsum

Proof