Theorem aks4d1p1p5 43316

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 12447	. . . 4 ⊢ 3 ∈ ℝ
5	4	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
6		4re 12451	. . . 4 ⊢ 4 ∈ ℝ
7	6	a1i 11	. . 3 ⊢ (𝜑 → 4 ∈ ℝ)
8	1	nnred 12374	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
9	5	lep1d 12272	. . . 4 ⊢ (𝜑 → 3 ≤ (3 + 1))
10		3p1e4 12511	. . . 4 ⊢ (3 + 1) = 4
11	9, 10	breqtrdi 5149	. . 3 ⊢ (𝜑 → 3 ≤ 4)
12		aks4d1p1p5.4	. . 3 ⊢ (𝜑 → 4 ≤ 𝑁)
13	5, 7, 8, 11, 12	letrd 11491	. 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 12441	. . . . . . . 8 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℝ)
19		2pos 12471	. . . . . . . . 9 ⊢ 0 < 2
20	19	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 2)
21		elicc2 13566	. . . . . . . . . . . . . . 15 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
22	7, 8, 21	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
23	22	biimpd 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
24	23	imp 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
25	24	simp1d 1160	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ)
26		0red 11335	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
27	26	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
28	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℝ)
29		4pos 12477	. . . . . . . . . . . . 13 ⊢ 0 < 4
30	29	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 4)
31	24	simp2d 1161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
32	27, 28, 25, 30, 31	ltletrd 11494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
33		1red 11333	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℝ)
34		1lt2 12539	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
35	34	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 2)
36	33, 35	ltned 11470	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≠ 2)
37	36	necomd 3014	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 1)
38	37	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 1)
39	18, 20, 25, 32, 38	relogbcld 43215	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈ ℝ)
40		5nn0 12650	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
41	40	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℕ0)
42	39, 41	reexpcld 14330	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑5) ∈ ℝ)
43		1red 11333	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ)
44	42, 43	readdcld 11362	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (((2 logb 𝑥)↑5) + 1) ∈ ℝ)
45	27, 43	readdcld 11362	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) ∈ ℝ)
46	27	ltp1d 12271	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (0 + 1))
47	41	nn0zd 12742	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℤ)
48		ax-resscn 11281	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
49	48, 18	sselid 3911	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℂ)
50	27, 20	gtned 11469	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 0)
51		logb1 27124	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) = 0)
52	49, 50, 38, 51	syl3anc 1399	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) = 0)
53		1lt4 12545	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
54	53	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 4)
55	43, 28, 25, 54, 31	ltletrd 11494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 𝑥)
56		2z 12752	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
57	56	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℤ)
58	57	uzidd 13005	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ (ℤ≥‘2))
59		1rp 13148	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ+
60	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ+)
61	25, 32	elrpd 13185	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ+)
62		logblt 27139	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 < 𝑥 ↔ (2 logb 1) < (2 logb 𝑥)))
63	58, 60, 61, 62	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (1 < 𝑥 ↔ (2 logb 1) < (2 logb 𝑥)))
64	55, 63	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) < (2 logb 𝑥))
65	52, 64	eqbrtrrd 5132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (2 logb 𝑥))
66		expgt0 14262	. . . . . . . . . . 11 ⊢ (((2 logb 𝑥) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑥)) → 0 < ((2 logb 𝑥)↑5))
67	39, 47, 65, 66	syl3anc 1399	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < ((2 logb 𝑥)↑5))
68	27, 42, 43, 67	ltadd1dd 11951	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) < (((2 logb 𝑥)↑5) + 1))
69	27, 45, 44, 46, 68	lttrd 11495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (((2 logb 𝑥)↑5) + 1))
70	18, 20, 44, 69, 38	relogbcld 43215	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ)
71	18, 70	remulcld 11363	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) ∈ ℝ)
72		0red 11335	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
73		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ (4[,]𝑁))
74	7, 8	jca 521	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 ∈ ℝ ∧ 𝑁 ∈ ℝ))
75	74	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (4 ∈ ℝ ∧ 𝑁 ∈ ℝ))
76	75, 21	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
77	73, 76	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
78	77	simp2d 1161	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
79	72, 28, 25, 30, 78	ltletrd 11494	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
80	18, 20, 25, 79, 38	relogbcld 43215	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈ ℝ)
81	80	resqcld 14292	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑2) ∈ ℝ)
82	71, 81	readdcld 11362	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈ ℝ)
83	82	fmpttd 7136	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ)
84	48	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
85		3lt4 12543	. . . . . . . . . . 11 ⊢ 3 < 4
86	85	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 4)
87	8, 33	readdcld 11362	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
88	8	ltp1d 12271	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
89	7, 8, 87, 12, 88	lelttrd 11492	. . . . . . . . . 10 ⊢ (𝜑 → 4 < (𝑁 + 1))
90	86, 89	jca 521	. . . . . . . . 9 ⊢ (𝜑 → (3 < 4 ∧ 4 < (𝑁 + 1)))
91	5	rexrd 11383	. . . . . . . . . 10 ⊢ (𝜑 → 3 ∈ ℝ*)
92	87	rexrd 11383	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ*)
93	7	rexrd 11383	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℝ*)
94		elioo5 13558	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 4 ∈ ℝ*) → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
95	91, 92, 93, 94	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
96	90, 95	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ (3(,)(𝑁 + 1)))
97	5, 7, 8, 86, 12	ltletrd 11494	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 𝑁)
98	97, 88	jca 521	. . . . . . . . 9 ⊢ (𝜑 → (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1)))
99	8	rexrd 11383	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ*)
100		elioo5 13558	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
101	91, 92, 99, 100	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
102	98, 101	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (3(,)(𝑁 + 1)))
103		iccssioo2 13574	. . . . . . . 8 ⊢ ((4 ∈ (3(,)(𝑁 + 1)) ∧ 𝑁 ∈ (3(,)(𝑁 + 1))) → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
104	96, 102, 103	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
105	104	resmptd 6043	. . . . . 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 12445	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℂ)
107	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ)
108	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 2)
109		elioore 13530	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 𝑥 ∈ ℝ)
110	109	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ)
111		0red 11335	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 ∈ ℝ)
112	4	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 ∈ ℝ)
113		3pos 12475	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 3
114	113	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 3)
115		eliooord 13560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → (3 < 𝑥 ∧ 𝑥 < (𝑁 + 1)))
116		simpl 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 < 𝑥 ∧ 𝑥 < (𝑁 + 1)) → 3 < 𝑥)
117	115, 116	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 3 < 𝑥)
118	117	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 < 𝑥)
119	111, 112, 110, 114, 118	lttrd 11495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 𝑥)
120	37	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
121	107, 108, 110, 119, 120	relogbcld 43215	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈ ℝ)
122	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℕ0)
123	121, 122	reexpcld 14330	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈ ℝ)
124		1red 11333	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℝ)
125	123, 124	readdcld 11362	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈ ℝ)
126	111, 124	readdcld 11362	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) ∈ ℝ)
127	111	ltp1d 12271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (0 + 1))
128	122	nn0zd 12742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℤ)
129	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 2)
130		2lt3 12540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 < 3
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 < 3)
132	124, 107, 112, 129, 131	lttrd 11495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 3)
133	124, 112, 110, 132, 118	lttrd 11495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 𝑥)
134	110, 119	elrpd 13185	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ+)
135		2rp 13149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ+
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ+)
137	134, 136, 129	jca32 525	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)))
138		logbgt0b 27148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝑥) ↔ 1 < 𝑥))
139	137, 138	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 < (2 logb 𝑥) ↔ 1 < 𝑥))
140	133, 139	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (2 logb 𝑥))
141	121, 128, 140, 66	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < ((2 logb 𝑥)↑5))
142	111, 123, 124, 141	ltadd1dd 11951	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) < (((2 logb 𝑥)↑5) + 1))
143	111, 126, 125, 127, 142	lttrd 11495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (((2 logb 𝑥)↑5) + 1))
144	124, 129	ltned 11470	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ≠ 2)
145	144	necomd 3014	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
146	107, 108, 125, 143, 145	relogbcld 43215	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ)
147	146	recnd 11361	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2 logb 𝑥)↑5) + 1)) ∈ ℂ)
148	106, 147	mulcld 11353	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) ∈ ℂ)
149	48, 121	sselid 3911	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈ ℂ)
150	149	sqcld 14311	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑2) ∈ ℂ)
151	148, 150	addcld 11352	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈ ℂ)
152	151	fmpttd 7136	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ)
153		ioossre 13562	. . . . . . . . . 10 ⊢ (3(,)(𝑁 + 1)) ⊆ ℝ
154	153	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (3(,)(𝑁 + 1)) ⊆ ℝ)
155	84, 152, 154	3jca 1146	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
156	136	relogcld 26978	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℝ)
157	125, 156	remulcld 11363	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) · (log‘2)) ∈ ℝ)
158	48, 123	sselid 3911	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈ ℂ)
159		1cnd 11326	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℂ)
160	158, 159	addcld 11352	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈ ℂ)
161	111, 108	gtned 11469	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 0)
162	106, 161	logcld 26925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℂ)
163	111, 143	gtned 11469	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ≠ 0)
164		loggt0b 26987	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
165	135, 164	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 < (log‘2) ↔ 1 < 2)
166	35, 165	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 < (log‘2))
167	26, 166	ltned 11470	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≠ (log‘2))
168	167	necomd 3014	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘2) ≠ 0)
169	168	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ≠ 0)
170	160, 162, 163, 169	mulne0d 11992	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) · (log‘2)) ≠ 0)
171	124, 157, 170	redivcld 12169	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) ∈ ℝ)
172		5re 12454	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℝ)
174		4nn0 12649	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℕ0
175	174	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℕ0)
176	121, 175	reexpcld 14330	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈ ℝ)
177	173, 176	remulcld 11363	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (5 · ((2 logb 𝑥)↑4)) ∈ ℝ)
178	110, 156	remulcld 11363	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ∈ ℝ)
179	48, 110	sselid 3911	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℂ)
180	111, 119	gtned 11469	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ≠ 0)
181	179, 162, 180, 169	mulne0d 11992	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ≠ 0)
182	124, 178, 181	redivcld 12169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / (𝑥 · (log‘2))) ∈ ℝ)
183	177, 182	remulcld 11363	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) ∈ ℝ)
184	183, 111	readdcld 11362	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0) ∈ ℝ)
185	171, 184	remulcld 11363	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈ ℝ)
186	107, 185	remulcld 11363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · ((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) ∈ ℝ)
187	156	resqcld 14292	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ∈ ℝ)
188	56	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℤ)
189	162, 169, 188	expne0d 14319	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ≠ 0)
190	107, 187, 189	redivcld 12169	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 / ((log‘2)↑2)) ∈ ℝ)
191	134	relogcld 26978	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘𝑥) ∈ ℝ)
192		2m1e1 12491	. . . . . . . . . . . . . . . . . 18 ⊢ (2 − 1) = 1
193		1nn0 12646	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
194	192, 193	eqeltri 2860	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) ∈ ℕ0
195	194	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 − 1) ∈ ℕ0)
196	191, 195	reexpcld 14330	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(2 − 1)) ∈ ℝ)
197	196, 110, 180	redivcld 12169	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ)
198	190, 197	remulcld 11363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ)
199	186, 198	readdcld 11362	. . . . . . . . . . . 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 3158	. . . . . . . . . . 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 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(3(,)(𝑁 + 1))
202	201	fnmptf 6694	. . . . . . . . . . 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 18	. . . . . . . . . 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 11906	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 3)
205	8	lep1d 12272	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
206	5, 8, 87, 13, 205	letrd 11491	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ (𝑁 + 1))
207	5, 87, 204, 206	aks4d1p1p6 43314	. . . . . . . . . . 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 6651	. . . . . . . . . 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 260	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)))
210	209	fndmd 6663	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (3(,)(𝑁 + 1)))
211		dvcn 26268	. . . . . . . 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 596	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
213		rescncf 25245	. . . . . . . 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 18	. . . . . . 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 16	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))
216	105, 215	eqeltrrd 2865	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ))
217		cncfcdm 25246	. . . . 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 596	. . . 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 260	. . 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 14330	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑4) ∈ ℝ)
222	221	fmpttd 7136	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ)
223	104	resmptd 6043	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)))
224	48, 176	sselid 3911	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈ ℂ)
225	224	fmpttd 7136	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ)
226	84, 225, 154	3jca 1146	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
227	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℝ)
228	156, 175	reexpcld 14330	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ∈ ℝ)
229		4z 12754	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℤ
230	229	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℤ)
231	162, 169, 230	expne0d 14319	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ≠ 0)
232	227, 228, 231	redivcld 12169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 / ((log‘2)↑4)) ∈ ℝ)
233		4m1e3 12495	. . . . . . . . . . . . . . . . 17 ⊢ (4 − 1) = 3
234		3nn0 12648	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℕ0
235	233, 234	eqeltri 2860	. . . . . . . . . . . . . . . 16 ⊢ (4 − 1) ∈ ℕ0
236	235	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 − 1) ∈ ℕ0)
237	191, 236	reexpcld 14330	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(4 − 1)) ∈ ℝ)
238	237, 110, 180	redivcld 12169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(4 − 1)) / 𝑥) ∈ ℝ)
239	232, 238	remulcld 11363	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
240	239	ralrimiva 3158	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
241	201	fnmptf 6694	. . . . . . . . . . 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 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1)))
243	113	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 3)
244		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))
245		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)))
246		eqid 2763	. . . . . . . . . . . 12 ⊢ (4 / ((log‘2)↑4)) = (4 / ((log‘2)↑4))
247		4nn 12450	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
248	247	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 4 ∈ ℕ)
249	5, 87, 243, 206, 244, 245, 246, 248	dvrelogpow2b 43309	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
250	249	fneq1d 6651	. . . . . . . . . 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 260	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) Fn (3(,)(𝑁 + 1)))
252	251	fndmd 6663	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (3(,)(𝑁 + 1)))
253		dvcn 26268	. . . . . . . 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 596	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
255		rescncf 25245	. . . . . . . 8 ⊢ ((4[,]𝑁) ⊆ (3(,)(𝑁 + 1)) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
256	104, 255	syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
257	254, 256	mpd 16	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))
258	223, 257	eqeltrrd 2865	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ))
259		cncfcdm 25246	. . . . 5 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
260	84, 258, 259	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
261	222, 260	mpbird 260	. . 3 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ))
262	7, 8, 11, 12	aks4d1p1p6 43314	. . 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 2763	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))
265		eqid 2763	. . . . 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 43309	. . . 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 7456	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((log‘𝑥)↑(4 − 1)) = ((log‘𝑥)↑3))
269	268	oveq1d 7455	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (((log‘𝑥)↑(4 − 1)) / 𝑥) = (((log‘𝑥)↑3) / 𝑥))
270	269	oveq2d 7456	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) = ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥)))
271	270	mpteq2dva 5201	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
272	266, 271	eqtrd 2798	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
273		elioore 13530	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) → 𝑥 ∈ ℝ)
274	273	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 𝑥 ∈ ℝ)
275	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ∈ ℝ)
276		eliooord 13560	. . . . . . 7 ⊢ (𝑥 ∈ (4(,)𝑁) → (4 < 𝑥 ∧ 𝑥 < 𝑁))
277	276	simpld 500	. . . . . 6 ⊢ (𝑥 ∈ (4(,)𝑁) → 4 < 𝑥)
278	277	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 < 𝑥)
279	275, 274, 278	ltled 11482	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ≤ 𝑥)
280	274, 279	aks4d1p1p7 43315	. . 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 7448	. . . . . . . 8 ⊢ (𝑥 = 4 → (2 logb 𝑥) = (2 logb 4))
282	281	oveq1d 7455	. . . . . . 7 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑5) = ((2 logb 4)↑5))
283	282	oveq1d 7455	. . . . . 6 ⊢ (𝑥 = 4 → (((2 logb 𝑥)↑5) + 1) = (((2 logb 4)↑5) + 1))
284	283	oveq2d 7456	. . . . 5 ⊢ (𝑥 = 4 → (2 logb (((2 logb 𝑥)↑5) + 1)) = (2 logb (((2 logb 4)↑5) + 1)))
285	284	oveq2d 7456	. . . 4 ⊢ (𝑥 = 4 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · (2 logb (((2 logb 4)↑5) + 1))))
286	281	oveq1d 7455	. . . 4 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑2) = ((2 logb 4)↑2))
287	285, 286	oveq12d 7458	. . 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 7455	. . 3 ⊢ (𝑥 = 4 → ((2 logb 𝑥)↑4) = ((2 logb 4)↑4))
289		oveq2 7448	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (2 logb 𝑥) = (2 logb 𝑁))
290	289	oveq1d 7455	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑5) = ((2 logb 𝑁)↑5))
291	290	oveq1d 7455	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((2 logb 𝑥)↑5) + 1) = (((2 logb 𝑁)↑5) + 1))
292	291	oveq2d 7456	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 logb (((2 logb 𝑥)↑5) + 1)) = (2 logb (((2 logb 𝑁)↑5) + 1)))
293	292	oveq2d 7456	. . . . 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 7456	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝐶) = (2 · (2 logb (((2 logb 𝑁)↑5) + 1))))
296	295	eqcomd 2769	. . . . 5 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑁)↑5) + 1))) = (2 · 𝐶))
297	293, 296	eqtrd 2798	. . . 4 ⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2 logb 𝑥)↑5) + 1))) = (2 · 𝐶))
298	289	oveq1d 7455	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = ((2 logb 𝑁)↑2))
299	15	a1i 11	. . . . . 6 ⊢ (𝑥 = 𝑁 → 𝐷 = ((2 logb 𝑁)↑2))
300	299	eqcomd 2769	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑2) = 𝐷)
301	298, 300	eqtrd 2798	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = 𝐷)
302	297, 301	oveq12d 7458	. . 3 ⊢ (𝑥 = 𝑁 → ((2 · (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) = ((2 · 𝐶) + 𝐷))
303	289	oveq1d 7455	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = ((2 logb 𝑁)↑4))
304	16	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑁 → 𝐸 = ((2 logb 𝑁)↑4))
305	304	eqcomd 2769	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑4) = 𝐸)
306	303, 305	eqtrd 2798	. . 3 ⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = 𝐸)
307		sq2 14364	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
308	307	oveq2i 7451	. . . . . . . . . . . . . . 15 ⊢ (2 logb (2↑2)) = (2 logb 4)
309	308	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
310	309	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 logb 4) = (2 logb (2↑2)))
311	135	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ+)
312	56	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
313		relogbexp 27135	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ+ ∧ 2 ≠ 1 ∧ 2 ∈ ℤ) → (2 logb (2↑2)) = 2)
314	311, 37, 312, 313	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
315	310, 314	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 logb 4) = 2)
316	315	oveq1d 7455	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 logb 4)↑5) = (2↑5))
317	316	oveq1d 7455	. . . . . . . . . 10 ⊢ (𝜑 → (((2 logb 4)↑5) + 1) = ((2↑5) + 1))
318	317	oveq2d 7456	. . . . . . . . 9 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) = (2 logb ((2↑5) + 1)))
319	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℝ)
320	319	leidd 11906	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 2)
321	315, 319	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 logb 4) ∈ ℝ)
322	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℕ0)
323	321, 322	reexpcld 14330	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 logb 4)↑5) ∈ ℝ)
324	316, 323	eqeltrrd 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) ∈ ℝ)
325	324, 33	readdcld 11362	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ∈ ℝ)
326	322	nn0zd 12742	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 5 ∈ ℤ)
327	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
328	327, 315	breqtrrd 5136	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < (2 logb 4))
329	321, 326, 328	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 logb 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 4)))
330		expgt0 14262	. . . . . . . . . . . . . 14 ⊢ (((2 logb 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 4)) → 0 < ((2 logb 4)↑5))
331	329, 330	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((2 logb 4)↑5))
332	331, 316	breqtrd 5134	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (2↑5))
333	324	ltp1d 12271	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) < ((2↑5) + 1))
334	26, 324, 325, 332, 333	lttrd 11495	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((2↑5) + 1))
335		6nn0 12651	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
336	335	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℕ0)
337	319, 336	reexpcld 14330	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑6) ∈ ℝ)
338	336	nn0zd 12742	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℤ)
339		expgt0 14262	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 6 ∈ ℤ ∧ 0 < 2) → 0 < (2↑6))
340	319, 338, 327, 339	syl3anc 1399	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (2↑6))
341	324, 324	readdcld 11362	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ∈ ℝ)
342	33, 319, 35	ltled 11482	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≤ 2)
343	319, 322, 342	expge1d 14332	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≤ (2↑5))
344	33, 324, 324, 343	leadd2dd 11955	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + 1) ≤ ((2↑5) + (2↑5)))
345	341	leidd 11906	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ ((2↑5) + (2↑5)))
346		df-6 12433	. . . . . . . . . . . . . . . . . . 19 ⊢ 6 = (5 + 1)
347	346	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 6 = (5 + 1))
348	347	oveq2d 7456	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑6) = (2↑(5 + 1)))
349		2cn 12442	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℂ)
351	193	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℕ0)
352	350, 351, 322	expaddd 14315	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑(5 + 1)) = ((2↑5) · (2↑1)))
353	348, 352	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑6) = ((2↑5) · (2↑1)))
354	350	exp1d 14308	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑1) = 2)
355	354	oveq2d 7456	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑5) · (2↑1)) = ((2↑5) · 2))
356	353, 355	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑6) = ((2↑5) · 2))
357	48, 324	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑5) ∈ ℂ)
358	357	times2d 12614	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2↑5) · 2) = ((2↑5) + (2↑5)))
359	356, 358	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2↑6) = ((2↑5) + (2↑5)))
360	359	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) = (2↑6))
361	345, 360	breqtrd 5134	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ (2↑6))
362	325, 341, 337, 344, 361	letrd 11491	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ≤ (2↑6))
363	312, 320, 325, 334, 337, 340, 362	logblebd 43218	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb ((2↑5) + 1)) ≤ (2 logb (2↑6)))
364	311, 37, 338	relogbexpd 43216	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb (2↑6)) = 6)
365	363, 364	breqtrd 5134	. . . . . . . . 9 ⊢ (𝜑 → (2 logb ((2↑5) + 1)) ≤ 6)
366	318, 365	eqbrtrd 5130	. . . . . . . 8 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ≤ 6)
367		6t2e12 12947	. . . . . . . . 9 ⊢ (6 · 2) = ;12
368		6cn 12458	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
369	368	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
370		2nn 12440	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
371	193, 370	decnncl 12862	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ
372	371	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;12 ∈ ℕ)
373	372	nnred 12374	. . . . . . . . . . 11 ⊢ (𝜑 → ;12 ∈ ℝ)
374	373	recnd 11361	. . . . . . . . . 10 ⊢ (𝜑 → ;12 ∈ ℂ)
375	26, 327	gtned 11469	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≠ 0)
376	369, 350, 374, 375	ldiv 12175	. . . . . . . . 9 ⊢ (𝜑 → ((6 · 2) = ;12 ↔ 6 = (;12 / 2)))
377	367, 376	mpbii 236	. . . . . . . 8 ⊢ (𝜑 → 6 = (;12 / 2))
378	366, 377	breqtrd 5134	. . . . . . 7 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ≤ (;12 / 2))
379	323, 33	readdcld 11362	. . . . . . . . 9 ⊢ (𝜑 → (((2 logb 4)↑5) + 1) ∈ ℝ)
380	26, 33	readdcld 11362	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
381	26	ltp1d 12271	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (0 + 1))
382	26, 323, 33, 331	ltadd1dd 11951	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) < (((2 logb 4)↑5) + 1))
383	26, 380, 379, 381, 382	lttrd 11495	. . . . . . . . 9 ⊢ (𝜑 → 0 < (((2 logb 4)↑5) + 1))
384	319, 327, 379, 383, 37	relogbcld 43215	. . . . . . . 8 ⊢ (𝜑 → (2 logb (((2 logb 4)↑5) + 1)) ∈ ℝ)
385	384, 373, 311	lemuldiv2d 13238	. . . . . . 7 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ ;12 ↔ (2 logb (((2 logb 4)↑5) + 1)) ≤ (;12 / 2)))
386	378, 385	mpbird 260	. . . . . 6 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ ;12)
387	315	oveq1d 7455	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 4)↑2) = (2↑2))
388	387, 307	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝜑 → ((2 logb 4)↑2) = 4)
389	388	oveq2d 7456	. . . . . . . 8 ⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = (;16 − 4))
390		2nn0 12647	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
391		eqid 2763	. . . . . . . . . 10 ⊢ ;12 = ;12
392		4cn 12452	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
393		4p2e6 12519	. . . . . . . . . . 11 ⊢ (4 + 2) = 6
394	392, 349, 393	addcomli 11526	. . . . . . . . . 10 ⊢ (2 + 4) = 6
395	193, 390, 174, 391, 394	decaddi 12903	. . . . . . . . 9 ⊢ (;12 + 4) = ;16
396	392	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℂ)
397		6nn 12456	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
398	193, 397	decnncl 12862	. . . . . . . . . . . . 13 ⊢ ;16 ∈ ℕ
399	398	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;16 ∈ ℕ)
400	399	nnred 12374	. . . . . . . . . . 11 ⊢ (𝜑 → ;16 ∈ ℝ)
401	48, 400	sselid 3911	. . . . . . . . . 10 ⊢ (𝜑 → ;16 ∈ ℂ)
402	374, 396, 401	addlsub 11756	. . . . . . . . 9 ⊢ (𝜑 → ((;12 + 4) = ;16 ↔ ;12 = (;16 − 4)))
403	395, 402	mpbii 236	. . . . . . . 8 ⊢ (𝜑 → ;12 = (;16 − 4))
404	389, 403	eqtr4d 2801	. . . . . . 7 ⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = ;12)
405	404	eqcomd 2769	. . . . . 6 ⊢ (𝜑 → ;12 = (;16 − ((2 logb 4)↑2)))
406	386, 405	breqtrd 5134	. . . . 5 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb 4)↑2)))
407	319, 384	remulcld 11363	. . . . . 6 ⊢ (𝜑 → (2 · (2 logb (((2 logb 4)↑5) + 1))) ∈ ℝ)
408	321	resqcld 14292	. . . . . 6 ⊢ (𝜑 → ((2 logb 4)↑2) ∈ ℝ)
409		leaddsub 11816	. . . . . 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 1399	. . . . 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 260	. . . 4 ⊢ (𝜑 → ((2 · (2 logb (((2 logb 4)↑5) + 1))) + ((2 logb 4)↑2)) ≤ ;16)
412	315	oveq1d 7455	. . . . . 6 ⊢ (𝜑 → ((2 logb 4)↑4) = (2↑4))
413		2exp4 17288	. . . . . 6 ⊢ (2↑4) = ;16
414	412, 413	eqtrdi 2814	. . . . 5 ⊢ (𝜑 → ((2 logb 4)↑4) = ;16)
415	414	eqcomd 2769	. . . 4 ⊢ (𝜑 → ;16 = ((2 logb 4)↑4))
416	411, 415	breqtrd 5134	. . 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 43313	. 2 ⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸)
418	1, 2, 3, 13, 14, 15, 16, 417	aks4d1p1p4 43312	1 ⊢ (𝜑 → 𝐴 < (2↑𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080   ⊆ wss 3900   class class class wbr 5106   ↦ cmpt 5189  dom cdm 5655   ↾ cres 5657   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440  ℂcc 11222  ℝcr 11223  0cc0 11224  1c1 11225   + caddc 11227   · cmul 11229  ℝ^*cxr 11366   < clt 11367   ≤ cle 11368   − cmin 11565   / cdiv 11997  ℕcn 12359  2c2 12421  3c3 12422  4c4 12423  5c5 12424  6c6 12425  ℕ₀cn0 12630  ℤcz 12717  ;cdc 12838  ℤ_≥cuz 12989  ℝ⁺crp 13144  (,)cioo 13500  [,]cicc 13503  ...cfz 13663  ⌊cfl 13954  ⌈cceil 13955  ↑cexp 14228  ∏cprod 16098  –cn→ccncf 25224   D cdv 26210  logclog 26909   log_b clogb 27119

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-inf2 9666  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301  ax-pre-sup 11302  ax-addf 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-isom 6564  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-of 7714  df-om 7899  df-1st 8022  df-2nd 8023  df-supp 8202  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-er 8742  df-map 8874  df-pm 8875  df-ixp 8951  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-fsupp 9379  df-fi 9427  df-sup 9458  df-inf 9459  df-oi 9528  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-div 11998  df-nn 12360  df-2 12429  df-3 12430  df-4 12431  df-5 12432  df-6 12433  df-7 12434  df-8 12435  df-9 12436  df-n0 12631  df-z 12718  df-dec 12839  df-uz 12990  df-q 13100  df-rp 13145  df-xneg 13265  df-xadd 13266  df-xmul 13267  df-ioo 13504  df-ioc 13505  df-ico 13506  df-icc 13507  df-fz 13664  df-fzo 13813  df-fl 13956  df-ceil 13957  df-mod 14034  df-seq 14169  df-exp 14229  df-fac 14442  df-bc 14471  df-hash 14499  df-shft 15246  df-cj 15292  df-re 15293  df-im 15294  df-sqrt 15428  df-abs 15429  df-limsup 15664  df-clim 15681  df-rlim 15682  df-sum 15880  df-prod 16099  df-ef 16259  df-e 16260  df-sin 16261  df-cos 16262  df-pi 16264  df-struct 17351  df-sets 17368  df-slot 17386  df-ndx 17398  df-base 17414  df-ress 17435  df-plusg 17467  df-mulr 17468  df-starv 17469  df-sca 17470  df-vsca 17471  df-ip 17472  df-tset 17473  df-ple 17474  df-ds 17476  df-unif 17477  df-hom 17478  df-cco 17479  df-rest 17619  df-topn 17620  df-0g 17638  df-gsum 17639  df-topgen 17640  df-pt 17641  df-prds 17644  df-xrs 17700  df-qtop 17705  df-imas 17706  df-xps 17708  df-mre 17782  df-mrc 17783  df-acs 17785  df-mgm 18842  df-sgrp 18934  df-mnd 18950  df-submnd 19005  df-mulg 19304  df-cntz 19558  df-cmn 20023  df-psmet 21697  df-xmet 21698  df-met 21699  df-bl 21700  df-mopn 21701  df-fbas 21702  df-fg 21703  df-cnfld 21706  df-top 23239  df-topon 23256  df-topsp 23278  df-bases 23291  df-cld 23364  df-ntr 23365  df-cls 23366  df-nei 23443  df-lp 23481  df-perf 23482  df-cn 23572  df-cnp 23573  df-haus 23660  df-cmp 23732  df-tx 23908  df-hmeo 24101  df-fil 24192  df-fm 24284  df-flim 24285  df-flf 24286  df-xms 24666  df-ms 24667  df-tms 24668  df-cncf 25226  df-limc 26213  df-dv 26214  df-log 26911  df-cxp 26912  df-logb 27120

This theorem is used by:  aks4d1p1  43317