Theorem chpchtsum

Description: The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	chpchtsum	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
2		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
3	2	elin2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
4		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
6	5	nnrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
7	6	relogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
9		fsumconst	⊢ ( ( ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin ∧ ( log ‘ 𝑝 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
10	1 8 9	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
11		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ )
12		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ∈ ℝ )
13	5	nnred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
14		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
15	3 14	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
16		eluz2gt1	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
17	15 16	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 )
18	2	elin1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 0 [,] 𝐴 ) )
19		0re	⊢ 0 ∈ ℝ
20		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
21	19 11 20	sylancr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
22	18 21	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) )
23	22	simp3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ 𝐴 )
24	12 13 11 17 23	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝐴 )
25	11 24	rplogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
26	13 17	rplogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
27	25 26	rpdivcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ+ )
28	27	rpred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
29	27	rpge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
30		flge0nn0	⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
31	28 29 30	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
32		hashfz1	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
33	31 32	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
34	33	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) = ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) )
35	28	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
36	35	zcnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℂ )
37	36 8	mulcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
38	10 34 37	3eqtrrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
39	38	sumeq2dv	⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
40		chpval2	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
41		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
42		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ∈ ℝ )
43		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 1 ∈ ℝ )
44		0lt1	⊢ 0 < 1
45	44	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 < 1 )
46		elfzuz2	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
47		eluzle	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ≤ ( ⌊ ‘ 𝐴 ) )
48	47	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → 1 ≤ ( ⌊ ‘ 𝐴 ) )
49		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → 𝐴 ∈ ℝ )
50		1z	⊢ 1 ∈ ℤ
51		flge	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ 𝐴 ↔ 1 ≤ ( ⌊ ‘ 𝐴 ) ) )
52	49 50 51	sylancl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( 1 ≤ 𝐴 ↔ 1 ≤ ( ⌊ ‘ 𝐴 ) ) )
53	48 52	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → 1 ≤ 𝐴 )
54	46 53	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 1 ≤ 𝐴 )
55	42 43 41 45 54	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 < 𝐴 )
56	42 41 55	ltled	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ≤ 𝐴 )
57		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ )
58	57	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑘 ∈ ℕ )
59	58	nnrecred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
60	41 56 59	recxpcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ )
61		chtval	⊢ ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ → ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
62	60 61	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
63	62	sumeq2dv	⊢ ( 𝐴 ∈ ℝ → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
64		ppifi	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
65		fzfid	⊢ ( 𝐴 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
66		elinel2	⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ℙ )
67		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
68	66 67	anim12i	⊢ ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
69	68	a1i	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
70		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ∈ ℝ )
71		inss2	⊢ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ℙ
72	71	a1i	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ℙ )
73	72	sselda	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
74	73 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
75	74	nnred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
76	74	nngt0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝑝 )
77	70 75 11 76 23	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝐴 )
78	77	ex	⊢ ( 𝐴 ∈ ℝ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 0 < 𝐴 ) )
79	78	adantrd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 0 < 𝐴 ) )
80	69 79	jcad	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) )
81		elinel2	⊢ ( 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) → 𝑝 ∈ ℙ )
82	57 81	anim12ci	⊢ ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
83	82	a1i	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
84	55	ex	⊢ ( 𝐴 ∈ ℝ → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 0 < 𝐴 ) )
85	84	adantrd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → 0 < 𝐴 ) )
86	83 85	jcad	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) )
87		elin	⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) )
88		simprll	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℙ )
89	88	biantrud	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) ) )
90		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ∈ ℝ )
91		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℝ )
92	88 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℕ )
93	92	nnred	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℝ )
94	92	nnnn0d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℕ0 )
95	94	nn0ge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ≤ 𝑝 )
96		df-3an	⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ 𝐴 ) )
97	20 96	bitrdi	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ 𝐴 ) ) )
98	97	baibd	⊢ ( ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
99	90 91 93 95 98	syl22anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
100	89 99	bitr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) ↔ 𝑝 ≤ 𝐴 ) )
101	87 100	bitrid	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ 𝑝 ≤ 𝐴 ) )
102		simprr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 < 𝐴 )
103	91 102	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℝ+ )
104	103	relogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
105	88 14	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
106	105 16	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 1 < 𝑝 )
107	93 106	rplogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
108	104 107	rerpdivcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
109		simprlr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℕ )
110	109	nnzd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℤ )
111		flge	⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
112	108 110 111	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
113	109	nnnn0d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℕ0 )
114	92 113	nnexpcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
115	114	nnrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ+ )
116	115 103	logled	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ) )
117	92	nnrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℝ+ )
118		relogexp	⊢ ( ( 𝑝 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
119	117 110 118	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
120	119	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ↔ ( 𝑘 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ) )
121	109	nnred	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℝ )
122	121 104 107	lemuldivd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑘 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
123	116 120 122	3bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
124		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
125	109 124	eleqtrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
126	108	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
127		elfz5	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
128	125 126 127	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
129	112 123 128	3bitr4rd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
130	101 129	anbi12d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑝 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
131	91	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
132		elfz5	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
133	125 131 132	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
134		flge	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ≤ 𝐴 ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
135	91 110 134	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ≤ 𝐴 ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
136	133 135	bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ 𝑘 ≤ 𝐴 ) )
137		elin	⊢ ( 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) )
138	88	biantrud	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) ) )
139	103	rpge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ≤ 𝐴 )
140	109	nnrecred	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 1 / 𝑘 ) ∈ ℝ )
141	91 139 140	recxpcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ )
142		elicc2	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ) )
143		df-3an	⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
144	142 143	bitrdi	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ) )
145	144	baibd	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
146	90 141 93 95 145	syl22anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
147	138 146	bitr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) ↔ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
148	91 139 140	cxpge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) )
149	109	nnrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℝ+ )
150	93 95 141 148 149	cxple2d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↔ ( 𝑝 ↑𝑐 𝑘 ) ≤ ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) ) )
151	92	nncnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℂ )
152		cxpexp	⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑝 ↑𝑐 𝑘 ) = ( 𝑝 ↑ 𝑘 ) )
153	151 113 152	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑𝑐 𝑘 ) = ( 𝑝 ↑ 𝑘 ) )
154	109	nncnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℂ )
155	109	nnne0d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ≠ 0 )
156	154 155	recid2d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 1 / 𝑘 ) · 𝑘 ) = 1 )
157	156	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑘 ) · 𝑘 ) ) = ( 𝐴 ↑𝑐 1 ) )
158	103 140 154	cxpmuld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑘 ) · 𝑘 ) ) = ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) )
159	91	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℂ )
160	159	cxp1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 1 ) = 𝐴 )
161	157 158 160	3eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) = 𝐴 )
162	153 161	breq12d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑𝑐 𝑘 ) ≤ ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
163	147 150 162	3bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
164	137 163	bitrid	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
165	136 164	anbi12d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ↔ ( 𝑘 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
166	114	nnred	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ )
167		bernneq3	⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 < ( 𝑝 ↑ 𝑘 ) )
168	105 113 167	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 < ( 𝑝 ↑ 𝑘 ) )
169	121 166 168	ltled	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ≤ ( 𝑝 ↑ 𝑘 ) )
170		letr	⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑘 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑘 ≤ 𝐴 ) )
171	121 166 91 170	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑘 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑘 ≤ 𝐴 ) )
172	169 171	mpand	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 → 𝑘 ≤ 𝐴 ) )
173	172	pm4.71rd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑘 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
174	151	exp1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 1 ) = 𝑝 )
175	92	nnge1d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 1 ≤ 𝑝 )
176	93 175 125	leexp2ad	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 1 ) ≤ ( 𝑝 ↑ 𝑘 ) )
177	174 176	eqbrtrrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) )
178		letr	⊢ ( ( 𝑝 ∈ ℝ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑝 ≤ 𝐴 ) )
179	93 166 91 178	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑝 ≤ 𝐴 ) )
180	177 179	mpand	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 → 𝑝 ≤ 𝐴 ) )
181	180	pm4.71rd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑝 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
182	165 173 181	3bitr2rd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) )
183	130 182	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) )
184	183	ex	⊢ ( 𝐴 ∈ ℝ → ( ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) ) )
185	80 86 184	pm5.21ndd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) )
186	8	adantrr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
187	64 65 1 185 186	fsumcom2	⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
188	63 187	eqtr4d	⊢ ( 𝐴 ∈ ℝ → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
189	39 40 188	3eqtr4d	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )