Theorem hgt750lemd 34285

Description: An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021.)

Hypotheses

Ref	Expression
hgt750lemc.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
hgt750lemd.0	⊢ (𝜑 → (;10↑;27) ≤ 𝑁)

Assertion

Ref	Expression
hgt750lemd	⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))

Distinct variable groups:   𝑖,𝑁   𝜑,𝑖

Proof of Theorem hgt750lemd

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 13976	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
2		diffi 9208	. . . . 5 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ∈ Fin)
4		vmaf 27069	. . . . . 6 ⊢ Λ:ℕ⟶ℝ
5	4	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) → Λ:ℕ⟶ℝ)
6		fz1ssnn 13570	. . . . . . . 8 ⊢ (1...𝑁) ⊆ ℕ
7	6	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
8	7	ssdifssd 4141	. . . . . 6 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
9	8	sselda 3980	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) → 𝑖 ∈ ℕ)
10	5, 9	ffvelcdmd 7098	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) → (Λ‘𝑖) ∈ ℝ)
11	3, 10	fsumrecl 15718	. . 3 ⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈ ℝ)
12		2rp 13017	. . . . 5 ⊢ 2 ∈ ℝ+
13	12	a1i 11	. . . 4 ⊢ (𝜑 → 2 ∈ ℝ+)
14	13	relogcld 26575	. . 3 ⊢ (𝜑 → (log‘2) ∈ ℝ)
15		1nn0 12524	. . . . . 6 ⊢ 1 ∈ ℕ0
16		4re 12332	. . . . . . . 8 ⊢ 4 ∈ ℝ
17		2re 12322	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
18		6re 12338	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
19	18, 17	pm3.2i 469	. . . . . . . . . . 11 ⊢ (6 ∈ ℝ ∧ 2 ∈ ℝ)
20		dp2cl 32621	. . . . . . . . . . 11 ⊢ ((6 ∈ ℝ ∧ 2 ∈ ℝ) → _62 ∈ ℝ)
21	19, 20	ax-mp 5	. . . . . . . . . 10 ⊢ _62 ∈ ℝ
22	17, 21	pm3.2i 469	. . . . . . . . 9 ⊢ (2 ∈ ℝ ∧ _62 ∈ ℝ)
23		dp2cl 32621	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ _62 ∈ ℝ) → _2_62 ∈ ℝ)
24	22, 23	ax-mp 5	. . . . . . . 8 ⊢ _2_62 ∈ ℝ
25	16, 24	pm3.2i 469	. . . . . . 7 ⊢ (4 ∈ ℝ ∧ _2_62 ∈ ℝ)
26		dp2cl 32621	. . . . . . 7 ⊢ ((4 ∈ ℝ ∧ _2_62 ∈ ℝ) → _4_2_62 ∈ ℝ)
27	25, 26	ax-mp 5	. . . . . 6 ⊢ _4_2_62 ∈ ℝ
28		dpcl 32632	. . . . . 6 ⊢ ((1 ∈ ℕ0 ∧ _4_2_62 ∈ ℝ) → (1._4_2_62) ∈ ℝ)
29	15, 27, 28	mp2an 690	. . . . 5 ⊢ (1._4_2_62) ∈ ℝ
30	29	a1i 11	. . . 4 ⊢ (𝜑 → (1._4_2_62) ∈ ℝ)
31		hgt750lemc.n	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
32	31	nnred 12263	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
33	31	nnrpd 13052	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ+)
34	33	rpge0d 13058	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑁)
35	32, 34	resqrtcld 15402	. . . 4 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
36	30, 35	remulcld 11280	. . 3 ⊢ (𝜑 → ((1._4_2_62) · (√‘𝑁)) ∈ ℝ)
37		0nn0 12523	. . . . . 6 ⊢ 0 ∈ ℕ0
38		0re 11252	. . . . . . . 8 ⊢ 0 ∈ ℝ
39		1re 11250	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
40	38, 39	pm3.2i 469	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ ∧ 1 ∈ ℝ)
41		dp2cl 32621	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → _01 ∈ ℝ)
42	40, 41	ax-mp 5	. . . . . . . . . 10 ⊢ _01 ∈ ℝ
43	38, 42	pm3.2i 469	. . . . . . . . 9 ⊢ (0 ∈ ℝ ∧ _01 ∈ ℝ)
44		dp2cl 32621	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ _01 ∈ ℝ) → _0_01 ∈ ℝ)
45	43, 44	ax-mp 5	. . . . . . . 8 ⊢ _0_01 ∈ ℝ
46	38, 45	pm3.2i 469	. . . . . . 7 ⊢ (0 ∈ ℝ ∧ _0_01 ∈ ℝ)
47		dp2cl 32621	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ _0_01 ∈ ℝ) → _0_0_01 ∈ ℝ)
48	46, 47	ax-mp 5	. . . . . 6 ⊢ _0_0_01 ∈ ℝ
49		dpcl 32632	. . . . . 6 ⊢ ((0 ∈ ℕ0 ∧ _0_0_01 ∈ ℝ) → (0._0_0_01) ∈ ℝ)
50	37, 48, 49	mp2an 690	. . . . 5 ⊢ (0._0_0_01) ∈ ℝ
51	50	a1i 11	. . . 4 ⊢ (𝜑 → (0._0_0_01) ∈ ℝ)
52	51, 35	remulcld 11280	. . 3 ⊢ (𝜑 → ((0._0_0_01) · (√‘𝑁)) ∈ ℝ)
53	31	nnzd 12621	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
54		chpvalz 34265	. . . . . . 7 ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖))
55	53, 54	syl 17	. . . . . 6 ⊢ (𝜑 → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖))
56		chtvalz 34266	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
57	53, 56	syl 17	. . . . . . 7 ⊢ (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
58		inss2 4230	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∩ ℙ) ⊆ ℙ
59	58	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∩ ℙ) ⊆ ℙ)
60	59	sselda 3980	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℙ)
61		vmaprm 27067	. . . . . . . . 9 ⊢ (𝑖 ∈ ℙ → (Λ‘𝑖) = (log‘𝑖))
62	60, 61	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) = (log‘𝑖))
63	62	sumeq2dv 15687	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
64	57, 63	eqtr4d 2770	. . . . . 6 ⊢ (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖))
65	55, 64	oveq12d 7442	. . . . 5 ⊢ (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) = (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)))
66		infi 9297	. . . . . . . 8 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∩ ℙ) ∈ Fin)
67	1, 66	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1...𝑁) ∩ ℙ) ∈ Fin)
68	4	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → Λ:ℕ⟶ℝ)
69		inss1 4229	. . . . . . . . . . . 12 ⊢ ((1...𝑁) ∩ ℙ) ⊆ (1...𝑁)
70	69, 6	sstri 3989	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∩ ℙ) ⊆ ℕ
71	70	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∩ ℙ) ⊆ ℕ)
72	71	sselda 3980	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℕ)
73	68, 72	ffvelcdmd 7098	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) ∈ ℝ)
74	73	recnd 11278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) ∈ ℂ)
75	67, 74	fsumcl 15717	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) ∈ ℂ)
76	10	recnd 11278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) → (Λ‘𝑖) ∈ ℂ)
77	3, 76	fsumcl 15717	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈ ℂ)
78		inindif 32330	. . . . . . . 8 ⊢ (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) = ∅
79	78	a1i 11	. . . . . . 7 ⊢ (𝜑 → (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) = ∅)
80		inundif 4480	. . . . . . . . 9 ⊢ (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ)) = (1...𝑁)
81	80	eqcomi 2736	. . . . . . . 8 ⊢ (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ))
82	81	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ)))
83	4	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
84	7	sselda 3980	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℕ)
85	83, 84	ffvelcdmd 7098	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℝ)
86	85	recnd 11278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℂ)
87	79, 82, 1, 86	fsumsplit 15725	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) + Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖)))
88	75, 77, 87	mvrladdd 11663	. . . . 5 ⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)) = Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖))
89	65, 88	eqtr2d 2768	. . . 4 ⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) = ((ψ‘𝑁) − (θ‘𝑁)))
90		fveq2 6900	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁))
91		fveq2 6900	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (θ‘𝑥) = (θ‘𝑁))
92	90, 91	oveq12d 7442	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((ψ‘𝑥) − (θ‘𝑥)) = ((ψ‘𝑁) − (θ‘𝑁)))
93		fveq2 6900	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (√‘𝑥) = (√‘𝑁))
94	93	oveq2d 7440	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((1._4_2_62) · (√‘𝑥)) = ((1._4_2_62) · (√‘𝑁)))
95	92, 94	breq12d 5163	. . . . 5 ⊢ (𝑥 = 𝑁 → (((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥)) ↔ ((ψ‘𝑁) − (θ‘𝑁)) < ((1._4_2_62) · (√‘𝑁))))
96		ax-ros336 34283	. . . . . 6 ⊢ ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥))
97	96	a1i 11	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥)))
98	95, 97, 33	rspcdva 3610	. . . 4 ⊢ (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) < ((1._4_2_62) · (√‘𝑁)))
99	89, 98	eqbrtrd 5172	. . 3 ⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) < ((1._4_2_62) · (√‘𝑁)))
100	39	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
101		log2le1 26900	. . . . 5 ⊢ (log‘2) < 1
102	101	a1i 11	. . . 4 ⊢ (𝜑 → (log‘2) < 1)
103		10nn0 12731	. . . . . . . . 9 ⊢ ;10 ∈ ℕ0
104		7nn0 12530	. . . . . . . . 9 ⊢ 7 ∈ ℕ0
105	103, 104	nn0expcli 14091	. . . . . . . 8 ⊢ (;10↑7) ∈ ℕ0
106	105	nn0rei 12519	. . . . . . 7 ⊢ (;10↑7) ∈ ℝ
107	106	a1i 11	. . . . . 6 ⊢ (𝜑 → (;10↑7) ∈ ℝ)
108	51, 107	remulcld 11280	. . . . 5 ⊢ (𝜑 → ((0._0_0_01) · (;10↑7)) ∈ ℝ)
109	103	nn0rei 12519	. . . . . . . . . . 11 ⊢ ;10 ∈ ℝ
110		0z 12605	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
111		3z 12631	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
112	109, 110, 111	3pm3.2i 1336	. . . . . . . . . 10 ⊢ (;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ)
113		1lt10 12852	. . . . . . . . . . 11 ⊢ 1 < ;10
114		3pos 12353	. . . . . . . . . . 11 ⊢ 0 < 3
115	113, 114	pm3.2i 469	. . . . . . . . . 10 ⊢ (1 < ;10 ∧ 0 < 3)
116		ltexp2a 14168	. . . . . . . . . 10 ⊢ (((;10 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < 3)) → (;10↑0) < (;10↑3))
117	112, 115, 116	mp2an 690	. . . . . . . . 9 ⊢ (;10↑0) < (;10↑3)
118	103	numexp0 17050	. . . . . . . . . 10 ⊢ (;10↑0) = 1
119	118	eqcomi 2736	. . . . . . . . 9 ⊢ 1 = (;10↑0)
120	109	recni 11264	. . . . . . . . . . 11 ⊢ ;10 ∈ ℂ
121		10pos 12730	. . . . . . . . . . . 12 ⊢ 0 < ;10
122	38, 121	gtneii 11362	. . . . . . . . . . 11 ⊢ ;10 ≠ 0
123		4z 12632	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
124		expm1 14115	. . . . . . . . . . 11 ⊢ ((;10 ∈ ℂ ∧ ;10 ≠ 0 ∧ 4 ∈ ℤ) → (;10↑(4 − 1)) = ((;10↑4) / ;10))
125	120, 122, 123, 124	mp3an 1457	. . . . . . . . . 10 ⊢ (;10↑(4 − 1)) = ((;10↑4) / ;10)
126		4m1e3 12377	. . . . . . . . . . 11 ⊢ (4 − 1) = 3
127	126	oveq2i 7435	. . . . . . . . . 10 ⊢ (;10↑(4 − 1)) = (;10↑3)
128		4nn0 12527	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ0
129	103, 128	nn0expcli 14091	. . . . . . . . . . . 12 ⊢ (;10↑4) ∈ ℕ0
130	129	nn0cni 12520	. . . . . . . . . . 11 ⊢ (;10↑4) ∈ ℂ
131		divrec2 11925	. . . . . . . . . . 11 ⊢ (((;10↑4) ∈ ℂ ∧ ;10 ∈ ℂ ∧ ;10 ≠ 0) → ((;10↑4) / ;10) = ((1 / ;10) · (;10↑4)))
132	130, 120, 122, 131	mp3an 1457	. . . . . . . . . 10 ⊢ ((;10↑4) / ;10) = ((1 / ;10) · (;10↑4))
133	125, 127, 132	3eqtr3ri 2764	. . . . . . . . 9 ⊢ ((1 / ;10) · (;10↑4)) = (;10↑3)
134	117, 119, 133	3brtr4i 5180	. . . . . . . 8 ⊢ 1 < ((1 / ;10) · (;10↑4))
135		1rp 13016	. . . . . . . . . 10 ⊢ 1 ∈ ℝ+
136	135	dp0h 32643	. . . . . . . . 9 ⊢ (0.1) = (1 / ;10)
137	136	oveq1i 7434	. . . . . . . 8 ⊢ ((0.1) · (;10↑4)) = ((1 / ;10) · (;10↑4))
138	134, 137	breqtrri 5177	. . . . . . 7 ⊢ 1 < ((0.1) · (;10↑4))
139	138	a1i 11	. . . . . 6 ⊢ (𝜑 → 1 < ((0.1) · (;10↑4)))
140		4p1e5 12394	. . . . . . . 8 ⊢ (4 + 1) = 5
141		5nn0 12528	. . . . . . . . 9 ⊢ 5 ∈ ℕ0
142	141	nn0zi 12623	. . . . . . . 8 ⊢ 5 ∈ ℤ
143	37, 135, 140, 123, 142	dpexpp1 32649	. . . . . . 7 ⊢ ((0.1) · (;10↑4)) = ((0._01) · (;10↑5))
144	37, 135	rpdp2cl 32623	. . . . . . . 8 ⊢ _01 ∈ ℝ+
145		5p1e6 12395	. . . . . . . 8 ⊢ (5 + 1) = 6
146		6nn0 12529	. . . . . . . . 9 ⊢ 6 ∈ ℕ0
147	146	nn0zi 12623	. . . . . . . 8 ⊢ 6 ∈ ℤ
148	37, 144, 145, 142, 147	dpexpp1 32649	. . . . . . 7 ⊢ ((0._01) · (;10↑5)) = ((0._0_01) · (;10↑6))
149	37, 144	rpdp2cl 32623	. . . . . . . 8 ⊢ _0_01 ∈ ℝ+
150		6p1e7 12396	. . . . . . . 8 ⊢ (6 + 1) = 7
151	104	nn0zi 12623	. . . . . . . 8 ⊢ 7 ∈ ℤ
152	37, 149, 150, 147, 151	dpexpp1 32649	. . . . . . 7 ⊢ ((0._0_01) · (;10↑6)) = ((0._0_0_01) · (;10↑7))
153	143, 148, 152	3eqtrri 2760	. . . . . 6 ⊢ ((0._0_0_01) · (;10↑7)) = ((0.1) · (;10↑4))
154	139, 153	breqtrrdi 5192	. . . . 5 ⊢ (𝜑 → 1 < ((0._0_0_01) · (;10↑7)))
155	37, 149	rpdp2cl 32623	. . . . . . . 8 ⊢ _0_0_01 ∈ ℝ+
156	37, 155	rpdpcl 32644	. . . . . . 7 ⊢ (0._0_0_01) ∈ ℝ+
157	156	a1i 11	. . . . . 6 ⊢ (𝜑 → (0._0_0_01) ∈ ℝ+)
158		2nn0 12525	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
159	158, 104	deccl 12728	. . . . . . . . . . 11 ⊢ ;27 ∈ ℕ0
160	103, 159	nn0expcli 14091	. . . . . . . . . 10 ⊢ (;10↑;27) ∈ ℕ0
161	160	nn0rei 12519	. . . . . . . . 9 ⊢ (;10↑;27) ∈ ℝ
162	161	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (;10↑;27) ∈ ℝ)
163	160	nn0ge0i 12535	. . . . . . . . 9 ⊢ 0 ≤ (;10↑;27)
164	163	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (;10↑;27))
165	162, 164	resqrtcld 15402	. . . . . . 7 ⊢ (𝜑 → (√‘(;10↑;27)) ∈ ℝ)
166		expmul 14110	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (;10↑(7 · 2)) = ((;10↑7)↑2))
167	120, 104, 158, 166	mp3an 1457	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = ((;10↑7)↑2)
168		7t2e14 12822	. . . . . . . . . . . . 13 ⊢ (7 · 2) = ;14
169	168	oveq2i 7435	. . . . . . . . . . . 12 ⊢ (;10↑(7 · 2)) = (;10↑;14)
170	167, 169	eqtr3i 2757	. . . . . . . . . . 11 ⊢ ((;10↑7)↑2) = (;10↑;14)
171	170	fveq2i 6903	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (√‘(;10↑;14))
172		expgt0 14098	. . . . . . . . . . . . 13 ⊢ ((;10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑7))
173	109, 151, 121, 172	mp3an 1457	. . . . . . . . . . . 12 ⊢ 0 < (;10↑7)
174	38, 106, 173	ltleii 11373	. . . . . . . . . . 11 ⊢ 0 ≤ (;10↑7)
175		sqrtsq 15254	. . . . . . . . . . 11 ⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤ (;10↑7)) → (√‘((;10↑7)↑2)) = (;10↑7))
176	106, 174, 175	mp2an 690	. . . . . . . . . 10 ⊢ (√‘((;10↑7)↑2)) = (;10↑7)
177	171, 176	eqtr3i 2757	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) = (;10↑7)
178	15, 128	deccl 12728	. . . . . . . . . . . . 13 ⊢ ;14 ∈ ℕ0
179	178	nn0zi 12623	. . . . . . . . . . . 12 ⊢ ;14 ∈ ℤ
180	159	nn0zi 12623	. . . . . . . . . . . 12 ⊢ ;27 ∈ ℤ
181	109, 179, 180	3pm3.2i 1336	. . . . . . . . . . 11 ⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ)
182		4lt10 12849	. . . . . . . . . . . . 13 ⊢ 4 < ;10
183		1lt2 12419	. . . . . . . . . . . . 13 ⊢ 1 < 2
184	15, 158, 128, 104, 182, 183	decltc 12742	. . . . . . . . . . . 12 ⊢ ;14 < ;27
185	113, 184	pm3.2i 469	. . . . . . . . . . 11 ⊢ (1 < ;10 ∧ ;14 < ;27)
186		ltexp2a 14168	. . . . . . . . . . 11 ⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27))
187	181, 185, 186	mp2an 690	. . . . . . . . . 10 ⊢ (;10↑;14) < (;10↑;27)
188	103, 178	nn0expcli 14091	. . . . . . . . . . . . 13 ⊢ (;10↑;14) ∈ ℕ0
189	188	nn0rei 12519	. . . . . . . . . . . 12 ⊢ (;10↑;14) ∈ ℝ
190		expgt0 14098	. . . . . . . . . . . . . 14 ⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14))
191	109, 179, 121, 190	mp3an 1457	. . . . . . . . . . . . 13 ⊢ 0 < (;10↑;14)
192	38, 189, 191	ltleii 11373	. . . . . . . . . . . 12 ⊢ 0 ≤ (;10↑;14)
193	189, 192	pm3.2i 469	. . . . . . . . . . 11 ⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14))
194	161, 163	pm3.2i 469	. . . . . . . . . . 11 ⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))
195		sqrtlt 15246	. . . . . . . . . . 11 ⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))))
196	193, 194, 195	mp2an 690	. . . . . . . . . 10 ⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))
197	187, 196	mpbi 229	. . . . . . . . 9 ⊢ (√‘(;10↑;14)) < (√‘(;10↑;27))
198	177, 197	eqbrtrri 5173	. . . . . . . 8 ⊢ (;10↑7) < (√‘(;10↑;27))
199	198	a1i 11	. . . . . . 7 ⊢ (𝜑 → (;10↑7) < (√‘(;10↑;27)))
200		hgt750lemd.0	. . . . . . . 8 ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)
201	162, 164, 32, 34	sqrtled 15411	. . . . . . . 8 ⊢ (𝜑 → ((;10↑;27) ≤ 𝑁 ↔ (√‘(;10↑;27)) ≤ (√‘𝑁)))
202	200, 201	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (√‘(;10↑;27)) ≤ (√‘𝑁))
203	107, 165, 35, 199, 202	ltletrd 11410	. . . . . 6 ⊢ (𝜑 → (;10↑7) < (√‘𝑁))
204	107, 35, 157, 203	ltmul2dd 13110	. . . . 5 ⊢ (𝜑 → ((0._0_0_01) · (;10↑7)) < ((0._0_0_01) · (√‘𝑁)))
205	100, 108, 52, 154, 204	lttrd 11411	. . . 4 ⊢ (𝜑 → 1 < ((0._0_0_01) · (√‘𝑁)))
206	14, 100, 52, 102, 205	lttrd 11411	. . 3 ⊢ (𝜑 → (log‘2) < ((0._0_0_01) · (√‘𝑁)))
207	11, 14, 36, 52, 99, 206	lt2addd 11873	. 2 ⊢ (𝜑 → (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)) < (((1._4_2_62) · (√‘𝑁)) + ((0._0_0_01) · (√‘𝑁))))
208		nfv 1909	. . 3 ⊢ Ⅎ𝑖𝜑
209		nfcv 2898	. . 3 ⊢ Ⅎ𝑖(log‘2)
210		2prm 16668	. . . 4 ⊢ 2 ∈ ℙ
211	210	a1i 11	. . 3 ⊢ (𝜑 → 2 ∈ ℙ)
212		elndif 4127	. . . 4 ⊢ (2 ∈ ℙ → ¬ 2 ∈ ((1...𝑁) ∖ ℙ))
213	211, 212	syl 17	. . 3 ⊢ (𝜑 → ¬ 2 ∈ ((1...𝑁) ∖ ℙ))
214		fveq2 6900	. . . 4 ⊢ (𝑖 = 2 → (Λ‘𝑖) = (Λ‘2))
215		vmaprm 27067	. . . . 5 ⊢ (2 ∈ ℙ → (Λ‘2) = (log‘2))
216	210, 215	ax-mp 5	. . . 4 ⊢ (Λ‘2) = (log‘2)
217	214, 216	eqtrdi 2783	. . 3 ⊢ (𝑖 = 2 → (Λ‘𝑖) = (log‘2))
218		2cnd 12326	. . . 4 ⊢ (𝜑 → 2 ∈ ℂ)
219		2ne0 12352	. . . . 5 ⊢ 2 ≠ 0
220	219	a1i 11	. . . 4 ⊢ (𝜑 → 2 ≠ 0)
221	218, 220	logcld 26522	. . 3 ⊢ (𝜑 → (log‘2) ∈ ℂ)
222	208, 209, 3, 211, 213, 76, 217, 221	fsumsplitsn 15728	. 2 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)))
223	146, 12	rpdp2cl 32623	. . . . . 6 ⊢ _62 ∈ ℝ+
224	158, 223	rpdp2cl 32623	. . . . 5 ⊢ _2_62 ∈ ℝ+
225		3rp 13018	. . . . . . 7 ⊢ 3 ∈ ℝ+
226	146, 225	rpdp2cl 32623	. . . . . 6 ⊢ _63 ∈ ℝ+
227	158, 226	rpdp2cl 32623	. . . . 5 ⊢ _2_63 ∈ ℝ+
228		1p0e1 12372	. . . . 5 ⊢ (1 + 0) = 1
229		4cn 12333	. . . . . . 7 ⊢ 4 ∈ ℂ
230	229	addridi 11437	. . . . . 6 ⊢ (4 + 0) = 4
231		2cn 12323	. . . . . . . 8 ⊢ 2 ∈ ℂ
232	231	addridi 11437	. . . . . . 7 ⊢ (2 + 0) = 2
233		3nn0 12526	. . . . . . . 8 ⊢ 3 ∈ ℕ0
234		eqid 2727	. . . . . . . . 9 ⊢ ;62 = ;62
235		eqid 2727	. . . . . . . . 9 ⊢ ;01 = ;01
236		6cn 12339	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
237	236	addridi 11437	. . . . . . . . 9 ⊢ (6 + 0) = 6
238		2p1e3 12390	. . . . . . . . 9 ⊢ (2 + 1) = 3
239	146, 158, 37, 15, 234, 235, 237, 238	decadd 12767	. . . . . . . 8 ⊢ (;62 + ;01) = ;63
240	146, 158, 37, 15, 146, 233, 239	dpadd 32652	. . . . . . 7 ⊢ ((6.2) + (0.1)) = (6.3)
241	146, 12, 37, 135, 146, 225, 158, 37, 232, 240	dpadd2 32651	. . . . . 6 ⊢ ((2._62) + (0._01)) = (2._63)
242	158, 223, 37, 144, 158, 226, 128, 37, 230, 241	dpadd2 32651	. . . . 5 ⊢ ((4._2_62) + (0._0_01)) = (4._2_63)
243	128, 224, 37, 149, 128, 227, 15, 37, 228, 242	dpadd2 32651	. . . 4 ⊢ ((1._4_2_62) + (0._0_0_01)) = (1._4_2_63)
244	243	oveq1i 7434	. . 3 ⊢ (((1._4_2_62) + (0._0_0_01)) · (√‘𝑁)) = ((1._4_2_63) · (√‘𝑁))
245	30	recnd 11278	. . . 4 ⊢ (𝜑 → (1._4_2_62) ∈ ℂ)
246	51	recnd 11278	. . . 4 ⊢ (𝜑 → (0._0_0_01) ∈ ℂ)
247	35	recnd 11278	. . . 4 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
248	245, 246, 247	adddird 11275	. . 3 ⊢ (𝜑 → (((1._4_2_62) + (0._0_0_01)) · (√‘𝑁)) = (((1._4_2_62) · (√‘𝑁)) + ((0._0_0_01) · (√‘𝑁))))
249	244, 248	eqtr3id 2781	. 2 ⊢ (𝜑 → ((1._4_2_63) · (√‘𝑁)) = (((1._4_2_62) · (√‘𝑁)) + ((0._0_0_01) · (√‘𝑁))))
250	207, 222, 249	3brtr4d 5182	1 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2936  ∀wral 3057   ∖ cdif 3944   ∪ cun 3945   ∩ cin 3946   ⊆ wss 3947  ∅c0 4324  {csn 4630   class class class wbr 5150  ⟶wf 6547  ‘cfv 6551  (class class class)co 7424  Fincfn 8968  ℂcc 11142  ℝcr 11143  0cc0 11144  1c1 11145   + caddc 11147   · cmul 11149   < clt 11284   ≤ cle 11285   − cmin 11480   / cdiv 11907  ℕcn 12248  2c2 12303  3c3 12304  4c4 12305  5c5 12306  6c6 12307  7c7 12308  ℕ₀cn0 12508  ℤcz 12594  ;cdc 12713  ℝ⁺crp 13012  ...cfz 13522  ↑cexp 14064  √csqrt 15218  Σcsu 15670  ℙcprime 16647  logclog 26506  θccht 27041  Λcvma 27042  ψcchp 27043  _cdp2 32612  .cdp 32629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-inf2 9670  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222  ax-addf 11223  ax-ros336 34283

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-iin 5001  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7689  df-om 7875  df-1st 7997  df-2nd 7998  df-supp 8170  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-oadd 8495  df-er 8729  df-map 8851  df-pm 8852  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9539  df-dju 9930  df-card 9968  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-xnn0 12581  df-z 12595  df-dec 12714  df-uz 12859  df-q 12969  df-rp 13013  df-xneg 13130  df-xadd 13131  df-xmul 13132  df-ioo 13366  df-ioc 13367  df-ico 13368  df-icc 13369  df-fz 13523  df-fzo 13666  df-fl 13795  df-mod 13873  df-seq 14005  df-exp 14065  df-fac 14271  df-bc 14300  df-hash 14328  df-shft 15052  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-limsup 15453  df-clim 15470  df-rlim 15471  df-sum 15671  df-ef 16049  df-sin 16051  df-cos 16052  df-tan 16053  df-pi 16054  df-dvds 16237  df-gcd 16475  df-prm 16648  df-pc 16811  df-struct 17121  df-sets 17138  df-slot 17156  df-ndx 17168  df-base 17186  df-ress 17215  df-plusg 17251  df-mulr 17252  df-starv 17253  df-sca 17254  df-vsca 17255  df-ip 17256  df-tset 17257  df-ple 17258  df-ds 17260  df-unif 17261  df-hom 17262  df-cco 17263  df-rest 17409  df-topn 17410  df-0g 17428  df-gsum 17429  df-topgen 17430  df-pt 17431  df-prds 17434  df-xrs 17489  df-qtop 17494  df-imas 17495  df-xps 17497  df-mre 17571  df-mrc 17572  df-acs 17574  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18746  df-mulg 19029  df-cntz 19273  df-cmn 19742  df-psmet 21276  df-xmet 21277  df-met 21278  df-bl 21279  df-mopn 21280  df-fbas 21281  df-fg 21282  df-cnfld 21285  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22867  df-cld 22941  df-ntr 22942  df-cls 22943  df-nei 23020  df-lp 23058  df-perf 23059  df-cn 23149  df-cnp 23150  df-haus 23237  df-cmp 23309  df-tx 23484  df-hmeo 23677  df-fil 23768  df-fm 23860  df-flim 23861  df-flf 23862  df-xms 24244  df-ms 24245  df-tms 24246  df-cncf 24816  df-limc 25813  df-dv 25814  df-ulm 26331  df-log 26508  df-atan 26817  df-cht 27047  df-vma 27048  df-chp 27049  df-dp2 32613  df-dp 32630

This theorem is referenced by:  hgt750leme  34295