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 42364

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 12227	. . . 4 ⊢ 3 ∈ ℝ
5	4	a1i 11	. . 3 ⊢ (𝜑 → 3 ∈ ℝ)
6		4re 12231	. . . 4 ⊢ 4 ∈ ℝ
7	6	a1i 11	. . 3 ⊢ (𝜑 → 4 ∈ ℝ)
8	1	nnred 12162	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
9	5	lep1d 12075	. . . 4 ⊢ (𝜑 → 3 ≤ (3 + 1))
10		3p1e4 12287	. . . 4 ⊢ (3 + 1) = 4
11	9, 10	breqtrdi 5138	. . 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 12221	. . . . . . . 8 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℝ)
19		2pos 12250	. . . . . . . . 9 ⊢ 0 < 2
20	19	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 2)
21		elicc2 13329	. . . . . . . . . . . . . . 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 11137	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
27	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ)
28	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℝ)
29		4pos 12254	. . . . . . . . . . . . 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 11135	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℝ)
34		1lt2 12313	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
35	34	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 2)
36	33, 35	ltned 11271	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≠ 2)
37	36	necomd 2986	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 1)
38	37	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 1)
39	18, 20, 25, 32, 38	relogbcld 42262	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b 𝑥) ∈ ℝ)
40		5nn0 12423	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ₀
41	40	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℕ₀)
42	39, 41	reexpcld 14088	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 log_b 𝑥)↑5) ∈ ℝ)
43		1red 11135	. . . . . . . . 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 12074	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (0 + 1))
47	41	nn0zd 12515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℤ)
48		ax-resscn 11085	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
49	48, 18	sselid 3930	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℂ)
50	27, 20	gtned 11270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 0)
51		logb1 26737	. . . . . . . . . . . . 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 12318	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
54	53	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 4)
55	43, 28, 25, 54, 31	ltletrd 11295	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 𝑥)
56		2z 12525	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
57	56	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℤ)
58	57	uzidd 12769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ (ℤ_≥‘2))
59		1rp 12911	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ⁺
60	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ⁺)
61	25, 32	elrpd 12948	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ⁺)
62		logblt 26752	. . . . . . . . . . . . . 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 5121	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (2 log_b 𝑥))
66		expgt0 14020	. . . . . . . . . . 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 42262	. . . . . . 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 11137	. . . . . . . . 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 42262	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 log_b 𝑥) ∈ ℝ)
81	80	resqcld 14050	. . . . . 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 7060	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(4[,]𝑁)⟶ℝ)
84	48	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
85		3lt4 12316	. . . . . . . . . . 11 ⊢ 3 < 4
86	85	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 3 < 4)
87	8, 33	readdcld 11163	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
88	8	ltp1d 12074	. . . . . . . . . . 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 13321	. . . . . . . . . 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 13321	. . . . . . . . . 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 13337	. . . . . . . 8 ⊢ ((4 ∈ (3(,)(𝑁 + 1)) ∧ 𝑁 ∈ (3(,)(𝑁 + 1))) → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
104	96, 102, 103	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1)))
105	104	resmptd 5998	. . . . . 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 12225	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℂ)
107	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ)
108	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 2)
109		elioore 13293	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 𝑥 ∈ ℝ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ)
111		0red 11137	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 ∈ ℝ)
112	4	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 ∈ ℝ)
113		3pos 12252	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 3
114	113	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 3)
115		eliooord 13323	. . . . . . . . . . . . . . . . . . . 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 42262	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 log_b 𝑥) ∈ ℝ)
122	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℕ₀)
123	121, 122	reexpcld 14088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑5) ∈ ℝ)
124		1red 11135	. . . . . . . . . . . . . . 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 12074	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (0 + 1))
128	122	nn0zd 12515	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℤ)
129	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 2)
130		2lt3 12314	. . . . . . . . . . . . . . . . . . . . 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 12948	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ⁺)
135		2rp 12912	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ⁺
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℝ⁺)
137	134, 136, 129	jca32 515	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 ∈ ℝ⁺ ∧ (2 ∈ ℝ⁺ ∧ 1 < 2)))
138		logbgt0b 26761	. . . . . . . . . . . . . . . . . . 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 2986	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1)
146	107, 108, 125, 143, 145	relogbcld 42262	. . . . . . . . . . . . 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 3930	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 log_b 𝑥) ∈ ℂ)
150	149	sqcld 14069	. . . . . . . . . . 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 7060	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ)
153		ioossre 13325	. . . . . . . . . 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 26590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℝ)
157	125, 156	remulcld 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 log_b 𝑥)↑5) + 1) · (log‘2)) ∈ ℝ)
158	48, 123	sselid 3930	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑5) ∈ ℂ)
159		1cnd 11129	. . . . . . . . . . . . . . . . . 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 26537	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈ ℂ)
163	111, 143	gtned 11270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 log_b 𝑥)↑5) + 1) ≠ 0)
164		loggt0b 26599	. . . . . . . . . . . . . . . . . . . . . 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 2986	. . . . . . . . . . . . . . . . . 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 11971	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) ∈ ℝ)
172		5re 12234	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈ ℝ)
174		4nn0 12422	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℕ₀
175	174	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℕ₀)
176	121, 175	reexpcld 14088	. . . . . . . . . . . . . . . . . 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 3930	. . . . . . . . . . . . . . . . . . 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 11971	. . . . . . . . . . . . . . . . 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 14050	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ∈ ℝ)
188	56	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈ ℤ)
189	162, 169, 188	expne0d 14077	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ≠ 0)
190	107, 187, 189	redivcld 11971	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 / ((log‘2)↑2)) ∈ ℝ)
191	134	relogcld 26590	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘𝑥) ∈ ℝ)
192		2m1e1 12268	. . . . . . . . . . . . . . . . . 18 ⊢ (2 − 1) = 1
193		1nn0 12419	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ₀
194	192, 193	eqeltri 2831	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) ∈ ℕ₀
195	194	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 − 1) ∈ ℕ₀)
196	191, 195	reexpcld 14088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(2 − 1)) ∈ ℝ)
197	196, 110, 180	redivcld 11971	. . . . . . . . . . . . . 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 6627	. . . . . . . . . . 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 12075	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
206	5, 8, 87, 13, 205	letrd 11292	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ (𝑁 + 1))
207	5, 87, 204, 206	aks4d1p1p6 42362	. . . . . . . . . . 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 6584	. . . . . . . . . 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 6596	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (3(,)(𝑁 + 1)))
211		dvcn 25881	. . . . . . . 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 24848	. . . . . . . 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 24849	. . . . 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 14088	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 log_b 𝑥)↑4) ∈ ℝ)
222	221	fmpttd 7060	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)):(4[,]𝑁)⟶ℝ)
223	104	resmptd 5998	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4)) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 log_b 𝑥)↑4)))
224	48, 176	sselid 3930	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 log_b 𝑥)↑4) ∈ ℂ)
225	224	fmpttd 7060	. . . . . . . . 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 14088	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ∈ ℝ)
229		4z 12527	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℤ
230	229	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈ ℤ)
231	162, 169, 230	expne0d 14077	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ≠ 0)
232	227, 228, 231	redivcld 11971	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 / ((log‘2)↑4)) ∈ ℝ)
233		4m1e3 12271	. . . . . . . . . . . . . . . . 17 ⊢ (4 − 1) = 3
234		3nn0 12421	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℕ₀
235	233, 234	eqeltri 2831	. . . . . . . . . . . . . . . 16 ⊢ (4 − 1) ∈ ℕ₀
236	235	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 − 1) ∈ ℕ₀)
237	191, 236	reexpcld 14088	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(4 − 1)) ∈ ℝ)
238	237, 110, 180	redivcld 11971	. . . . . . . . . . . . 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 6627	. . . . . . . . . . 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 12230	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
248	247	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 4 ∈ ℕ)
249	5, 87, 243, 206, 244, 245, 246, 248	dvrelogpow2b 42357	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥))))
250	249	fneq1d 6584	. . . . . . . . . 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 6596	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 log_b 𝑥)↑4))) = (3(,)(𝑁 + 1)))
253		dvcn 25881	. . . . . . . 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 24848	. . . . . . . 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 24849	. . . . 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 42362	. . 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 42357	. . . 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 7374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((log‘𝑥)↑(4 − 1)) = ((log‘𝑥)↑3))
269	268	oveq1d 7373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (((log‘𝑥)↑(4 − 1)) / 𝑥) = (((log‘𝑥)↑3) / 𝑥))
270	269	oveq2d 7374	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) = ((4 / ((log‘2)↑4)) · (((log‘𝑥)↑3) / 𝑥)))
271	270	mpteq2dva 5190	. . . 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 13293	. . . . 5 ⊢ (𝑥 ∈ (4(,)𝑁) → 𝑥 ∈ ℝ)
274	273	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 𝑥 ∈ ℝ)
275	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ∈ ℝ)
276		eliooord 13323	. . . . . . 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 42363	. . 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 7366	. . . . . . . 8 ⊢ (𝑥 = 4 → (2 log_b 𝑥) = (2 log_b 4))
282	281	oveq1d 7373	. . . . . . 7 ⊢ (𝑥 = 4 → ((2 log_b 𝑥)↑5) = ((2 log_b 4)↑5))
283	282	oveq1d 7373	. . . . . 6 ⊢ (𝑥 = 4 → (((2 log_b 𝑥)↑5) + 1) = (((2 log_b 4)↑5) + 1))
284	283	oveq2d 7374	. . . . 5 ⊢ (𝑥 = 4 → (2 log_b (((2 log_b 𝑥)↑5) + 1)) = (2 log_b (((2 log_b 4)↑5) + 1)))
285	284	oveq2d 7374	. . . 4 ⊢ (𝑥 = 4 → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) = (2 · (2 log_b (((2 log_b 4)↑5) + 1))))
286	281	oveq1d 7373	. . . 4 ⊢ (𝑥 = 4 → ((2 log_b 𝑥)↑2) = ((2 log_b 4)↑2))
287	285, 286	oveq12d 7376	. . 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 7373	. . 3 ⊢ (𝑥 = 4 → ((2 log_b 𝑥)↑4) = ((2 log_b 4)↑4))
289		oveq2 7366	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (2 log_b 𝑥) = (2 log_b 𝑁))
290	289	oveq1d 7373	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → ((2 log_b 𝑥)↑5) = ((2 log_b 𝑁)↑5))
291	290	oveq1d 7373	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((2 log_b 𝑥)↑5) + 1) = (((2 log_b 𝑁)↑5) + 1))
292	291	oveq2d 7374	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 log_b (((2 log_b 𝑥)↑5) + 1)) = (2 log_b (((2 log_b 𝑁)↑5) + 1)))
293	292	oveq2d 7374	. . . . 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 7374	. . . . . 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 7373	. . . . 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 7376	. . 3 ⊢ (𝑥 = 𝑁 → ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)) = ((2 · 𝐶) + 𝐷))
303	289	oveq1d 7373	. . . 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 14122	. . . . . . . . . . . . . . . 16 ⊢ (2↑2) = 4
308	307	oveq2i 7369	. . . . . . . . . . . . . . 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 26748	. . . . . . . . . . . . . 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 7373	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 log_b 4)↑5) = (2↑5))
317	316	oveq1d 7373	. . . . . . . . . 10 ⊢ (𝜑 → (((2 log_b 4)↑5) + 1) = ((2↑5) + 1))
318	317	oveq2d 7374	. . . . . . . . 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 14088	. . . . . . . . . . . . 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 12515	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 5 ∈ ℤ)
327	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
328	327, 315	breqtrrd 5125	. . . . . . . . . . . . . . 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 14020	. . . . . . . . . . . . . 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 5123	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (2↑5))
333	324	ltp1d 12074	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑5) < ((2↑5) + 1))
334	26, 324, 325, 332, 333	lttrd 11296	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((2↑5) + 1))
335		6nn0 12424	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ₀
336	335	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℕ₀)
337	319, 336	reexpcld 14088	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑6) ∈ ℝ)
338	336	nn0zd 12515	. . . . . . . . . . . 12 ⊢ (𝜑 → 6 ∈ ℤ)
339		expgt0 14020	. . . . . . . . . . . 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 14090	. . . . . . . . . . . . 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 12214	. . . . . . . . . . . . . . . . . . 19 ⊢ 6 = (5 + 1)
347	346	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 6 = (5 + 1))
348	347	oveq2d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑6) = (2↑(5 + 1)))
349		2cn 12222	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
350	349	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℂ)
351	193	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℕ₀)
352	350, 351, 322	expaddd 14073	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑(5 + 1)) = ((2↑5) · (2↑1)))
353	348, 352	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑6) = ((2↑5) · (2↑1)))
354	350	exp1d 14066	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑1) = 2)
355	354	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑5) · (2↑1)) = ((2↑5) · 2))
356	353, 355	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑6) = ((2↑5) · 2))
357	48, 324	sselid 3930	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑5) ∈ ℂ)
358	357	times2d 12387	. . . . . . . . . . . . . . 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 5123	. . . . . . . . . . . 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 42265	. . . . . . . . . 10 ⊢ (𝜑 → (2 log_b ((2↑5) + 1)) ≤ (2 log_b (2↑6)))
364	311, 37, 338	relogbexpd 42263	. . . . . . . . . 10 ⊢ (𝜑 → (2 log_b (2↑6)) = 6)
365	363, 364	breqtrd 5123	. . . . . . . . 9 ⊢ (𝜑 → (2 log_b ((2↑5) + 1)) ≤ 6)
366	318, 365	eqbrtrd 5119	. . . . . . . 8 ⊢ (𝜑 → (2 log_b (((2 log_b 4)↑5) + 1)) ≤ 6)
367		6t2e12 12713	. . . . . . . . 9 ⊢ (6 · 2) = ;12
368		6cn 12238	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
369	368	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 6 ∈ ℂ)
370		2nn 12220	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
371	193, 370	decnncl 12629	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ
372	371	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;12 ∈ ℕ)
373	372	nnred 12162	. . . . . . . . . . 11 ⊢ (𝜑 → ;12 ∈ ℝ)
374	373	recnd 11162	. . . . . . . . . 10 ⊢ (𝜑 → ;12 ∈ ℂ)
375	26, 327	gtned 11270	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≠ 0)
376	369, 350, 374, 375	ldiv 11977	. . . . . . . . 9 ⊢ (𝜑 → ((6 · 2) = ;12 ↔ 6 = (;12 / 2)))
377	367, 376	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → 6 = (;12 / 2))
378	366, 377	breqtrd 5123	. . . . . . 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 12074	. . . . . . . . . 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 42262	. . . . . . . 8 ⊢ (𝜑 → (2 log_b (((2 log_b 4)↑5) + 1)) ∈ ℝ)
385	384, 373, 311	lemuldiv2d 13001	. . . . . . 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 7373	. . . . . . . . . 10 ⊢ (𝜑 → ((2 log_b 4)↑2) = (2↑2))
388	387, 307	eqtrdi 2786	. . . . . . . . 9 ⊢ (𝜑 → ((2 log_b 4)↑2) = 4)
389	388	oveq2d 7374	. . . . . . . 8 ⊢ (𝜑 → (;16 − ((2 log_b 4)↑2)) = (;16 − 4))
390		2nn0 12420	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
391		eqid 2735	. . . . . . . . . 10 ⊢ ;12 = ;12
392		4cn 12232	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
393		4p2e6 12295	. . . . . . . . . . 11 ⊢ (4 + 2) = 6
394	392, 349, 393	addcomli 11327	. . . . . . . . . 10 ⊢ (2 + 4) = 6
395	193, 390, 174, 391, 394	decaddi 12669	. . . . . . . . 9 ⊢ (;12 + 4) = ;16
396	392	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℂ)
397		6nn 12236	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℕ
398	193, 397	decnncl 12629	. . . . . . . . . . . . 13 ⊢ ;16 ∈ ℕ
399	398	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ;16 ∈ ℕ)
400	399	nnred 12162	. . . . . . . . . . 11 ⊢ (𝜑 → ;16 ∈ ℝ)
401	48, 400	sselid 3930	. . . . . . . . . 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 5123	. . . . 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 14050	. . . . . 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 7373	. . . . . 6 ⊢ (𝜑 → ((2 log_b 4)↑4) = (2↑4))
413		2exp4 17014	. . . . . 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 5123	. . 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 42361	. 2 ⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸)
418	1, 2, 3, 13, 14, 15, 16, 417	aks4d1p1p4 42360	1 ⊢ (𝜑 → 𝐴 < (2↑𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2931 ∀wral 3050 ⊆ wss 3900 class class class wbr 5097 ↦ cmpt 5178 dom cdm 5623 ↾ cres 5625 Fn wfn 6486 ⟶wf 6487 ‘cfv 6491 (class class class)co 7358 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11366 / cdiv 11796 ℕcn 12147 2c2 12202 3c3 12203 4c4 12204 5c5 12205 6c6 12206 ℕ₀cn0 12403 ℤcz 12490 cdc 12609 ℤ_≥cuz 12753 ℝ⁺crp 12907 (,)cioo 13263 [,]cicc 13266 ...cfz 13425 ⌊cfl 13712 ⌈cceil 13713 ↑cexp 13986 ∏cprod 15828 –cn→ccncf 24827 D cdv 25822 logclog 26521 log_b clogb 26732

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 2183 ax-ext 2707 ax-rep 5223 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-inf2 9552 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

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 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3349 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4902 df-iun 4947 df-iin 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6258 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-isom 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-map 8767 df-pm 8768 df-ixp 8838 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-fsupp 9267 df-fi 9316 df-sup 9347 df-inf 9348 df-oi 9417 df-card 9853 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 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-z 12491 df-dec 12610 df-uz 12754 df-q 12864 df-rp 12908 df-xneg 13028 df-xadd 13029 df-xmul 13030 df-ioo 13267 df-ioc 13268 df-ico 13269 df-icc 13270 df-fz 13426 df-fzo 13573 df-fl 13714 df-ceil 13715 df-mod 13792 df-seq 13927 df-exp 13987 df-fac 14199 df-bc 14228 df-hash 14256 df-shft 14992 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-limsup 15396 df-clim 15413 df-rlim 15414 df-sum 15612 df-prod 15829 df-ef 15992 df-e 15993 df-sin 15994 df-cos 15995 df-pi 15997 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-xrs 17425 df-qtop 17430 df-imas 17431 df-xps 17433 df-mre 17507 df-mrc 17508 df-acs 17510 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19248 df-cmn 19713 df-psmet 21303 df-xmet 21304 df-met 21305 df-bl 21306 df-mopn 21307 df-fbas 21308 df-fg 21309 df-cnfld 21312 df-top 22840 df-topon 22857 df-topsp 22879 df-bases 22892 df-cld 22965 df-ntr 22966 df-cls 22967 df-nei 23044 df-lp 23082 df-perf 23083 df-cn 23173 df-cnp 23174 df-haus 23261 df-cmp 23333 df-tx 23508 df-hmeo 23701 df-fil 23792 df-fm 23884 df-flim 23885 df-flf 23886 df-xms 24266 df-ms 24267 df-tms 24268 df-cncf 24829 df-limc 25825 df-dv 25826 df-log 26523 df-cxp 26524 df-logb 26733

This theorem is referenced by: aks4d1p1 42365

W3C validator