Theorem hgt750lemd

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

	Ref	Expression
Hypotheses	hgt750lemc.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	hgt750lemd.0	⊢ ( 𝜑 → ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 )
Assertion	hgt750lemd	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hgt750lemc.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		hgt750lemd.0	⊢ ( 𝜑 → ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 )
3		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
4		diffi	⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
5	3 4	syl	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
6		vmaf	⊢ Λ : ℕ ⟶ ℝ
7	6	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → Λ : ℕ ⟶ ℝ )
8		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
9	8	a1i	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
10	9	ssdifssd	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ℕ )
11	10	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → 𝑖 ∈ ℕ )
12	7 11	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
13	5 12	fsumrecl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℝ )
14		2rp	⊢ 2 ∈ ℝ+
15	14	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
16	15	relogcld	⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
17		1nn0	⊢ 1 ∈ ℕ0
18		4re	⊢ 4 ∈ ℝ
19		2re	⊢ 2 ∈ ℝ
20		6re	⊢ 6 ∈ ℝ
21	20 19	pm3.2i	⊢ ( 6 ∈ ℝ ∧ 2 ∈ ℝ )
22		dp2cl	⊢ ( ( 6 ∈ ℝ ∧ 2 ∈ ℝ ) → _ 6 2 ∈ ℝ )
23	21 22	ax-mp	⊢ _ 6 2 ∈ ℝ
24	19 23	pm3.2i	⊢ ( 2 ∈ ℝ ∧ _ 6 2 ∈ ℝ )
25		dp2cl	⊢ ( ( 2 ∈ ℝ ∧ _ 6 2 ∈ ℝ ) → _ 2 _ 6 2 ∈ ℝ )
26	24 25	ax-mp	⊢ _ 2 _ 6 2 ∈ ℝ
27	18 26	pm3.2i	⊢ ( 4 ∈ ℝ ∧ _ 2 _ 6 2 ∈ ℝ )
28		dp2cl	⊢ ( ( 4 ∈ ℝ ∧ _ 2 _ 6 2 ∈ ℝ ) → _ 4 _ 2 _ 6 2 ∈ ℝ )
29	27 28	ax-mp	⊢ _ 4 _ 2 _ 6 2 ∈ ℝ
30		dpcl	⊢ ( ( 1 ∈ ℕ0 ∧ _ 4 _ 2 _ 6 2 ∈ ℝ ) → ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℝ )
31	17 29 30	mp2an	⊢ ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℝ
32	31	a1i	⊢ ( 𝜑 → ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℝ )
33	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
34	1	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
35	34	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝑁 )
36	33 35	resqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
37	32 36	remulcld	⊢ ( 𝜑 → ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
38		0nn0	⊢ 0 ∈ ℕ0
39		0re	⊢ 0 ∈ ℝ
40		1re	⊢ 1 ∈ ℝ
41	39 40	pm3.2i	⊢ ( 0 ∈ ℝ ∧ 1 ∈ ℝ )
42		dp2cl	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → _ 0 1 ∈ ℝ )
43	41 42	ax-mp	⊢ _ 0 1 ∈ ℝ
44	39 43	pm3.2i	⊢ ( 0 ∈ ℝ ∧ _ 0 1 ∈ ℝ )
45		dp2cl	⊢ ( ( 0 ∈ ℝ ∧ _ 0 1 ∈ ℝ ) → _ 0 _ 0 1 ∈ ℝ )
46	44 45	ax-mp	⊢ _ 0 _ 0 1 ∈ ℝ
47	39 46	pm3.2i	⊢ ( 0 ∈ ℝ ∧ _ 0 _ 0 1 ∈ ℝ )
48		dp2cl	⊢ ( ( 0 ∈ ℝ ∧ _ 0 _ 0 1 ∈ ℝ ) → _ 0 _ 0 _ 0 1 ∈ ℝ )
49	47 48	ax-mp	⊢ _ 0 _ 0 _ 0 1 ∈ ℝ
50		dpcl	⊢ ( ( 0 ∈ ℕ0 ∧ _ 0 _ 0 _ 0 1 ∈ ℝ ) → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ )
51	38 49 50	mp2an	⊢ ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ
52	51	a1i	⊢ ( 𝜑 → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ )
53	52 36	remulcld	⊢ ( 𝜑 → ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
54	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
55		chpvalz	⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) )
56	54 55	syl	⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) )
57		chtvalz	⊢ ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
58	54 57	syl	⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
59		inss2	⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ
60	59	a1i	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ )
61	60	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℙ )
62		vmaprm	⊢ ( 𝑖 ∈ ℙ → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) )
63	61 62	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) )
64	63	sumeq2dv	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
65	58 64	eqtr4d	⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) )
66	56 65	oveq12d	⊢ ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) )
67		infi	⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin )
68	3 67	syl	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin )
69	6	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → Λ : ℕ ⟶ ℝ )
70		inss1	⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ( 1 ... 𝑁 )
71	70 8	sstri	⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ
72	71	a1i	⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ )
73	72	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℕ )
74	69 73	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
75	74	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
76	68 75	fsumcl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ )
77	12	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
78	5 77	fsumcl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ )
79		inindif	⊢ ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅
80	79	a1i	⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅ )
81		inundif	⊢ ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ( 1 ... 𝑁 )
82	81	eqcomi	⊢ ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
83	82	a1i	⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) )
84	6	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → Λ : ℕ ⟶ ℝ )
85	9	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ℕ )
86	84 85	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
87	86	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
88	80 83 3 87	fsumsplit	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ) )
89	76 78 88	mvrladdd	⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) )
90	66 89	eqtr2d	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) )
91		fveq2	⊢ ( 𝑥 = 𝑁 → ( ψ ‘ 𝑥 ) = ( ψ ‘ 𝑁 ) )
92		fveq2	⊢ ( 𝑥 = 𝑁 → ( θ ‘ 𝑥 ) = ( θ ‘ 𝑁 ) )
93	91 92	oveq12d	⊢ ( 𝑥 = 𝑁 → ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) )
94		fveq2	⊢ ( 𝑥 = 𝑁 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝑁 ) )
95	94	oveq2d	⊢ ( 𝑥 = 𝑁 → ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) = ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) )
96	93 95	breq12d	⊢ ( 𝑥 = 𝑁 → ( ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) ↔ ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ) )
97		ax-ros336	⊢ ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) )
98	97	a1i	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) )
99	96 98 34	rspcdva	⊢ ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) )
100	90 99	eqbrtrd	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) )
101	40	a1i	⊢ ( 𝜑 → 1 ∈ ℝ )
102		log2le1	⊢ ( log ‘ 2 ) < 1
103	102	a1i	⊢ ( 𝜑 → ( log ‘ 2 ) < 1 )
104		10nn0	⊢ ; 1 0 ∈ ℕ0
105		7nn0	⊢ 7 ∈ ℕ0
106	104 105	nn0expcli	⊢ ( ; 1 0 ↑ 7 ) ∈ ℕ0
107	106	nn0rei	⊢ ( ; 1 0 ↑ 7 ) ∈ ℝ
108	107	a1i	⊢ ( 𝜑 → ( ; 1 0 ↑ 7 ) ∈ ℝ )
109	52 108	remulcld	⊢ ( 𝜑 → ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) ∈ ℝ )
110	104	nn0rei	⊢ ; 1 0 ∈ ℝ
111		0z	⊢ 0 ∈ ℤ
112		3z	⊢ 3 ∈ ℤ
113	110 111 112	3pm3.2i	⊢ ( ; 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ )
114		1lt10	⊢ 1 < ; 1 0
115		3pos	⊢ 0 < 3
116	114 115	pm3.2i	⊢ ( 1 < ; 1 0 ∧ 0 < 3 )
117		ltexp2a	⊢ ( ( ( ; 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ ) ∧ ( 1 < ; 1 0 ∧ 0 < 3 ) ) → ( ; 1 0 ↑ 0 ) < ( ; 1 0 ↑ 3 ) )
118	113 116 117	mp2an	⊢ ( ; 1 0 ↑ 0 ) < ( ; 1 0 ↑ 3 )
119	104	numexp0	⊢ ( ; 1 0 ↑ 0 ) = 1
120	119	eqcomi	⊢ 1 = ( ; 1 0 ↑ 0 )
121	110	recni	⊢ ; 1 0 ∈ ℂ
122		10pos	⊢ 0 < ; 1 0
123	39 122	gtneii	⊢ ; 1 0 ≠ 0
124		4z	⊢ 4 ∈ ℤ
125		expm1	⊢ ( ( ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ∧ 4 ∈ ℤ ) → ( ; 1 0 ↑ ( 4 − 1 ) ) = ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) )
126	121 123 124 125	mp3an	⊢ ( ; 1 0 ↑ ( 4 − 1 ) ) = ( ( ; 1 0 ↑ 4 ) / ; 1 0 )
127		4m1e3	⊢ ( 4 − 1 ) = 3
128	127	oveq2i	⊢ ( ; 1 0 ↑ ( 4 − 1 ) ) = ( ; 1 0 ↑ 3 )
129		4nn0	⊢ 4 ∈ ℕ0
130	104 129	nn0expcli	⊢ ( ; 1 0 ↑ 4 ) ∈ ℕ0
131	130	nn0cni	⊢ ( ; 1 0 ↑ 4 ) ∈ ℂ
132		divrec2	⊢ ( ( ( ; 1 0 ↑ 4 ) ∈ ℂ ∧ ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ) → ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) )
133	131 121 123 132	mp3an	⊢ ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) )
134	126 128 133	3eqtr3ri	⊢ ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) = ( ; 1 0 ↑ 3 )
135	118 120 134	3brtr4i	⊢ 1 < ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) )
136		1rp	⊢ 1 ∈ ℝ+
137	136	dp0h	⊢ ( 0 . 1 ) = ( 1 / ; 1 0 )
138	137	oveq1i	⊢ ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) = ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) )
139	135 138	breqtrri	⊢ 1 < ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) )
140	139	a1i	⊢ ( 𝜑 → 1 < ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) )
141		4p1e5	⊢ ( 4 + 1 ) = 5
142		5nn0	⊢ 5 ∈ ℕ0
143	142	nn0zi	⊢ 5 ∈ ℤ
144	38 136 141 124 143	dpexpp1	⊢ ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) = ( ( 0 . _ 0 1 ) · ( ; 1 0 ↑ 5 ) )
145	38 136	rpdp2cl	⊢ _ 0 1 ∈ ℝ+
146		5p1e6	⊢ ( 5 + 1 ) = 6
147		6nn0	⊢ 6 ∈ ℕ0
148	147	nn0zi	⊢ 6 ∈ ℤ
149	38 145 146 143 148	dpexpp1	⊢ ( ( 0 . _ 0 1 ) · ( ; 1 0 ↑ 5 ) ) = ( ( 0 . _ 0 _ 0 1 ) · ( ; 1 0 ↑ 6 ) )
150	38 145	rpdp2cl	⊢ _ 0 _ 0 1 ∈ ℝ+
151		6p1e7	⊢ ( 6 + 1 ) = 7
152	105	nn0zi	⊢ 7 ∈ ℤ
153	38 150 151 148 152	dpexpp1	⊢ ( ( 0 . _ 0 _ 0 1 ) · ( ; 1 0 ↑ 6 ) ) = ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) )
154	144 149 153	3eqtrri	⊢ ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) = ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) )
155	140 154	breqtrrdi	⊢ ( 𝜑 → 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) )
156	38 150	rpdp2cl	⊢ _ 0 _ 0 _ 0 1 ∈ ℝ+
157	38 156	rpdpcl	⊢ ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ+
158	157	a1i	⊢ ( 𝜑 → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ+ )
159		2nn0	⊢ 2 ∈ ℕ0
160	159 105	deccl	⊢ ; 2 7 ∈ ℕ0
161	104 160	nn0expcli	⊢ ( ; 1 0 ↑ ; 2 7 ) ∈ ℕ0
162	161	nn0rei	⊢ ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ
163	162	a1i	⊢ ( 𝜑 → ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ )
164	161	nn0ge0i	⊢ 0 ≤ ( ; 1 0 ↑ ; 2 7 )
165	164	a1i	⊢ ( 𝜑 → 0 ≤ ( ; 1 0 ↑ ; 2 7 ) )
166	163 165	resqrtcld	⊢ ( 𝜑 → ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ )
167		expmul	⊢ ( ( ; 1 0 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ( ; 1 0 ↑ 7 ) ↑ 2 ) )
168	121 105 159 167	mp3an	⊢ ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ( ; 1 0 ↑ 7 ) ↑ 2 )
169		7t2e14	⊢ ( 7 · 2 ) = ; 1 4
170	169	oveq2i	⊢ ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ; 1 0 ↑ ; 1 4 )
171	168 170	eqtr3i	⊢ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) = ( ; 1 0 ↑ ; 1 4 )
172	171	fveq2i	⊢ ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) )
173		expgt0	⊢ ( ( ; 1 0 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ; 1 0 ) → 0 < ( ; 1 0 ↑ 7 ) )
174	110 152 122 173	mp3an	⊢ 0 < ( ; 1 0 ↑ 7 )
175	39 107 174	ltleii	⊢ 0 ≤ ( ; 1 0 ↑ 7 )
176		sqrtsq	⊢ ( ( ( ; 1 0 ↑ 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ 7 ) ) → ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( ; 1 0 ↑ 7 ) )
177	107 175 176	mp2an	⊢ ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( ; 1 0 ↑ 7 )
178	172 177	eqtr3i	⊢ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) = ( ; 1 0 ↑ 7 )
179	17 129	deccl	⊢ ; 1 4 ∈ ℕ0
180	179	nn0zi	⊢ ; 1 4 ∈ ℤ
181	160	nn0zi	⊢ ; 2 7 ∈ ℤ
182	110 180 181	3pm3.2i	⊢ ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ ; 2 7 ∈ ℤ )
183		4lt10	⊢ 4 < ; 1 0
184		1lt2	⊢ 1 < 2
185	17 159 129 105 183 184	decltc	⊢ ; 1 4 < ; 2 7
186	114 185	pm3.2i	⊢ ( 1 < ; 1 0 ∧ ; 1 4 < ; 2 7 )
187		ltexp2a	⊢ ( ( ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ ; 2 7 ∈ ℤ ) ∧ ( 1 < ; 1 0 ∧ ; 1 4 < ; 2 7 ) ) → ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) )
188	182 186 187	mp2an	⊢ ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 )
189	104 179	nn0expcli	⊢ ( ; 1 0 ↑ ; 1 4 ) ∈ ℕ0
190	189	nn0rei	⊢ ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ
191		expgt0	⊢ ( ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ 0 < ; 1 0 ) → 0 < ( ; 1 0 ↑ ; 1 4 ) )
192	110 180 122 191	mp3an	⊢ 0 < ( ; 1 0 ↑ ; 1 4 )
193	39 190 192	ltleii	⊢ 0 ≤ ( ; 1 0 ↑ ; 1 4 )
194	190 193	pm3.2i	⊢ ( ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) )
195	162 164	pm3.2i	⊢ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) )
196		sqrtlt	⊢ ( ( ( ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) ) ∧ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) ) ) → ( ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ↔ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) )
197	194 195 196	mp2an	⊢ ( ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ↔ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) )
198	188 197	mpbi	⊢ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) )
199	178 198	eqbrtrri	⊢ ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) )
200	199	a1i	⊢ ( 𝜑 → ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) )
201	163 165 33 35	sqrtled	⊢ ( 𝜑 → ( ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ↔ ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ≤ ( √ ‘ 𝑁 ) ) )
202	2 201	mpbid	⊢ ( 𝜑 → ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ≤ ( √ ‘ 𝑁 ) )
203	108 166 36 200 202	ltletrd	⊢ ( 𝜑 → ( ; 1 0 ↑ 7 ) < ( √ ‘ 𝑁 ) )
204	108 36 158 203	ltmul2dd	⊢ ( 𝜑 → ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) )
205	101 109 53 155 204	lttrd	⊢ ( 𝜑 → 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) )
206	16 101 53 103 205	lttrd	⊢ ( 𝜑 → ( log ‘ 2 ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) )
207	13 16 37 53 100 206	lt2addd	⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) < ( ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
208		nfv	⊢ Ⅎ 𝑖 𝜑
209		nfcv	⊢ Ⅎ 𝑖 ( log ‘ 2 )
210		2prm	⊢ 2 ∈ ℙ
211	210	a1i	⊢ ( 𝜑 → 2 ∈ ℙ )
212		elndif	⊢ ( 2 ∈ ℙ → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
213	211 212	syl	⊢ ( 𝜑 → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
214		fveq2	⊢ ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( Λ ‘ 2 ) )
215		vmaprm	⊢ ( 2 ∈ ℙ → ( Λ ‘ 2 ) = ( log ‘ 2 ) )
216	210 215	ax-mp	⊢ ( Λ ‘ 2 ) = ( log ‘ 2 )
217	214 216	eqtrdi	⊢ ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( log ‘ 2 ) )
218		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
219		2ne0	⊢ 2 ≠ 0
220	219	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
221	218 220	logcld	⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
222	208 209 5 211 213 77 217 221	fsumsplitsn	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) )
223	147 14	rpdp2cl	⊢ _ 6 2 ∈ ℝ+
224	159 223	rpdp2cl	⊢ _ 2 _ 6 2 ∈ ℝ+
225		3rp	⊢ 3 ∈ ℝ+
226	147 225	rpdp2cl	⊢ _ 6 3 ∈ ℝ+
227	159 226	rpdp2cl	⊢ _ 2 _ 6 3 ∈ ℝ+
228		1p0e1	⊢ ( 1 + 0 ) = 1
229		4cn	⊢ 4 ∈ ℂ
230	229	addridi	⊢ ( 4 + 0 ) = 4
231		2cn	⊢ 2 ∈ ℂ
232	231	addridi	⊢ ( 2 + 0 ) = 2
233		3nn0	⊢ 3 ∈ ℕ0
234		eqid	⊢ ; 6 2 = ; 6 2
235		eqid	⊢ ; 0 1 = ; 0 1
236		6cn	⊢ 6 ∈ ℂ
237	236	addridi	⊢ ( 6 + 0 ) = 6
238		2p1e3	⊢ ( 2 + 1 ) = 3
239	147 159 38 17 234 235 237 238	decadd	⊢ ( ; 6 2 + ; 0 1 ) = ; 6 3
240	147 159 38 17 147 233 239	dpadd	⊢ ( ( 6 . 2 ) + ( 0 . 1 ) ) = ( 6 . 3 )
241	147 14 38 136 147 225 159 38 232 240	dpadd2	⊢ ( ( 2 . _ 6 2 ) + ( 0 . _ 0 1 ) ) = ( 2 . _ 6 3 )
242	159 223 38 145 159 226 129 38 230 241	dpadd2	⊢ ( ( 4 . _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 1 ) ) = ( 4 . _ 2 _ 6 3 )
243	129 224 38 150 129 227 17 38 228 242	dpadd2	⊢ ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) = ( 1 . _ 4 _ 2 _ 6 3 )
244	243	oveq1i	⊢ ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) )
245	32	recnd	⊢ ( 𝜑 → ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℂ )
246	52	recnd	⊢ ( 𝜑 → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℂ )
247	36	recnd	⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℂ )
248	245 246 247	adddird	⊢ ( 𝜑 → ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
249	244 248	eqtr3id	⊢ ( 𝜑 → ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
250	207 222 249	3brtr4d	⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) ) )