Theorem aks4d1p1p5 42032

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 12373	. . . 4 ⊢ 3 ∈ ℝ
5	4	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
6		4re 12377	. . . 4 ⊢ 4 ∈ ℝ
7	6	a1i 11	. . 3 ⊢ (𝜑 → 4 ∈ ℝ)
8	1	nnred 12308	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
9	5	lep1d 12226	. . . 4 ⊢ (𝜑 → 3 ≤ (3 + 1))
10		3p1e4 12438	. . . 4 ⊢ (3 + 1) = 4
11	9, 10	breqtrdi 5207	. . 3 ⊢ (𝜑 → 3 ≤ 4)
12		aks4d1p1p5.4	. . 3 ⊢ (𝜑 → 4 ≤ 𝑁)
13	5, 7, 8, 11, 12	letrd 11447	. 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 12367	. . . . . . . 8 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℝ)
19		2pos 12396	. . . . . . . . 9 ⊢ 0 < 2
20	19	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 2)
21		elicc2 13472	. . . . . . . . . . . . . . 15 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
22	7, 8, 21	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
23	22	biimpd 229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
24	23	imp 406	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
25	24	simp1d 1142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ)
26		0red 11293	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
27	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
28	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℝ)
29		4pos 12400	. . . . . . . . . . . . 13 ⊢ 0 < 4
30	29	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 4)
31	24	simp2d 1143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
32	27, 28, 25, 30, 31	ltletrd 11450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
33		1red 11291	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℝ)
34		1lt2 12464	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
35	34	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 2)
36	33, 35	ltned 11426	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≠ 2)
37	36	necomd 3002	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 1)
38	37	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 1)
39	18, 20, 25, 32, 38	relogbcld 41929	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈ ℝ)
40		5nn0 12573	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
41	40	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℕ0)
42	39, 41	reexpcld 14213	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑5) ∈ ℝ)
43		1red 11291	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ)
44	42, 43	readdcld 11319	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (((2 logb 𝑥)↑5) + 1) ∈ ℝ)
45	27, 43	readdcld 11319	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) ∈ ℝ)
46	27	ltp1d 12225	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (0 + 1))
47	41	nn0zd 12665	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℤ)
48		ax-resscn 11241	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
49	48, 18	sselid 4006	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℂ)
50	27, 20	gtned 11425	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 0)
51		logb1 26830	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) = 0)
52	49, 50, 38, 51	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) = 0)
53		1lt4 12469	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
54	53	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 4)
55	43, 28, 25, 54, 31	ltletrd 11450	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 𝑥)
56		2z 12675	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
57	56	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℤ)
58	57	uzidd 12919	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ (ℤ≥‘2))
59		1rp 13061	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ+
60	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ+)
61	25, 32	elrpd 13096	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ+)
62		logblt 26845	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 < 𝑥 ↔ (2 logb 1) < (2 logb 𝑥)))
63	58, 60, 61, 62	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (1 < 𝑥 ↔ (2 logb 1) < (2 logb 𝑥)))
64	55, 63	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) < (2 logb 𝑥))
65	52, 64	eqbrtrrd 5190	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (2 logb 𝑥))
66		expgt0 14146	. . . . . . . . . . 11 ⊢ (((2 logb 𝑥) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑥)) → 0 < ((2 logb 𝑥)↑5))
67	39, 47, 65, 66	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < ((2 logb 𝑥)↑5))
68	27, 42, 43, 67	ltadd1dd 11901	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) < (((2 logb 𝑥)↑5) + 1))
69	27, 45, 44, 46, 68	lttrd 11451	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (((2 logb 𝑥)↑5) + 1))
70	18, 20, 44, 69, 38	relogbcld 41929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ)
71	18, 70	remulcld 11320	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) ∈ ℝ)
72		0red 11293	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
73		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ (4[,]𝑁))
74	7, 8	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 ∈ ℝ ∧ 𝑁 ∈ ℝ))
75	74	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (4 ∈ ℝ ∧ 𝑁 ∈ ℝ))
76	75, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
77	73, 76	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
78	77	simp2d 1143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
79	72, 28, 25, 30, 78	ltletrd 11450	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
80	18, 20, 25, 79, 38	relogbcld 41929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈ ℝ)
81	80	resqcld 14175	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑2) ∈ ℝ)
82	71, 81	readdcld 11319	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈ ℝ)
83	82	fmpttd 7149	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ)
84	48	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
85		3lt4 12467	. . . . . . . . . . 11 ⊢ 3 < 4
86	85	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 4)
87	8, 33	readdcld 11319	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
88	8	ltp1d 12225	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
89	7, 8, 87, 12, 88	lelttrd 11448	. . . . . . . . . 10 ⊢ (𝜑 → 4 < (𝑁 + 1))
90	86, 89	jca 511	. . . . . . . . 9 ⊢ (𝜑 → (3 < 4 ∧ 4 < (𝑁 + 1)))
91	5	rexrd 11340	. . . . . . . . . 10 ⊢ (𝜑 → 3 ∈ ℝ*)
92	87	rexrd 11340	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ*)
93	7	rexrd 11340	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℝ*)
94		elioo5 13464	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 4 ∈ ℝ*) → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
95	91, 92, 93, 94	syl3anc 1371	. . . . . . . . 9 ⊢ (𝜑 → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
96	90, 95	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ (3(,)(𝑁 + 1)))
97	5, 7, 8, 86, 12	ltletrd 11450	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 𝑁)
98	97, 88	jca 511	. . . . . . . . 9 ⊢ (𝜑 → (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1)))
99	8	rexrd 11340	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ*)
100		elioo5 13464	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
101	91, 92, 99, 100	syl3anc 1371	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
102	98, 101	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (3(,)(𝑁 + 1)))
103		iccssioo2 13480	. . . . . . . 8 ⊢ ((4 ∈ (3(,)(𝑁 + 1)) ∧ 𝑁 ∈ (3(,)(𝑁 + 1))) → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
104	96, 102, 103	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
105	104	resmptd 6069	. . . . . 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 12371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℂ)
107	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ)
108	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 2)
109		elioore 13437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 𝑥 ∈ ℝ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ)
111		0red 11293	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 ∈ ℝ)
112	4	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 ∈ ℝ)
113		3pos 12398	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 3
114	113	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 3)
115		eliooord 13466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → (3 < 𝑥 ∧ 𝑥 < (𝑁 + 1)))
116		simpl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 < 𝑥 ∧ 𝑥 < (𝑁 + 1)) → 3 < 𝑥)
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 3 < 𝑥)
118	117	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 < 𝑥)
119	111, 112, 110, 114, 118	lttrd 11451	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 𝑥)
120	37	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
121	107, 108, 110, 119, 120	relogbcld 41929	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈ ℝ)
122	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℕ0)
123	121, 122	reexpcld 14213	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈ ℝ)
124		1red 11291	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℝ)
125	123, 124	readdcld 11319	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈ ℝ)
126	111, 124	readdcld 11319	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) ∈ ℝ)
127	111	ltp1d 12225	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (0 + 1))
128	122	nn0zd 12665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℤ)
129	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 2)
130		2lt3 12465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 < 3
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 < 3)
132	124, 107, 112, 129, 131	lttrd 11451	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 3)
133	124, 112, 110, 132, 118	lttrd 11451	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 𝑥)
134	110, 119	elrpd 13096	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ+)
135		2rp 13062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ+
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ+)
137	134, 136, 129	jca32 515	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)))
138		logbgt0b 26854	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝑥) ↔ 1 < 𝑥))
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 < (2 logb 𝑥) ↔ 1 < 𝑥))
140	133, 139	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (2 logb 𝑥))
141	121, 128, 140, 66	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < ((2 logb 𝑥)↑5))
142	111, 123, 124, 141	ltadd1dd 11901	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) < (((2 logb 𝑥)↑5) + 1))
143	111, 126, 125, 127, 142	lttrd 11451	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (((2 logb 𝑥)↑5) + 1))
144	124, 129	ltned 11426	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ≠ 2)
145	144	necomd 3002	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
146	107, 108, 125, 143, 145	relogbcld 41929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ)
147	146	recnd 11318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℂ)
148	106, 147	mulcld 11310	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) ∈ ℂ)
149	48, 121	sselid 4006	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈ ℂ)
150	149	sqcld 14194	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑2) ∈ ℂ)
151	148, 150	addcld 11309	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈ ℂ)
152	151	fmpttd 7149	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ)
153		ioossre 13468	. . . . . . . . . 10 ⊢ (3(,)(𝑁 + 1)) ⊆ ℝ
154	153	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (3(,)(𝑁 + 1)) ⊆ ℝ)
155	84, 152, 154	3jca 1128	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
156	136	relogcld 26683	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℝ)
157	125, 156	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) · (log‘2)) ∈ ℝ)
158	48, 123	sselid 4006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈ ℂ)
159		1cnd 11285	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℂ)
160	158, 159	addcld 11309	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈ ℂ)
161	111, 108	gtned 11425	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 0)
162	106, 161	logcld 26630	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℂ)
163	111, 143	gtned 11425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ≠ 0)
164		loggt0b 26692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
165	135, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 < (log‘2) ↔ 1 < 2)
166	35, 165	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 < (log‘2))
167	26, 166	ltned 11426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≠ (log‘2))
168	167	necomd 3002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘2) ≠ 0)
169	168	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ≠ 0)
170	160, 162, 163, 169	mulne0d 11942	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) · (log‘2)) ≠ 0)
171	124, 157, 170	redivcld 12122	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) ∈ ℝ)
172		5re 12380	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℝ)
174		4nn0 12572	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℕ0
175	174	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℕ0)
176	121, 175	reexpcld 14213	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈ ℝ)
177	173, 176	remulcld 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (5 · ((2 logb 𝑥)↑4)) ∈ ℝ)
178	110, 156	remulcld 11320	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ∈ ℝ)
179	48, 110	sselid 4006	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℂ)
180	111, 119	gtned 11425	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ≠ 0)
181	179, 162, 180, 169	mulne0d 11942	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ≠ 0)
182	124, 178, 181	redivcld 12122	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / (𝑥 · (log‘2))) ∈ ℝ)
183	177, 182	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) ∈ ℝ)
184	183, 111	readdcld 11319	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0) ∈ ℝ)
185	171, 184	remulcld 11320	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈ ℝ)
186	107, 185	remulcld 11320	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) ∈ ℝ)
187	156	resqcld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ∈ ℝ)
188	56	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℤ)
189	162, 169, 188	expne0d 14202	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ≠ 0)
190	107, 187, 189	redivcld 12122	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 / ((log‘2)↑2)) ∈ ℝ)
191	134	relogcld 26683	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘𝑥) ∈ ℝ)
192		2m1e1 12419	. . . . . . . . . . . . . . . . . 18 ⊢ (2 − 1) = 1
193		1nn0 12569	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
194	192, 193	eqeltri 2840	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) ∈ ℕ0
195	194	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 − 1) ∈ ℕ0)
196	191, 195	reexpcld 14213	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(2 − 1)) ∈ ℝ)
197	196, 110, 180	redivcld 12122	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ)
198	190, 197	remulcld 11320	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ)
199	186, 198	readdcld 11319	. . . . . . . . . . . 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 3152	. . . . . . . . . . 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 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(3(,)(𝑁 + 1))
202	201	fnmptf 6716	. . . . . . . . . . 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 11856	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 3)
205	8	lep1d 12226	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
206	5, 8, 87, 13, 205	letrd 11447	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ (𝑁 + 1))
207	5, 87, 204, 206	aks4d1p1p6 42030	. . . . . . . . . . 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 6672	. . . . . . . . . 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 257	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)))
210	209	fndmd 6684	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (3(,)(𝑁 + 1)))
211		dvcn 25977	. . . . . . . 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 583	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
213		rescncf 24942	. . . . . . . 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 2845	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ))
217		cncfcdm 24943	. . . . 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 583	. . . 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 257	. . 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 14213	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑4) ∈ ℝ)
222	221	fmpttd 7149	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ)
223	104	resmptd 6069	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)))
224	48, 176	sselid 4006	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈ ℂ)
225	224	fmpttd 7149	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ)
226	84, 225, 154	3jca 1128	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
227	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℝ)
228	156, 175	reexpcld 14213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ∈ ℝ)
229		4z 12677	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℤ
230	229	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℤ)
231	162, 169, 230	expne0d 14202	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ≠ 0)
232	227, 228, 231	redivcld 12122	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 / ((log‘2)↑4)) ∈ ℝ)
233		4m1e3 12422	. . . . . . . . . . . . . . . . 17 ⊢ (4 − 1) = 3
234		3nn0 12571	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℕ0
235	233, 234	eqeltri 2840	. . . . . . . . . . . . . . . 16 ⊢ (4 − 1) ∈ ℕ0
236	235	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 − 1) ∈ ℕ0)
237	191, 236	reexpcld 14213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(4 − 1)) ∈ ℝ)
238	237, 110, 180	redivcld 12122	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(4 − 1)) / 𝑥) ∈ ℝ)
239	232, 238	remulcld 11320	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
240	239	ralrimiva 3152	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
241	201	fnmptf 6716	. . . . . . . . . . 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 2740	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))
245		eqid 2740	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)))
246		eqid 2740	. . . . . . . . . . . 12 ⊢ (4 / ((log‘2)↑4)) = (4 / ((log‘2)↑4))
247		4nn 12376	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
248	247	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 4 ∈ ℕ)
249	5, 87, 243, 206, 244, 245, 246, 248	dvrelogpow2b 42025	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
250	249	fneq1d 6672	. . . . . . . . . 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 257	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) Fn (3(,)(𝑁 + 1)))
252	251	fndmd 6684	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (3(,)(𝑁 + 1)))
253		dvcn 25977	. . . . . . . 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 583	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
255		rescncf 24942	. . . . . . . 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 2845	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ))
259		cncfcdm 24943	. . . . 5 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
260	84, 258, 259	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
261	222, 260	mpbird 257	. . 3 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ))
262	7, 8, 11, 12	aks4d1p1p6 42030	. . 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 2740	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))
265		eqid 2740	. . . . 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 42025	. . . 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 7464	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((log‘𝑥)↑(4 − 1)) = ((log‘𝑥)↑3))
269	268	oveq1d 7463	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (((log‘𝑥)↑(4 − 1)) / 𝑥) = (((log‘𝑥)↑3) / 𝑥))
270	269	oveq2d 7464	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) = ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥)))
271	270	mpteq2dva 5266	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
272	266, 271	eqtrd 2780	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
273		elioore 13437	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) → 𝑥 ∈ ℝ)
274	273	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 𝑥 ∈ ℝ)
275	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ∈ ℝ)
276		eliooord 13466	. . . . . . 7 ⊢ (𝑥 ∈ (4(,)𝑁) → (4 < 𝑥 ∧ 𝑥 < 𝑁))
277	276	simpld 494	. . . . . 6 ⊢ (𝑥 ∈ (4(,)𝑁) → 4 < 𝑥)
278	277	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 < 𝑥)
279	275, 274, 278	ltled 11438	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ≤ 𝑥)
280	274, 279	aks4d1p1p7 42031	. . 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 7456	. . . . . . . 8 ⊢ (𝑥 = 4 → (2 logb 𝑥) = (2 logb 4))
282	281	oveq1d 7463	. . . . . . 7 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑5) = ((2 logb 4)↑5))
283	282	oveq1d 7463	. . . . . 6 ⊢ (𝑥 = 4 → (((2 logb 𝑥)↑5) + 1) = (((2 logb 4)↑5) + 1))
284	283	oveq2d 7464	. . . . 5 ⊢ (𝑥 = 4 → (2 logb (((2 logb 𝑥)↑5) + 1)) = (2 logb (((2 logb 4)↑5) + 1)))
285	284	oveq2d 7464	. . . 4 ⊢ (𝑥 = 4 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · (2 logb (((2 logb 4)↑5) + 1))))
286	281	oveq1d 7463	. . . 4 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑2) = ((2 logb 4)↑2))
287	285, 286	oveq12d 7466	. . 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 7463	. . 3 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑4) = ((2 logb 4)↑4))
289		oveq2 7456	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (2 logb 𝑥) = (2 logb 𝑁))
290	289	oveq1d 7463	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑5) = ((2 logb 𝑁)↑5))
291	290	oveq1d 7463	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((2 logb 𝑥)↑5) + 1) = (((2 logb 𝑁)↑5) + 1))
292	291	oveq2d 7464	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 logb (((2 logb 𝑥)↑5) + 1)) = (2 logb (((2 logb 𝑁)↑5) + 1)))
293	292	oveq2d 7464	. . . . 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 7464	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝐶) = (2 · (2 logb (((2 logb 𝑁)↑5) + 1))))
296	295	eqcomd 2746	. . . . 5 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑁)↑5) + 1))) = (2 · 𝐶))
297	293, 296	eqtrd 2780	. . . 4 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · 𝐶))
298	289	oveq1d 7463	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = ((2 logb 𝑁)↑2))
299	15	a1i 11	. . . . . 6 ⊢ (𝑥 = 𝑁 → 𝐷 = ((2 logb 𝑁)↑2))
300	299	eqcomd 2746	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑2) = 𝐷)
301	298, 300	eqtrd 2780	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = 𝐷)
302	297, 301	oveq12d 7466	. . 3 ⊢ (𝑥 = 𝑁 → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) = ((2 · 𝐶) + 𝐷))
303	289	oveq1d 7463	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = ((2 logb 𝑁)↑4))
304	16	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑁 → 𝐸 = ((2 logb 𝑁)↑4))
305	304	eqcomd 2746	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑4) = 𝐸)
306	303, 305	eqtrd 2780	. . 3 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = 𝐸)
307		sq2 14246	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
308	307	oveq2i 7459	. . . . . . . . . . . . . . 15 ⊢ (2 logb (2↑2)) = (2 logb 4)
309	308	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
310	309	eqcomd 2746	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 logb 4) = (2 logb (2↑2)))
311	135	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ+)
312	56	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
313		relogbexp 26841	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ+ ∧ 2 ≠ 1 ∧ 2 ∈ ℤ) → (2 logb (2↑2)) = 2)
314	311, 37, 312, 313	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
315	310, 314	eqtrd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 logb 4) = 2)
316	315	oveq1d 7463	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 logb 4)↑5) = (2↑5))
317	316	oveq1d 7463	. . . . . . . . . 10 ⊢ (𝜑 → (((2 logb 4)↑5) + 1) = ((2↑5) + 1))
318	317	oveq2d 7464	. . . . . . . . 9 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) = (2 logb ((2↑5) + 1)))
319	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℝ)
320	319	leidd 11856	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 2)
321	315, 319	eqeltrd 2844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 logb 4) ∈ ℝ)
322	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℕ0)
323	321, 322	reexpcld 14213	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 logb 4)↑5) ∈ ℝ)
324	316, 323	eqeltrrd 2845	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) ∈ ℝ)
325	324, 33	readdcld 11319	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ∈ ℝ)
326	322	nn0zd 12665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 5 ∈ ℤ)
327	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
328	327, 315	breqtrrd 5194	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < (2 logb 4))
329	321, 326, 328	3jca 1128	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 logb 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 4)))
330		expgt0 14146	. . . . . . . . . . . . . 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 5192	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (2↑5))
333	324	ltp1d 12225	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) < ((2↑5) + 1))
334	26, 324, 325, 332, 333	lttrd 11451	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((2↑5) + 1))
335		6nn0 12574	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
336	335	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℕ0)
337	319, 336	reexpcld 14213	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑6) ∈ ℝ)
338	336	nn0zd 12665	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℤ)
339		expgt0 14146	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 6 ∈ ℤ ∧ 0 < 2) → 0 < (2↑6))
340	319, 338, 327, 339	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (2↑6))
341	324, 324	readdcld 11319	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ∈ ℝ)
342	33, 319, 35	ltled 11438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≤ 2)
343	319, 322, 342	expge1d 14215	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≤ (2↑5))
344	33, 324, 324, 343	leadd2dd 11905	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + 1) ≤ ((2↑5) + (2↑5)))
345	341	leidd 11856	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ ((2↑5) + (2↑5)))
346		df-6 12360	. . . . . . . . . . . . . . . . . . 19 ⊢ 6 = (5 + 1)
347	346	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 6 = (5 + 1))
348	347	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑6) = (2↑(5 + 1)))
349		2cn 12368	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℂ)
351	193	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℕ0)
352	350, 351, 322	expaddd 14198	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑(5 + 1)) = ((2↑5) · (2↑1)))
353	348, 352	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑6) = ((2↑5) · (2↑1)))
354	350	exp1d 14191	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑1) = 2)
355	354	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑5) · (2↑1)) = ((2↑5) · 2))
356	353, 355	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑6) = ((2↑5) · 2))
357	48, 324	sselid 4006	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑5) ∈ ℂ)
358	357	times2d 12537	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2↑5) · 2) = ((2↑5) + (2↑5)))
359	356, 358	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2↑6) = ((2↑5) + (2↑5)))
360	359	eqcomd 2746	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) = (2↑6))
361	345, 360	breqtrd 5192	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ (2↑6))
362	325, 341, 337, 344, 361	letrd 11447	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ≤ (2↑6))
363	312, 320, 325, 334, 337, 340, 362	logblebd 41932	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb ((2↑5) + 1)) ≤ (2 logb (2↑6)))
364	311, 37, 338	relogbexpd 41930	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb (2↑6)) = 6)
365	363, 364	breqtrd 5192	. . . . . . . . 9 ⊢ (𝜑 → (2 logb ((2↑5) + 1)) ≤ 6)
366	318, 365	eqbrtrd 5188	. . . . . . . 8 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ≤ 6)
367		6t2e12 12862	. . . . . . . . 9 ⊢ (6 · 2) = ;12
368		6cn 12384	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
369	368	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
370		2nn 12366	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
371	193, 370	decnncl 12778	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ
372	371	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;12 ∈ ℕ)
373	372	nnred 12308	. . . . . . . . . . 11 ⊢ (𝜑 → ;12 ∈ ℝ)
374	373	recnd 11318	. . . . . . . . . 10 ⊢ (𝜑 → ;12 ∈ ℂ)
375	26, 327	gtned 11425	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≠ 0)
376	369, 350, 374, 375	ldiv 12128	. . . . . . . . 9 ⊢ (𝜑 → ((6 · 2) = ;12 ↔ 6 = (;12 / 2)))
377	367, 376	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → 6 = (;12 / 2))
378	366, 377	breqtrd 5192	. . . . . . 7 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ≤ (;12 / 2))
379	323, 33	readdcld 11319	. . . . . . . . 9 ⊢ (𝜑 → (((2 logb 4)↑5) + 1) ∈ ℝ)
380	26, 33	readdcld 11319	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
381	26	ltp1d 12225	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (0 + 1))
382	26, 323, 33, 331	ltadd1dd 11901	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) < (((2 logb 4)↑5) + 1))
383	26, 380, 379, 381, 382	lttrd 11451	. . . . . . . . 9 ⊢ (𝜑 → 0 < (((2 logb 4)↑5) + 1))
384	319, 327, 379, 383, 37	relogbcld 41929	. . . . . . . 8 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ∈ ℝ)
385	384, 373, 311	lemuldiv2d 13149	. . . . . . 7 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ ;12 ↔ (2 logb (((2 logb 4)↑5) + 1)) ≤ (;12 / 2)))
386	378, 385	mpbird 257	. . . . . 6 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ ;12)
387	315	oveq1d 7463	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 4)↑2) = (2↑2))
388	387, 307	eqtrdi 2796	. . . . . . . . 9 ⊢ (𝜑 → ((2 logb 4)↑2) = 4)
389	388	oveq2d 7464	. . . . . . . 8 ⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = (;16 − 4))
390		2nn0 12570	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
391		eqid 2740	. . . . . . . . . 10 ⊢ ;12 = ;12
392		4cn 12378	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
393		4p2e6 12446	. . . . . . . . . . 11 ⊢ (4 + 2) = 6
394	392, 349, 393	addcomli 11482	. . . . . . . . . 10 ⊢ (2 + 4) = 6
395	193, 390, 174, 391, 394	decaddi 12818	. . . . . . . . 9 ⊢ (;12 + 4) = ;16
396	392	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℂ)
397		6nn 12382	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
398	193, 397	decnncl 12778	. . . . . . . . . . . . 13 ⊢ ;16 ∈ ℕ
399	398	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;16 ∈ ℕ)
400	399	nnred 12308	. . . . . . . . . . 11 ⊢ (𝜑 → ;16 ∈ ℝ)
401	48, 400	sselid 4006	. . . . . . . . . 10 ⊢ (𝜑 → ;16 ∈ ℂ)
402	374, 396, 401	addlsub 11706	. . . . . . . . 9 ⊢ (𝜑 → ((;12 + 4) = ;16 ↔ ;12 = (;16 − 4)))
403	395, 402	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → ;12 = (;16 − 4))
404	389, 403	eqtr4d 2783	. . . . . . 7 ⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = ;12)
405	404	eqcomd 2746	. . . . . 6 ⊢ (𝜑 → ;12 = (;16 − ((2 logb 4)↑2)))
406	386, 405	breqtrd 5192	. . . . 5 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb 4)↑2)))
407	319, 384	remulcld 11320	. . . . . 6 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ∈ ℝ)
408	321	resqcld 14175	. . . . . 6 ⊢ (𝜑 → ((2 logb 4)↑2) ∈ ℝ)
409		leaddsub 11766	. . . . . 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 1371	. . . . 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 257	. . . 4 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)) ≤ ;16)
412	315	oveq1d 7463	. . . . . 6 ⊢ (𝜑 → ((2 logb 4)↑4) = (2↑4))
413		2exp4 17132	. . . . . 6 ⊢ (2↑4) = ;16
414	412, 413	eqtrdi 2796	. . . . 5 ⊢ (𝜑 → ((2 logb 4)↑4) = ;16)
415	414	eqcomd 2746	. . . 4 ⊢ (𝜑 → ;16 = ((2 logb 4)↑4))
416	411, 415	breqtrd 5192	. . 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 42029	. 2 ⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸)
418	1, 2, 3, 13, 14, 15, 16, 417	aks4d1p1p4 42028	1 ⊢ (𝜑 → 𝐴 < (2↑𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067   ⊆ wss 3976   class class class wbr 5166   ↦ cmpt 5249  dom cdm 5700   ↾ cres 5702   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325   − cmin 11520   / cdiv 11947  ℕcn 12293  2c2 12348  3c3 12349  4c4 12350  5c5 12351  6c6 12352  ℕ₀cn0 12553  ℤcz 12639  ;cdc 12758  ℤ_≥cuz 12903  ℝ⁺crp 13057  (,)cioo 13407  [,]cicc 13410  ...cfz 13567  ⌊cfl 13841  ⌈cceil 13842  ↑cexp 14112  ∏cprod 15951  –cn→ccncf 24921   D cdv 25918  logclog 26614   log_b clogb 26825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ioc 13412  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-ceil 13844  df-mod 13921  df-seq 14053  df-exp 14113  df-fac 14323  df-bc 14352  df-hash 14380  df-shft 15116  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-limsup 15517  df-clim 15534  df-rlim 15535  df-sum 15735  df-prod 15952  df-ef 16115  df-e 16116  df-sin 16117  df-cos 16118  df-pi 16120  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-rest 17482  df-topn 17483  df-0g 17501  df-gsum 17502  df-topgen 17503  df-pt 17504  df-prds 17507  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-mulg 19108  df-cntz 19357  df-cmn 19824  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-fbas 21384  df-fg 21385  df-cnfld 21388  df-top 22921  df-topon 22938  df-topsp 22960  df-bases 22974  df-cld 23048  df-ntr 23049  df-cls 23050  df-nei 23127  df-lp 23165  df-perf 23166  df-cn 23256  df-cnp 23257  df-haus 23344  df-cmp 23416  df-tx 23591  df-hmeo 23784  df-fil 23875  df-fm 23967  df-flim 23968  df-flf 23969  df-xms 24351  df-ms 24352  df-tms 24353  df-cncf 24923  df-limc 25921  df-dv 25922  df-log 26616  df-cxp 26617  df-logb 26826

This theorem is referenced by:  aks4d1p1  42033