aks4d1p1p5 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aks4d1p1p5		Structured version Visualization version GIF version

Theorem aks4d1p1p5 42502

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

**Hypotheses**
Ref	Expression
aks4d1p1p5.1	⊢ (𝜑 → 𝑁 ∈ ℕ)
aks4d1p1p5.2	⊢ 𝐴 = ((𝑁↑(⌊‘(2 log_b 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 log_b 𝑁)↑2)))((𝑁↑𝑘) − 1))
aks4d1p1p5.3	⊢ 𝐵 = (⌈‘((2 log_b 𝑁)↑5))
aks4d1p1p5.4	⊢ (𝜑 → 4 ≤ 𝑁)
aks4d1p1p5.5	⊢ 𝐶 = (2 log_b (((2 log_b 𝑁)↑5) + 1))
aks4d1p1p5.6	⊢ 𝐷 = ((2 log_b 𝑁)↑2)
aks4d1p1p5.7	⊢ 𝐸 = ((2 log_b 𝑁)↑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 log_b 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 log_b 𝑁)↑2)))((𝑁↑𝑘) − 1))
3		aks4d1p1p5.3	. 2 ⊢ 𝐵 = (⌈‘((2 log_b 𝑁)↑5))
4		3re 12250	. . . 4 ⊢ 3 ∈ ℝ
5	4	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
6		4re 12254	. . . 4 ⊢ 4 ∈ ℝ
7	6	a1i 11	. . 3 ⊢ (𝜑 → 4 ∈ ℝ)
8	1	nnred 12178	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
9	5	lep1d 12076	. . . 4 ⊢ (𝜑 → 3 ≤ (3 + 1))
10		3p1e4 12310	. . . 4 ⊢ (3 + 1) = 4
11	9, 10	breqtrdi 5115	. . 3 ⊢ (𝜑 → 3 ≤ 4)
12		aks4d1p1p5.4	. . 3 ⊢ (𝜑 → 4 ≤ 𝑁)
13	5, 7, 8, 11, 12	letrd 11292	. 2 ⊢ (𝜑 → 3 ≤ 𝑁)
14		aks4d1p1p5.5	. 2 ⊢ 𝐶 = (2 log_b (((2 log_b 𝑁)↑5) + 1))
15		aks4d1p1p5.6	. 2 ⊢ 𝐷 = ((2 log_b 𝑁)↑2)
16		aks4d1p1p5.7	. 2 ⊢ 𝐸 = ((2 log_b 𝑁)↑4)
17		2re 12244	. . . . . . . 8 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℝ)
19		2pos 12273	. . . . . . . . 9 ⊢ 0 < 2
20	19	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 2)
21		elicc2 13353	. . . . . . . . . . . . . . 15 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
22	7, 8, 21	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
23	22	biimpd 229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)))
24	23	imp 406	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))
25	24	simp1d 1143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ)
26		0red 11136	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
27	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
28	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℝ)
29		4pos 12277	. . . . . . . . . . . . 13 ⊢ 0 < 4
30	29	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 4)
31	24	simp2d 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
32	27, 28, 25, 30, 31	ltletrd 11295	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
33		1red 11134	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℝ)
34		1lt2 12336	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
35	34	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 2)
36	33, 35	ltned 11271	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≠ 2)
37	36	necomd 2985	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 1)
38	37	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 1)
39	18, 20, 25, 32, 38	relogbcld 42401	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b 𝑥) ∈ ℝ)
40		5nn0 12446	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ₀
41	40	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℕ₀)
42	39, 41	reexpcld 14114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 log_b 𝑥)↑5) ∈ ℝ)
43		1red 11134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ)
44	42, 43	readdcld 11163	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (((2 log_b 𝑥)↑5) + 1) ∈ ℝ)
45	27, 43	readdcld 11163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) ∈ ℝ)
46	27	ltp1d 12075	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (0 + 1))
47	41	nn0zd 12538	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℤ)
48		ax-resscn 11084	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
49	48, 18	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℂ)
50	27, 20	gtned 11270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 0)
51		logb1 26721	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 log_b 1) = 0)
52	49, 50, 38, 51	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b 1) = 0)
53		1lt4 12341	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
54	53	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 4)
55	43, 28, 25, 54, 31	ltletrd 11295	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 𝑥)
56		2z 12548	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
57	56	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℤ)
58	57	uzidd 12793	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ (ℤ_≥‘2))
59		1rp 12935	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ⁺
60	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ⁺)
61	25, 32	elrpd 12972	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ⁺)
62		logblt 26736	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 1 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (1 < 𝑥 ↔ (2 log_b 1) < (2 log_b 𝑥)))
63	58, 60, 61, 62	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (1 < 𝑥 ↔ (2 log_b 1) < (2 log_b 𝑥)))
64	55, 63	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b 1) < (2 log_b 𝑥))
65	52, 64	eqbrtrrd 5098	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (2 log_b 𝑥))
66		expgt0 14046	. . . . . . . . . . 11 ⊢ (((2 log_b 𝑥) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 log_b 𝑥)) → 0 < ((2 log_b 𝑥)↑5))
67	39, 47, 65, 66	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < ((2 log_b 𝑥)↑5))
68	27, 42, 43, 67	ltadd1dd 11750	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) < (((2 log_b 𝑥)↑5) + 1))
69	27, 45, 44, 46, 68	lttrd 11296	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (((2 log_b 𝑥)↑5) + 1))
70	18, 20, 44, 69, 38	relogbcld 42401	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℝ)
71	18, 70	remulcld 11164	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) ∈ ℝ)
72		0red 11136	. . . . . . . . 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 1144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥)
79	72, 28, 25, 30, 78	ltletrd 11295	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥)
80	18, 20, 25, 79, 38	relogbcld 42401	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b 𝑥) ∈ ℝ)
81	80	resqcld 14076	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 log_b 𝑥)↑2) ∈ ℝ)
82	71, 81	readdcld 11163	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)) ∈ ℝ)
83	82	fmpttd 7056	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(4[,]𝑁)⟶ℝ)
84	48	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
85		3lt4 12339	. . . . . . . . . . 11 ⊢ 3 < 4
86	85	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 4)
87	8, 33	readdcld 11163	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
88	8	ltp1d 12075	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
89	7, 8, 87, 12, 88	lelttrd 11293	. . . . . . . . . 10 ⊢ (𝜑 → 4 < (𝑁 + 1))
90	86, 89	jca 511	. . . . . . . . 9 ⊢ (𝜑 → (3 < 4 ∧ 4 < (𝑁 + 1)))
91	5	rexrd 11184	. . . . . . . . . 10 ⊢ (𝜑 → 3 ∈ ℝ^*)
92	87	rexrd 11184	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ^*)
93	7	rexrd 11184	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℝ^*)
94		elioo5 13345	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ^* ∧ (𝑁 + 1) ∈ ℝ^* ∧ 4 ∈ ℝ^*) → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
95	91, 92, 93, 94	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1))))
96	90, 95	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 4 ∈ (3(,)(𝑁 + 1)))
97	5, 7, 8, 86, 12	ltletrd 11295	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 𝑁)
98	97, 88	jca 511	. . . . . . . . 9 ⊢ (𝜑 → (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1)))
99	8	rexrd 11184	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
100		elioo5 13345	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ^* ∧ (𝑁 + 1) ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
101	91, 92, 99, 100	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))))
102	98, 101	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (3(,)(𝑁 + 1)))
103		iccssioo2 13361	. . . . . . . 8 ⊢ ((4 ∈ (3(,)(𝑁 + 1)) ∧ 𝑁 ∈ (3(,)(𝑁 + 1))) → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
104	96, 102, 103	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
105	104	resmptd 5994	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))))
106		2cnd 12248	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℂ)
107	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ)
108	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 2)
109		elioore 13317	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 𝑥 ∈ ℝ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ)
111		0red 11136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 ∈ ℝ)
112	4	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 ∈ ℝ)
113		3pos 12275	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 3
114	113	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 3)
115		eliooord 13347	. . . . . . . . . . . . . . . . . . . 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 11296	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 𝑥)
120	37	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
121	107, 108, 110, 119, 120	relogbcld 42401	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 log_b 𝑥) ∈ ℝ)
122	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℕ₀)
123	121, 122	reexpcld 14114	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑5) ∈ ℝ)
124		1red 11134	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℝ)
125	123, 124	readdcld 11163	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 log_b 𝑥)↑5) + 1) ∈ ℝ)
126	111, 124	readdcld 11163	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) ∈ ℝ)
127	111	ltp1d 12075	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (0 + 1))
128	122	nn0zd 12538	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℤ)
129	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 2)
130		2lt3 12337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 < 3
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 < 3)
132	124, 107, 112, 129, 131	lttrd 11296	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 3)
133	124, 112, 110, 132, 118	lttrd 11296	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 𝑥)
134	110, 119	elrpd 12972	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ⁺)
135		2rp 12936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ⁺
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ⁺)
137	134, 136, 129	jca32 515	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 ∈ ℝ⁺ ∧ (2 ∈ ℝ⁺ ∧ 1 < 2)))
138		logbgt0b 26745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ⁺ ∧ (2 ∈ ℝ⁺ ∧ 1 < 2)) → (0 < (2 log_b 𝑥) ↔ 1 < 𝑥))
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 < (2 log_b 𝑥) ↔ 1 < 𝑥))
140	133, 139	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (2 log_b 𝑥))
141	121, 128, 140, 66	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < ((2 log_b 𝑥)↑5))
142	111, 123, 124, 141	ltadd1dd 11750	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) < (((2 log_b 𝑥)↑5) + 1))
143	111, 126, 125, 127, 142	lttrd 11296	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (((2 log_b 𝑥)↑5) + 1))
144	124, 129	ltned 11271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ≠ 2)
145	144	necomd 2985	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
146	107, 108, 125, 143, 145	relogbcld 42401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℝ)
147	146	recnd 11162	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℂ)
148	106, 147	mulcld 11154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) ∈ ℂ)
149	48, 121	sselid 3915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 log_b 𝑥) ∈ ℂ)
150	149	sqcld 14095	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑2) ∈ ℂ)
151	148, 150	addcld 11153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)) ∈ ℂ)
152	151	fmpttd 7056	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ)
153		ioossre 13349	. . . . . . . . . 10 ⊢ (3(,)(𝑁 + 1)) ⊆ ℝ
154	153	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (3(,)(𝑁 + 1)) ⊆ ℝ)
155	84, 152, 154	3jca 1129	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
156	136	relogcld 26575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℝ)
157	125, 156	remulcld 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 log_b 𝑥)↑5) + 1) · (log‘2)) ∈ ℝ)
158	48, 123	sselid 3915	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑5) ∈ ℂ)
159		1cnd 11128	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈ ℂ)
160	158, 159	addcld 11153	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 log_b 𝑥)↑5) + 1) ∈ ℂ)
161	111, 108	gtned 11270	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 0)
162	106, 161	logcld 26522	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℂ)
163	111, 143	gtned 11270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 log_b 𝑥)↑5) + 1) ≠ 0)
164		loggt0b 26584	. . . . . . . . . . . . . . . . . . . . . 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 11271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ≠ (log‘2))
168	167	necomd 2985	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘2) ≠ 0)
169	168	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ≠ 0)
170	160, 162, 163, 169	mulne0d 11791	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 log_b 𝑥)↑5) + 1) · (log‘2)) ≠ 0)
171	124, 157, 170	redivcld 11972	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) ∈ ℝ)
172		5re 12257	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℝ)
174		4nn0 12445	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℕ₀
175	174	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℕ₀)
176	121, 175	reexpcld 14114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑4) ∈ ℝ)
177	173, 176	remulcld 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (5 · ((2 log_b 𝑥)↑4)) ∈ ℝ)
178	110, 156	remulcld 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ∈ ℝ)
179	48, 110	sselid 3915	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℂ)
180	111, 119	gtned 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ≠ 0)
181	179, 162, 180, 169	mulne0d 11791	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ≠ 0)
182	124, 178, 181	redivcld 11972	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / (𝑥 · (log‘2))) ∈ ℝ)
183	177, 182	remulcld 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) ∈ ℝ)
184	183, 111	readdcld 11163	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0) ∈ ℝ)
185	171, 184	remulcld 11164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈ ℝ)
186	107, 185	remulcld 11164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) ∈ ℝ)
187	156	resqcld 14076	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ∈ ℝ)
188	56	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℤ)
189	162, 169, 188	expne0d 14103	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ≠ 0)
190	107, 187, 189	redivcld 11972	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 / ((log‘2)↑2)) ∈ ℝ)
191	134	relogcld 26575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘𝑥) ∈ ℝ)
192		2m1e1 12291	. . . . . . . . . . . . . . . . . 18 ⊢ (2 − 1) = 1
193		1nn0 12442	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ₀
194	192, 193	eqeltri 2831	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) ∈ ℕ₀
195	194	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 − 1) ∈ ℕ₀)
196	191, 195	reexpcld 14114	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(2 − 1)) ∈ ℝ)
197	196, 110, 180	redivcld 11972	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ)
198	190, 197	remulcld 11164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ)
199	186, 198	readdcld 11163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ)
200	199	ralrimiva 3127	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ)
201		nfcv 2897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(3(,)(𝑁 + 1))
202	201	fnmptf 6623	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ (3(,)(𝑁 + 1))((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑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 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1)))
204	5	leidd 11705	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 3)
205	8	lep1d 12076	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
206	5, 8, 87, 13, 205	letrd 11292	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ (𝑁 + 1))
207	5, 87, 204, 206	aks4d1p1p6 42500	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))))
208	207	fneq1d 6580	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)) ↔ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑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 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)))
210	209	fndmd 6592	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (3(,)(𝑁 + 1)))
211		dvcn 25876	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ) ∧ dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (3(,)(𝑁 + 1))) → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
212	155, 210, 211	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
213		rescncf 24852	. . . . . . . 8 ⊢ ((4[,]𝑁) ⊆ (3(,)(𝑁 + 1)) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
214	104, 213	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
215	212, 214	mpd 15	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))
216	105, 215	eqeltrrd 2836	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ))
217		cncfcdm 24853	. . . . 5 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(4[,]𝑁)⟶ℝ))
218	84, 216, 217	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(4[,]𝑁)⟶ℝ))
219	83, 218	mpbird 257	. . 3 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ))
220	174	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℕ₀)
221	39, 220	reexpcld 14114	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 log_b 𝑥)↑4) ∈ ℝ)
222	221	fmpttd 7056	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)):(4[,]𝑁)⟶ℝ)
223	104	resmptd 5994	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)))
224	48, 176	sselid 3915	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑4) ∈ ℂ)
225	224	fmpttd 7056	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ)
226	84, 225, 154	3jca 1129	. . . . . . . 8 ⊢ (𝜑 → (ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ))
227	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℝ)
228	156, 175	reexpcld 14114	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ∈ ℝ)
229		4z 12550	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℤ
230	229	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℤ)
231	162, 169, 230	expne0d 14103	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ≠ 0)
232	227, 228, 231	redivcld 11972	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 / ((log‘2)↑4)) ∈ ℝ)
233		4m1e3 12294	. . . . . . . . . . . . . . . . 17 ⊢ (4 − 1) = 3
234		3nn0 12444	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℕ₀
235	233, 234	eqeltri 2831	. . . . . . . . . . . . . . . 16 ⊢ (4 − 1) ∈ ℕ₀
236	235	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 − 1) ∈ ℕ₀)
237	191, 236	reexpcld 14114	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(4 − 1)) ∈ ℝ)
238	237, 110, 180	redivcld 11972	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(4 − 1)) / 𝑥) ∈ ℝ)
239	232, 238	remulcld 11164	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
240	239	ralrimiva 3127	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ)
241	201	fnmptf 6623	. . . . . . . . . . 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 2735	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4))
245		eqid 2735	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)))
246		eqid 2735	. . . . . . . . . . . 12 ⊢ (4 / ((log‘2)↑4)) = (4 / ((log‘2)↑4))
247		4nn 12253	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
248	247	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 4 ∈ ℕ)
249	5, 87, 243, 206, 244, 245, 246, 248	dvrelogpow2b 42495	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
250	249	fneq1d 6580	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑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 log_b 𝑥)↑4))) Fn (3(,)(𝑁 + 1)))
252	251	fndmd 6592	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4))) = (3(,)(𝑁 + 1)))
253		dvcn 25876	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆ ℝ) ∧ dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4))) = (3(,)(𝑁 + 1))) → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
254	226, 252, 253	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ))
255		rescncf 24852	. . . . . . . 8 ⊢ ((4[,]𝑁) ⊆ (3(,)(𝑁 + 1)) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
256	104, 255	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)))
257	254, 256	mpd 15	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))
258	223, 257	eqeltrrd 2836	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ))
259		cncfcdm 24853	. . . . 5 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
260	84, 258, 259	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)):(4[,]𝑁)⟶ℝ))
261	222, 260	mpbird 257	. . 3 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ))
262	7, 8, 11, 12	aks4d1p1p6 42500	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))))
263	29	a1i 11	. . . . 5 ⊢ (𝜑 → 0 < 4)
264		eqid 2735	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((2 log_b 𝑥)↑4)) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 log_b 𝑥)↑4))
265		eqid 2735	. . . . 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 42495	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 log_b 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
267	233	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (4 − 1) = 3)
268	267	oveq2d 7372	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((log‘𝑥)↑(4 − 1)) = ((log‘𝑥)↑3))
269	268	oveq1d 7371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (((log‘𝑥)↑(4 − 1)) / 𝑥) = (((log‘𝑥)↑3) / 𝑥))
270	269	oveq2d 7372	. . . . 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 2770	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 log_b 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥))))
273		elioore 13317	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) → 𝑥 ∈ ℝ)
274	273	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 𝑥 ∈ ℝ)
275	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ∈ ℝ)
276		eliooord 13347	. . . . . . 7 ⊢ (𝑥 ∈ (4(,)𝑁) → (4 < 𝑥 ∧ 𝑥 < 𝑁))
277	276	simpld 494	. . . . . 6 ⊢ (𝑥 ∈ (4(,)𝑁) → 4 < 𝑥)
278	277	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 < 𝑥)
279	275, 274, 278	ltled 11283	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ≤ 𝑥)
280	274, 279	aks4d1p1p7 42501	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥)))
281		oveq2 7364	. . . . . . . 8 ⊢ (𝑥 = 4 → (2 log_b 𝑥) = (2 log_b 4))
282	281	oveq1d 7371	. . . . . . 7 ⊢ (𝑥 = 4 → ((2 log_b 𝑥)↑5) = ((2 log_b 4)↑5))
283	282	oveq1d 7371	. . . . . 6 ⊢ (𝑥 = 4 → (((2 log_b 𝑥)↑5) + 1) = (((2 log_b 4)↑5) + 1))
284	283	oveq2d 7372	. . . . 5 ⊢ (𝑥 = 4 → (2 log_b (((2 log_b 𝑥)↑5) + 1)) = (2 log_b (((2 log_b 4)↑5) + 1)))
285	284	oveq2d 7372	. . . 4 ⊢ (𝑥 = 4 → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) = (2 · (2 log_b (((2 log_b 4)↑5) + 1))))
286	281	oveq1d 7371	. . . 4 ⊢ (𝑥 = 4 → ((2 log_b 𝑥)↑2) = ((2 log_b 4)↑2))
287	285, 286	oveq12d 7374	. . 3 ⊢ (𝑥 = 4 → ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)) = ((2 · (2 log_b (((2 log_b 4)↑5) + 1))) + ((2 log_b 4)↑2)))
288	281	oveq1d 7371	. . 3 ⊢ (𝑥 = 4 → ((2 log_b 𝑥)↑4) = ((2 log_b 4)↑4))
289		oveq2 7364	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (2 log_b 𝑥) = (2 log_b 𝑁))
290	289	oveq1d 7371	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑥)↑5) = ((2 log_b 𝑁)↑5))
291	290	oveq1d 7371	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((2 log_b 𝑥)↑5) + 1) = (((2 log_b 𝑁)↑5) + 1))
292	291	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 log_b (((2 log_b 𝑥)↑5) + 1)) = (2 log_b (((2 log_b 𝑁)↑5) + 1)))
293	292	oveq2d 7372	. . . . 5 ⊢ (𝑥 = 𝑁 → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) = (2 · (2 log_b (((2 log_b 𝑁)↑5) + 1))))
294	14	a1i 11	. . . . . . 7 ⊢ (𝑥 = 𝑁 → 𝐶 = (2 log_b (((2 log_b 𝑁)↑5) + 1)))
295	294	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝐶) = (2 · (2 log_b (((2 log_b 𝑁)↑5) + 1))))
296	295	eqcomd 2741	. . . . 5 ⊢ (𝑥 = 𝑁 → (2 · (2 log_b (((2 log_b 𝑁)↑5) + 1))) = (2 · 𝐶))
297	293, 296	eqtrd 2770	. . . 4 ⊢ (𝑥 = 𝑁 → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) = (2 · 𝐶))
298	289	oveq1d 7371	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑥)↑2) = ((2 log_b 𝑁)↑2))
299	15	a1i 11	. . . . . 6 ⊢ (𝑥 = 𝑁 → 𝐷 = ((2 log_b 𝑁)↑2))
300	299	eqcomd 2741	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑁)↑2) = 𝐷)
301	298, 300	eqtrd 2770	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑥)↑2) = 𝐷)
302	297, 301	oveq12d 7374	. . 3 ⊢ (𝑥 = 𝑁 → ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)) = ((2 · 𝐶) + 𝐷))
303	289	oveq1d 7371	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑥)↑4) = ((2 log_b 𝑁)↑4))
304	16	a1i 11	. . . . 5 ⊢ (𝑥 = 𝑁 → 𝐸 = ((2 log_b 𝑁)↑4))
305	304	eqcomd 2741	. . . 4 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑁)↑4) = 𝐸)
306	303, 305	eqtrd 2770	. . 3 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑥)↑4) = 𝐸)
307		sq2 14148	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
308	307	oveq2i 7367	. . . . . . . . . . . . . . 15 ⊢ (2 log_b (2↑2)) = (2 log_b 4)
309	308	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 log_b (2↑2)) = (2 log_b 4))
310	309	eqcomd 2741	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 log_b 4) = (2 log_b (2↑2)))
311	135	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ⁺)
312	56	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
313		relogbexp 26732	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ⁺ ∧ 2 ≠ 1 ∧ 2 ∈ ℤ) → (2 log_b (2↑2)) = 2)
314	311, 37, 312, 313	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 log_b (2↑2)) = 2)
315	310, 314	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 log_b 4) = 2)
316	315	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 log_b 4)↑5) = (2↑5))
317	316	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝜑 → (((2 log_b 4)↑5) + 1) = ((2↑5) + 1))
318	317	oveq2d 7372	. . . . . . . . 9 ⊢ (𝜑 → (2 log_b (((2 log_b 4)↑5) + 1)) = (2 log_b ((2↑5) + 1)))
319	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℝ)
320	319	leidd 11705	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 2)
321	315, 319	eqeltrd 2835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 log_b 4) ∈ ℝ)
322	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℕ₀)
323	321, 322	reexpcld 14114	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 log_b 4)↑5) ∈ ℝ)
324	316, 323	eqeltrrd 2836	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) ∈ ℝ)
325	324, 33	readdcld 11163	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ∈ ℝ)
326	322	nn0zd 12538	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 5 ∈ ℤ)
327	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
328	327, 315	breqtrrd 5102	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < (2 log_b 4))
329	321, 326, 328	3jca 1129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 log_b 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 log_b 4)))
330		expgt0 14046	. . . . . . . . . . . . . 14 ⊢ (((2 log_b 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 log_b 4)) → 0 < ((2 log_b 4)↑5))
331	329, 330	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < ((2 log_b 4)↑5))
332	331, 316	breqtrd 5100	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (2↑5))
333	324	ltp1d 12075	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) < ((2↑5) + 1))
334	26, 324, 325, 332, 333	lttrd 11296	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((2↑5) + 1))
335		6nn0 12447	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ₀
336	335	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℕ₀)
337	319, 336	reexpcld 14114	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑6) ∈ ℝ)
338	336	nn0zd 12538	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℤ)
339		expgt0 14046	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 6 ∈ ℤ ∧ 0 < 2) → 0 < (2↑6))
340	319, 338, 327, 339	syl3anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (2↑6))
341	324, 324	readdcld 11163	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + (2↑5)) ∈ ℝ)
342	33, 319, 35	ltled 11283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≤ 2)
343	319, 322, 342	expge1d 14116	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≤ (2↑5))
344	33, 324, 324, 343	leadd2dd 11754	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑5) + 1) ≤ ((2↑5) + (2↑5)))
345	341	leidd 11705	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑5) + (2↑5)) ≤ ((2↑5) + (2↑5)))
346		df-6 12237	. . . . . . . . . . . . . . . . . . 19 ⊢ 6 = (5 + 1)
347	346	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 6 = (5 + 1))
348	347	oveq2d 7372	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑6) = (2↑(5 + 1)))
349		2cn 12245	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℂ)
351	193	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℕ₀)
352	350, 351, 322	expaddd 14099	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑(5 + 1)) = ((2↑5) · (2↑1)))
353	348, 352	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑6) = ((2↑5) · (2↑1)))
354	350	exp1d 14092	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑1) = 2)
355	354	oveq2d 7372	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑5) · (2↑1)) = ((2↑5) · 2))
356	353, 355	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑6) = ((2↑5) · 2))
357	48, 324	sselid 3915	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑5) ∈ ℂ)
358	357	times2d 12410	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2↑5) · 2) = ((2↑5) + (2↑5)))
359	356, 358	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2↑6) = ((2↑5) + (2↑5)))
360	359	eqcomd 2741	. . . . . . . . . . . . 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 11292	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑5) + 1) ≤ (2↑6))
363	312, 320, 325, 334, 337, 340, 362	logblebd 42404	. . . . . . . . . 10 ⊢ (𝜑 → (2 log_b ((2↑5) + 1)) ≤ (2 log_b (2↑6)))
364	311, 37, 338	relogbexpd 42402	. . . . . . . . . 10 ⊢ (𝜑 → (2 log_b (2↑6)) = 6)
365	363, 364	breqtrd 5100	. . . . . . . . 9 ⊢ (𝜑 → (2 log_b ((2↑5) + 1)) ≤ 6)
366	318, 365	eqbrtrd 5096	. . . . . . . 8 ⊢ (𝜑 → (2 log_b (((2 log_b 4)↑5) + 1)) ≤ 6)
367		6t2e12 12737	. . . . . . . . 9 ⊢ (6 · 2) = ;12
368		6cn 12261	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
369	368	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
370		2nn 12243	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
371	193, 370	decnncl 12653	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ
372	371	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;12 ∈ ℕ)
373	372	nnred 12178	. . . . . . . . . . 11 ⊢ (𝜑 → ;12 ∈ ℝ)
374	373	recnd 11162	. . . . . . . . . 10 ⊢ (𝜑 → ;12 ∈ ℂ)
375	26, 327	gtned 11270	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≠ 0)
376	369, 350, 374, 375	ldiv 11978	. . . . . . . . 9 ⊢ (𝜑 → ((6 · 2) = ;12 ↔ 6 = (;12 / 2)))
377	367, 376	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → 6 = (;12 / 2))
378	366, 377	breqtrd 5100	. . . . . . 7 ⊢ (𝜑 → (2 log_b (((2 log_b 4)↑5) + 1)) ≤ (;12 / 2))
379	323, 33	readdcld 11163	. . . . . . . . 9 ⊢ (𝜑 → (((2 log_b 4)↑5) + 1) ∈ ℝ)
380	26, 33	readdcld 11163	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ∈ ℝ)
381	26	ltp1d 12075	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (0 + 1))
382	26, 323, 33, 331	ltadd1dd 11750	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) < (((2 log_b 4)↑5) + 1))
383	26, 380, 379, 381, 382	lttrd 11296	. . . . . . . . 9 ⊢ (𝜑 → 0 < (((2 log_b 4)↑5) + 1))
384	319, 327, 379, 383, 37	relogbcld 42401	. . . . . . . 8 ⊢ (𝜑 → (2 log_b (((2 log_b 4)↑5) + 1)) ∈ ℝ)
385	384, 373, 311	lemuldiv2d 13025	. . . . . . 7 ⊢ (𝜑 → ((2 · (2 log_b (((2 log_b 4)↑5) + 1))) ≤ ;12 ↔ (2 log_b (((2 log_b 4)↑5) + 1)) ≤ (;12 / 2)))
386	378, 385	mpbird 257	. . . . . 6 ⊢ (𝜑 → (2 · (2 log_b (((2 log_b 4)↑5) + 1))) ≤ ;12)
387	315	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝜑 → ((2 log_b 4)↑2) = (2↑2))
388	387, 307	eqtrdi 2786	. . . . . . . . 9 ⊢ (𝜑 → ((2 log_b 4)↑2) = 4)
389	388	oveq2d 7372	. . . . . . . 8 ⊢ (𝜑 → (;16 − ((2 log_b 4)↑2)) = (;16 − 4))
390		2nn0 12443	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
391		eqid 2735	. . . . . . . . . 10 ⊢ ;12 = ;12
392		4cn 12255	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
393		4p2e6 12318	. . . . . . . . . . 11 ⊢ (4 + 2) = 6
394	392, 349, 393	addcomli 11327	. . . . . . . . . 10 ⊢ (2 + 4) = 6
395	193, 390, 174, 391, 394	decaddi 12693	. . . . . . . . 9 ⊢ (;12 + 4) = ;16
396	392	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℂ)
397		6nn 12259	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
398	193, 397	decnncl 12653	. . . . . . . . . . . . 13 ⊢ ;16 ∈ ℕ
399	398	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;16 ∈ ℕ)
400	399	nnred 12178	. . . . . . . . . . 11 ⊢ (𝜑 → ;16 ∈ ℝ)
401	48, 400	sselid 3915	. . . . . . . . . 10 ⊢ (𝜑 → ;16 ∈ ℂ)
402	374, 396, 401	addlsub 11555	. . . . . . . . 9 ⊢ (𝜑 → ((;12 + 4) = ;16 ↔ ;12 = (;16 − 4)))
403	395, 402	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → ;12 = (;16 − 4))
404	389, 403	eqtr4d 2773	. . . . . . 7 ⊢ (𝜑 → (;16 − ((2 log_b 4)↑2)) = ;12)
405	404	eqcomd 2741	. . . . . 6 ⊢ (𝜑 → ;12 = (;16 − ((2 log_b 4)↑2)))
406	386, 405	breqtrd 5100	. . . . 5 ⊢ (𝜑 → (2 · (2 log_b (((2 log_b 4)↑5) + 1))) ≤ (;16 − ((2 log_b 4)↑2)))
407	319, 384	remulcld 11164	. . . . . 6 ⊢ (𝜑 → (2 · (2 log_b (((2 log_b 4)↑5) + 1))) ∈ ℝ)
408	321	resqcld 14076	. . . . . 6 ⊢ (𝜑 → ((2 log_b 4)↑2) ∈ ℝ)
409		leaddsub 11615	. . . . . 6 ⊢ (((2 · (2 log_b (((2 log_b 4)↑5) + 1))) ∈ ℝ ∧ ((2 log_b 4)↑2) ∈ ℝ ∧ ;16 ∈ ℝ) → (((2 · (2 log_b (((2 log_b 4)↑5) + 1))) + ((2 log_b 4)↑2)) ≤ ;16 ↔ (2 · (2 log_b (((2 log_b 4)↑5) + 1))) ≤ (;16 − ((2 log_b 4)↑2))))
410	407, 408, 400, 409	syl3anc 1374	. . . . 5 ⊢ (𝜑 → (((2 · (2 log_b (((2 log_b 4)↑5) + 1))) + ((2 log_b 4)↑2)) ≤ ;16 ↔ (2 · (2 log_b (((2 log_b 4)↑5) + 1))) ≤ (;16 − ((2 log_b 4)↑2))))
411	406, 410	mpbird 257	. . . 4 ⊢ (𝜑 → ((2 · (2 log_b (((2 log_b 4)↑5) + 1))) + ((2 log_b 4)↑2)) ≤ ;16)
412	315	oveq1d 7371	. . . . . 6 ⊢ (𝜑 → ((2 log_b 4)↑4) = (2↑4))
413		2exp4 17044	. . . . . 6 ⊢ (2↑4) = ;16
414	412, 413	eqtrdi 2786	. . . . 5 ⊢ (𝜑 → ((2 log_b 4)↑4) = ;16)
415	414	eqcomd 2741	. . . 4 ⊢ (𝜑 → ;16 = ((2 log_b 4)↑4))
416	411, 415	breqtrd 5100	. . 3 ⊢ (𝜑 → ((2 · (2 log_b (((2 log_b 4)↑5) + 1))) + ((2 log_b 4)↑2)) ≤ ((2 log_b 4)↑4))
417	7, 8, 219, 261, 262, 272, 280, 287, 288, 302, 306, 416, 12	dvle2 42499	. 2 ⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸)
418	1, 2, 3, 13, 14, 15, 16, 417	aks4d1p1p4 42498	1 ⊢ (𝜑 → 𝐴 < (2↑𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2930 ∀wral 3049 ⊆ wss 3885 class class class wbr 5074 ↦ cmpt 5155 dom cdm 5620 ↾ cres 5622 Fn wfn 6482 ⟶wf 6483 ‘cfv 6487 (class class class)co 7356 ℂcc 11025 ℝcr 11026 0cc0 11027 1c1 11028 + caddc 11030 · cmul 11032 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11366 / cdiv 11796 ℕcn 12163 2c2 12225 3c3 12226 4c4 12227 5c5 12228 6c6 12229 ℕ₀cn0 12426 ℤcz 12513 cdc 12633 ℤ_≥cuz 12777 ℝ⁺crp 12931 (,)cioo 13287 [,]cicc 13290 ...cfz 13450 ⌊cfl 13738 ⌈cceil 13739 ↑cexp 14012 ∏cprod 15857 –cn→ccncf 24831 D cdv 25818 logclog 26506 log_b clogb 26716

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2184 ax-ext 2707 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7678 ax-inf2 9551 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105 ax-addf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3060 df-rmo 3340 df-reu 3341 df-rab 3388 df-v 3429 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 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 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8100 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-er 8632 df-map 8764 df-pm 8765 df-ixp 8835 df-en 8883 df-dom 8884 df-sdom 8885 df-fin 8886 df-fsupp 9264 df-fi 9313 df-sup 9344 df-inf 9345 df-oi 9414 df-card 9852 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-7 12238 df-8 12239 df-9 12240 df-n0 12427 df-z 12514 df-dec 12634 df-uz 12778 df-q 12888 df-rp 12932 df-xneg 13052 df-xadd 13053 df-xmul 13054 df-ioo 13291 df-ioc 13292 df-ico 13293 df-icc 13294 df-fz 13451 df-fzo 13598 df-fl 13740 df-ceil 13741 df-mod 13818 df-seq 13953 df-exp 14013 df-fac 14225 df-bc 14254 df-hash 14282 df-shft 15018 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-limsup 15422 df-clim 15439 df-rlim 15440 df-sum 15638 df-prod 15858 df-ef 16021 df-e 16022 df-sin 16023 df-cos 16024 df-pi 16026 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-starv 17224 df-sca 17225 df-vsca 17226 df-ip 17227 df-tset 17228 df-ple 17229 df-ds 17231 df-unif 17232 df-hom 17233 df-cco 17234 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17455 df-qtop 17460 df-imas 17461 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-submnd 18741 df-mulg 19033 df-cntz 19281 df-cmn 19746 df-psmet 21333 df-xmet 21334 df-met 21335 df-bl 21336 df-mopn 21337 df-fbas 21338 df-fg 21339 df-cnfld 21342 df-top 22847 df-topon 22864 df-topsp 22886 df-bases 22899 df-cld 22972 df-ntr 22973 df-cls 22974 df-nei 23051 df-lp 23089 df-perf 23090 df-cn 23180 df-cnp 23181 df-haus 23268 df-cmp 23340 df-tx 23515 df-hmeo 23708 df-fil 23799 df-fm 23891 df-flim 23892 df-flf 23893 df-xms 24273 df-ms 24274 df-tms 24275 df-cncf 24833 df-limc 25821 df-dv 25822 df-log 26508 df-cxp 26509 df-logb 26717

This theorem is referenced by: aks4d1p1 42503

W3C validator