dchrvmasum2if

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrvmasum.a	$⊢ φ \to A \in ℝ^{+}$
	dchrvmasum2.2	$⊢ φ \to 1 \leq A$
Assertion	dchrvmasum2if	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m})$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrvmasum.a	$⊢ φ \to A \in ℝ^{+}$
10		dchrvmasum2.2	$⊢ φ \to 1 \leq A$
11		fzfid	$⊢ φ \to (1 \dots ⌊A⌋) \in Fin$
12	7	adantr	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X \in D$
13		elfzelz	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℤ$
14	13	adantl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℤ$
15	4 1 5 2 12 14	dchrzrhcl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) \in ℂ$
16		elfznn	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℕ$
17	16	adantl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℕ$
18		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
19	18	zred	$⊢ d \in ℕ \to μ (d) \in ℝ$
20		nndivre	$⊢ (μ (d) \in ℝ \land d \in ℕ) \to \frac{μ (d)}{d} \in ℝ$
21	19 20	mpancom	$⊢ d \in ℕ \to \frac{μ (d)}{d} \in ℝ$
22	17 21	syl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{μ (d)}{d} \in ℝ$
23	22	recnd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{μ (d)}{d} \in ℂ$
24	15 23	mulcld	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
25		fzfid	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{d}⌋) \in Fin$
26	12	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X \in D$
27		elfzelz	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℤ$
28	27	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℤ$
29	4 1 5 2 26 28	dchrzrhcl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) \in ℂ$
30		elfznn	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℕ$
31	30	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℕ$
32	31	nnrpd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℝ^{+}$
33	32	relogcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log m \in ℝ$
34	33 31	nndivred	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log m}{m} \in ℝ$
35	34	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log m}{m} \in ℂ$
36	29 35	mulcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log m}{m}) \in ℂ$
37	25 36	fsumcl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) \in ℂ$
38	24 37	mulcld	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) \in ℂ$
39	16	nnrpd	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℝ^{+}$
40		rpdivcl	$⊢ (A \in ℝ^{+} \land d \in ℝ^{+}) \to \frac{A}{d} \in ℝ^{+}$
41	9 39 40	syl2an	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{A}{d} \in ℝ^{+}$
42	41	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{A}{d} \in ℝ^{+}$
43	42 32	rpdivcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\frac{A}{d}}{m} \in ℝ^{+}$
44	43	relogcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{\frac{A}{d}}{m}) \in ℝ$
45	44 31	nndivred	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log (\frac{\frac{A}{d}}{m})}{m} \in ℝ$
46	45	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log (\frac{\frac{A}{d}}{m})}{m} \in ℂ$
47	29 46	mulcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) \in ℂ$
48	25 47	fsumcl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) \in ℂ$
49	24 48	mulcld	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) \in ℂ$
50	11 38 49	fsumadd	$⊢ φ \to \sum_{d = 1}^{⌊A⌋} (X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
51	42 32	relogdivd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{\frac{A}{d}}{m}) = \log (\frac{A}{d}) - \log m$
52	51	oveq2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log m + \log (\frac{\frac{A}{d}}{m}) = \log m + \log (\frac{A}{d}) - \log m$
53	33	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log m \in ℂ$
54	41	relogcld	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \log (\frac{A}{d}) \in ℝ$
55	54	recnd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \log (\frac{A}{d}) \in ℂ$
56	55	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{A}{d}) \in ℂ$
57	53 56	pncan3d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log m + \log (\frac{A}{d}) - \log m = \log (\frac{A}{d})$
58	52 57	eqtr2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{A}{d}) = \log m + \log (\frac{\frac{A}{d}}{m})$
59	58	oveq1d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log (\frac{A}{d})}{m} = \frac{\log m + \log (\frac{\frac{A}{d}}{m})}{m}$
60	44	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{\frac{A}{d}}{m}) \in ℂ$
61	31	nncnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℂ$
62	31	nnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \neq 0$
63	53 60 61 62	divdird	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log m + \log (\frac{\frac{A}{d}}{m})}{m} = (\frac{\log m}{m}) + (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
64	59 63	eqtrd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log (\frac{A}{d})}{m} = (\frac{\log m}{m}) + (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
65	64	oveq2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = X (L (m)) ((\frac{\log m}{m}) + (\frac{\log (\frac{\frac{A}{d}}{m})}{m}))$
66	29 35 46	adddid	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) ((\frac{\log m}{m}) + (\frac{\log (\frac{\frac{A}{d}}{m})}{m})) = X (L (m)) (\frac{\log m}{m}) + X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
67	65 66	eqtrd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = X (L (m)) (\frac{\log m}{m}) + X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
68	67	sumeq2dv	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} (X (L (m)) (\frac{\log m}{m}) + X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}))$
69	25 36 47	fsumadd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} (X (L (m)) (\frac{\log m}{m}) + X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
70	68 69	eqtrd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
71	70	oveq2d	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = X (L (d)) (\frac{μ (d)}{d}) (\sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}))$
72	24 37 48	adddid	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) (\sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})) = X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
73	71 72	eqtrd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
74	73	sumeq2dv	$⊢ φ \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m}) = \sum_{d = 1}^{⌊A⌋} (X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}))$
75	1 2 3 4 5 6 7 8 9	dchrvmasumlem1	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m})$
76	1 2 3 4 5 6 7 8 9 10	dchrvmasum2lem	$⊢ φ \to \log A = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
77	75 76	oveq12d	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + \log A = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) + \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
78	50 74 77	3eqtr4rd	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + \log A = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
79	78	adantr	$⊢ (φ \land ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + \log A = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
80		iftrue	$⊢ ψ \to if (ψ, \log A, 0) = \log A$
81	80	oveq2d	$⊢ ψ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + \log A$
82	81	adantl	$⊢ (φ \land ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + \log A$
83		iftrue	$⊢ ψ \to if (ψ, \frac{A}{d}, m) = \frac{A}{d}$
84	83	fveq2d	$⊢ ψ \to \log if (ψ, \frac{A}{d}, m) = \log (\frac{A}{d})$
85	84	oveq1d	$⊢ ψ \to \frac{\log if (ψ, \frac{A}{d}, m)}{m} = \frac{\log (\frac{A}{d})}{m}$
86	85	oveq2d	$⊢ ψ \to X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
87	86	sumeq2sdv	$⊢ ψ \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
88	87	oveq2d	$⊢ ψ \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
89	88	sumeq2sdv	$⊢ ψ \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
90	89	adantl	$⊢ (φ \land ψ) \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{A}{d})}{m})$
91	79 82 90	3eqtr4d	$⊢ (φ \land ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m})$
92	7	adantr	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X \in D$
93		elfzelz	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℤ$
94	93	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℤ$
95	4 1 5 2 92 94	dchrzrhcl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) \in ℂ$
96		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
97	96	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
98		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
99		nndivre	$⊢ (Λ (n) \in ℝ \land n \in ℕ) \to \frac{Λ (n)}{n} \in ℝ$
100	98 99	mpancom	$⊢ n \in ℕ \to \frac{Λ (n)}{n} \in ℝ$
101	100	recnd	$⊢ n \in ℕ \to \frac{Λ (n)}{n} \in ℂ$
102	97 101	syl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \frac{Λ (n)}{n} \in ℂ$
103	95 102	mulcld	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
104	11 103	fsumcl	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
105	104	adantr	$⊢ (φ \land \neg ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
106	105	addid1d	$⊢ (φ \land \neg ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + 0 = \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n})$
107		iffalse	$⊢ \neg ψ \to if (ψ, \log A, 0) = 0$
108	107	adantl	$⊢ (φ \land \neg ψ) \to if (ψ, \log A, 0) = 0$
109	108	oveq2d	$⊢ (φ \land \neg ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + 0$
110		iffalse	$⊢ \neg ψ \to if (ψ, \frac{A}{d}, m) = m$
111	110	fveq2d	$⊢ \neg ψ \to \log if (ψ, \frac{A}{d}, m) = \log m$
112	111	oveq1d	$⊢ \neg ψ \to \frac{\log if (ψ, \frac{A}{d}, m)}{m} = \frac{\log m}{m}$
113	112	oveq2d	$⊢ \neg ψ \to X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = X (L (m)) (\frac{\log m}{m})$
114	113	sumeq2sdv	$⊢ \neg ψ \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m})$
115	114	oveq2d	$⊢ \neg ψ \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m})$
116	115	sumeq2sdv	$⊢ \neg ψ \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m})$
117	75	eqcomd	$⊢ φ \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) = \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n})$
118	116 117	sylan9eqr	$⊢ (φ \land \neg ψ) \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m}) = \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n})$
119	106 109 118	3eqtr4d	$⊢ (φ \land \neg ψ) \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m})$
120	91 119	pm2.61dan	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (ψ, \log A, 0) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log if (ψ, \frac{A}{d}, m)}{m})$

Metamath Proof Explorer

Theorem dchrvmasum2if

Proof