dchrisum0flblem1

Description: Lemma for dchrisum0flb . Base case, prime power. (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} ⟶ ℝ$
	dchrisum0flblem1.1	$⊢ φ \to P \in ℙ$
	dchrisum0flblem1.2	$⊢ φ \to A \in ℕ_{0}$
Assertion	dchrisum0flblem1	$⊢ φ \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq F (P^{A})$

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		dchrisum0flblem1.1	$⊢ φ \to P \in ℙ$
11		dchrisum0flblem1.2	$⊢ φ \to A \in ℕ_{0}$
12		1red	$⊢ ((φ \land X (L (P)) = 1) \land \sqrt{P^{A}} \in ℕ) \to 1 \in ℝ$
13		0red	$⊢ ((φ \land X (L (P)) = 1) \land \neg \sqrt{P^{A}} \in ℕ) \to 0 \in ℝ$
14	12 13	ifclda	$⊢ (φ \land X (L (P)) = 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \in ℝ$
15		1red	$⊢ (φ \land X (L (P)) = 1) \to 1 \in ℝ$
16		fzfid	$⊢ φ \to (0 \dots A) \in Fin$
17	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
18		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
19	1 18 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
20		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
21	17 19 20	3syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
22		prmz	$⊢ P \in ℙ \to P \in ℤ$
23	10 22	syl	$⊢ φ \to P \in ℤ$
24	21 23	ffvelrnd	$⊢ φ \to L (P) \in {Base}_{Z}$
25	9 24	ffvelrnd	$⊢ φ \to X (L (P)) \in ℝ$
26		elfznn0	$⊢ i \in (0 \dots A) \to i \in ℕ_{0}$
27		reexpcl	$⊢ (X (L (P)) \in ℝ \land i \in ℕ_{0}) \to {X (L (P))}^{i} \in ℝ$
28	25 26 27	syl2an	$⊢ (φ \land i \in (0 \dots A)) \to {X (L (P))}^{i} \in ℝ$
29	16 28	fsumrecl	$⊢ φ \to \sum_{i = 0}^{A} {X (L (P))}^{i} \in ℝ$
30	29	adantr	$⊢ (φ \land X (L (P)) = 1) \to \sum_{i = 0}^{A} {X (L (P))}^{i} \in ℝ$
31		breq1	$⊢ 1 = if (\sqrt{P^{A}} \in ℕ, 1, 0) \to (1 \leq 1 \leftrightarrow if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq 1)$
32		breq1	$⊢ 0 = if (\sqrt{P^{A}} \in ℕ, 1, 0) \to (0 \leq 1 \leftrightarrow if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq 1)$
33		1le1	$⊢ 1 \leq 1$
34		0le1	$⊢ 0 \leq 1$
35	31 32 33 34	keephyp	$⊢ if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq 1$
36	35	a1i	$⊢ (φ \land X (L (P)) = 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq 1$
37		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
38	11 37	eleqtrdi	$⊢ φ \to A \in ℤ_{\geq 0}$
39		fzn0	$⊢ (0 \dots A) \neq \emptyset \leftrightarrow A \in ℤ_{\geq 0}$
40	38 39	sylibr	$⊢ φ \to (0 \dots A) \neq \emptyset$
41		hashnncl	$⊢ (0 \dots A) \in Fin \to (\|(0 \dots A)\| \in ℕ \leftrightarrow (0 \dots A) \neq \emptyset)$
42	16 41	syl	$⊢ φ \to (\|(0 \dots A)\| \in ℕ \leftrightarrow (0 \dots A) \neq \emptyset)$
43	40 42	mpbird	$⊢ φ \to \|(0 \dots A)\| \in ℕ$
44	43	adantr	$⊢ (φ \land X (L (P)) = 1) \to \|(0 \dots A)\| \in ℕ$
45	44	nnge1d	$⊢ (φ \land X (L (P)) = 1) \to 1 \leq \|(0 \dots A)\|$
46		simpr	$⊢ (φ \land X (L (P)) = 1) \to X (L (P)) = 1$
47	46	oveq1d	$⊢ (φ \land X (L (P)) = 1) \to {X (L (P))}^{i} = 1^{i}$
48		elfzelz	$⊢ i \in (0 \dots A) \to i \in ℤ$
49		1exp	$⊢ i \in ℤ \to 1^{i} = 1$
50	48 49	syl	$⊢ i \in (0 \dots A) \to 1^{i} = 1$
51	47 50	sylan9eq	$⊢ ((φ \land X (L (P)) = 1) \land i \in (0 \dots A)) \to {X (L (P))}^{i} = 1$
52	51	sumeq2dv	$⊢ (φ \land X (L (P)) = 1) \to \sum_{i = 0}^{A} {X (L (P))}^{i} = \sum_{i = 0}^{A} 1$
53		fzfid	$⊢ (φ \land X (L (P)) = 1) \to (0 \dots A) \in Fin$
54		ax-1cn	$⊢ 1 \in ℂ$
55		fsumconst	$⊢ ((0 \dots A) \in Fin \land 1 \in ℂ) \to \sum_{i = 0}^{A} 1 = \|(0 \dots A)\| \cdot 1$
56	53 54 55	sylancl	$⊢ (φ \land X (L (P)) = 1) \to \sum_{i = 0}^{A} 1 = \|(0 \dots A)\| \cdot 1$
57	44	nncnd	$⊢ (φ \land X (L (P)) = 1) \to \|(0 \dots A)\| \in ℂ$
58	57	mulid1d	$⊢ (φ \land X (L (P)) = 1) \to \|(0 \dots A)\| \cdot 1 = \|(0 \dots A)\|$
59	52 56 58	3eqtrd	$⊢ (φ \land X (L (P)) = 1) \to \sum_{i = 0}^{A} {X (L (P))}^{i} = \|(0 \dots A)\|$
60	45 59	breqtrrd	$⊢ (φ \land X (L (P)) = 1) \to 1 \leq \sum_{i = 0}^{A} {X (L (P))}^{i}$
61	14 15 30 36 60	letrd	$⊢ (φ \land X (L (P)) = 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq \sum_{i = 0}^{A} {X (L (P))}^{i}$
62		oveq1	$⊢ 1 = if (\sqrt{P^{A}} \in ℕ, 1, 0) \to 1 (1 - X (L (P))) = if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P)))$
63	62	breq1d	$⊢ 1 = if (\sqrt{P^{A}} \in ℕ, 1, 0) \to (1 (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1} \leftrightarrow if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1})$
64		oveq1	$⊢ 0 = if (\sqrt{P^{A}} \in ℕ, 1, 0) \to 0 \cdot (1 - X (L (P))) = if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P)))$
65	64	breq1d	$⊢ 0 = if (\sqrt{P^{A}} \in ℕ, 1, 0) \to (0 \cdot (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1} \leftrightarrow if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1})$
66		1re	$⊢ 1 \in ℝ$
67	25	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to X (L (P)) \in ℝ$
68		resubcl	$⊢ (1 \in ℝ \land X (L (P)) \in ℝ) \to 1 - X (L (P)) \in ℝ$
69	66 67 68	sylancr	$⊢ (φ \land X (L (P)) \neq 1) \to 1 - X (L (P)) \in ℝ$
70	69	adantr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1 - X (L (P)) \in ℝ$
71	70	leidd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1 - X (L (P)) \leq 1 - X (L (P))$
72	69	recnd	$⊢ (φ \land X (L (P)) \neq 1) \to 1 - X (L (P)) \in ℂ$
73	72	adantr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1 - X (L (P)) \in ℂ$
74	73	mulid2d	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1 (1 - X (L (P))) = 1 - X (L (P))$
75		nn0p1nn	$⊢ A \in ℕ_{0} \to A + 1 \in ℕ$
76	11 75	syl	$⊢ φ \to A + 1 \in ℕ$
77	76	ad3antrrr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) = 0) \to A + 1 \in ℕ$
78	77	0expd	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) = 0) \to 0^{A + 1} = 0$
79		simpr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) = 0) \to X (L (P)) = 0$
80	79	oveq1d	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) = 0) \to {X (L (P))}^{A + 1} = 0^{A + 1}$
81	78 80 79	3eqtr4d	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) = 0) \to {X (L (P))}^{A + 1} = X (L (P))$
82		neg1cn	$⊢ - 1 \in ℂ$
83	11	ad2antrr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to A \in ℕ_{0}$
84		expp1	$⊢ (- 1 \in ℂ \land A \in ℕ_{0}) \to {(- 1)}^{A + 1} = {(- 1)}^{A} -1$
85	82 83 84	sylancr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{A + 1} = {(- 1)}^{A} -1$
86		prmnn	$⊢ P \in ℙ \to P \in ℕ$
87	10 86	syl	$⊢ φ \to P \in ℕ$
88	87 11	nnexpcld	$⊢ φ \to P^{A} \in ℕ$
89	88	nncnd	$⊢ φ \to P^{A} \in ℂ$
90	89	ad2antrr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P^{A} \in ℂ$
91	90	sqsqrtd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {\sqrt{P^{A}}}^{2} = P^{A}$
92	91	oveq2d	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P pCnt {\sqrt{P^{A}}}^{2} = P pCnt P^{A}$
93	10	ad2antrr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P \in ℙ$
94		nnq	$⊢ \sqrt{P^{A}} \in ℕ \to \sqrt{P^{A}} \in ℚ$
95	94	adantl	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to \sqrt{P^{A}} \in ℚ$
96		nnne0	$⊢ \sqrt{P^{A}} \in ℕ \to \sqrt{P^{A}} \neq 0$
97	96	adantl	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to \sqrt{P^{A}} \neq 0$
98		2z	$⊢ 2 \in ℤ$
99	98	a1i	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 2 \in ℤ$
100		pcexp	$⊢ (P \in ℙ \land (\sqrt{P^{A}} \in ℚ \land \sqrt{P^{A}} \neq 0) \land 2 \in ℤ) \to P pCnt {\sqrt{P^{A}}}^{2} = 2 (P pCnt \sqrt{P^{A}})$
101	93 95 97 99 100	syl121anc	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P pCnt {\sqrt{P^{A}}}^{2} = 2 (P pCnt \sqrt{P^{A}})$
102	83	nn0zd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to A \in ℤ$
103		pcid	$⊢ (P \in ℙ \land A \in ℤ) \to P pCnt P^{A} = A$
104	93 102 103	syl2anc	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P pCnt P^{A} = A$
105	92 101 104	3eqtr3rd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to A = 2 (P pCnt \sqrt{P^{A}})$
106	105	oveq2d	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{A} = {(- 1)}^{2 (P pCnt \sqrt{P^{A}})}$
107	82	a1i	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to - 1 \in ℂ$
108		simpr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to \sqrt{P^{A}} \in ℕ$
109	93 108	pccld	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P pCnt \sqrt{P^{A}} \in ℕ_{0}$
110		2nn0	$⊢ 2 \in ℕ_{0}$
111	110	a1i	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 2 \in ℕ_{0}$
112	107 109 111	expmuld	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{2 (P pCnt \sqrt{P^{A}})} = {({-1}^{2})}^{P pCnt \sqrt{P^{A}}}$
113		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
114	113	oveq1i	$⊢ {({-1}^{2})}^{P pCnt \sqrt{P^{A}}} = 1^{P pCnt \sqrt{P^{A}}}$
115	109	nn0zd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to P pCnt \sqrt{P^{A}} \in ℤ$
116		1exp	$⊢ P pCnt \sqrt{P^{A}} \in ℤ \to 1^{P pCnt \sqrt{P^{A}}} = 1$
117	115 116	syl	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1^{P pCnt \sqrt{P^{A}}} = 1$
118	114 117	syl5eq	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {({-1}^{2})}^{P pCnt \sqrt{P^{A}}} = 1$
119	106 112 118	3eqtrd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{A} = 1$
120	119	oveq1d	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{A} -1 = 1 -1$
121	82	mulid2i	$⊢ 1 -1 = - 1$
122	120 121	eqtrdi	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{A} -1 = - 1$
123	85 122	eqtrd	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {(- 1)}^{A + 1} = - 1$
124	123	adantr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to {(- 1)}^{A + 1} = - 1$
125	25	recnd	$⊢ φ \to X (L (P)) \in ℂ$
126	125	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to X (L (P)) \in ℂ$
127	126	ad2antrr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to X (L (P)) \in ℂ$
128	127	negnegd	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to - (- X (L (P))) = X (L (P))$
129		simpr	$⊢ (φ \land X (L (P)) \neq 1) \to X (L (P)) \neq 1$
130	129	ad2antrr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to X (L (P)) \neq 1$
131	8	ad3antrrr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to X \in D$
132		eqid	$⊢ Unit (Z) = Unit (Z)$
133	4 1 5 18 132 8 24	dchrn0	$⊢ φ \to (X (L (P)) \neq 0 \leftrightarrow L (P) \in Unit (Z))$
134	133	ad2antrr	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to (X (L (P)) \neq 0 \leftrightarrow L (P) \in Unit (Z))$
135	134	biimpa	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to L (P) \in Unit (Z)$
136	4 5 131 1 132 135	dchrabs	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to \|X (L (P))\| = 1$
137		eqeq1	$⊢ \|X (L (P))\| = X (L (P)) \to (\|X (L (P))\| = 1 \leftrightarrow X (L (P)) = 1)$
138	136 137	syl5ibcom	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to (\|X (L (P))\| = X (L (P)) \to X (L (P)) = 1)$
139	138	necon3ad	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to (X (L (P)) \neq 1 \to \neg \|X (L (P))\| = X (L (P)))$
140	130 139	mpd	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to \neg \|X (L (P))\| = X (L (P))$
141	67	ad2antrr	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to X (L (P)) \in ℝ$
142	141	absord	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to (\|X (L (P))\| = X (L (P)) \lor \|X (L (P))\| = - X (L (P)))$
143	142	ord	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to (\neg \|X (L (P))\| = X (L (P)) \to \|X (L (P))\| = - X (L (P)))$
144	140 143	mpd	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to \|X (L (P))\| = - X (L (P))$
145	144 136	eqtr3d	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to - X (L (P)) = 1$
146	145	negeqd	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to - (- X (L (P))) = - 1$
147	128 146	eqtr3d	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to X (L (P)) = - 1$
148	147	oveq1d	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to {X (L (P))}^{A + 1} = {(- 1)}^{A + 1}$
149	124 148 147	3eqtr4d	$⊢ (((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \land X (L (P)) \neq 0) \to {X (L (P))}^{A + 1} = X (L (P))$
150	81 149	pm2.61dane	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to {X (L (P))}^{A + 1} = X (L (P))$
151	150	oveq2d	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1 - {X (L (P))}^{A + 1} = 1 - X (L (P))$
152	71 74 151	3brtr4d	$⊢ ((φ \land X (L (P)) \neq 1) \land \sqrt{P^{A}} \in ℕ) \to 1 (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1}$
153	72	mul02d	$⊢ (φ \land X (L (P)) \neq 1) \to 0 \cdot (1 - X (L (P))) = 0$
154		peano2nn0	$⊢ A \in ℕ_{0} \to A + 1 \in ℕ_{0}$
155	11 154	syl	$⊢ φ \to A + 1 \in ℕ_{0}$
156	25 155	reexpcld	$⊢ φ \to {X (L (P))}^{A + 1} \in ℝ$
157	156	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to {X (L (P))}^{A + 1} \in ℝ$
158	157	recnd	$⊢ (φ \land X (L (P)) \neq 1) \to {X (L (P))}^{A + 1} \in ℂ$
159	158	abscld	$⊢ (φ \land X (L (P)) \neq 1) \to \|{X (L (P))}^{A + 1}\| \in ℝ$
160		1red	$⊢ (φ \land X (L (P)) \neq 1) \to 1 \in ℝ$
161	157	leabsd	$⊢ (φ \land X (L (P)) \neq 1) \to {X (L (P))}^{A + 1} \leq \|{X (L (P))}^{A + 1}\|$
162	155	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to A + 1 \in ℕ_{0}$
163	126 162	absexpd	$⊢ (φ \land X (L (P)) \neq 1) \to \|{X (L (P))}^{A + 1}\| = {\|X (L (P))\|}^{A + 1}$
164	126	abscld	$⊢ (φ \land X (L (P)) \neq 1) \to \|X (L (P))\| \in ℝ$
165	126	absge0d	$⊢ (φ \land X (L (P)) \neq 1) \to 0 \leq \|X (L (P))\|$
166	4 5 1 18 8 24	dchrabs2	$⊢ φ \to \|X (L (P))\| \leq 1$
167	166	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to \|X (L (P))\| \leq 1$
168		exple1	$⊢ ((\|X (L (P))\| \in ℝ \land 0 \leq \|X (L (P))\| \land \|X (L (P))\| \leq 1) \land A + 1 \in ℕ_{0}) \to {\|X (L (P))\|}^{A + 1} \leq 1$
169	164 165 167 162 168	syl31anc	$⊢ (φ \land X (L (P)) \neq 1) \to {\|X (L (P))\|}^{A + 1} \leq 1$
170	163 169	eqbrtrd	$⊢ (φ \land X (L (P)) \neq 1) \to \|{X (L (P))}^{A + 1}\| \leq 1$
171	157 159 160 161 170	letrd	$⊢ (φ \land X (L (P)) \neq 1) \to {X (L (P))}^{A + 1} \leq 1$
172		subge0	$⊢ (1 \in ℝ \land {X (L (P))}^{A + 1} \in ℝ) \to (0 \leq 1 - {X (L (P))}^{A + 1} \leftrightarrow {X (L (P))}^{A + 1} \leq 1)$
173	66 157 172	sylancr	$⊢ (φ \land X (L (P)) \neq 1) \to (0 \leq 1 - {X (L (P))}^{A + 1} \leftrightarrow {X (L (P))}^{A + 1} \leq 1)$
174	171 173	mpbird	$⊢ (φ \land X (L (P)) \neq 1) \to 0 \leq 1 - {X (L (P))}^{A + 1}$
175	153 174	eqbrtrd	$⊢ (φ \land X (L (P)) \neq 1) \to 0 \cdot (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1}$
176	175	adantr	$⊢ ((φ \land X (L (P)) \neq 1) \land \neg \sqrt{P^{A}} \in ℕ) \to 0 \cdot (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1}$
177	63 65 152 176	ifbothda	$⊢ (φ \land X (L (P)) \neq 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1}$
178		0re	$⊢ 0 \in ℝ$
179	66 178	ifcli	$⊢ if (\sqrt{P^{A}} \in ℕ, 1, 0) \in ℝ$
180	179	a1i	$⊢ (φ \land X (L (P)) \neq 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \in ℝ$
181		resubcl	$⊢ (1 \in ℝ \land {X (L (P))}^{A + 1} \in ℝ) \to 1 - {X (L (P))}^{A + 1} \in ℝ$
182	66 157 181	sylancr	$⊢ (φ \land X (L (P)) \neq 1) \to 1 - {X (L (P))}^{A + 1} \in ℝ$
183	67	leabsd	$⊢ (φ \land X (L (P)) \neq 1) \to X (L (P)) \leq \|X (L (P))\|$
184	67 164 160 183 167	letrd	$⊢ (φ \land X (L (P)) \neq 1) \to X (L (P)) \leq 1$
185	129	necomd	$⊢ (φ \land X (L (P)) \neq 1) \to 1 \neq X (L (P))$
186	67 160 184 185	leneltd	$⊢ (φ \land X (L (P)) \neq 1) \to X (L (P)) < 1$
187		posdif	$⊢ (X (L (P)) \in ℝ \land 1 \in ℝ) \to (X (L (P)) < 1 \leftrightarrow 0 < 1 - X (L (P)))$
188	67 66 187	sylancl	$⊢ (φ \land X (L (P)) \neq 1) \to (X (L (P)) < 1 \leftrightarrow 0 < 1 - X (L (P)))$
189	186 188	mpbid	$⊢ (φ \land X (L (P)) \neq 1) \to 0 < 1 - X (L (P))$
190		lemuldiv	$⊢ (if (\sqrt{P^{A}} \in ℕ, 1, 0) \in ℝ \land 1 - {X (L (P))}^{A + 1} \in ℝ \land (1 - X (L (P)) \in ℝ \land 0 < 1 - X (L (P)))) \to (if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1} \leftrightarrow if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq \frac{1 - {X (L (P))}^{A + 1}}{1 - X (L (P))})$
191	180 182 69 189 190	syl112anc	$⊢ (φ \land X (L (P)) \neq 1) \to (if (\sqrt{P^{A}} \in ℕ, 1, 0) (1 - X (L (P))) \leq 1 - {X (L (P))}^{A + 1} \leftrightarrow if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq \frac{1 - {X (L (P))}^{A + 1}}{1 - X (L (P))})$
192	177 191	mpbid	$⊢ (φ \land X (L (P)) \neq 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq \frac{1 - {X (L (P))}^{A + 1}}{1 - X (L (P))}$
193	11	nn0zd	$⊢ φ \to A \in ℤ$
194		fzval3	$⊢ A \in ℤ \to (0 \dots A) = (0 ..^A + 1)$
195	193 194	syl	$⊢ φ \to (0 \dots A) = (0 ..^A + 1)$
196	195	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to (0 \dots A) = (0 ..^A + 1)$
197	196	sumeq1d	$⊢ (φ \land X (L (P)) \neq 1) \to \sum_{i = 0}^{A} {X (L (P))}^{i} = \sum_{i \in (0 ..^A + 1)} {X (L (P))}^{i}$
198		0nn0	$⊢ 0 \in ℕ_{0}$
199	198	a1i	$⊢ (φ \land X (L (P)) \neq 1) \to 0 \in ℕ_{0}$
200	155 37	eleqtrdi	$⊢ φ \to A + 1 \in ℤ_{\geq 0}$
201	200	adantr	$⊢ (φ \land X (L (P)) \neq 1) \to A + 1 \in ℤ_{\geq 0}$
202	126 129 199 201	geoserg	$⊢ (φ \land X (L (P)) \neq 1) \to \sum_{i \in (0 ..^A + 1)} {X (L (P))}^{i} = \frac{{X (L (P))}^{0} - {X (L (P))}^{A + 1}}{1 - X (L (P))}$
203	126	exp0d	$⊢ (φ \land X (L (P)) \neq 1) \to {X (L (P))}^{0} = 1$
204	203	oveq1d	$⊢ (φ \land X (L (P)) \neq 1) \to {X (L (P))}^{0} - {X (L (P))}^{A + 1} = 1 - {X (L (P))}^{A + 1}$
205	204	oveq1d	$⊢ (φ \land X (L (P)) \neq 1) \to \frac{{X (L (P))}^{0} - {X (L (P))}^{A + 1}}{1 - X (L (P))} = \frac{1 - {X (L (P))}^{A + 1}}{1 - X (L (P))}$
206	197 202 205	3eqtrd	$⊢ (φ \land X (L (P)) \neq 1) \to \sum_{i = 0}^{A} {X (L (P))}^{i} = \frac{1 - {X (L (P))}^{A + 1}}{1 - X (L (P))}$
207	192 206	breqtrrd	$⊢ (φ \land X (L (P)) \neq 1) \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq \sum_{i = 0}^{A} {X (L (P))}^{i}$
208	61 207	pm2.61dane	$⊢ φ \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq \sum_{i = 0}^{A} {X (L (P))}^{i}$
209	1 2 3 4 5 6 7	dchrisum0fval	$⊢ P^{A} \in ℕ \to F (P^{A}) = \sum_{k \in \{q \in ℕ \| q ∥ P^{A}\}} X (L (k))$
210	88 209	syl	$⊢ φ \to F (P^{A}) = \sum_{k \in \{q \in ℕ \| q ∥ P^{A}\}} X (L (k))$
211		2fveq3	$⊢ k = P^{i} \to X (L (k)) = X (L (P^{i}))$
212		eqid	$⊢ (b \in (0 \dots A) ⟼ P^{b}) = (b \in (0 \dots A) ⟼ P^{b})$
213	212	dvdsppwf1o	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to (b \in (0 \dots A) ⟼ P^{b}) : (0 \dots A) \underset{1-1 onto}{⟶} \{q \in ℕ \| q ∥ P^{A}\}$
214	10 11 213	syl2anc	$⊢ φ \to (b \in (0 \dots A) ⟼ P^{b}) : (0 \dots A) \underset{1-1 onto}{⟶} \{q \in ℕ \| q ∥ P^{A}\}$
215		oveq2	$⊢ b = i \to P^{b} = P^{i}$
216		ovex	$⊢ P^{b} \in V$
217	215 212 216	fvmpt3i	$⊢ i \in (0 \dots A) \to (b \in (0 \dots A) ⟼ P^{b}) (i) = P^{i}$
218	217	adantl	$⊢ (φ \land i \in (0 \dots A)) \to (b \in (0 \dots A) ⟼ P^{b}) (i) = P^{i}$
219	9	adantr	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ P^{A}\}) \to X : {Base}_{Z} ⟶ ℝ$
220		elrabi	$⊢ k \in \{q \in ℕ \| q ∥ P^{A}\} \to k \in ℕ$
221	220	nnzd	$⊢ k \in \{q \in ℕ \| q ∥ P^{A}\} \to k \in ℤ$
222		ffvelrn	$⊢ (L : ℤ ⟶ {Base}_{Z} \land k \in ℤ) \to L (k) \in {Base}_{Z}$
223	21 221 222	syl2an	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ P^{A}\}) \to L (k) \in {Base}_{Z}$
224	219 223	ffvelrnd	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ P^{A}\}) \to X (L (k)) \in ℝ$
225	224	recnd	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ P^{A}\}) \to X (L (k)) \in ℂ$
226	211 16 214 218 225	fsumf1o	$⊢ φ \to \sum_{k \in \{q \in ℕ \| q ∥ P^{A}\}} X (L (k)) = \sum_{i = 0}^{A} X (L (P^{i}))$
227		zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$
228		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
229	228	subrgsubm	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}})$
230	227 229	mp1i	$⊢ (φ \land i \in (0 \dots A)) \to ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}})$
231	26	adantl	$⊢ (φ \land i \in (0 \dots A)) \to i \in ℕ_{0}$
232	23	adantr	$⊢ (φ \land i \in (0 \dots A)) \to P \in ℤ$
233		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
234		zringmpg	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ = {mulGrp}_{ℤ_{ring}}$
235	234	eqcomi	$⊢ {mulGrp}_{ℤ_{ring}} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ$
236		eqid	$⊢ \cdot_{{mulGrp}_{ℤ_{ring}}} = \cdot_{{mulGrp}_{ℤ_{ring}}}$
237	233 235 236	submmulg	$⊢ (ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}}) \land i \in ℕ_{0} \land P \in ℤ) \to i \cdot_{{mulGrp}_{ℂ_{fld}}} P = i \cdot_{{mulGrp}_{ℤ_{ring}}} P$
238	230 231 232 237	syl3anc	$⊢ (φ \land i \in (0 \dots A)) \to i \cdot_{{mulGrp}_{ℂ_{fld}}} P = i \cdot_{{mulGrp}_{ℤ_{ring}}} P$
239	87	nncnd	$⊢ φ \to P \in ℂ$
240		cnfldexp	$⊢ (P \in ℂ \land i \in ℕ_{0}) \to i \cdot_{{mulGrp}_{ℂ_{fld}}} P = P^{i}$
241	239 26 240	syl2an	$⊢ (φ \land i \in (0 \dots A)) \to i \cdot_{{mulGrp}_{ℂ_{fld}}} P = P^{i}$
242	238 241	eqtr3d	$⊢ (φ \land i \in (0 \dots A)) \to i \cdot_{{mulGrp}_{ℤ_{ring}}} P = P^{i}$
243	242	fveq2d	$⊢ (φ \land i \in (0 \dots A)) \to L (i \cdot_{{mulGrp}_{ℤ_{ring}}} P) = L (P^{i})$
244	1	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
245		crngring	$⊢ Z \in CRing \to Z \in Ring$
246	17 244 245	3syl	$⊢ φ \to Z \in Ring$
247	2	zrhrhm	$⊢ Z \in Ring \to L \in (ℤ_{ring} RingHom Z)$
248		eqid	$⊢ {mulGrp}_{ℤ_{ring}} = {mulGrp}_{ℤ_{ring}}$
249		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
250	248 249	rhmmhm	$⊢ L \in (ℤ_{ring} RingHom Z) \to L \in ({mulGrp}_{ℤ_{ring}} MndHom {mulGrp}_{Z})$
251	246 247 250	3syl	$⊢ φ \to L \in ({mulGrp}_{ℤ_{ring}} MndHom {mulGrp}_{Z})$
252	251	adantr	$⊢ (φ \land i \in (0 \dots A)) \to L \in ({mulGrp}_{ℤ_{ring}} MndHom {mulGrp}_{Z})$
253		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
254	248 253	mgpbas	$⊢ ℤ = {Base}_{{mulGrp}_{ℤ_{ring}}}$
255		eqid	$⊢ \cdot_{{mulGrp}_{Z}} = \cdot_{{mulGrp}_{Z}}$
256	254 236 255	mhmmulg	$⊢ (L \in ({mulGrp}_{ℤ_{ring}} MndHom {mulGrp}_{Z}) \land i \in ℕ_{0} \land P \in ℤ) \to L (i \cdot_{{mulGrp}_{ℤ_{ring}}} P) = i \cdot_{{mulGrp}_{Z}} L (P)$
257	252 231 232 256	syl3anc	$⊢ (φ \land i \in (0 \dots A)) \to L (i \cdot_{{mulGrp}_{ℤ_{ring}}} P) = i \cdot_{{mulGrp}_{Z}} L (P)$
258	243 257	eqtr3d	$⊢ (φ \land i \in (0 \dots A)) \to L (P^{i}) = i \cdot_{{mulGrp}_{Z}} L (P)$
259	258	fveq2d	$⊢ (φ \land i \in (0 \dots A)) \to X (L (P^{i})) = X (i \cdot_{{mulGrp}_{Z}} L (P))$
260	4 1 5	dchrmhm	$⊢ D \subseteq {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
261	260 8	sselid	$⊢ φ \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
262	261	adantr	$⊢ (φ \land i \in (0 \dots A)) \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
263	24	adantr	$⊢ (φ \land i \in (0 \dots A)) \to L (P) \in {Base}_{Z}$
264	249 18	mgpbas	$⊢ {Base}_{Z} = {Base}_{{mulGrp}_{Z}}$
265	264 255 233	mhmmulg	$⊢ (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land i \in ℕ_{0} \land L (P) \in {Base}_{Z}) \to X (i \cdot_{{mulGrp}_{Z}} L (P)) = i \cdot_{{mulGrp}_{ℂ_{fld}}} X (L (P))$
266	262 231 263 265	syl3anc	$⊢ (φ \land i \in (0 \dots A)) \to X (i \cdot_{{mulGrp}_{Z}} L (P)) = i \cdot_{{mulGrp}_{ℂ_{fld}}} X (L (P))$
267		cnfldexp	$⊢ (X (L (P)) \in ℂ \land i \in ℕ_{0}) \to i \cdot_{{mulGrp}_{ℂ_{fld}}} X (L (P)) = {X (L (P))}^{i}$
268	125 26 267	syl2an	$⊢ (φ \land i \in (0 \dots A)) \to i \cdot_{{mulGrp}_{ℂ_{fld}}} X (L (P)) = {X (L (P))}^{i}$
269	259 266 268	3eqtrd	$⊢ (φ \land i \in (0 \dots A)) \to X (L (P^{i})) = {X (L (P))}^{i}$
270	269	sumeq2dv	$⊢ φ \to \sum_{i = 0}^{A} X (L (P^{i})) = \sum_{i = 0}^{A} {X (L (P))}^{i}$
271	210 226 270	3eqtrd	$⊢ φ \to F (P^{A}) = \sum_{i = 0}^{A} {X (L (P))}^{i}$
272	208 271	breqtrrd	$⊢ φ \to if (\sqrt{P^{A}} \in ℕ, 1, 0) \leq F (P^{A})$

Metamath Proof Explorer

Theorem dchrisum0flblem1

Proof