Theorem rplogsumlem2

Description: Lemma for rplogsum . Equation 9.2.14 of Shapiro, p. 331. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Assertion	rplogsumlem2	⊢ ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ≤ 2 )

Proof

Step	Hyp	Ref	Expression
1		flid	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
2	1	oveq2d	⊢ ( 𝐴 ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( 1 ... 𝐴 ) )
3	2	sumeq1d	⊢ ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) )
4		fveq2	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
5		eleq1	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( 𝑛 ∈ ℙ ↔ ( 𝑝 ↑ 𝑘 ) ∈ ℙ ) )
6		fveq2	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( log ‘ 𝑛 ) = ( log ‘ ( 𝑝 ↑ 𝑘 ) ) )
7	5 6	ifbieq1d	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) = if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) )
8	4 7	oveq12d	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) )
9		id	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → 𝑛 = ( 𝑝 ↑ 𝑘 ) )
10	8 9	oveq12d	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
11		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
12		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
14		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
15	13 14	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
16	13	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ+ )
17	16	relogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
18		0re	⊢ 0 ∈ ℝ
19		ifcl	⊢ ( ( ( log ‘ 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ∈ ℝ )
20	17 18 19	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ∈ ℝ )
21	15 20	resubcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ∈ ℝ )
22	21 13	nndivred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ∈ ℝ )
23	22	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ∈ ℂ )
24		simprr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( Λ ‘ 𝑛 ) = 0 )
25		vmaprm	⊢ ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) = ( log ‘ 𝑛 ) )
26		prmnn	⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℕ )
27	26	nnred	⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℝ )
28		prmgt1	⊢ ( 𝑛 ∈ ℙ → 1 < 𝑛 )
29	27 28	rplogcld	⊢ ( 𝑛 ∈ ℙ → ( log ‘ 𝑛 ) ∈ ℝ+ )
30	25 29	eqeltrd	⊢ ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) ∈ ℝ+ )
31	30	rpne0d	⊢ ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) ≠ 0 )
32	31	necon2bi	⊢ ( ( Λ ‘ 𝑛 ) = 0 → ¬ 𝑛 ∈ ℙ )
33	32	ad2antll	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ¬ 𝑛 ∈ ℙ )
34	33	iffalsed	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) = 0 )
35	24 34	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = ( 0 − 0 ) )
36		0m0e0	⊢ ( 0 − 0 ) = 0
37	35 36	eqtrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = 0 )
38	37	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = ( 0 / 𝑛 ) )
39	12	ad2antrl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ∈ ℕ )
40	39	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ∈ ℝ+ )
41	40	rpcnne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
42		div0	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) → ( 0 / 𝑛 ) = 0 )
43	41 42	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( 0 / 𝑛 ) = 0 )
44	38 43	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = 0 )
45	10 11 23 44	fsumvma2	⊢ ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
46	3 45	eqtr3d	⊢ ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
47		fzfid	⊢ ( 𝐴 ∈ ℤ → ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ∈ Fin )
48		simpr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
49	48	elin2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
50		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
51	49 50	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
52	51	nnred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
53	11	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ )
54		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
55	54	abscld	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℝ )
56		peano2re	⊢ ( ( abs ‘ 𝐴 ) ∈ ℝ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
57	55 56	syl	⊢ ( 𝐴 ∈ ℤ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
58	57	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
59		elinel1	⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ( 0 [,] 𝐴 ) )
60		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
61	18 11 60	sylancr	⊢ ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
62	59 61	imbitrid	⊢ ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
63	62	imp	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) )
64	63	simp3d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ 𝐴 )
65	54	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℂ )
66	65	abscld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
67	53	leabsd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
68	66	lep1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( abs ‘ 𝐴 ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) )
69	53 66 58 67 68	letrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ≤ ( ( abs ‘ 𝐴 ) + 1 ) )
70	52 53 58 64 69	letrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ ( ( abs ‘ 𝐴 ) + 1 ) )
71		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
72	49 71	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
73		nn0abscl	⊢ ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℕ0 )
74		nn0p1nn	⊢ ( ( abs ‘ 𝐴 ) ∈ ℕ0 → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℕ )
75	73 74	syl	⊢ ( 𝐴 ∈ ℤ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℕ )
76	75	nnzd	⊢ ( 𝐴 ∈ ℤ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℤ )
77	76	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℤ )
78		elfz5	⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℤ ) → ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ↔ 𝑝 ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
79	72 77 78	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ↔ 𝑝 ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
80	70 79	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) )
81	80	ex	⊢ ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) )
82	81	ssrdv	⊢ ( 𝐴 ∈ ℤ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) )
83	47 82	ssfid	⊢ ( 𝐴 ∈ ℤ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
84		fzfid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
85		simprl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
86	85	elin2d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℙ )
87		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
88	87	ad2antll	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ )
89		vmappw	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
90	86 88 89	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
91	51	adantrr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℕ )
92	91	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℝ+ )
93	92	relogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
94	90 93	eqeltrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
95	88	nnnn0d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ0 )
96		nnexpcl	⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
97	91 95 96	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
98	97	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ+ )
99	98	relogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
100		ifcl	⊢ ( ( ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ∈ ℝ )
101	99 18 100	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ∈ ℝ )
102	94 101	resubcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) ∈ ℝ )
103	102 97	nndivred	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
104	103	anassrs	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
105	84 104	fsumrecl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
106	83 105	fsumrecl	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
107	51	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
108	107	relogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
109		uz2m1nn	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑝 − 1 ) ∈ ℕ )
110	72 109	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 − 1 ) ∈ ℕ )
111	51 110	nnmulcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℕ )
112	108 111	nndivred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
113	83 112	fsumrecl	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
114		2re	⊢ 2 ∈ ℝ
115	114	a1i	⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℝ )
116	18	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ∈ ℝ )
117	51	nngt0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝑝 )
118	116 52 53 117 64	ltletrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝐴 )
119	53 118	elrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ+ )
120	119	relogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
121		prmgt1	⊢ ( 𝑝 ∈ ℙ → 1 < 𝑝 )
122	49 121	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 )
123	52 122	rplogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
124	120 123	rerpdivcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
125	123	rpcnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
126	125	mullidd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 · ( log ‘ 𝑝 ) ) = ( log ‘ 𝑝 ) )
127	107 119	logled	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ≤ 𝐴 ↔ ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ) )
128	64 127	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) )
129	126 128	eqbrtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) )
130		1re	⊢ 1 ∈ ℝ
131	130	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ∈ ℝ )
132	131 120 123	lemuldivd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
133	129 132	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
134		flge1nn	⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ )
135	124 133 134	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ )
136		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
137	135 136	eleqtrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ( ℤ≥ ‘ 1 ) )
138	103	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
139	138	anassrs	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
140		oveq2	⊢ ( 𝑘 = 1 → ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ 1 ) )
141	140	fveq2d	⊢ ( 𝑘 = 1 → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( Λ ‘ ( 𝑝 ↑ 1 ) ) )
142	140	eleq1d	⊢ ( 𝑘 = 1 → ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ ↔ ( 𝑝 ↑ 1 ) ∈ ℙ ) )
143	140	fveq2d	⊢ ( 𝑘 = 1 → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ ( 𝑝 ↑ 1 ) ) )
144	142 143	ifbieq1d	⊢ ( 𝑘 = 1 → if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) = if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) )
145	141 144	oveq12d	⊢ ( 𝑘 = 1 → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) = ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) )
146	145 140	oveq12d	⊢ ( 𝑘 = 1 → ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) )
147	137 139 146	fsum1p	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) + Σ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
148	51	nncnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℂ )
149	148	exp1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ↑ 1 ) = 𝑝 )
150	149	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ ( 𝑝 ↑ 1 ) ) = ( Λ ‘ 𝑝 ) )
151		vmaprm	⊢ ( 𝑝 ∈ ℙ → ( Λ ‘ 𝑝 ) = ( log ‘ 𝑝 ) )
152	49 151	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ 𝑝 ) = ( log ‘ 𝑝 ) )
153	150 152	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ ( 𝑝 ↑ 1 ) ) = ( log ‘ 𝑝 ) )
154	149 49	eqeltrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ↑ 1 ) ∈ ℙ )
155	154	iftrued	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) = ( log ‘ ( 𝑝 ↑ 1 ) ) )
156	149	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ ( 𝑝 ↑ 1 ) ) = ( log ‘ 𝑝 ) )
157	155 156	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) = ( log ‘ 𝑝 ) )
158	153 157	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) = ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) )
159	125	subidd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) = 0 )
160	158 159	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) = 0 )
161	160 149	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) = ( 0 / 𝑝 ) )
162	107	rpcnne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) )
163		div0	⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) → ( 0 / 𝑝 ) = 0 )
164	162 163	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 0 / 𝑝 ) = 0 )
165	161 164	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) = 0 )
166		1p1e2	⊢ ( 1 + 1 ) = 2
167	166	oveq1i	⊢ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
168	167	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
169		elfzuz	⊢ ( 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
170		eluz2nn	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 𝑘 ∈ ℕ )
171	169 170	syl	⊢ ( 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
172	171 167	eleq2s	⊢ ( 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
173	49 172 89	syl2an	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
174	51	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑝 ∈ ℕ )
175		nnq	⊢ ( 𝑝 ∈ ℕ → 𝑝 ∈ ℚ )
176	174 175	syl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑝 ∈ ℚ )
177	169 167	eleq2s	⊢ ( 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
178	177	adantl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
179		expnprm	⊢ ( ( 𝑝 ∈ ℚ ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝑝 ↑ 𝑘 ) ∈ ℙ )
180	176 178 179	syl2anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ¬ ( 𝑝 ↑ 𝑘 ) ∈ ℙ )
181	180	iffalsed	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) = 0 )
182	173 181	oveq12d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) = ( ( log ‘ 𝑝 ) − 0 ) )
183	125	subid1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) − 0 ) = ( log ‘ 𝑝 ) )
184	183	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) − 0 ) = ( log ‘ 𝑝 ) )
185	182 184	eqtrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) = ( log ‘ 𝑝 ) )
186	185	oveq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) )
187	168 186	sumeq12dv	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) )
188	165 187	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) + Σ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = ( 0 + Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ) )
189		fzfid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
190	108	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ∈ ℝ )
191		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
192	51 191 96	syl2an	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
193	190 192	nndivred	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
194	171 193	sylan2	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
195	189 194	fsumrecl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
196	195	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
197	196	addlidd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 0 + Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) )
198	147 188 197	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) )
199	107	rpreccld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ∈ ℝ+ )
200	124	flcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
201	200	peano2zd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℤ )
202	199 201	rpexpcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ∈ ℝ+ )
203	202	rpge0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
204	51	nnrecred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ∈ ℝ )
205	204	resqcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ 2 ) ∈ ℝ )
206	135	peano2nnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℕ )
207	206	nnnn0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℕ0 )
208	204 207	reexpcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ∈ ℝ )
209	205 208	subge02d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 0 ≤ ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ↔ ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 / 𝑝 ) ↑ 2 ) ) )
210	203 209	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 / 𝑝 ) ↑ 2 ) )
211	110	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 − 1 ) ∈ ℝ+ )
212	211	rpcnne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) )
213	199	rpcnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ∈ ℂ )
214		dmdcan	⊢ ( ( ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ∧ ( 1 / 𝑝 ) ∈ ℂ ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) ) = ( ( 1 / 𝑝 ) / 𝑝 ) )
215	212 162 213 214	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) ) = ( ( 1 / 𝑝 ) / 𝑝 ) )
216	131	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ∈ ℂ )
217		divsubdir	⊢ ( ( 𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) )
218	148 216 162 217	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) )
219		divid	⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) → ( 𝑝 / 𝑝 ) = 1 )
220	162 219	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 / 𝑝 ) = 1 )
221	220	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) = ( 1 − ( 1 / 𝑝 ) ) )
222	218 221	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( 1 − ( 1 / 𝑝 ) ) )
223		divdiv1	⊢ ( ( 1 ∈ ℂ ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ∧ ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) ) → ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) = ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
224	216 162 212 223	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) = ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
225	222 224	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) ) = ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
226	51	nnne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≠ 0 )
227	213 148 226	divrecd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) / 𝑝 ) = ( ( 1 / 𝑝 ) · ( 1 / 𝑝 ) ) )
228	213	sqvald	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ 2 ) = ( ( 1 / 𝑝 ) · ( 1 / 𝑝 ) ) )
229	227 228	eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) / 𝑝 ) = ( ( 1 / 𝑝 ) ↑ 2 ) )
230	215 225 229	3eqtr3d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) = ( ( 1 / 𝑝 ) ↑ 2 ) )
231	210 230	breqtrrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
232	205 208	resubcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ∈ ℝ )
233	111	nnrecred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
234		resubcl	⊢ ( ( 1 ∈ ℝ ∧ ( 1 / 𝑝 ) ∈ ℝ ) → ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ )
235	130 204 234	sylancr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ )
236		recgt1	⊢ ( ( 𝑝 ∈ ℝ ∧ 0 < 𝑝 ) → ( 1 < 𝑝 ↔ ( 1 / 𝑝 ) < 1 ) )
237	52 117 236	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 < 𝑝 ↔ ( 1 / 𝑝 ) < 1 ) )
238	122 237	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) < 1 )
239		posdif	⊢ ( ( ( 1 / 𝑝 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 𝑝 ) < 1 ↔ 0 < ( 1 − ( 1 / 𝑝 ) ) ) )
240	204 130 239	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) < 1 ↔ 0 < ( 1 − ( 1 / 𝑝 ) ) ) )
241	238 240	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < ( 1 − ( 1 / 𝑝 ) ) )
242		ledivmul	⊢ ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ∈ ℝ ∧ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ ∧ ( ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ ∧ 0 < ( 1 − ( 1 / 𝑝 ) ) ) ) → ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ↔ ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) ) )
243	232 233 235 241 242	syl112anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ↔ ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) ) )
244	231 243	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
245	235 241	elrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ+ )
246	232 245	rerpdivcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ∈ ℝ )
247	246 233 123	lemul2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ↔ ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) ) )
248	244 247	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
249	125	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ∈ ℂ )
250	192	nncnd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℂ )
251	192	nnne0d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ≠ 0 )
252	249 250 251	divrecd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 ↑ 𝑘 ) ) ) )
253	148	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℂ )
254	51	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℕ )
255	254	nnne0d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ≠ 0 )
256		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
257	256	adantl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
258	253 255 257	exprecd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( 1 / ( 𝑝 ↑ 𝑘 ) ) )
259	258	oveq2d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 ↑ 𝑘 ) ) ) )
260	252 259	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
261	171 260	sylan2	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
262	261	sumeq2dv	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
263	171	nnnn0d	⊢ ( 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ0 )
264		expcl	⊢ ( ( ( 1 / 𝑝 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
265	213 263 264	syl2an	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
266	189 125 265	fsummulc2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
267		fzval3	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ → ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
268	200 267	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
269	268	sumeq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) )
270	204 238	ltned	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ≠ 1 )
271		2nn0	⊢ 2 ∈ ℕ0
272	271	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 2 ∈ ℕ0 )
273		eluzp1p1	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
274	137 273	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
275		df-2	⊢ 2 = ( 1 + 1 )
276	275	fveq2i	⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
277	274 276	eleqtrrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
278	213 270 272 277	geoserg	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) )
279	269 278	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) )
280	279	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) )
281	262 266 280	3eqtr2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) )
282	111	nncnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℂ )
283	111	nnne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ≠ 0 )
284	125 282 283	divrecd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
285	248 281 284	3brtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 ↑ 𝑘 ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
286	198 285	eqbrtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
287	83 105 112 286	fsumle	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ≤ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
288		elfzuz	⊢ ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
289		eluz2nn	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 𝑝 ∈ ℕ )
290	288 289	syl	⊢ ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) → 𝑝 ∈ ℕ )
291	290	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 𝑝 ∈ ℕ )
292	291	nnred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 𝑝 ∈ ℝ )
293	288	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
294		eluz2gt1	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
295	293 294	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 1 < 𝑝 )
296	292 295	rplogcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
297	293 109	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( 𝑝 − 1 ) ∈ ℕ )
298	291 297	nnmulcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℕ )
299	298	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℝ+ )
300	296 299	rpdivcld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ+ )
301	300	rpred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
302	47 301	fsumrecl	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
303	300	rpge0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 0 ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
304	47 301 303 82	fsumless	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
305		rplogsumlem1	⊢ ( ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℕ → Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ 2 )
306	75 305	syl	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ 2 )
307	113 302 115 304 306	letrd	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ 2 )
308	106 113 115 287 307	letrd	⊢ ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) − if ( ( 𝑝 ↑ 𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 𝑘 ) ) , 0 ) ) / ( 𝑝 ↑ 𝑘 ) ) ≤ 2 )
309	46 308	eqbrtrd	⊢ ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ≤ 2 )