dchrisum0fno1

Description: The sum sum_ k <_ x , F ( x ) / sqrt k is divergent (i.e. not eventually bounded). Equation 9.4.30 of Shapiro, p. 383. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum2.g	$⊢ G = DChr (N)$
	rpvmasum2.d	$⊢ D = {Base}_{G}$
	rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum0f.f	$⊢ F = (b \in ℕ ⟼ \sum_{v \in \{q \in ℕ \| q ∥ b\}} X (L (v)))$
	dchrisum0f.x	$⊢ φ \to X \in D$
	dchrisum0flb.r	$⊢ φ \to X : {Base}_{Z} ⟶ ℝ$
	dchrisum0fno1.a	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})) \in 𝑂 (1)$
Assertion	dchrisum0fno1	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum2.g	$⊢ G = DChr (N)$
5		rpvmasum2.d	$⊢ D = {Base}_{G}$
6		rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum0f.f	$⊢ F = (b \in ℕ ⟼ \sum_{v \in \{q \in ℕ \| q ∥ b\}} X (L (v)))$
8		dchrisum0f.x	$⊢ φ \to X \in D$
9		dchrisum0flb.r	$⊢ φ \to X : {Base}_{Z} ⟶ ℝ$
10		dchrisum0fno1.a	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})) \in 𝑂 (1)$
11		logno1	$⊢ \neg (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1)$
12		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
13	12	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
14	13	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
15		2cnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
16		2ne0	$⊢ 2 \neq 0$
17	16	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 \neq 0$
18	14 15 17	divcan2d	$⊢ (φ \land x \in ℝ^{+}) \to 2 (\frac{\log x}{2}) = \log x$
19	18	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 (\frac{\log x}{2})) = (x \in ℝ^{+} ⟼ \log x)$
20	13	rehalfcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\log x}{2} \in ℝ$
21	20	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\log x}{2} \in ℂ$
22		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
23		2cn	$⊢ 2 \in ℂ$
24		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 2 \in ℂ) \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
25	22 23 24	mp2an	$⊢ (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
26	25	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
27		1red	$⊢ φ \to 1 \in ℝ$
28		sumex	$⊢ \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}}) \in V$
29	28	a1i	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}}) \in V$
30	20	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log x}{2} \in ℝ$
31	12	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℝ$
32		log1	$⊢ \log 1 = 0$
33		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
34		1rp	$⊢ 1 \in ℝ^{+}$
35		simprl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
36		logleb	$⊢ (1 \in ℝ^{+} \land x \in ℝ^{+}) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
37	34 35 36	sylancr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
38	33 37	mpbid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log 1 \leq \log x$
39	32 38	eqbrtrrid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \log x$
40		2re	$⊢ 2 \in ℝ$
41	40	a1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 \in ℝ$
42		2pos	$⊢ 0 < 2$
43	42	a1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 < 2$
44		divge0	$⊢ ((\log x \in ℝ \land 0 \leq \log x) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{\log x}{2}$
45	31 39 41 43 44	syl22anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \frac{\log x}{2}$
46	30 45	absidd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{\log x}{2}\| = \frac{\log x}{2}$
47		fzfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
48	1 2 3 4 5 6 7 8 9	dchrisum0ff	$⊢ φ \to F : ℕ ⟶ ℝ$
49	48	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to F : ℕ ⟶ ℝ$
50		elfznn	$⊢ k \in (1 \dots ⌊x⌋) \to k \in ℕ$
51		ffvelrn	$⊢ (F : ℕ ⟶ ℝ \land k \in ℕ) \to F (k) \in ℝ$
52	49 50 51	syl2an	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to F (k) \in ℝ$
53	50	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to k \in ℕ$
54	53	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to k \in ℝ^{+}$
55	54	rpsqrtcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to \sqrt{k} \in ℝ^{+}$
56	52 55	rerpdivcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to \frac{F (k)}{\sqrt{k}} \in ℝ$
57	47 56	fsumrecl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}}) \in ℝ$
58	57	recnd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}}) \in ℂ$
59	58	abscld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})\| \in ℝ$
60		fzfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊\sqrt{x}⌋) \in Fin$
61		elfznn	$⊢ i \in (1 \dots ⌊\sqrt{x}⌋) \to i \in ℕ$
62	61	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to i \in ℕ$
63	62	nnrecred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to \frac{1}{i} \in ℝ$
64	60 63	fsumrecl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i}) \in ℝ$
65		logsqrt	$⊢ x \in ℝ^{+} \to \log \sqrt{x} = \frac{\log x}{2}$
66	65	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log \sqrt{x} = \frac{\log x}{2}$
67		rpsqrtcl	$⊢ x \in ℝ^{+} \to \sqrt{x} \in ℝ^{+}$
68	67	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sqrt{x} \in ℝ^{+}$
69		harmoniclbnd	$⊢ \sqrt{x} \in ℝ^{+} \to \log \sqrt{x} \leq \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i})$
70	68 69	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log \sqrt{x} \leq \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i})$
71	66 70	eqbrtrrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log x}{2} \leq \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i})$
72		eqid	$⊢ (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) = (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})$
73		ovex	$⊢ m^{2} \in V$
74	72 73	elrnmpti	$⊢ k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) \leftrightarrow \exists m \in (1 \dots ⌊\sqrt{x}⌋) k = m^{2}$
75		elfznn	$⊢ m \in (1 \dots ⌊\sqrt{x}⌋) \to m \in ℕ$
76	75	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m \in ℕ$
77	76	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m \in ℝ^{+}$
78	77	rprege0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to (m \in ℝ \land 0 \leq m)$
79		sqrtsq	$⊢ (m \in ℝ \land 0 \leq m) \to \sqrt{m^{2}} = m$
80	78 79	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to \sqrt{m^{2}} = m$
81	80 76	eqeltrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to \sqrt{m^{2}} \in ℕ$
82		fveq2	$⊢ k = m^{2} \to \sqrt{k} = \sqrt{m^{2}}$
83	82	eleq1d	$⊢ k = m^{2} \to (\sqrt{k} \in ℕ \leftrightarrow \sqrt{m^{2}} \in ℕ)$
84	81 83	syl5ibrcom	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to (k = m^{2} \to \sqrt{k} \in ℕ)$
85	84	rexlimdva	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (\exists m \in (1 \dots ⌊\sqrt{x}⌋) k = m^{2} \to \sqrt{k} \in ℕ)$
86	74 85	syl5bi	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) \to \sqrt{k} \in ℕ)$
87	86	imp	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to \sqrt{k} \in ℕ$
88	87	iftrued	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to if (\sqrt{k} \in ℕ, 1, 0) = 1$
89	88	oveq1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} = \frac{1}{\sqrt{k}}$
90	89	sumeq2dv	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})} (\frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}}) = \sum_{k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})} (\frac{1}{\sqrt{k}})$
91		fveq2	$⊢ k = i^{2} \to \sqrt{k} = \sqrt{i^{2}}$
92	91	oveq2d	$⊢ k = i^{2} \to \frac{1}{\sqrt{k}} = \frac{1}{\sqrt{i^{2}}}$
93	76	nnsqcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m^{2} \in ℕ$
94	68	rpred	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sqrt{x} \in ℝ$
95		fznnfl	$⊢ \sqrt{x} \in ℝ \to (m \in (1 \dots ⌊\sqrt{x}⌋) \leftrightarrow (m \in ℕ \land m \leq \sqrt{x}))$
96	94 95	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (m \in (1 \dots ⌊\sqrt{x}⌋) \leftrightarrow (m \in ℕ \land m \leq \sqrt{x}))$
97	96	simplbda	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m \leq \sqrt{x}$
98	68	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to \sqrt{x} \in ℝ^{+}$
99	98	rprege0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to (\sqrt{x} \in ℝ \land 0 \leq \sqrt{x})$
100		le2sq	$⊢ ((m \in ℝ \land 0 \leq m) \land (\sqrt{x} \in ℝ \land 0 \leq \sqrt{x})) \to (m \leq \sqrt{x} \leftrightarrow m^{2} \leq {\sqrt{x}}^{2})$
101	78 99 100	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to (m \leq \sqrt{x} \leftrightarrow m^{2} \leq {\sqrt{x}}^{2})$
102	97 101	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m^{2} \leq {\sqrt{x}}^{2}$
103	35	rpred	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
104	103	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to x \in ℝ$
105	104	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to x \in ℂ$
106	105	sqsqrtd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to {\sqrt{x}}^{2} = x$
107	102 106	breqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m^{2} \leq x$
108		fznnfl	$⊢ x \in ℝ \to (m^{2} \in (1 \dots ⌊x⌋) \leftrightarrow (m^{2} \in ℕ \land m^{2} \leq x))$
109	104 108	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to (m^{2} \in (1 \dots ⌊x⌋) \leftrightarrow (m^{2} \in ℕ \land m^{2} \leq x))$
110	93 107 109	mpbir2and	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊\sqrt{x}⌋)) \to m^{2} \in (1 \dots ⌊x⌋)$
111	110	ex	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (m \in (1 \dots ⌊\sqrt{x}⌋) \to m^{2} \in (1 \dots ⌊x⌋))$
112	75	nnrpd	$⊢ m \in (1 \dots ⌊\sqrt{x}⌋) \to m \in ℝ^{+}$
113	112	rprege0d	$⊢ m \in (1 \dots ⌊\sqrt{x}⌋) \to (m \in ℝ \land 0 \leq m)$
114	61	nnrpd	$⊢ i \in (1 \dots ⌊\sqrt{x}⌋) \to i \in ℝ^{+}$
115	114	rprege0d	$⊢ i \in (1 \dots ⌊\sqrt{x}⌋) \to (i \in ℝ \land 0 \leq i)$
116		sq11	$⊢ ((m \in ℝ \land 0 \leq m) \land (i \in ℝ \land 0 \leq i)) \to (m^{2} = i^{2} \leftrightarrow m = i)$
117	113 115 116	syl2an	$⊢ (m \in (1 \dots ⌊\sqrt{x}⌋) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to (m^{2} = i^{2} \leftrightarrow m = i)$
118	117	a1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ((m \in (1 \dots ⌊\sqrt{x}⌋) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to (m^{2} = i^{2} \leftrightarrow m = i))$
119	111 118	dom2lem	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) \underset{1-1}{⟶} (1 \dots ⌊x⌋)$
120		f1f1orn	$⊢ (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) \underset{1-1}{⟶} (1 \dots ⌊x⌋) \to (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) \underset{1-1 onto}{⟶} ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})$
121	119 120	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) \underset{1-1 onto}{⟶} ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})$
122		oveq1	$⊢ m = i \to m^{2} = i^{2}$
123	122 72 73	fvmpt3i	$⊢ i \in (1 \dots ⌊\sqrt{x}⌋) \to (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) (i) = i^{2}$
124	123	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) (i) = i^{2}$
125		f1f	$⊢ (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) \underset{1-1}{⟶} (1 \dots ⌊x⌋) \to (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) ⟶ (1 \dots ⌊x⌋)$
126		frn	$⊢ (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) : (1 \dots ⌊\sqrt{x}⌋) ⟶ (1 \dots ⌊x⌋) \to ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) \subseteq (1 \dots ⌊x⌋)$
127	119 125 126	3syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) \subseteq (1 \dots ⌊x⌋)$
128	127	sselda	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to k \in (1 \dots ⌊x⌋)$
129		1re	$⊢ 1 \in ℝ$
130		0re	$⊢ 0 \in ℝ$
131	129 130	ifcli	$⊢ if (\sqrt{k} \in ℕ, 1, 0) \in ℝ$
132		rerpdivcl	$⊢ (if (\sqrt{k} \in ℕ, 1, 0) \in ℝ \land \sqrt{k} \in ℝ^{+}) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} \in ℝ$
133	131 55 132	sylancr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} \in ℝ$
134	133	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} \in ℂ$
135	128 134	syldan	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} \in ℂ$
136	89 135	eqeltrrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to \frac{1}{\sqrt{k}} \in ℂ$
137	92 60 121 124 136	fsumf1o	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})} (\frac{1}{\sqrt{k}}) = \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{\sqrt{i^{2}}})$
138	90 137	eqtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})} (\frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}}) = \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{\sqrt{i^{2}}})$
139		eldif	$⊢ k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \leftrightarrow (k \in (1 \dots ⌊x⌋) \land \neg k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))$
140	50	ad2antrl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to k \in ℕ$
141	140	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to k \in ℂ$
142	141	sqsqrtd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to {\sqrt{k}}^{2} = k$
143		simprr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to \sqrt{k} \in ℕ$
144		fznnfl	$⊢ x \in ℝ \to (k \in (1 \dots ⌊x⌋) \leftrightarrow (k \in ℕ \land k \leq x))$
145	103 144	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (k \in (1 \dots ⌊x⌋) \leftrightarrow (k \in ℕ \land k \leq x))$
146	145	simplbda	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to k \leq x$
147	146	adantrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to k \leq x$
148	140	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to k \in ℝ^{+}$
149	148	rprege0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to (k \in ℝ \land 0 \leq k)$
150	35	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to x \in ℝ^{+}$
151	150	rprege0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to (x \in ℝ \land 0 \leq x)$
152		sqrtle	$⊢ ((k \in ℝ \land 0 \leq k) \land (x \in ℝ \land 0 \leq x)) \to (k \leq x \leftrightarrow \sqrt{k} \leq \sqrt{x})$
153	149 151 152	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to (k \leq x \leftrightarrow \sqrt{k} \leq \sqrt{x})$
154	147 153	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to \sqrt{k} \leq \sqrt{x}$
155	68	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to \sqrt{x} \in ℝ^{+}$
156	155	rpred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to \sqrt{x} \in ℝ$
157		fznnfl	$⊢ \sqrt{x} \in ℝ \to (\sqrt{k} \in (1 \dots ⌊\sqrt{x}⌋) \leftrightarrow (\sqrt{k} \in ℕ \land \sqrt{k} \leq \sqrt{x}))$
158	156 157	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to (\sqrt{k} \in (1 \dots ⌊\sqrt{x}⌋) \leftrightarrow (\sqrt{k} \in ℕ \land \sqrt{k} \leq \sqrt{x}))$
159	143 154 158	mpbir2and	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to \sqrt{k} \in (1 \dots ⌊\sqrt{x}⌋)$
160	142 140	eqeltrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to {\sqrt{k}}^{2} \in ℕ$
161		oveq1	$⊢ m = \sqrt{k} \to m^{2} = {\sqrt{k}}^{2}$
162	72 161	elrnmpt1s	$⊢ (\sqrt{k} \in (1 \dots ⌊\sqrt{x}⌋) \land {\sqrt{k}}^{2} \in ℕ) \to {\sqrt{k}}^{2} \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})$
163	159 160 162	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to {\sqrt{k}}^{2} \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})$
164	142 163	eqeltrrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \sqrt{k} \in ℕ)) \to k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})$
165	164	expr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to (\sqrt{k} \in ℕ \to k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))$
166	165	con3d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to (\neg k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}) \to \neg \sqrt{k} \in ℕ)$
167	166	impr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (k \in (1 \dots ⌊x⌋) \land \neg k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to \neg \sqrt{k} \in ℕ$
168	139 167	sylan2b	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to \neg \sqrt{k} \in ℕ$
169	168	iffalsed	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to if (\sqrt{k} \in ℕ, 1, 0) = 0$
170	169	oveq1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} = \frac{0}{\sqrt{k}}$
171		eldifi	$⊢ k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})) \to k \in (1 \dots ⌊x⌋)$
172	171 55	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to \sqrt{k} \in ℝ^{+}$
173	172	rpcnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to (\sqrt{k} \in ℂ \land \sqrt{k} \neq 0)$
174		div0	$⊢ (\sqrt{k} \in ℂ \land \sqrt{k} \neq 0) \to \frac{0}{\sqrt{k}} = 0$
175	173 174	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to \frac{0}{\sqrt{k}} = 0$
176	170 175	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in ((1 \dots ⌊x⌋) ∖ ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2}))) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} = 0$
177	127 135 176 47	fsumss	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k \in ran (m \in (1 \dots ⌊\sqrt{x}⌋) ⟼ m^{2})} (\frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}}) = \sum_{k = 1}^{⌊x⌋} (\frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}})$
178	62	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to i \in ℝ^{+}$
179	178	rprege0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to (i \in ℝ \land 0 \leq i)$
180		sqrtsq	$⊢ (i \in ℝ \land 0 \leq i) \to \sqrt{i^{2}} = i$
181	179 180	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to \sqrt{i^{2}} = i$
182	181	oveq2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land i \in (1 \dots ⌊\sqrt{x}⌋)) \to \frac{1}{\sqrt{i^{2}}} = \frac{1}{i}$
183	182	sumeq2dv	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{\sqrt{i^{2}}}) = \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i})$
184	138 177 183	3eqtr3d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 1}^{⌊x⌋} (\frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}}) = \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i})$
185	131	a1i	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to if (\sqrt{k} \in ℕ, 1, 0) \in ℝ$
186	3	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to N \in ℕ$
187	8	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to X \in D$
188	9	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to X : {Base}_{Z} ⟶ ℝ$
189	1 2 186 4 5 6 7 187 188 53	dchrisum0flb	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to if (\sqrt{k} \in ℕ, 1, 0) \leq F (k)$
190	185 52 55 189	lediv1dd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to \frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}} \leq \frac{F (k)}{\sqrt{k}}$
191	47 133 56 190	fsumle	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 1}^{⌊x⌋} (\frac{if (\sqrt{k} \in ℕ, 1, 0)}{\sqrt{k}}) \leq \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})$
192	184 191	eqbrtrrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{i = 1}^{⌊\sqrt{x}⌋} (\frac{1}{i}) \leq \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})$
193	30 64 57 71 192	letrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log x}{2} \leq \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})$
194	57	leabsd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}}) \leq \|\sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})\|$
195	30 57 59 193 194	letrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log x}{2} \leq \|\sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})\|$
196	46 195	eqbrtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{\log x}{2}\| \leq \|\sum_{k = 1}^{⌊x⌋} (\frac{F (k)}{\sqrt{k}})\|$
197	27 10 29 21 196	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{\log x}{2}) \in 𝑂 (1)$
198	15 21 26 197	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 (\frac{\log x}{2})) \in 𝑂 (1)$
199	19 198	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1)$
200	11 199	mto	$⊢ \neg φ$

Metamath Proof Explorer

Theorem dchrisum0fno1

Proof