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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum2.1	⊢ 1 = ( 0_g ‘ 𝐺 )
	dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
	dchrisum0f.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum0flb.r	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
	dchrisum0flb.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
	dchrisum0flb.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	dchrisum0flb.3	⊢ ( 𝜑 → 𝑃 ∥ 𝐴 )
	dchrisum0flb.4	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ..^ 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
Assertion	dchrisum0flblem2	⊢ ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum2.1	⊢ 1 = ( 0_g ‘ 𝐺 )
7		dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
8		dchrisum0f.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		dchrisum0flb.r	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
10		dchrisum0flb.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
11		dchrisum0flb.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
12		dchrisum0flb.3	⊢ ( 𝜑 → 𝑃 ∥ 𝐴 )
13		dchrisum0flb.4	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ..^ 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
14		breq1	⊢ ( 1 = if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) → ( 1 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ↔ if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
15		breq1	⊢ ( 0 = if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ↔ if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
16		1t1e1	⊢ ( 1 · 1 ) = 1
17	11	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝑃 ∈ ℙ )
18		nnq	⊢ ( ( √ ‘ 𝐴 ) ∈ ℕ → ( √ ‘ 𝐴 ) ∈ ℚ )
19	18	adantl	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ 𝐴 ) ∈ ℚ )
20		nnne0	⊢ ( ( √ ‘ 𝐴 ) ∈ ℕ → ( √ ‘ 𝐴 ) ≠ 0 )
21	20	adantl	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ 𝐴 ) ≠ 0 )
22		2z	⊢ 2 ∈ ℤ
23	22	a1i	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 2 ∈ ℤ )
24		pcexp	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( √ ‘ 𝐴 ) ∈ ℚ ∧ ( √ ‘ 𝐴 ) ≠ 0 ) ∧ 2 ∈ ℤ ) → ( 𝑃 pCnt ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
25	17 19 21 23 24	syl121anc	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
26		eluz2nn	⊢ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) → 𝐴 ∈ ℕ )
27	10 26	syl	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
28	27	nncnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
29	28	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℂ )
30	29	sqsqrtd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
31	30	oveq2d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( 𝑃 pCnt 𝐴 ) )
32		2cnd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 2 ∈ ℂ )
33		simpr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ 𝐴 ) ∈ ℕ )
34	17 33	pccld	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ∈ ℕ₀ )
35	34	nn0cnd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ∈ ℂ )
36	32 35	mulcomd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 2 · ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) = ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) )
37	25 31 36	3eqtr3rd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) = ( 𝑃 pCnt 𝐴 ) )
38	37	oveq2d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
39		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
40	17 39	syl	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝑃 ∈ ℕ )
41	40	nncnd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝑃 ∈ ℂ )
42		2nn0	⊢ 2 ∈ ℕ₀
43	42	a1i	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 2 ∈ ℕ₀ )
44	41 43 34	expmuld	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) )
45	38 44	eqtr3d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) )
46	45	fveq2d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( √ ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) ) )
47	40 34	nnexpcld	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℕ )
48	47	nnrpd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℝ⁺ )
49	48	rprege0d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ) )
50		sqrtsq	⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ) → ( √ ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
51	49 50	syl	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
52	46 51	eqtrd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
53	52 47	eqeltrd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ )
54	53	iftrued	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) = 1 )
55	11 27	pccld	⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ∈ ℕ₀ )
56	1 2 3 4 5 6 7 8 9 11 55	dchrisum0flblem1	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
57	56	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
58	54 57	eqbrtrrd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 1 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
59		pcdvds	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
60	11 27 59	syl2anc	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
61	11 39	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
62	61 55	nnexpcld	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
63		nndivdvds	⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ ) )
64	27 62 63	syl2anc	⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ ) )
65	60 64	mpbid	⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ )
66	65	nnzd	⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ )
67	66	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ )
68	27	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℕ )
69	68	nnrpd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℝ⁺ )
70	69	rprege0d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
71	62	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
72	71	nnrpd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ⁺ )
73		sqrtdiv	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ⁺ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
74	70 72 73	syl2anc	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
75		nnz	⊢ ( ( √ ‘ 𝐴 ) ∈ ℕ → ( √ ‘ 𝐴 ) ∈ ℤ )
76		znq	⊢ ( ( ( √ ‘ 𝐴 ) ∈ ℤ ∧ ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ ) → ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ )
77	75 53 76	syl2an2	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ )
78	74 77	eqeltrd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ )
79		zsqrtelqelz	⊢ ( ( ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ ∧ ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℤ )
80	67 78 79	syl2anc	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℤ )
81	65	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ )
82	81	nnrpd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ⁺ )
83	82	sqrtgt0d	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 0 < ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
84		elnnz	⊢ ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ ↔ ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℤ ∧ 0 < ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
85	80 83 84	sylanbrc	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ )
86	85	iftrued	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) = 1 )
87		fveq2	⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
88	87	eleq1d	⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( ( √ ‘ 𝑦 ) ∈ ℕ ↔ ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ ) )
89	88	ifbid	⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) = if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) )
90		fveq2	⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
91	89 90	breq12d	⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
92		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
93	65 92	eleqtrdi	⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( ℤ_≥ ‘ 1 ) )
94	27	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
95	61	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
96		pcelnn	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ ↔ 𝑃 ∥ 𝐴 ) )
97	11 27 96	syl2anc	⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ ↔ 𝑃 ∥ 𝐴 ) )
98	12 97	mpbird	⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ∈ ℕ )
99		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ_≥ ‘ 2 ) )
100		eluz2gt1	⊢ ( 𝑃 ∈ ( ℤ_≥ ‘ 2 ) → 1 < 𝑃 )
101	11 99 100	3syl	⊢ ( 𝜑 → 1 < 𝑃 )
102		expgt1	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ ∧ 1 < 𝑃 ) → 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
103	95 98 101 102	syl3anc	⊢ ( 𝜑 → 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
104		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
105		0lt1	⊢ 0 < 1
106	105	a1i	⊢ ( 𝜑 → 0 < 1 )
107	62	nnred	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ )
108	62	nngt0d	⊢ ( 𝜑 → 0 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
109	27	nnred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
110	27	nngt0d	⊢ ( 𝜑 → 0 < 𝐴 )
111		ltdiv2	⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ ∧ 0 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < ( 𝐴 / 1 ) ) )
112	104 106 107 108 109 110 111	syl222anc	⊢ ( 𝜑 → ( 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < ( 𝐴 / 1 ) ) )
113	103 112	mpbid	⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < ( 𝐴 / 1 ) )
114	28	div1d	⊢ ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )
115	113 114	breqtrd	⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < 𝐴 )
116		elfzo2	⊢ ( ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( 1 ..^ 𝐴 ) ↔ ( ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < 𝐴 ) )
117	93 94 115 116	syl3anbrc	⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( 1 ..^ 𝐴 ) )
118	91 13 117	rspcdva	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
119	118	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
120	86 119	eqbrtrrd	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 1 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
121		1re	⊢ 1 ∈ ℝ
122		0le1	⊢ 0 ≤ 1
123	121 122	pm3.2i	⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 )
124	123	a1i	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 1 ∈ ℝ ∧ 0 ≤ 1 ) )
125	1 2 3 4 5 6 7 8 9	dchrisum0ff	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
126	125 62	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ )
127	126	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ )
128	125 65	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℝ )
129	128	adantr	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℝ )
130		lemul12a	⊢ ( ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ ) ∧ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℝ ) ) → ( ( 1 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∧ 1 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) → ( 1 · 1 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
131	124 127 124 129 130	syl22anc	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( 1 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∧ 1 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) → ( 1 · 1 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
132	58 120 131	mp2and	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 1 · 1 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
133	16 132	eqbrtrrid	⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 1 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
134		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
135		0re	⊢ 0 ∈ ℝ
136	121 135	ifcli	⊢ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ
137	136	a1i	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
138		breq2	⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 1 ↔ 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ) )
139		breq2	⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ) )
140		0le0	⊢ 0 ≤ 0
141	138 139 122 140	keephyp	⊢ 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 )
142	141	a1i	⊢ ( 𝜑 → 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) )
143	134 137 126 142 56	letrd	⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
144	121 135	ifcli	⊢ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ
145	144	a1i	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
146		breq2	⊢ ( 1 = if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 1 ↔ 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ) )
147		breq2	⊢ ( 0 = if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ) )
148	146 147 122 140	keephyp	⊢ 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 )
149	148	a1i	⊢ ( 𝜑 → 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) )
150	134 145 128 149 118	letrd	⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
151	126 128 143 150	mulge0d	⊢ ( 𝜑 → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
152	151	adantr	⊢ ( ( 𝜑 ∧ ¬ ( √ ‘ 𝐴 ) ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
153	14 15 133 152	ifbothda	⊢ ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
154	62	nncnd	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℂ )
155	62	nnne0d	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ≠ 0 )
156	28 154 155	divcan2d	⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 𝐴 )
157	156	fveq2d	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) = ( 𝐹 ‘ 𝐴 ) )
158		pcndvds2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
159	11 27 158	syl2anc	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
160		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ↔ ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
161	11 66 160	syl2anc	⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ↔ ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
162	159 161	mpbid	⊢ ( 𝜑 → ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 )
163		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
164	11 163	syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
165		rpexp1i	⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ₀ ) → ( ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
166	164 66 55 165	syl3anc	⊢ ( 𝜑 → ( ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
167	162 166	mpd	⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 )
168	1 2 3 4 5 6 7 8 62 65 167	dchrisum0fmul	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
169	157 168	eqtr3d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
170	153 169	breqtrrd	⊢ ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem dchrisum0flblem2

Proof