dchrisum0flblem2

Description: Lemma for dchrisum0flb . Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020)

	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} ⟶ ℝ$
	dchrisum0flb.1	$⊢ φ \to A \in ℤ_{\geq 2}$
	dchrisum0flb.2	$⊢ φ \to P \in ℙ$
	dchrisum0flb.3	$⊢ φ \to P ∥ A$
	dchrisum0flb.4	$⊢ φ \to \forall y \in (1 ..^A) if (\sqrt{y} \in ℕ, 1, 0) \leq F (y)$
Assertion	dchrisum0flblem2	$⊢ φ \to if (\sqrt{A} \in ℕ, 1, 0) \leq F (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		dchrisum0flb.1	$⊢ φ \to A \in ℤ_{\geq 2}$
11		dchrisum0flb.2	$⊢ φ \to P \in ℙ$
12		dchrisum0flb.3	$⊢ φ \to P ∥ A$
13		dchrisum0flb.4	$⊢ φ \to \forall y \in (1 ..^A) if (\sqrt{y} \in ℕ, 1, 0) \leq F (y)$
14		breq1	$⊢ 1 = if (\sqrt{A} \in ℕ, 1, 0) \to (1 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}}) \leftrightarrow if (\sqrt{A} \in ℕ, 1, 0) \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}}))$
15		breq1	$⊢ 0 = if (\sqrt{A} \in ℕ, 1, 0) \to (0 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}}) \leftrightarrow if (\sqrt{A} \in ℕ, 1, 0) \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}}))$
16		1t1e1	$⊢ 1 \cdot 1 = 1$
17	11	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to P \in ℙ$
18		nnq	$⊢ \sqrt{A} \in ℕ \to \sqrt{A} \in ℚ$
19	18	adantl	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{A} \in ℚ$
20		nnne0	$⊢ \sqrt{A} \in ℕ \to \sqrt{A} \neq 0$
21	20	adantl	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{A} \neq 0$
22		2z	$⊢ 2 \in ℤ$
23	22	a1i	$⊢ (φ \land \sqrt{A} \in ℕ) \to 2 \in ℤ$
24		pcexp	$⊢ (P \in ℙ \land (\sqrt{A} \in ℚ \land \sqrt{A} \neq 0) \land 2 \in ℤ) \to P pCnt {\sqrt{A}}^{2} = 2 (P pCnt \sqrt{A})$
25	17 19 21 23 24	syl121anc	$⊢ (φ \land \sqrt{A} \in ℕ) \to P pCnt {\sqrt{A}}^{2} = 2 (P pCnt \sqrt{A})$
26		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
27	10 26	syl	$⊢ φ \to A \in ℕ$
28	27	nncnd	$⊢ φ \to A \in ℂ$
29	28	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to A \in ℂ$
30	29	sqsqrtd	$⊢ (φ \land \sqrt{A} \in ℕ) \to {\sqrt{A}}^{2} = A$
31	30	oveq2d	$⊢ (φ \land \sqrt{A} \in ℕ) \to P pCnt {\sqrt{A}}^{2} = P pCnt A$
32		2cnd	$⊢ (φ \land \sqrt{A} \in ℕ) \to 2 \in ℂ$
33		simpr	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{A} \in ℕ$
34	17 33	pccld	$⊢ (φ \land \sqrt{A} \in ℕ) \to P pCnt \sqrt{A} \in ℕ_{0}$
35	34	nn0cnd	$⊢ (φ \land \sqrt{A} \in ℕ) \to P pCnt \sqrt{A} \in ℂ$
36	32 35	mulcomd	$⊢ (φ \land \sqrt{A} \in ℕ) \to 2 (P pCnt \sqrt{A}) = (P pCnt \sqrt{A}) \cdot 2$
37	25 31 36	3eqtr3rd	$⊢ (φ \land \sqrt{A} \in ℕ) \to (P pCnt \sqrt{A}) \cdot 2 = P pCnt A$
38	37	oveq2d	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{(P pCnt \sqrt{A}) \cdot 2} = P^{P pCnt A}$
39		prmnn	$⊢ P \in ℙ \to P \in ℕ$
40	17 39	syl	$⊢ (φ \land \sqrt{A} \in ℕ) \to P \in ℕ$
41	40	nncnd	$⊢ (φ \land \sqrt{A} \in ℕ) \to P \in ℂ$
42		2nn0	$⊢ 2 \in ℕ_{0}$
43	42	a1i	$⊢ (φ \land \sqrt{A} \in ℕ) \to 2 \in ℕ_{0}$
44	41 43 34	expmuld	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{(P pCnt \sqrt{A}) \cdot 2} = {(P^{P pCnt \sqrt{A}})}^{2}$
45	38 44	eqtr3d	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{P pCnt A} = {(P^{P pCnt \sqrt{A}})}^{2}$
46	45	fveq2d	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{P^{P pCnt A}} = \sqrt{{(P^{P pCnt \sqrt{A}})}^{2}}$
47	40 34	nnexpcld	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{P pCnt \sqrt{A}} \in ℕ$
48	47	nnrpd	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{P pCnt \sqrt{A}} \in ℝ^{+}$
49	48	rprege0d	$⊢ (φ \land \sqrt{A} \in ℕ) \to (P^{P pCnt \sqrt{A}} \in ℝ \land 0 \leq P^{P pCnt \sqrt{A}})$
50		sqrtsq	$⊢ (P^{P pCnt \sqrt{A}} \in ℝ \land 0 \leq P^{P pCnt \sqrt{A}}) \to \sqrt{{(P^{P pCnt \sqrt{A}})}^{2}} = P^{P pCnt \sqrt{A}}$
51	49 50	syl	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{{(P^{P pCnt \sqrt{A}})}^{2}} = P^{P pCnt \sqrt{A}}$
52	46 51	eqtrd	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{P^{P pCnt A}} = P^{P pCnt \sqrt{A}}$
53	52 47	eqeltrd	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{P^{P pCnt A}} \in ℕ$
54	53	iftrued	$⊢ (φ \land \sqrt{A} \in ℕ) \to if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) = 1$
55	11 27	pccld	$⊢ φ \to P pCnt A \in ℕ_{0}$
56	1 2 3 4 5 6 7 8 9 11 55	dchrisum0flblem1	$⊢ φ \to if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) \leq F (P^{P pCnt A})$
57	56	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) \leq F (P^{P pCnt A})$
58	54 57	eqbrtrrd	$⊢ (φ \land \sqrt{A} \in ℕ) \to 1 \leq F (P^{P pCnt A})$
59		pcdvds	$⊢ (P \in ℙ \land A \in ℕ) \to P^{P pCnt A} ∥ A$
60	11 27 59	syl2anc	$⊢ φ \to P^{P pCnt A} ∥ A$
61	11 39	syl	$⊢ φ \to P \in ℕ$
62	61 55	nnexpcld	$⊢ φ \to P^{P pCnt A} \in ℕ$
63		nndivdvds	$⊢ (A \in ℕ \land P^{P pCnt A} \in ℕ) \to (P^{P pCnt A} ∥ A \leftrightarrow \frac{A}{P^{P pCnt A}} \in ℕ)$
64	27 62 63	syl2anc	$⊢ φ \to (P^{P pCnt A} ∥ A \leftrightarrow \frac{A}{P^{P pCnt A}} \in ℕ)$
65	60 64	mpbid	$⊢ φ \to \frac{A}{P^{P pCnt A}} \in ℕ$
66	65	nnzd	$⊢ φ \to \frac{A}{P^{P pCnt A}} \in ℤ$
67	66	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to \frac{A}{P^{P pCnt A}} \in ℤ$
68	27	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to A \in ℕ$
69	68	nnrpd	$⊢ (φ \land \sqrt{A} \in ℕ) \to A \in ℝ^{+}$
70	69	rprege0d	$⊢ (φ \land \sqrt{A} \in ℕ) \to (A \in ℝ \land 0 \leq A)$
71	62	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{P pCnt A} \in ℕ$
72	71	nnrpd	$⊢ (φ \land \sqrt{A} \in ℕ) \to P^{P pCnt A} \in ℝ^{+}$
73		sqrtdiv	$⊢ ((A \in ℝ \land 0 \leq A) \land P^{P pCnt A} \in ℝ^{+}) \to \sqrt{\frac{A}{P^{P pCnt A}}} = \frac{\sqrt{A}}{\sqrt{P^{P pCnt A}}}$
74	70 72 73	syl2anc	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{\frac{A}{P^{P pCnt A}}} = \frac{\sqrt{A}}{\sqrt{P^{P pCnt A}}}$
75		nnz	$⊢ \sqrt{A} \in ℕ \to \sqrt{A} \in ℤ$
76		znq	$⊢ (\sqrt{A} \in ℤ \land \sqrt{P^{P pCnt A}} \in ℕ) \to \frac{\sqrt{A}}{\sqrt{P^{P pCnt A}}} \in ℚ$
77	75 53 76	syl2an2	$⊢ (φ \land \sqrt{A} \in ℕ) \to \frac{\sqrt{A}}{\sqrt{P^{P pCnt A}}} \in ℚ$
78	74 77	eqeltrd	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{\frac{A}{P^{P pCnt A}}} \in ℚ$
79		zsqrtelqelz	$⊢ (\frac{A}{P^{P pCnt A}} \in ℤ \land \sqrt{\frac{A}{P^{P pCnt A}}} \in ℚ) \to \sqrt{\frac{A}{P^{P pCnt A}}} \in ℤ$
80	67 78 79	syl2anc	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{\frac{A}{P^{P pCnt A}}} \in ℤ$
81	65	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to \frac{A}{P^{P pCnt A}} \in ℕ$
82	81	nnrpd	$⊢ (φ \land \sqrt{A} \in ℕ) \to \frac{A}{P^{P pCnt A}} \in ℝ^{+}$
83	82	sqrtgt0d	$⊢ (φ \land \sqrt{A} \in ℕ) \to 0 < \sqrt{\frac{A}{P^{P pCnt A}}}$
84		elnnz	$⊢ \sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ \leftrightarrow (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℤ \land 0 < \sqrt{\frac{A}{P^{P pCnt A}}})$
85	80 83 84	sylanbrc	$⊢ (φ \land \sqrt{A} \in ℕ) \to \sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ$
86	85	iftrued	$⊢ (φ \land \sqrt{A} \in ℕ) \to if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) = 1$
87		fveq2	$⊢ y = \frac{A}{P^{P pCnt A}} \to \sqrt{y} = \sqrt{\frac{A}{P^{P pCnt A}}}$
88	87	eleq1d	$⊢ y = \frac{A}{P^{P pCnt A}} \to (\sqrt{y} \in ℕ \leftrightarrow \sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ)$
89	88	ifbid	$⊢ y = \frac{A}{P^{P pCnt A}} \to if (\sqrt{y} \in ℕ, 1, 0) = if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0)$
90		fveq2	$⊢ y = \frac{A}{P^{P pCnt A}} \to F (y) = F (\frac{A}{P^{P pCnt A}})$
91	89 90	breq12d	$⊢ y = \frac{A}{P^{P pCnt A}} \to (if (\sqrt{y} \in ℕ, 1, 0) \leq F (y) \leftrightarrow if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \leq F (\frac{A}{P^{P pCnt A}}))$
92		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
93	65 92	eleqtrdi	$⊢ φ \to \frac{A}{P^{P pCnt A}} \in ℤ_{\geq 1}$
94	27	nnzd	$⊢ φ \to A \in ℤ$
95	61	nnred	$⊢ φ \to P \in ℝ$
96		pcelnn	$⊢ (P \in ℙ \land A \in ℕ) \to (P pCnt A \in ℕ \leftrightarrow P ∥ A)$
97	11 27 96	syl2anc	$⊢ φ \to (P pCnt A \in ℕ \leftrightarrow P ∥ A)$
98	12 97	mpbird	$⊢ φ \to P pCnt A \in ℕ$
99		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
100		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
101	11 99 100	3syl	$⊢ φ \to 1 < P$
102		expgt1	$⊢ (P \in ℝ \land P pCnt A \in ℕ \land 1 < P) \to 1 < P^{P pCnt A}$
103	95 98 101 102	syl3anc	$⊢ φ \to 1 < P^{P pCnt A}$
104		1red	$⊢ φ \to 1 \in ℝ$
105		0lt1	$⊢ 0 < 1$
106	105	a1i	$⊢ φ \to 0 < 1$
107	62	nnred	$⊢ φ \to P^{P pCnt A} \in ℝ$
108	62	nngt0d	$⊢ φ \to 0 < P^{P pCnt A}$
109	27	nnred	$⊢ φ \to A \in ℝ$
110	27	nngt0d	$⊢ φ \to 0 < A$
111		ltdiv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (P^{P pCnt A} \in ℝ \land 0 < P^{P pCnt A}) \land (A \in ℝ \land 0 < A)) \to (1 < P^{P pCnt A} \leftrightarrow \frac{A}{P^{P pCnt A}} < \frac{A}{1})$
112	104 106 107 108 109 110 111	syl222anc	$⊢ φ \to (1 < P^{P pCnt A} \leftrightarrow \frac{A}{P^{P pCnt A}} < \frac{A}{1})$
113	103 112	mpbid	$⊢ φ \to \frac{A}{P^{P pCnt A}} < \frac{A}{1}$
114	28	div1d	$⊢ φ \to \frac{A}{1} = A$
115	113 114	breqtrd	$⊢ φ \to \frac{A}{P^{P pCnt A}} < A$
116		elfzo2	$⊢ \frac{A}{P^{P pCnt A}} \in (1 ..^A) \leftrightarrow (\frac{A}{P^{P pCnt A}} \in ℤ_{\geq 1} \land A \in ℤ \land \frac{A}{P^{P pCnt A}} < A)$
117	93 94 115 116	syl3anbrc	$⊢ φ \to \frac{A}{P^{P pCnt A}} \in (1 ..^A)$
118	91 13 117	rspcdva	$⊢ φ \to if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \leq F (\frac{A}{P^{P pCnt A}})$
119	118	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \leq F (\frac{A}{P^{P pCnt A}})$
120	86 119	eqbrtrrd	$⊢ (φ \land \sqrt{A} \in ℕ) \to 1 \leq F (\frac{A}{P^{P pCnt A}})$
121		1re	$⊢ 1 \in ℝ$
122		0le1	$⊢ 0 \leq 1$
123	121 122	pm3.2i	$⊢ (1 \in ℝ \land 0 \leq 1)$
124	123	a1i	$⊢ (φ \land \sqrt{A} \in ℕ) \to (1 \in ℝ \land 0 \leq 1)$
125	1 2 3 4 5 6 7 8 9	dchrisum0ff	$⊢ φ \to F : ℕ ⟶ ℝ$
126	125 62	ffvelrnd	$⊢ φ \to F (P^{P pCnt A}) \in ℝ$
127	126	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to F (P^{P pCnt A}) \in ℝ$
128	125 65	ffvelrnd	$⊢ φ \to F (\frac{A}{P^{P pCnt A}}) \in ℝ$
129	128	adantr	$⊢ (φ \land \sqrt{A} \in ℕ) \to F (\frac{A}{P^{P pCnt A}}) \in ℝ$
130		lemul12a	$⊢ (((1 \in ℝ \land 0 \leq 1) \land F (P^{P pCnt A}) \in ℝ) \land ((1 \in ℝ \land 0 \leq 1) \land F (\frac{A}{P^{P pCnt A}}) \in ℝ)) \to ((1 \leq F (P^{P pCnt A}) \land 1 \leq F (\frac{A}{P^{P pCnt A}})) \to 1 \cdot 1 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}}))$
131	124 127 124 129 130	syl22anc	$⊢ (φ \land \sqrt{A} \in ℕ) \to ((1 \leq F (P^{P pCnt A}) \land 1 \leq F (\frac{A}{P^{P pCnt A}})) \to 1 \cdot 1 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}}))$
132	58 120 131	mp2and	$⊢ (φ \land \sqrt{A} \in ℕ) \to 1 \cdot 1 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
133	16 132	eqbrtrrid	$⊢ (φ \land \sqrt{A} \in ℕ) \to 1 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
134		0red	$⊢ φ \to 0 \in ℝ$
135		0re	$⊢ 0 \in ℝ$
136	121 135	ifcli	$⊢ if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) \in ℝ$
137	136	a1i	$⊢ φ \to if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) \in ℝ$
138		breq2	$⊢ 1 = if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) \to (0 \leq 1 \leftrightarrow 0 \leq if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0))$
139		breq2	$⊢ 0 = if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0))$
140		0le0	$⊢ 0 \leq 0$
141	138 139 122 140	keephyp	$⊢ 0 \leq if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0)$
142	141	a1i	$⊢ φ \to 0 \leq if (\sqrt{P^{P pCnt A}} \in ℕ, 1, 0)$
143	134 137 126 142 56	letrd	$⊢ φ \to 0 \leq F (P^{P pCnt A})$
144	121 135	ifcli	$⊢ if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \in ℝ$
145	144	a1i	$⊢ φ \to if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \in ℝ$
146		breq2	$⊢ 1 = if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \to (0 \leq 1 \leftrightarrow 0 \leq if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0))$
147		breq2	$⊢ 0 = if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0))$
148	146 147 122 140	keephyp	$⊢ 0 \leq if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0)$
149	148	a1i	$⊢ φ \to 0 \leq if (\sqrt{\frac{A}{P^{P pCnt A}}} \in ℕ, 1, 0)$
150	134 145 128 149 118	letrd	$⊢ φ \to 0 \leq F (\frac{A}{P^{P pCnt A}})$
151	126 128 143 150	mulge0d	$⊢ φ \to 0 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
152	151	adantr	$⊢ (φ \land \neg \sqrt{A} \in ℕ) \to 0 \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
153	14 15 133 152	ifbothda	$⊢ φ \to if (\sqrt{A} \in ℕ, 1, 0) \leq F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
154	62	nncnd	$⊢ φ \to P^{P pCnt A} \in ℂ$
155	62	nnne0d	$⊢ φ \to P^{P pCnt A} \neq 0$
156	28 154 155	divcan2d	$⊢ φ \to P^{P pCnt A} (\frac{A}{P^{P pCnt A}}) = A$
157	156	fveq2d	$⊢ φ \to F (P^{P pCnt A} (\frac{A}{P^{P pCnt A}})) = F (A)$
158		pcndvds2	$⊢ (P \in ℙ \land A \in ℕ) \to \neg P ∥ (\frac{A}{P^{P pCnt A}})$
159	11 27 158	syl2anc	$⊢ φ \to \neg P ∥ (\frac{A}{P^{P pCnt A}})$
160		coprm	$⊢ (P \in ℙ \land \frac{A}{P^{P pCnt A}} \in ℤ) \to (\neg P ∥ (\frac{A}{P^{P pCnt A}}) \leftrightarrow P \gcd (\frac{A}{P^{P pCnt A}}) = 1)$
161	11 66 160	syl2anc	$⊢ φ \to (\neg P ∥ (\frac{A}{P^{P pCnt A}}) \leftrightarrow P \gcd (\frac{A}{P^{P pCnt A}}) = 1)$
162	159 161	mpbid	$⊢ φ \to P \gcd (\frac{A}{P^{P pCnt A}}) = 1$
163		prmz	$⊢ P \in ℙ \to P \in ℤ$
164	11 163	syl	$⊢ φ \to P \in ℤ$
165		rpexp1i	$⊢ (P \in ℤ \land \frac{A}{P^{P pCnt A}} \in ℤ \land P pCnt A \in ℕ_{0}) \to (P \gcd (\frac{A}{P^{P pCnt A}}) = 1 \to P^{P pCnt A} \gcd (\frac{A}{P^{P pCnt A}}) = 1)$
166	164 66 55 165	syl3anc	$⊢ φ \to (P \gcd (\frac{A}{P^{P pCnt A}}) = 1 \to P^{P pCnt A} \gcd (\frac{A}{P^{P pCnt A}}) = 1)$
167	162 166	mpd	$⊢ φ \to P^{P pCnt A} \gcd (\frac{A}{P^{P pCnt A}}) = 1$
168	1 2 3 4 5 6 7 8 62 65 167	dchrisum0fmul	$⊢ φ \to F (P^{P pCnt A} (\frac{A}{P^{P pCnt A}})) = F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
169	157 168	eqtr3d	$⊢ φ \to F (A) = F (P^{P pCnt A}) F (\frac{A}{P^{P pCnt A}})$
170	153 169	breqtrrd	$⊢ φ \to if (\sqrt{A} \in ℕ, 1, 0) \leq F (A)$

Metamath Proof Explorer

Theorem dchrisum0flblem2

Proof