dchrisum0re

Description: Suppose X is a non-principal Dirichlet character with sum_ n e. NN , X ( n ) / n = 0 . Then X is a real character. Part of Lemma 9.4.4 of Shapiro, p. 382. (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}$
	rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
	dchrisum0.b	$⊢ φ \to X \in W$
Assertion	dchrisum0re	$⊢ φ \to X : {Base}_{Z} ⟶ ℝ$

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		rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
8		dchrisum0.b	$⊢ φ \to X \in W$
9		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
10	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
11	10 8	sselid	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
12	11	eldifad	$⊢ φ \to X \in D$
13	4 1 5 9 12	dchrf	$⊢ φ \to X : {Base}_{Z} ⟶ ℂ$
14	13	ffnd	$⊢ φ \to X Fn {Base}_{Z}$
15	13	ffvelcdmda	$⊢ (φ \land x \in {Base}_{Z}) \to X (x) \in ℂ$
16		fvco3	$⊢ (X : {Base}_{Z} ⟶ ℂ \land x \in {Base}_{Z}) \to (* \circ X) (x) = \overline{X (x)}$
17	13 16	sylan	$⊢ (φ \land x \in {Base}_{Z}) \to (* \circ X) (x) = \overline{X (x)}$
18		logno1	$⊢ \neg (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1)$
19		1red	$⊢ (φ \land * \circ X \neq X) \to 1 \in ℝ$
20		eqid	$⊢ Unit (Z) = Unit (Z)$
21	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
22	1	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
23	21 22	syl	$⊢ φ \to Z \in CRing$
24		crngring	$⊢ Z \in CRing \to Z \in Ring$
25	23 24	syl	$⊢ φ \to Z \in Ring$
26		eqid	$⊢ 1_{Z} = 1_{Z}$
27	20 26	1unit	$⊢ Z \in Ring \to 1_{Z} \in Unit (Z)$
28	25 27	syl	$⊢ φ \to 1_{Z} \in Unit (Z)$
29		eqid	$⊢ L^{-1} [\{1_{Z}\}] = L^{-1} [\{1_{Z}\}]$
30		eqidd	$⊢ (φ \land f \in W) \to 1_{Z} = 1_{Z}$
31	1 2 3 4 5 6 7 20 28 29 30	rpvmasum2	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)) \in 𝑂 (1)$
32	31	adantr	$⊢ (φ \land * \circ X \neq X) \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)) \in 𝑂 (1)$
33	3	phicld	$⊢ φ \to ϕ (N) \in ℕ$
34	33	nnnn0d	$⊢ φ \to ϕ (N) \in ℕ_{0}$
35	34	adantr	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \in ℕ_{0}$
36	35	nn0red	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \in ℝ$
37		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
38		inss1	$⊢ (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}] \subseteq (1 \dots ⌊x⌋)$
39		ssfi	$⊢ ((1 \dots ⌊x⌋) \in Fin \land (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}] \subseteq (1 \dots ⌊x⌋)) \to (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}] \in Fin$
40	37 38 39	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}] \in Fin$
41		elinel1	$⊢ n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]) \to n \in (1 \dots ⌊x⌋)$
42		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
43	42	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
44	41 43	sylan2	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to n \in ℕ$
45		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
46		nndivre	$⊢ (Λ (n) \in ℝ \land n \in ℕ) \to \frac{Λ (n)}{n} \in ℝ$
47	45 46	mpancom	$⊢ n \in ℕ \to \frac{Λ (n)}{n} \in ℝ$
48	44 47	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to \frac{Λ (n)}{n} \in ℝ$
49	40 48	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \in ℝ$
50	36 49	remulcld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \in ℝ$
51		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
52	51	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
53		1re	$⊢ 1 \in ℝ$
54	4 5	dchrfi	$⊢ N \in ℕ \to D \in Fin$
55	3 54	syl	$⊢ φ \to D \in Fin$
56		difss	$⊢ D ∖ \{\underset{˙}{1}\} \subseteq D$
57	10 56	sstri	$⊢ W \subseteq D$
58		ssfi	$⊢ (D \in Fin \land W \subseteq D) \to W \in Fin$
59	55 57 58	sylancl	$⊢ φ \to W \in Fin$
60		hashcl	$⊢ W \in Fin \to \|W\| \in ℕ_{0}$
61	59 60	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
62	61	nn0red	$⊢ φ \to \|W\| \in ℝ$
63		resubcl	$⊢ (1 \in ℝ \land \|W\| \in ℝ) \to 1 - \|W\| \in ℝ$
64	53 62 63	sylancr	$⊢ φ \to 1 - \|W\| \in ℝ$
65	64	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 1 - \|W\| \in ℝ$
66	52 65	remulcld	$⊢ (φ \land x \in ℝ^{+}) \to \log x (1 - \|W\|) \in ℝ$
67	50 66	resubcld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|) \in ℝ$
68	67	recnd	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|) \in ℂ$
69	68	adantlr	$⊢ ((φ \land * \circ X \neq X) \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|) \in ℂ$
70	51	adantl	$⊢ ((φ \land * \circ X \neq X) \land x \in ℝ^{+}) \to \log x \in ℝ$
71	70	recnd	$⊢ ((φ \land * \circ X \neq X) \land x \in ℝ^{+}) \to \log x \in ℂ$
72	51	ad2antrl	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℝ$
73	66	ad2ant2r	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x (1 - \|W\|) \in ℝ$
74	72 73	readdcld	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x + \log x (1 - \|W\|) \in ℝ$
75		0red	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \in ℝ$
76	50	ad2ant2r	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \in ℝ$
77		2re	$⊢ 2 \in ℝ$
78	77	a1i	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 \in ℝ$
79	62	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \|W\| \in ℝ$
80	78 79	resubcld	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 - \|W\| \in ℝ$
81		log1	$⊢ \log 1 = 0$
82		simprr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
83		1rp	$⊢ 1 \in ℝ^{+}$
84		simprl	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
85		logleb	$⊢ (1 \in ℝ^{+} \land x \in ℝ^{+}) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
86	83 84 85	sylancr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
87	82 86	mpbid	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log 1 \leq \log x$
88	81 87	eqbrtrrid	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \log x$
89	59	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to W \in Fin$
90		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
91	4 5 12 90	dchrinv	$⊢ φ \to {inv}_{g} (G) (X) = * \circ X$
92	4	dchrabl	$⊢ N \in ℕ \to G \in Abel$
93	3 92	syl	$⊢ φ \to G \in Abel$
94		ablgrp	$⊢ G \in Abel \to G \in Grp$
95	93 94	syl	$⊢ φ \to G \in Grp$
96	5 90	grpinvcl	$⊢ (G \in Grp \land X \in D) \to {inv}_{g} (G) (X) \in D$
97	95 12 96	syl2anc	$⊢ φ \to {inv}_{g} (G) (X) \in D$
98	91 97	eqeltrrd	$⊢ φ \to * \circ X \in D$
99		eldifsni	$⊢ X \in (D ∖ \{\underset{˙}{1}\}) \to X \neq \underset{˙}{1}$
100	11 99	syl	$⊢ φ \to X \neq \underset{˙}{1}$
101	5 6	grpidcl	$⊢ G \in Grp \to \underset{˙}{1} \in D$
102	95 101	syl	$⊢ φ \to \underset{˙}{1} \in D$
103	5 90 95 12 102	grpinv11	$⊢ φ \to ({inv}_{g} (G) (X) = {inv}_{g} (G) (\underset{˙}{1}) \leftrightarrow X = \underset{˙}{1})$
104	103	necon3bid	$⊢ φ \to ({inv}_{g} (G) (X) \neq {inv}_{g} (G) (\underset{˙}{1}) \leftrightarrow X \neq \underset{˙}{1})$
105	100 104	mpbird	$⊢ φ \to {inv}_{g} (G) (X) \neq {inv}_{g} (G) (\underset{˙}{1})$
106	6 90	grpinvid	$⊢ G \in Grp \to {inv}_{g} (G) (\underset{˙}{1}) = \underset{˙}{1}$
107	95 106	syl	$⊢ φ \to {inv}_{g} (G) (\underset{˙}{1}) = \underset{˙}{1}$
108	105 91 107	3netr3d	$⊢ φ \to * \circ X \neq \underset{˙}{1}$
109		eldifsn	$⊢ * \circ X \in (D ∖ \{\underset{˙}{1}\}) \leftrightarrow (* \circ X \in D \land * \circ X \neq \underset{˙}{1})$
110	98 108 109	sylanbrc	$⊢ φ \to * \circ X \in (D ∖ \{\underset{˙}{1}\})$
111		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
112		1zzd	$⊢ φ \to 1 \in ℤ$
113		2fveq3	$⊢ n = m \to X (L (n)) = X (L (m))$
114		id	$⊢ n = m \to n = m$
115	113 114	oveq12d	$⊢ n = m \to \frac{X (L (n))}{n} = \frac{X (L (m))}{m}$
116	115	fveq2d	$⊢ n = m \to \overline{\frac{X (L (n))}{n}} = \overline{\frac{X (L (m))}{m}}$
117		eqid	$⊢ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}}) = (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})$
118		fvex	$⊢ \overline{\frac{X (L (m))}{m}} \in V$
119	116 117 118	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}}) (m) = \overline{\frac{X (L (m))}{m}}$
120	119	adantl	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}}) (m) = \overline{\frac{X (L (m))}{m}}$
121		nnre	$⊢ m \in ℕ \to m \in ℝ$
122	121	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℝ$
123	122	cjred	$⊢ (φ \land m \in ℕ) \to \overline{m} = m$
124	123	oveq2d	$⊢ (φ \land m \in ℕ) \to \frac{\overline{X (L (m))}}{\overline{m}} = \frac{\overline{X (L (m))}}{m}$
125	13	adantr	$⊢ (φ \land m \in ℕ) \to X : {Base}_{Z} ⟶ ℂ$
126	1 9 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
127	21 126	syl	$⊢ φ \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
128		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
129	127 128	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
130		nnz	$⊢ m \in ℕ \to m \in ℤ$
131		ffvelcdm	$⊢ (L : ℤ ⟶ {Base}_{Z} \land m \in ℤ) \to L (m) \in {Base}_{Z}$
132	129 130 131	syl2an	$⊢ (φ \land m \in ℕ) \to L (m) \in {Base}_{Z}$
133	125 132	ffvelcdmd	$⊢ (φ \land m \in ℕ) \to X (L (m)) \in ℂ$
134		nncn	$⊢ m \in ℕ \to m \in ℂ$
135	134	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
136		nnne0	$⊢ m \in ℕ \to m \neq 0$
137	136	adantl	$⊢ (φ \land m \in ℕ) \to m \neq 0$
138	133 135 137	cjdivd	$⊢ (φ \land m \in ℕ) \to \overline{\frac{X (L (m))}{m}} = \frac{\overline{X (L (m))}}{\overline{m}}$
139		fvco3	$⊢ (X : {Base}_{Z} ⟶ ℂ \land L (m) \in {Base}_{Z}) \to (* \circ X) (L (m)) = \overline{X (L (m))}$
140	125 132 139	syl2anc	$⊢ (φ \land m \in ℕ) \to (* \circ X) (L (m)) = \overline{X (L (m))}$
141	140	oveq1d	$⊢ (φ \land m \in ℕ) \to \frac{(* \circ X) (L (m))}{m} = \frac{\overline{X (L (m))}}{m}$
142	124 138 141	3eqtr4d	$⊢ (φ \land m \in ℕ) \to \overline{\frac{X (L (m))}{m}} = \frac{(* \circ X) (L (m))}{m}$
143	120 142	eqtrd	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}}) (m) = \frac{(* \circ X) (L (m))}{m}$
144	133	cjcld	$⊢ (φ \land m \in ℕ) \to \overline{X (L (m))} \in ℂ$
145	144 135 137	divcld	$⊢ (φ \land m \in ℕ) \to \frac{\overline{X (L (m))}}{m} \in ℂ$
146	141 145	eqeltrd	$⊢ (φ \land m \in ℕ) \to \frac{(* \circ X) (L (m))}{m} \in ℂ$
147		eqid	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{a}) = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
148	1 2 3 4 5 6 12 100 147	dchrmusumlema	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y})$
149		simprrl	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t$
150	8	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to X \in W$
151	3	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to N \in ℕ$
152	12	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to X \in D$
153	100	adantr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to X \neq \underset{˙}{1}$
154		simprl	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to c \in [0, +∞)$
155		simprrr	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}$
156	1 2 151 4 5 6 152 153 147 154 149 155 7	dchrvmaeq0	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (X \in W \leftrightarrow t = 0)$
157	150 156	mpbid	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to t = 0$
158	149 157	breqtrd	$⊢ (φ \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ 0$
159	158	rexlimdvaa	$⊢ φ \to (\exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ 0)$
160	159	exlimdv	$⊢ φ \to (\exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ 0)$
161	148 160	mpd	$⊢ φ \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) ⇝ 0$
162		seqex	$⊢ seq 1 (+ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})) \in V$
163	162	a1i	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})) \in V$
164		2fveq3	$⊢ a = m \to X (L (a)) = X (L (m))$
165		id	$⊢ a = m \to a = m$
166	164 165	oveq12d	$⊢ a = m \to \frac{X (L (a))}{a} = \frac{X (L (m))}{m}$
167		ovex	$⊢ \frac{X (L (m))}{m} \in V$
168	166 147 167	fvmpt	$⊢ m \in ℕ \to (a \in ℕ ⟼ \frac{X (L (a))}{a}) (m) = \frac{X (L (m))}{m}$
169	168	adantl	$⊢ (φ \land m \in ℕ) \to (a \in ℕ ⟼ \frac{X (L (a))}{a}) (m) = \frac{X (L (m))}{m}$
170	133 135 137	divcld	$⊢ (φ \land m \in ℕ) \to \frac{X (L (m))}{m} \in ℂ$
171	169 170	eqeltrd	$⊢ (φ \land m \in ℕ) \to (a \in ℕ ⟼ \frac{X (L (a))}{a}) (m) \in ℂ$
172	111 112 171	serf	$⊢ φ \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) : ℕ ⟶ ℂ$
173	172	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (k) \in ℂ$
174		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots k) \in Fin$
175		simpl	$⊢ (φ \land k \in ℕ) \to φ$
176		elfznn	$⊢ m \in (1 \dots k) \to m \in ℕ$
177	175 176 170	syl2an	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to \frac{X (L (m))}{m} \in ℂ$
178	174 177	fsumcj	$⊢ (φ \land k \in ℕ) \to \overline{\sum_{m = 1}^{k} (\frac{X (L (m))}{m})} = \sum_{m = 1}^{k} \overline{\frac{X (L (m))}{m}}$
179	175 176 169	syl2an	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to (a \in ℕ ⟼ \frac{X (L (a))}{a}) (m) = \frac{X (L (m))}{m}$
180		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
181	180 111	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
182	179 181 177	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} (\frac{X (L (m))}{m}) = seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (k)$
183	182	fveq2d	$⊢ (φ \land k \in ℕ) \to \overline{\sum_{m = 1}^{k} (\frac{X (L (m))}{m})} = \overline{seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (k)}$
184	175 176 120	syl2an	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}}) (m) = \overline{\frac{X (L (m))}{m}}$
185	170	cjcld	$⊢ (φ \land m \in ℕ) \to \overline{\frac{X (L (m))}{m}} \in ℂ$
186	175 176 185	syl2an	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to \overline{\frac{X (L (m))}{m}} \in ℂ$
187	184 181 186	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} \overline{\frac{X (L (m))}{m}} = seq 1 (+ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})) (k)$
188	178 183 187	3eqtr3rd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})) (k) = \overline{seq 1 (+ (a \in ℕ ⟼ \frac{X (L (a))}{a})) (k)}$
189	111 161 163 112 173 188	climcj	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})) ⇝ \overline{0}$
190		cj0	$⊢ \overline{0} = 0$
191	189 190	breqtrdi	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ \overline{\frac{X (L (n))}{n}})) ⇝ 0$
192	111 112 143 146 191	isumclim	$⊢ φ \to \sum_{m \in ℕ} (\frac{(* \circ X) (L (m))}{m}) = 0$
193		fveq1	$⊢ y = * \circ X \to y (L (m)) = (* \circ X) (L (m))$
194	193	oveq1d	$⊢ y = * \circ X \to \frac{y (L (m))}{m} = \frac{(* \circ X) (L (m))}{m}$
195	194	sumeq2sdv	$⊢ y = * \circ X \to \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = \sum_{m \in ℕ} (\frac{(* \circ X) (L (m))}{m})$
196	195	eqeq1d	$⊢ y = * \circ X \to (\sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0 \leftrightarrow \sum_{m \in ℕ} (\frac{(* \circ X) (L (m))}{m}) = 0)$
197	196 7	elrab2	$⊢ * \circ X \in W \leftrightarrow (* \circ X \in (D ∖ \{\underset{˙}{1}\}) \land \sum_{m \in ℕ} (\frac{(* \circ X) (L (m))}{m}) = 0)$
198	110 192 197	sylanbrc	$⊢ φ \to * \circ X \in W$
199	198	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to * \circ X \in W$
200	8	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to X \in W$
201		simplr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to * \circ X \neq X$
202	89 199 200 201	nehash2	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 \leq \|W\|$
203		suble0	$⊢ (2 \in ℝ \land \|W\| \in ℝ) \to (2 - \|W\| \leq 0 \leftrightarrow 2 \leq \|W\|)$
204	77 79 203	sylancr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to (2 - \|W\| \leq 0 \leftrightarrow 2 \leq \|W\|)$
205	202 204	mpbird	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 - \|W\| \leq 0$
206	80 75 72 88 205	lemul2ad	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x (2 - \|W\|) \leq \log x \cdot 0$
207		df-2	$⊢ 2 = 1 + 1$
208	207	oveq1i	$⊢ 2 - \|W\| = 1 + 1 - \|W\|$
209		1cnd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℂ$
210	79	recnd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \|W\| \in ℂ$
211	209 209 210	addsubassd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 + 1 - \|W\| = 1 + 1 - \|W\|$
212	208 211	eqtrid	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 - \|W\| = 1 + 1 - \|W\|$
213	212	oveq2d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x (2 - \|W\|) = \log x (1 + 1 - \|W\|)$
214	71	adantrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℂ$
215	64	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 - \|W\| \in ℝ$
216	215	recnd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 - \|W\| \in ℂ$
217	214 209 216	adddid	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x (1 + 1 - \|W\|) = \log x \cdot 1 + \log x (1 - \|W\|)$
218	214	mulridd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \cdot 1 = \log x$
219	218	oveq1d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \cdot 1 + \log x (1 - \|W\|) = \log x + \log x (1 - \|W\|)$
220	213 217 219	3eqtrd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x (2 - \|W\|) = \log x + \log x (1 - \|W\|)$
221	214	mul01d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \cdot 0 = 0$
222	206 220 221	3brtr3d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x + \log x (1 - \|W\|) \leq 0$
223	33	nnred	$⊢ φ \to ϕ (N) \in ℝ$
224	223	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to ϕ (N) \in ℝ$
225	49	ad2ant2r	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \in ℝ$
226	34	ad2antrr	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to ϕ (N) \in ℕ_{0}$
227	226	nn0ge0d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq ϕ (N)$
228	44 45	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to Λ (n) \in ℝ$
229		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
230	44 229	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to 0 \leq Λ (n)$
231	44	nnred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to n \in ℝ$
232	44	nngt0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to 0 < n$
233		divge0	$⊢ ((Λ (n) \in ℝ \land 0 \leq Λ (n)) \land (n \in ℝ \land 0 < n)) \to 0 \leq \frac{Λ (n)}{n}$
234	228 230 231 232 233	syl22anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}])) \to 0 \leq \frac{Λ (n)}{n}$
235	40 48 234	fsumge0	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n})$
236	235	ad2ant2r	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n})$
237	224 225 227 236	mulge0d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n})$
238	74 75 76 222 237	letrd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x + \log x (1 - \|W\|) \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n})$
239		leaddsub	$⊢ (\log x \in ℝ \land \log x (1 - \|W\|) \in ℝ \land ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \in ℝ) \to (\log x + \log x (1 - \|W\|) \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \leftrightarrow \log x \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|))$
240	72 73 76 239	syl3anc	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to (\log x + \log x (1 - \|W\|) \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) \leftrightarrow \log x \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|))$
241	238 240	mpbid	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)$
242	72 88	absidd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log x\| = \log x$
243	67	ad2ant2r	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|) \in ℝ$
244	75 72 243 88 241	letrd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)$
245	243 244	absidd	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \|ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)\| = ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)$
246	241 242 245	3brtr4d	$⊢ ((φ \land * \circ X \neq X) \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log x\| \leq \|ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap L^{-1} [\{1_{Z}\}]} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)\|$
247	19 32 69 71 246	o1le	$⊢ (φ \land * \circ X \neq X) \to (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1)$
248	247	ex	$⊢ φ \to (* \circ X \neq X \to (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1))$
249	248	necon1bd	$⊢ φ \to (\neg (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to * \circ X = X)$
250	18 249	mpi	$⊢ φ \to * \circ X = X$
251	250	adantr	$⊢ (φ \land x \in {Base}_{Z}) \to * \circ X = X$
252	251	fveq1d	$⊢ (φ \land x \in {Base}_{Z}) \to (* \circ X) (x) = X (x)$
253	17 252	eqtr3d	$⊢ (φ \land x \in {Base}_{Z}) \to \overline{X (x)} = X (x)$
254	15 253	cjrebd	$⊢ (φ \land x \in {Base}_{Z}) \to X (x) \in ℝ$
255	254	ralrimiva	$⊢ φ \to \forall x \in {Base}_{Z} X (x) \in ℝ$
256		ffnfv	$⊢ X : {Base}_{Z} ⟶ ℝ \leftrightarrow (X Fn {Base}_{Z} \land \forall x \in {Base}_{Z} X (x) \in ℝ)$
257	14 255 256	sylanbrc	$⊢ φ \to X : {Base}_{Z} ⟶ ℝ$

Metamath Proof Explorer

Theorem dchrisum0re

Proof