Theorem chtppilimlem1

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Hypotheses	chtppilim.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	chtppilim.2	⊢ ( 𝜑 → 𝐴 < 1 )
	chtppilim.3	⊢ ( 𝜑 → 𝑁 ∈ ( 2 [,) +∞ ) )
	chtppilim.4	⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) < ( 1 − 𝐴 ) )
Assertion	chtppilimlem1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		chtppilim.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		chtppilim.2	⊢ ( 𝜑 → 𝐴 < 1 )
3		chtppilim.3	⊢ ( 𝜑 → 𝑁 ∈ ( 2 [,) +∞ ) )
4		chtppilim.4	⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) < ( 1 − 𝐴 ) )
5	1	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6	5	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7	6	sqvald	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
8	7	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 𝐴 · 𝐴 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
9		2re	⊢ 2 ∈ ℝ
10		elicopnf	⊢ ( 2 ∈ ℝ → ( 𝑁 ∈ ( 2 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) ) )
11	9 10	ax-mp	⊢ ( 𝑁 ∈ ( 2 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) )
12	3 11	sylib	⊢ ( 𝜑 → ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) )
13	12	simpld	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
14		ppicl	⊢ ( 𝑁 ∈ ℝ → ( π ‘ 𝑁 ) ∈ ℕ0 )
15	13 14	syl	⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℕ0 )
16	15	nn0red	⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℝ )
17	16	recnd	⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℂ )
18		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
19	9	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
20		2pos	⊢ 0 < 2
21	20	a1i	⊢ ( 𝜑 → 0 < 2 )
22	12	simprd	⊢ ( 𝜑 → 2 ≤ 𝑁 )
23	18 19 13 21 22	ltletrd	⊢ ( 𝜑 → 0 < 𝑁 )
24	13 23	elrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
25	24	relogcld	⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
26	25	recnd	⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
27	6 6 17 26	mul4d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐴 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
28	8 27	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
29	5 16	remulcld	⊢ ( 𝜑 → ( 𝐴 · ( π ‘ 𝑁 ) ) ∈ ℝ )
30	5 25	remulcld	⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ )
31	29 30	remulcld	⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ∈ ℝ )
32	24 5	rpcxpcld	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ+ )
33	32	rpred	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ )
34		ppicl	⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
35	33 34	syl	⊢ ( 𝜑 → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
36	35	nn0red	⊢ ( 𝜑 → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ )
37	16 36	resubcld	⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ∈ ℝ )
38	37 30	remulcld	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ∈ ℝ )
39		chtcl	⊢ ( 𝑁 ∈ ℝ → ( θ ‘ 𝑁 ) ∈ ℝ )
40	13 39	syl	⊢ ( 𝜑 → ( θ ‘ 𝑁 ) ∈ ℝ )
41		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
42		1lt2	⊢ 1 < 2
43	42	a1i	⊢ ( 𝜑 → 1 < 2 )
44	41 19 13 43 22	ltletrd	⊢ ( 𝜑 → 1 < 𝑁 )
45	13 44	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ+ )
46	1 45	rpmulcld	⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ+ )
47	16 33	resubcld	⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ )
48		ppinncl	⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℕ )
49	12 48	syl	⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℕ )
50	33 49	nndivred	⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ∈ ℝ )
51	50 41 5 4	ltsub13d	⊢ ( 𝜑 → 𝐴 < ( 1 − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
52	33	recnd	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℂ )
53	49	nnrpd	⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℝ+ )
54	53	rpcnne0d	⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑁 ) ≠ 0 ) )
55		divsubdir	⊢ ( ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( 𝑁 ↑𝑐 𝐴 ) ∈ ℂ ∧ ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑁 ) ≠ 0 ) ) → ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) = ( ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
56	17 52 54 55	syl3anc	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) = ( ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
57		divid	⊢ ( ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑁 ) ≠ 0 ) → ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) = 1 )
58	54 57	syl	⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) = 1 )
59	58	oveq1d	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) = ( 1 − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
60	56 59	eqtrd	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) = ( 1 − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
61	51 60	breqtrrd	⊢ ( 𝜑 → 𝐴 < ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) )
62	5 47 53	ltmuldivd	⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) < ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) ↔ 𝐴 < ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) ) )
63	61 62	mpbird	⊢ ( 𝜑 → ( 𝐴 · ( π ‘ 𝑁 ) ) < ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) )
64		ppiltx	⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ+ → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) < ( 𝑁 ↑𝑐 𝐴 ) )
65	32 64	syl	⊢ ( 𝜑 → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) < ( 𝑁 ↑𝑐 𝐴 ) )
66	36 33 16 65	ltsub2dd	⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) < ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
67	29 47 37 63 66	lttrd	⊢ ( 𝜑 → ( 𝐴 · ( π ‘ 𝑁 ) ) < ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
68	29 37 46 67	ltmul1dd	⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) < ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
69		fzfid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin )
70		inss1	⊢ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) )
71		ssfi	⊢ ( ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ) → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
72	69 70 71	sylancl	⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
73		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
74	73	elin2d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
75		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
76	75	nnrpd	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ+ )
77	74 76	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
78	77	relogcld	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
79	72 78	fsumrecl	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ∈ ℝ )
80	30	recnd	⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℂ )
81		fsumconst	⊢ ( ( ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin ∧ ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℂ ) → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) = ( ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
82	72 80 81	syl2anc	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) = ( ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
83		ppifl	⊢ ( 𝑁 ∈ ℝ → ( π ‘ ( ⌊ ‘ 𝑁 ) ) = ( π ‘ 𝑁 ) )
84	13 83	syl	⊢ ( 𝜑 → ( π ‘ ( ⌊ ‘ 𝑁 ) ) = ( π ‘ 𝑁 ) )
85		ppifl	⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) = ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) )
86	33 85	syl	⊢ ( 𝜑 → ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) = ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) )
87	84 86	oveq12d	⊢ ( 𝜑 → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ) = ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
88	41 13 44	ltled	⊢ ( 𝜑 → 1 ≤ 𝑁 )
89		1re	⊢ 1 ∈ ℝ
90		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 < 1 → 𝐴 ≤ 1 ) )
91	5 89 90	sylancl	⊢ ( 𝜑 → ( 𝐴 < 1 → 𝐴 ≤ 1 ) )
92	2 91	mpd	⊢ ( 𝜑 → 𝐴 ≤ 1 )
93	13 88 5 41 92	cxplead	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( 𝑁 ↑𝑐 1 ) )
94	13	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
95	94	cxp1d	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 1 ) = 𝑁 )
96	93 95	breqtrd	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ≤ 𝑁 )
97		flword2	⊢ ( ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ↑𝑐 𝐴 ) ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
98	33 13 96 97	syl3anc	⊢ ( 𝜑 → ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
99		ppidif	⊢ ( ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ) = ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
100	98 99	syl	⊢ ( 𝜑 → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ) = ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
101	87 100	eqtr3d	⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) = ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
102	101	oveq1d	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) = ( ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
103	82 102	eqtr4d	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) = ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
104	30	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ )
105	33	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ )
106		reflcl	⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ )
107		peano2re	⊢ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℝ )
108	33 106 107	3syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℝ )
109	108	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℝ )
110	77	rpred	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
111		fllep1	⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) )
112	33 111	syl	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) )
113	112	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) )
114	73	elin1d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) )
115		elfzle1	⊢ ( 𝑝 ∈ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ≤ 𝑝 )
116	114 115	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ≤ 𝑝 )
117	105 109 110 113 116	letrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑁 ↑𝑐 𝐴 ) ≤ 𝑝 )
118	24	rpne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
119	94 118 6	cxpefd	⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
120	119	eqcomd	⊢ ( 𝜑 → ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) = ( 𝑁 ↑𝑐 𝐴 ) )
121	120	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) = ( 𝑁 ↑𝑐 𝐴 ) )
122	77	reeflogd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) = 𝑝 )
123	117 121 122	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑝 ) ) )
124		efle	⊢ ( ( ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ ∧ ( log ‘ 𝑝 ) ∈ ℝ ) → ( ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ ( log ‘ 𝑝 ) ↔ ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑝 ) ) ) )
125	104 78 124	syl2anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ ( log ‘ 𝑝 ) ↔ ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑝 ) ) ) )
126	123 125	mpbird	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ ( log ‘ 𝑝 ) )
127	72 104 78 126	fsumle	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
128	103 127	eqbrtrrd	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
129		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin )
130		inss1	⊢ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) )
131		ssfi	⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
132	129 130 131	sylancl	⊢ ( 𝜑 → ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
133		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
134	133	elin2d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
135		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
136	134 135	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
137		eluz2b2	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
138	136 137	sylib	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
139	138	simpld	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
140	139	nnred	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
141	138	simprd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 1 < 𝑝 )
142	140 141	rplogcld	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
143	142	rpred	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
144	142	rpge0d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 0 ≤ ( log ‘ 𝑝 ) )
145	32	rpge0d	⊢ ( 𝜑 → 0 ≤ ( 𝑁 ↑𝑐 𝐴 ) )
146		flge0nn0	⊢ ( ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ↑𝑐 𝐴 ) ) → ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
147	33 145 146	syl2anc	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
148		nn0p1nn	⊢ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℕ )
149	147 148	syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℕ )
150		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
151	149 150	eleqtrdi	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
152		fzss1	⊢ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) ) )
153		ssrin	⊢ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) ) → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
154	151 152 153	3syl	⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
155	132 143 144 154	fsumless	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ≤ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
156		chtval	⊢ ( 𝑁 ∈ ℝ → ( θ ‘ 𝑁 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
157	13 156	syl	⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
158		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
159		ppisval2	⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
160	13 158 159	sylancl	⊢ ( 𝜑 → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
161	160	sumeq1d	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
162	157 161	eqtrd	⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
163	155 162	breqtrrd	⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ≤ ( θ ‘ 𝑁 ) )
164	38 79 40 128 163	letrd	⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( θ ‘ 𝑁 ) )
165	31 38 40 68 164	ltletrd	⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )
166	28 165	eqbrtrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )