Theorem aks4d1p1p5 42573

Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 19-Aug-2024.)

Hypotheses

Ref	Expression
aks4d1p1p5.1	⊢ (𝜑 → 𝑁 ∈ ℕ)
aks4d1p1p5.2	⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1))
aks4d1p1p5.3	⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))
aks4d1p1p5.4	⊢ (𝜑 → 4 ≤ 𝑁)
aks4d1p1p5.5	⊢ 𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1))
aks4d1p1p5.6	⊢ 𝐷 = ((2 logb 𝑁)↑2)
aks4d1p1p5.7	⊢ 𝐸 = ((2 logb 𝑁)↑4)

Assertion

Ref	Expression
aks4d1p1p5	⊢ (𝜑 → 𝐴 < (2↑𝐵))

Distinct variable groups:   𝑘,𝑁   𝜑,𝑘

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)   𝐶(𝑘)   𝐷(𝑘)   𝐸(𝑘)

Proof of Theorem aks4d1p1p5

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks4d1p1p5.1	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		aks4d1p1p5.2	. 2 ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1))
3		aks4d1p1p5.3	. 2 ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))
4		3re 12256	. . . 4 ⊢ 3 ∈ ℝ
5	4	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
6		4re 12260	. . . 4 ⊢ 4 ∈ ℝ
7	6	a1i 11	. . 3 ⊢ (𝜑 → 4 ∈ ℝ)
8	1	nnred 12184	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
9	5	lep1d 12082	. . . 4 ⊢ (𝜑 → 3 ≤ (3 + 1))
10		3p1e4 12316	. . . 4 ⊢ (3 + 1) = 4
11	9, 10	breqtrdi 5115	. . 3 ⊢ (𝜑 → 3 ≤ 4)
12		aks4d1p1p5.4	. . 3 ⊢ (𝜑 → 4 ≤ 𝑁)
13	5, 7, 8, 11, 12	letrd 11299	. 2 ⊢ (𝜑 → 3 ≤ 𝑁)
14		aks4d1p1p5.5	. 2 ⊢ 𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1))
15		aks4d1p1p5.6	. 2 ⊢ 𝐷 = ((2 logb 𝑁)↑2)
16		aks4d1p1p5.7	. 2 ⊢ 𝐸 = ((2 logb 𝑁)↑4)
17		2re 12250	. . . . . . . 8 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℝ)
19		2pos 12279	. . . . . . . . 9 ⊢ 0 < 2
20	19	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 2)
21		elicc2 13359	. . . . . . . . . . . . . . 15 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
22	7, 8, 21	syl2anc 591	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
23	22	biimpd 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
24	23	imp 408	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
25	24	simp1d 1149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ)
26		0red 11143	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
27	26	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
28	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℝ)
29		4pos 12283	. . . . . . . . . . . . 13 ⊢ 0 < 4
30	29	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 4)
31	24	simp2d 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
32	27, 28, 25, 30, 31	ltletrd 11302	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
33		1red 11141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℝ)
34		1lt2 12342	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
35	34	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 2)
36	33, 35	ltned 11278	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≠ 2)
37	36	necomd 2991	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 1)
38	37	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 1)
39	18, 20, 25, 32, 38	relogbcld 42472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈ ℝ)
40		5nn0 12452	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
41	40	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℕ0)
42	39, 41	reexpcld 14120	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑5) ∈ ℝ)
43		1red 11141	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ)
44	42, 43	readdcld 11170	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (((2 logb 𝑥)↑5) + 1) ∈ ℝ)
45	27, 43	readdcld 11170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) ∈ ℝ)
46	27	ltp1d 12081	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (0 + 1))
47	41	nn0zd 12544	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℤ)
48		ax-resscn 11091	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
49	48, 18	sselid 3914	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℂ)
50	27, 20	gtned 11277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 0)
51		logb1 26754	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) = 0)
52	49, 50, 38, 51	syl3anc 1380	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) = 0)
53		1lt4 12347	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
54	53	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 4)
55	43, 28, 25, 54, 31	ltletrd 11302	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 𝑥)
56		2z 12554	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
57	56	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℤ)
58	57	uzidd 12799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ (ℤ≥‘2))
59		1rp 12941	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ+
60	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ+)
61	25, 32	elrpd 12978	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ+)
62		logblt 26769	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 < 𝑥 ↔ (2 logb 1) < (2 logb 𝑥)))
63	58, 60, 61, 62	syl3anc 1380	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (1 < 𝑥 ↔ (2 logb 1) < (2 logb 𝑥)))
64	55, 63	mpbid 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) < (2 logb 𝑥))
65	52, 64	eqbrtrrd 5098	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (2 logb 𝑥))
66		expgt0 14052	. . . . . . . . . . 11 ⊢ (((2 logb 𝑥) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑥)) → 0 < ((2 logb 𝑥)↑5))
67	39, 47, 65, 66	syl3anc 1380	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < ((2 logb 𝑥)↑5))
68	27, 42, 43, 67	ltadd1dd 11757	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) < (((2 logb 𝑥)↑5) + 1))
69	27, 45, 44, 46, 68	lttrd 11303	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (((2 logb 𝑥)↑5) + 1))
70	18, 20, 44, 69, 38	relogbcld 42472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ)
71	18, 70	remulcld 11171	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) ∈ ℝ)
72		0red 11143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
73		simpr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ (4[,]𝑁))
74	7, 8	jca 517	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 ∈ ℝ ∧ 𝑁 ∈ ℝ))
75	74	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (4 ∈ ℝ ∧ 𝑁 ∈ ℝ))
76	75, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
77	73, 76	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
78	77	simp2d 1150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
79	72, 28, 25, 30, 78	ltletrd 11302	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
80	18, 20, 25, 79, 38	relogbcld 42472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈ ℝ)
81	80	resqcld 14082	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑2) ∈ ℝ)
82	71, 81	readdcld 11170	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈ ℝ)
83	82	fmpttd 7059	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ)
84	48	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
85		3lt4 12345	. . . . . . . . . . 11 ⊢ 3 < 4
86	85	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 4)
87	8, 33	readdcld 11170	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
88	8	ltp1d 12081	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
89	7, 8, 87, 12, 88	lelttrd 11300	. . . . . . . . . 10 ⊢ (𝜑 → 4 < (𝑁 + 1))
90	86, 89	jca 517	. . . . . . . . 9 ⊢ (𝜑 → (3 < 4 ∧ 4 < (𝑁 + 1)))
91	5	rexrd 11191	. . . . . . . . . 10 ⊢ (𝜑 → 3 ∈ ℝ*)
92	87	rexrd 11191	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ*)
93	7	rexrd 11191	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℝ*)
94		elioo5 13351	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 4 ∈ ℝ*) → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
95	91, 92, 93, 94	syl3anc 1380	. . . . . . . . 9 ⊢ (𝜑 → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
96	90, 95	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ (3(,)(𝑁 + 1)))
97	5, 7, 8, 86, 12	ltletrd 11302	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 𝑁)
98	97, 88	jca 517	. . . . . . . . 9 ⊢ (𝜑 → (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1)))
99	8	rexrd 11191	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ*)
100		elioo5 13351	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
101	91, 92, 99, 100	syl3anc 1380	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
102	98, 101	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (3(,)(𝑁 + 1)))
103		iccssioo2 13367	. . . . . . . 8 ⊢ ((4 ∈ (3(,)(𝑁 + 1)) ∧ 𝑁 ∈ (3(,)(𝑁 + 1))) → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
104	96, 102, 103	syl2anc 591	. . . . . . 7 ⊢ (𝜑 → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
105	104	resmptd 5998	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))))
106		2cnd 12254	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℂ)
107	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ)
108	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 2)
109		elioore 13323	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 𝑥 ∈ ℝ)
110	109	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ)
111		0red 11143	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 ∈ ℝ)
112	4	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 ∈ ℝ)
113		3pos 12281	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 3
114	113	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 3)
115		eliooord 13353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → (3 < 𝑥 ∧ 𝑥 < (𝑁 + 1)))
116		simpl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 < 𝑥 ∧ 𝑥 < (𝑁 + 1)) → 3 < 𝑥)
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 3 < 𝑥)
118	117	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 < 𝑥)
119	111, 112, 110, 114, 118	lttrd 11303	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 𝑥)
120	37	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
121	107, 108, 110, 119, 120	relogbcld 42472	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈ ℝ)
122	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℕ0)
123	121, 122	reexpcld 14120	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈ ℝ)
124		1red 11141	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℝ)
125	123, 124	readdcld 11170	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈ ℝ)
126	111, 124	readdcld 11170	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) ∈ ℝ)
127	111	ltp1d 12081	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (0 + 1))
128	122	nn0zd 12544	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℤ)
129	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 2)
130		2lt3 12343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 < 3
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 < 3)
132	124, 107, 112, 129, 131	lttrd 11303	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 3)
133	124, 112, 110, 132, 118	lttrd 11303	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 𝑥)
134	110, 119	elrpd 12978	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ+)
135		2rp 12942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ+
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ+)
137	134, 136, 129	jca32 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)))
138		logbgt0b 26778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝑥) ↔ 1 < 𝑥))
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 < (2 logb 𝑥) ↔ 1 < 𝑥))
140	133, 139	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (2 logb 𝑥))
141	121, 128, 140, 66	syl3anc 1380	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < ((2 logb 𝑥)↑5))
142	111, 123, 124, 141	ltadd1dd 11757	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) < (((2 logb 𝑥)↑5) + 1))
143	111, 126, 125, 127, 142	lttrd 11303	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (((2 logb 𝑥)↑5) + 1))
144	124, 129	ltned 11278	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ≠ 2)
145	144	necomd 2991	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
146	107, 108, 125, 143, 145	relogbcld 42472	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ)
147	146	recnd 11169	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℂ)
148	106, 147	mulcld 11161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) ∈ ℂ)
149	48, 121	sselid 3914	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈ ℂ)
150	149	sqcld 14101	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑2) ∈ ℂ)
151	148, 150	addcld 11160	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈ ℂ)
152	151	fmpttd 7059	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ)
153		ioossre 13355	. . . . . . . . . 10 ⊢ (3(,)(𝑁 + 1)) ⊆ ℝ
154	153	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (3(,)(𝑁 + 1)) ⊆ ℝ)
155	84, 152, 154	3jca 1135	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
156	136	relogcld 26608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℝ)
157	125, 156	remulcld 11171	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) · (log‘2)) ∈ ℝ)
158	48, 123	sselid 3914	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈ ℂ)
159		1cnd 11135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℂ)
160	158, 159	addcld 11160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈ ℂ)
161	111, 108	gtned 11277	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 0)
162	106, 161	logcld 26555	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℂ)
163	111, 143	gtned 11277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ≠ 0)
164		loggt0b 26617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
165	135, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 < (log‘2) ↔ 1 < 2)
166	35, 165	sylibr 236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 < (log‘2))
167	26, 166	ltned 11278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≠ (log‘2))
168	167	necomd 2991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘2) ≠ 0)
169	168	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ≠ 0)
170	160, 162, 163, 169	mulne0d 11798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) · (log‘2)) ≠ 0)
171	124, 157, 170	redivcld 11978	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) ∈ ℝ)
172		5re 12263	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℝ)
174		4nn0 12451	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℕ0
175	174	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℕ0)
176	121, 175	reexpcld 14120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈ ℝ)
177	173, 176	remulcld 11171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (5 · ((2 logb 𝑥)↑4)) ∈ ℝ)
178	110, 156	remulcld 11171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ∈ ℝ)
179	48, 110	sselid 3914	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℂ)
180	111, 119	gtned 11277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ≠ 0)
181	179, 162, 180, 169	mulne0d 11798	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ≠ 0)
182	124, 178, 181	redivcld 11978	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / (𝑥 · (log‘2))) ∈ ℝ)
183	177, 182	remulcld 11171	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) ∈ ℝ)
184	183, 111	readdcld 11170	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0) ∈ ℝ)
185	171, 184	remulcld 11171	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈ ℝ)
186	107, 185	remulcld 11171	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) ∈ ℝ)
187	156	resqcld 14082	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ∈ ℝ)
188	56	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℤ)
189	162, 169, 188	expne0d 14109	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ≠ 0)
190	107, 187, 189	redivcld 11978	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 / ((log‘2)↑2)) ∈ ℝ)
191	134	relogcld 26608	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘𝑥) ∈ ℝ)
192		2m1e1 12297	. . . . . . . . . . . . . . . . . 18 ⊢ (2 − 1) = 1
193		1nn0 12448	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
194	192, 193	eqeltri 2837	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) ∈ ℕ0
195	194	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 − 1) ∈ ℕ0)
196	191, 195	reexpcld 14120	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(2 − 1)) ∈ ℝ)
197	196, 110, 180	redivcld 11978	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ)
198	190, 197	remulcld 11171	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ)
199	186, 198	readdcld 11170	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ)
200	199	ralrimiva 3133	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ)
201		nfcv 2903	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(3(,)(𝑁 + 1))
202	201	fnmptf 6624	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ (3(,)(𝑁 + 1))((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1)))
203	200, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1)))
204	5	leidd 11712	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 3)
205	8	lep1d 12082	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
206	5, 8, 87, 13, 205	letrd 11299	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ (𝑁 + 1))
207	5, 87, 204, 206	aks4d1p1p6 42571	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))))
208	207	fneq1d 6581	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)) ↔ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1))))
209	203, 208	mpbird 259	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)))
210	209	fndmd 6593	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (3(,)(𝑁 + 1)))
211		dvcn 25909	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ) ∧ dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (3(,)(𝑁 + 1))) → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
212	155, 210, 211	syl2anc 591	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
213		rescncf 24885	. . . . . . . 8 ⊢ ((4[,]𝑁) ⊆ (3(,)(𝑁 + 1)) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
214	104, 213	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
215	212, 214	mpd 15	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))
216	105, 215	eqeltrrd 2842	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ))
217		cncfcdm 24886	. . . . 5 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ))
218	84, 216, 217	syl2anc 591	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ))
219	83, 218	mpbird 259	. . 3 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ))
220	174	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℕ0)
221	39, 220	reexpcld 14120	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑4) ∈ ℝ)
222	221	fmpttd 7059	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ)
223	104	resmptd 5998	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)))
224	48, 176	sselid 3914	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈ ℂ)
225	224	fmpttd 7059	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ)
226	84, 225, 154	3jca 1135	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
227	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℝ)
228	156, 175	reexpcld 14120	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ∈ ℝ)
229		4z 12556	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℤ
230	229	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℤ)
231	162, 169, 230	expne0d 14109	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ≠ 0)
232	227, 228, 231	redivcld 11978	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 / ((log‘2)↑4)) ∈ ℝ)
233		4m1e3 12300	. . . . . . . . . . . . . . . . 17 ⊢ (4 − 1) = 3
234		3nn0 12450	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℕ0
235	233, 234	eqeltri 2837	. . . . . . . . . . . . . . . 16 ⊢ (4 − 1) ∈ ℕ0
236	235	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 − 1) ∈ ℕ0)
237	191, 236	reexpcld 14120	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(4 − 1)) ∈ ℝ)
238	237, 110, 180	redivcld 11978	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(4 − 1)) / 𝑥) ∈ ℝ)
239	232, 238	remulcld 11171	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
240	239	ralrimiva 3133	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
241	201	fnmptf 6624	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ (3(,)(𝑁 + 1))((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1)))
242	240, 241	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1)))
243	113	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 3)
244		eqid 2741	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))
245		eqid 2741	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)))
246		eqid 2741	. . . . . . . . . . . 12 ⊢ (4 / ((log‘2)↑4)) = (4 / ((log‘2)↑4))
247		4nn 12259	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
248	247	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 4 ∈ ℕ)
249	5, 87, 243, 206, 244, 245, 246, 248	dvrelogpow2b 42566	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
250	249	fneq1d 6581	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) Fn (3(,)(𝑁 + 1)) ↔ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1))))
251	242, 250	mpbird 259	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) Fn (3(,)(𝑁 + 1)))
252	251	fndmd 6593	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (3(,)(𝑁 + 1)))
253		dvcn 25909	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ) ∧ dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (3(,)(𝑁 + 1))) → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
254	226, 252, 253	syl2anc 591	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
255		rescncf 24885	. . . . . . . 8 ⊢ ((4[,]𝑁) ⊆ (3(,)(𝑁 + 1)) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
256	104, 255	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
257	254, 256	mpd 15	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))
258	223, 257	eqeltrrd 2842	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ))
259		cncfcdm 24886	. . . . 5 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
260	84, 258, 259	syl2anc 591	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
261	222, 260	mpbird 259	. . 3 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ))
262	7, 8, 11, 12	aks4d1p1p6 42571	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))))
263	29	a1i 11	. . . . 5 ⊢ (𝜑 → 0 < 4)
264		eqid 2741	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))
265		eqid 2741	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)))
266	7, 8, 263, 12, 264, 265, 246, 248	dvrelogpow2b 42566	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
267	233	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (4 − 1) = 3)
268	267	oveq2d 7375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((log‘𝑥)↑(4 − 1)) = ((log‘𝑥)↑3))
269	268	oveq1d 7374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (((log‘𝑥)↑(4 − 1)) / 𝑥) = (((log‘𝑥)↑3) / 𝑥))
270	269	oveq2d 7375	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) = ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥)))
271	270	mpteq2dva 5167	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
272	266, 271	eqtrd 2776	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
273		elioore 13323	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) → 𝑥 ∈ ℝ)
274	273	adantl 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 𝑥 ∈ ℝ)
275	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ∈ ℝ)
276		eliooord 13353	. . . . . . 7 ⊢ (𝑥 ∈ (4(,)𝑁) → (4 < 𝑥 ∧ 𝑥 < 𝑁))
277	276	simpld 496	. . . . . 6 ⊢ (𝑥 ∈ (4(,)𝑁) → 4 < 𝑥)
278	277	adantl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 < 𝑥)
279	275, 274, 278	ltled 11290	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ≤ 𝑥)
280	274, 279	aks4d1p1p7 42572	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥)))
281		oveq2 7367	. . . . . . . 8 ⊢ (𝑥 = 4 → (2 logb 𝑥) = (2 logb 4))
282	281	oveq1d 7374	. . . . . . 7 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑5) = ((2 logb 4)↑5))
283	282	oveq1d 7374	. . . . . 6 ⊢ (𝑥 = 4 → (((2 logb 𝑥)↑5) + 1) = (((2 logb 4)↑5) + 1))
284	283	oveq2d 7375	. . . . 5 ⊢ (𝑥 = 4 → (2 logb (((2 logb 𝑥)↑5) + 1)) = (2 logb (((2 logb 4)↑5) + 1)))
285	284	oveq2d 7375	. . . 4 ⊢ (𝑥 = 4 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · (2 logb (((2 logb 4)↑5) + 1))))
286	281	oveq1d 7374	. . . 4 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑2) = ((2 logb 4)↑2))
287	285, 286	oveq12d 7377	. . 3 ⊢ (𝑥 = 4 → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) = ((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)))
288	281	oveq1d 7374	. . 3 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑4) = ((2 logb 4)↑4))
289		oveq2 7367	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (2 logb 𝑥) = (2 logb 𝑁))
290	289	oveq1d 7374	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑5) = ((2 logb 𝑁)↑5))
291	290	oveq1d 7374	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((2 logb 𝑥)↑5) + 1) = (((2 logb 𝑁)↑5) + 1))
292	291	oveq2d 7375	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 logb (((2 logb 𝑥)↑5) + 1)) = (2 logb (((2 logb 𝑁)↑5) + 1)))
293	292	oveq2d 7375	. . . . 5 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · (2 logb (((2 logb 𝑁)↑5) + 1))))
294	14	a1i 11	. . . . . . 7 ⊢ (𝑥 = 𝑁 → 𝐶 = (2 logb (((2 logb 𝑁)↑5) + 1)))
295	294	oveq2d 7375	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝐶) = (2 · (2 logb (((2 logb 𝑁)↑5) + 1))))
296	295	eqcomd 2747	. . . . 5 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑁)↑5) + 1))) = (2 · 𝐶))
297	293, 296	eqtrd 2776	. . . 4 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · 𝐶))
298	289	oveq1d 7374	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = ((2 logb 𝑁)↑2))
299	15	a1i 11	. . . . . 6 ⊢ (𝑥 = 𝑁 → 𝐷 = ((2 logb 𝑁)↑2))
300	299	eqcomd 2747	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑2) = 𝐷)
301	298, 300	eqtrd 2776	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = 𝐷)
302	297, 301	oveq12d 7377	. . 3 ⊢ (𝑥 = 𝑁 → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) = ((2 · 𝐶) + 𝐷))
303	289	oveq1d 7374	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = ((2 logb 𝑁)↑4))
304	16	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑁 → 𝐸 = ((2 logb 𝑁)↑4))
305	304	eqcomd 2747	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑4) = 𝐸)
306	303, 305	eqtrd 2776	. . 3 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = 𝐸)
307		sq2 14154	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
308	307	oveq2i 7370	. . . . . . . . . . . . . . 15 ⊢ (2 logb (2↑2)) = (2 logb 4)
309	308	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
310	309	eqcomd 2747	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 logb 4) = (2 logb (2↑2)))
311	135	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ+)
312	56	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
313		relogbexp 26765	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ+ ∧ 2 ≠ 1 ∧ 2 ∈ ℤ) → (2 logb (2↑2)) = 2)
314	311, 37, 312, 313	syl3anc 1380	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
315	310, 314	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 logb 4) = 2)
316	315	oveq1d 7374	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 logb 4)↑5) = (2↑5))
317	316	oveq1d 7374	. . . . . . . . . 10 ⊢ (𝜑 → (((2 logb 4)↑5) + 1) = ((2↑5) + 1))
318	317	oveq2d 7375	. . . . . . . . 9 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) = (2 logb ((2↑5) + 1)))
319	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℝ)
320	319	leidd 11712	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 2)
321	315, 319	eqeltrd 2841	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 logb 4) ∈ ℝ)
322	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℕ0)
323	321, 322	reexpcld 14120	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 logb 4)↑5) ∈ ℝ)
324	316, 323	eqeltrrd 2842	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) ∈ ℝ)
325	324, 33	readdcld 11170	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ∈ ℝ)
326	322	nn0zd 12544	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 5 ∈ ℤ)
327	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
328	327, 315	breqtrrd 5102	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < (2 logb 4))
329	321, 326, 328	3jca 1135	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 logb 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 4)))
330		expgt0 14052	. . . . . . . . . . . . . 14 ⊢ (((2 logb 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 4)) → 0 < ((2 logb 4)↑5))
331	329, 330	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((2 logb 4)↑5))
332	331, 316	breqtrd 5100	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (2↑5))
333	324	ltp1d 12081	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) < ((2↑5) + 1))
334	26, 324, 325, 332, 333	lttrd 11303	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((2↑5) + 1))
335		6nn0 12453	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
336	335	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℕ0)
337	319, 336	reexpcld 14120	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑6) ∈ ℝ)
338	336	nn0zd 12544	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℤ)
339		expgt0 14052	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 6 ∈ ℤ ∧ 0 < 2) → 0 < (2↑6))
340	319, 338, 327, 339	syl3anc 1380	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (2↑6))
341	324, 324	readdcld 11170	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ∈ ℝ)
342	33, 319, 35	ltled 11290	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≤ 2)
343	319, 322, 342	expge1d 14122	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≤ (2↑5))
344	33, 324, 324, 343	leadd2dd 11761	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + 1) ≤ ((2↑5) + (2↑5)))
345	341	leidd 11712	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ ((2↑5) + (2↑5)))
346		df-6 12243	. . . . . . . . . . . . . . . . . . 19 ⊢ 6 = (5 + 1)
347	346	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 6 = (5 + 1))
348	347	oveq2d 7375	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑6) = (2↑(5 + 1)))
349		2cn 12251	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℂ)
351	193	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℕ0)
352	350, 351, 322	expaddd 14105	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑(5 + 1)) = ((2↑5) · (2↑1)))
353	348, 352	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑6) = ((2↑5) · (2↑1)))
354	350	exp1d 14098	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑1) = 2)
355	354	oveq2d 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑5) · (2↑1)) = ((2↑5) · 2))
356	353, 355	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑6) = ((2↑5) · 2))
357	48, 324	sselid 3914	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑5) ∈ ℂ)
358	357	times2d 12416	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2↑5) · 2) = ((2↑5) + (2↑5)))
359	356, 358	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2↑6) = ((2↑5) + (2↑5)))
360	359	eqcomd 2747	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) = (2↑6))
361	345, 360	breqtrd 5100	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ (2↑6))
362	325, 341, 337, 344, 361	letrd 11299	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ≤ (2↑6))
363	312, 320, 325, 334, 337, 340, 362	logblebd 42475	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb ((2↑5) + 1)) ≤ (2 logb (2↑6)))
364	311, 37, 338	relogbexpd 42473	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb (2↑6)) = 6)
365	363, 364	breqtrd 5100	. . . . . . . . 9 ⊢ (𝜑 → (2 logb ((2↑5) + 1)) ≤ 6)
366	318, 365	eqbrtrd 5096	. . . . . . . 8 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ≤ 6)
367		6t2e12 12743	. . . . . . . . 9 ⊢ (6 · 2) = ;12
368		6cn 12267	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
369	368	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
370		2nn 12249	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
371	193, 370	decnncl 12659	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ
372	371	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;12 ∈ ℕ)
373	372	nnred 12184	. . . . . . . . . . 11 ⊢ (𝜑 → ;12 ∈ ℝ)
374	373	recnd 11169	. . . . . . . . . 10 ⊢ (𝜑 → ;12 ∈ ℂ)
375	26, 327	gtned 11277	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≠ 0)
376	369, 350, 374, 375	ldiv 11984	. . . . . . . . 9 ⊢ (𝜑 → ((6 · 2) = ;12 ↔ 6 = (;12 / 2)))
377	367, 376	mpbii 235	. . . . . . . 8 ⊢ (𝜑 → 6 = (;12 / 2))
378	366, 377	breqtrd 5100	. . . . . . 7 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ≤ (;12 / 2))
379	323, 33	readdcld 11170	. . . . . . . . 9 ⊢ (𝜑 → (((2 logb 4)↑5) + 1) ∈ ℝ)
380	26, 33	readdcld 11170	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
381	26	ltp1d 12081	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (0 + 1))
382	26, 323, 33, 331	ltadd1dd 11757	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) < (((2 logb 4)↑5) + 1))
383	26, 380, 379, 381, 382	lttrd 11303	. . . . . . . . 9 ⊢ (𝜑 → 0 < (((2 logb 4)↑5) + 1))
384	319, 327, 379, 383, 37	relogbcld 42472	. . . . . . . 8 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ∈ ℝ)
385	384, 373, 311	lemuldiv2d 13031	. . . . . . 7 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ ;12 ↔ (2 logb (((2 logb 4)↑5) + 1)) ≤ (;12 / 2)))
386	378, 385	mpbird 259	. . . . . 6 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ ;12)
387	315	oveq1d 7374	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 4)↑2) = (2↑2))
388	387, 307	eqtrdi 2792	. . . . . . . . 9 ⊢ (𝜑 → ((2 logb 4)↑2) = 4)
389	388	oveq2d 7375	. . . . . . . 8 ⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = (;16 − 4))
390		2nn0 12449	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
391		eqid 2741	. . . . . . . . . 10 ⊢ ;12 = ;12
392		4cn 12261	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
393		4p2e6 12324	. . . . . . . . . . 11 ⊢ (4 + 2) = 6
394	392, 349, 393	addcomli 11334	. . . . . . . . . 10 ⊢ (2 + 4) = 6
395	193, 390, 174, 391, 394	decaddi 12699	. . . . . . . . 9 ⊢ (;12 + 4) = ;16
396	392	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℂ)
397		6nn 12265	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
398	193, 397	decnncl 12659	. . . . . . . . . . . . 13 ⊢ ;16 ∈ ℕ
399	398	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;16 ∈ ℕ)
400	399	nnred 12184	. . . . . . . . . . 11 ⊢ (𝜑 → ;16 ∈ ℝ)
401	48, 400	sselid 3914	. . . . . . . . . 10 ⊢ (𝜑 → ;16 ∈ ℂ)
402	374, 396, 401	addlsub 11562	. . . . . . . . 9 ⊢ (𝜑 → ((;12 + 4) = ;16 ↔ ;12 = (;16 − 4)))
403	395, 402	mpbii 235	. . . . . . . 8 ⊢ (𝜑 → ;12 = (;16 − 4))
404	389, 403	eqtr4d 2779	. . . . . . 7 ⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = ;12)
405	404	eqcomd 2747	. . . . . 6 ⊢ (𝜑 → ;12 = (;16 − ((2 logb 4)↑2)))
406	386, 405	breqtrd 5100	. . . . 5 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb 4)↑2)))
407	319, 384	remulcld 11171	. . . . . 6 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ∈ ℝ)
408	321	resqcld 14082	. . . . . 6 ⊢ (𝜑 → ((2 logb 4)↑2) ∈ ℝ)
409		leaddsub 11622	. . . . . 6 ⊢ (((2 · (2 logb (((2 logb 4)↑5) + 1))) ∈ ℝ ∧ ((2 logb 4)↑2) ∈ ℝ ∧ ;16 ∈ ℝ) → (((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)) ≤ ;16 ↔ (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb 4)↑2))))
410	407, 408, 400, 409	syl3anc 1380	. . . . 5 ⊢ (𝜑 → (((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)) ≤ ;16 ↔ (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb 4)↑2))))
411	406, 410	mpbird 259	. . . 4 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)) ≤ ;16)
412	315	oveq1d 7374	. . . . . 6 ⊢ (𝜑 → ((2 logb 4)↑4) = (2↑4))
413		2exp4 17050	. . . . . 6 ⊢ (2↑4) = ;16
414	412, 413	eqtrdi 2792	. . . . 5 ⊢ (𝜑 → ((2 logb 4)↑4) = ;16)
415	414	eqcomd 2747	. . . 4 ⊢ (𝜑 → ;16 = ((2 logb 4)↑4))
416	411, 415	breqtrd 5100	. . 3 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)) ≤ ((2 logb 4)↑4))
417	7, 8, 219, 261, 262, 272, 280, 287, 288, 302, 306, 416, 12	dvle2 42570	. 2 ⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸)
418	1, 2, 3, 13, 14, 15, 16, 417	aks4d1p1p4 42569	1 ⊢ (𝜑 → 𝐴 < (2↑𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121   ≠ wne 2936  ∀wral 3055   ⊆ wss 3884   class class class wbr 5074   ↦ cmpt 5155  dom cdm 5620   ↾ cres 5622   Fn wfn 6483  ⟶wf 6484  ‘cfv 6488  (class class class)co 7359  ℂcc 11032  ℝcr 11033  0cc0 11034  1c1 11035   + caddc 11037   · cmul 11039  ℝ^*cxr 11174   < clt 11175   ≤ cle 11176   − cmin 11373   / cdiv 11803  ℕcn 12169  2c2 12231  3c3 12232  4c4 12233  5c5 12234  6c6 12235  ℕ₀cn0 12432  ℤcz 12519  ;cdc 12639  ℤ_≥cuz 12783  ℝ⁺crp 12937  (,)cioo 13293  [,]cicc 13296  ...cfz 13456  ⌊cfl 13744  ⌈cceil 13745  ↑cexp 14018  ∏cprod 15863  –cn→ccncf 24864   D cdv 25851  logclog 26539   log_b clogb 26749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681  ax-inf2 9557  ax-cnex 11090  ax-resscn 11091  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-addrcl 11095  ax-mulcl 11096  ax-mulrcl 11097  ax-mulcom 11098  ax-addass 11099  ax-mulass 11100  ax-distr 11101  ax-i2m1 11102  ax-1ne0 11103  ax-1rid 11104  ax-rnegex 11105  ax-rrecex 11106  ax-cnre 11107  ax-pre-lttri 11108  ax-pre-lttrn 11109  ax-pre-ltadd 11110  ax-pre-mulgt0 11111  ax-pre-sup 11112  ax-addf 11113

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4841  df-int 4880  df-iun 4925  df-iin 4926  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-se 5574  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-of 7623  df-om 7810  df-1st 7933  df-2nd 7934  df-supp 8103  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-fi 9318  df-sup 9349  df-inf 9350  df-oi 9419  df-card 9858  df-pnf 11177  df-mnf 11178  df-xr 11179  df-ltxr 11180  df-le 11181  df-sub 11375  df-neg 11376  df-div 11804  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-q 12894  df-rp 12938  df-xneg 13058  df-xadd 13059  df-xmul 13060  df-ioo 13297  df-ioc 13298  df-ico 13299  df-icc 13300  df-fz 13457  df-fzo 13604  df-fl 13746  df-ceil 13747  df-mod 13824  df-seq 13959  df-exp 14019  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15024  df-cj 15056  df-re 15057  df-im 15058  df-sqrt 15192  df-abs 15193  df-limsup 15428  df-clim 15445  df-rlim 15446  df-sum 15644  df-prod 15864  df-ef 16027  df-e 16028  df-sin 16029  df-cos 16030  df-pi 16032  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-starv 17230  df-sca 17231  df-vsca 17232  df-ip 17233  df-tset 17234  df-ple 17235  df-ds 17237  df-unif 17238  df-hom 17239  df-cco 17240  df-rest 17380  df-topn 17381  df-0g 17399  df-gsum 17400  df-topgen 17401  df-pt 17402  df-prds 17405  df-xrs 17461  df-qtop 17466  df-imas 17467  df-xps 17469  df-mre 17543  df-mrc 17544  df-acs 17546  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18747  df-mulg 19039  df-cntz 19286  df-cmn 19751  df-psmet 21342  df-xmet 21343  df-met 21344  df-bl 21345  df-mopn 21346  df-fbas 21347  df-fg 21348  df-cnfld 21351  df-top 22880  df-topon 22897  df-topsp 22919  df-bases 22932  df-cld 23005  df-ntr 23006  df-cls 23007  df-nei 23084  df-lp 23122  df-perf 23123  df-cn 23213  df-cnp 23214  df-haus 23301  df-cmp 23373  df-tx 23548  df-hmeo 23741  df-fil 23832  df-fm 23924  df-flim 23925  df-flf 23926  df-xms 24306  df-ms 24307  df-tms 24308  df-cncf 24866  df-limc 25854  df-dv 25855  df-log 26541  df-cxp 26542  df-logb 26750

This theorem is referenced by:  aks4d1p1  42574