aks4d1p1p6 - Mathbox for metakunt

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

Theorem aks4d1p1p6 40530

Description: Inequality lift to differentiable functions for a term in AKS inequality lemma. (Contributed by metakunt, 19-Aug-2024.)

**Hypotheses**
Ref	Expression
aks4d1p1p6.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
aks4d1p1p6.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
aks4d1p1p6.3	⊢ (𝜑 → 3 ≤ 𝐴)
aks4d1p1p6.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)

**Assertion**
Ref	Expression
aks4d1p1p6	⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((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)) / 𝑥)))))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝜑,𝑥

Proof of Theorem aks4d1p1p6 Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reelprrecn 11143	. . 3 ⊢ ℝ ∈ {ℝ, ℂ}
2	1	a1i 11	. 2 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
3		2cnd 12231	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
4		2re 12227	. . . . . 6 ⊢ 2 ∈ ℝ
5	4	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
6		2pos 12256	. . . . . 6 ⊢ 0 < 2
7	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 2)
8		elioore 13294	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
9	8	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ)
10		0red 11158	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
11		aks4d1p1p6.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℝ)
12	11	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
13		3re 12233	. . . . . . . . . . 11 ⊢ 3 ∈ ℝ
14	13	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 3 ∈ ℝ)
15		3pos 12258	. . . . . . . . . . 11 ⊢ 0 < 3
16	15	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 3)
17		aks4d1p1p6.3	. . . . . . . . . . 11 ⊢ (𝜑 → 3 ≤ 𝐴)
18	17	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 3 ≤ 𝐴)
19	10, 14, 12, 16, 18	ltletrd 11315	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 𝐴)
20		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵))
21	11	rexrd 11205	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
22	21	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ^*)
23		aks4d1p1p6.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
24	23	rexrd 11205	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
25	24	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ^*)
26	9	rexrd 11205	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ^*)
27		elioo5 13321	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
28	22, 25, 26, 27	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
29	20, 28	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
30	29	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑥)
31	10, 12, 9, 19, 30	lttrd 11316	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 𝑥)
32		1red 11156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ)
33		1lt2 12324	. . . . . . . . . . 11 ⊢ 1 < 2
34	33	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 2)
35	32, 34	ltned 11291	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ≠ 2)
36	35	necomd 2999	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 1)
37	5, 7, 9, 31, 36	relogbcld 40430	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 log_b 𝑥) ∈ ℝ)
38		5nn0 12433	. . . . . . . 8 ⊢ 5 ∈ ℕ₀
39	38	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℕ₀)
40	37, 39	reexpcld 14068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 log_b 𝑥)↑5) ∈ ℝ)
41	40, 32	readdcld 11184	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 log_b 𝑥)↑5) + 1) ∈ ℝ)
42	10, 32	readdcld 11184	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (0 + 1) ∈ ℝ)
43	10	ltp1d 12085	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (0 + 1))
44	39	nn0zd 12525	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℤ)
45		2cnd 12231	. . . . . . . . . . 11 ⊢ (⊤ → 2 ∈ ℂ)
46		0red 11158	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℝ)
47	6	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 < 2)
48	46, 47	ltned 11291	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ≠ 2)
49	48	necomd 2999	. . . . . . . . . . 11 ⊢ (⊤ → 2 ≠ 0)
50		1red 11156	. . . . . . . . . . . . 13 ⊢ (⊤ → 1 ∈ ℝ)
51	33	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 1 < 2)
52	50, 51	ltned 11291	. . . . . . . . . . . 12 ⊢ (⊤ → 1 ≠ 2)
53	52	necomd 2999	. . . . . . . . . . 11 ⊢ (⊤ → 2 ≠ 1)
54		logb1 26119	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 log_b 1) = 0)
55	45, 49, 53, 54	syl3anc 1371	. . . . . . . . . 10 ⊢ (⊤ → (2 log_b 1) = 0)
56	55	mptru 1548	. . . . . . . . 9 ⊢ (2 log_b 1) = 0
57		2lt3 12325	. . . . . . . . . . . . . 14 ⊢ 2 < 3
58	57	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 < 3)
59	32, 5, 14, 34, 58	lttrd 11316	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 3)
60	32, 14, 12, 59, 18	ltletrd 11315	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 𝐴)
61	32, 12, 9, 60, 30	lttrd 11316	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 𝑥)
62		2z 12535	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
63	62	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ)
64	63	uzidd 12779	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ (ℤ_≥‘2))
65		1rp 12919	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
66	65	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ⁺)
67	9, 31	elrpd 12954	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ⁺)
68		logblt 26134	. . . . . . . . . . 11 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 1 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (1 < 𝑥 ↔ (2 log_b 1) < (2 log_b 𝑥)))
69	64, 66, 67, 68	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 < 𝑥 ↔ (2 log_b 1) < (2 log_b 𝑥)))
70	61, 69	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 log_b 1) < (2 log_b 𝑥))
71	56, 70	eqbrtrrid 5141	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (2 log_b 𝑥))
72		expgt0 14001	. . . . . . . 8 ⊢ (((2 log_b 𝑥) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 log_b 𝑥)) → 0 < ((2 log_b 𝑥)↑5))
73	37, 44, 71, 72	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < ((2 log_b 𝑥)↑5))
74	10, 40, 32, 73	ltadd1dd 11766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (0 + 1) < (((2 log_b 𝑥)↑5) + 1))
75	10, 42, 41, 43, 74	lttrd 11316	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (((2 log_b 𝑥)↑5) + 1))
76	5, 7, 41, 75, 36	relogbcld 40430	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℝ)
77		recn 11141	. . . 4 ⊢ ((2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℝ → (2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℂ)
78	76, 77	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 log_b (((2 log_b 𝑥)↑5) + 1)) ∈ ℂ)
79	3, 78	mulcld 11175	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) ∈ ℂ)
80		2rp 12920	. . . . . . . 8 ⊢ 2 ∈ ℝ⁺
81	80	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ⁺)
82	81	relogcld 25978	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈ ℝ)
83	41, 82	remulcld 11185	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((2 log_b 𝑥)↑5) + 1) · (log‘2)) ∈ ℝ)
84	40	recnd 11183	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 log_b 𝑥)↑5) ∈ ℂ)
85		1cnd 11150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ)
86	84, 85	addcld 11174	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 log_b 𝑥)↑5) + 1) ∈ ℂ)
87	7	gt0ne0d 11719	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
88	3, 87	logcld 25926	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈ ℂ)
89	75	gt0ne0d 11719	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 log_b 𝑥)↑5) + 1) ≠ 0)
90		0red 11158	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
91		loggt0b 25987	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ⁺ → (0 < (log‘2) ↔ 1 < 2))
92	80, 91	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 < (log‘2) ↔ 1 < 2)
93	33, 92	mpbir 230	. . . . . . . . . 10 ⊢ 0 < (log‘2)
94	93	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 < (log‘2))
95	90, 94	ltned 11291	. . . . . . . 8 ⊢ (𝜑 → 0 ≠ (log‘2))
96	95	necomd 2999	. . . . . . 7 ⊢ (𝜑 → (log‘2) ≠ 0)
97	96	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ≠ 0)
98	86, 88, 89, 97	mulne0d 11807	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((2 log_b 𝑥)↑5) + 1) · (log‘2)) ≠ 0)
99	32, 83, 98	redivcld 11983	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) ∈ ℝ)
100		5re 12240	. . . . . . . 8 ⊢ 5 ∈ ℝ
101	100	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℝ)
102		4nn0 12432	. . . . . . . . 9 ⊢ 4 ∈ ℕ₀
103	102	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 4 ∈ ℕ₀)
104	37, 103	reexpcld 14068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 log_b 𝑥)↑4) ∈ ℝ)
105	101, 104	remulcld 11185	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (5 · ((2 log_b 𝑥)↑4)) ∈ ℝ)
106	9, 82	remulcld 11185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 · (log‘2)) ∈ ℝ)
107	9	recnd 11183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ)
108	10, 31	gtned 11290	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 0)
109	107, 88, 108, 97	mulne0d 11807	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 · (log‘2)) ≠ 0)
110	32, 106, 109	redivcld 11983	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / (𝑥 · (log‘2))) ∈ ℝ)
111	105, 110	remulcld 11185	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) ∈ ℝ)
112	111, 10	readdcld 11184	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0) ∈ ℝ)
113	99, 112	remulcld 11185	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈ ℝ)
114	5, 113	remulcld 11185	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) ∈ ℝ)
115	41, 75	elrpd 12954	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 log_b 𝑥)↑5) + 1) ∈ ℝ⁺)
116	4	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 2 ∈ ℝ)
117	6	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 0 < 2)
118		rpre 12923	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
119	118	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ)
120		rpgt0 12927	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ → 0 < 𝑦)
121	120	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 0 < 𝑦)
122		1red 11156	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 1 ∈ ℝ)
123	33	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 1 < 2)
124	122, 123	ltned 11291	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 1 ≠ 2)
125	124	necomd 2999	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 2 ≠ 1)
126	116, 117, 119, 121, 125	relogbcld 40430	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (2 log_b 𝑦) ∈ ℝ)
127	126	recnd 11183	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (2 log_b 𝑦) ∈ ℂ)
128	80	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 2 ∈ ℝ⁺)
129	128	relogcld 25978	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (log‘2) ∈ ℝ)
130	119, 129	remulcld 11185	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · (log‘2)) ∈ ℝ)
131	119	recnd 11183	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℂ)
132		2cnd 12231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 2 ∈ ℂ)
133	128	rpne0d 12962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 2 ≠ 0)
134	132, 133	logcld 25926	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (log‘2) ∈ ℂ)
135		rpne0 12931	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ≠ 0)
136	135	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ≠ 0)
137	96	necomd 2999	. . . . . . . 8 ⊢ (𝜑 → 0 ≠ (log‘2))
138	137	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 0 ≠ (log‘2))
139	138	necomd 2999	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (log‘2) ≠ 0)
140	131, 134, 136, 139	mulne0d 11807	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · (log‘2)) ≠ 0)
141	122, 130, 140	redivcld 11983	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (1 / (𝑦 · (log‘2))) ∈ ℝ)
142		cnelprrecn 11144	. . . . . . 7 ⊢ ℂ ∈ {ℝ, ℂ}
143	142	a1i 11	. . . . . 6 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
144	37	recnd 11183	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 log_b 𝑥) ∈ ℂ)
145		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
146	38	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 5 ∈ ℕ₀)
147	145, 146	expcld 14051	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑5) ∈ ℂ)
148		5cn 12241	. . . . . . . 8 ⊢ 5 ∈ ℂ
149	148	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 5 ∈ ℂ)
150	102	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 4 ∈ ℕ₀)
151	145, 150	expcld 14051	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑4) ∈ ℂ)
152	149, 151	mulcld 11175	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 · (𝑧↑4)) ∈ ℂ)
153	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 3 ∈ ℝ)
154	15	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 < 3)
155	90, 153, 11, 154, 17	ltletrd 11315	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝐴)
156	90, 11, 155	ltled 11303	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝐴)
157		aks4d1p1p6.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
158		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 log_b 𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 log_b 𝑥))
159		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))
160	21, 24, 156, 157, 158, 159	dvrelog2b 40523	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 log_b 𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))))
161		5nn 12239	. . . . . . . 8 ⊢ 5 ∈ ℕ
162		dvexp 25317	. . . . . . . 8 ⊢ (5 ∈ ℕ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 − 1)))))
163	161, 162	ax-mp 5	. . . . . . 7 ⊢ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 − 1))))
164		5m1e4 12283	. . . . . . . . . . 11 ⊢ (5 − 1) = 4
165	164	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 − 1) = 4)
166	165	oveq2d 7373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑(5 − 1)) = (𝑧↑4))
167	166	oveq2d 7373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 · (𝑧↑(5 − 1))) = (5 · (𝑧↑4)))
168	167	mpteq2dva 5205	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 − 1)))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑4))))
169	163, 168	eqtrid 2788	. . . . . 6 ⊢ (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑4))))
170		oveq1 7364	. . . . . 6 ⊢ (𝑧 = (2 log_b 𝑥) → (𝑧↑5) = ((2 log_b 𝑥)↑5))
171		oveq1 7364	. . . . . . 7 ⊢ (𝑧 = (2 log_b 𝑥) → (𝑧↑4) = ((2 log_b 𝑥)↑4))
172	171	oveq2d 7373	. . . . . 6 ⊢ (𝑧 = (2 log_b 𝑥) → (5 · (𝑧↑4)) = (5 · ((2 log_b 𝑥)↑4)))
173	2, 143, 144, 110, 147, 152, 160, 169, 170, 172	dvmptco 25336	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 log_b 𝑥)↑5))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2))))))
174		1cnd 11150	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
175	174	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
176		0red 11158	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
177	2, 174	dvmptc 25322	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ 1)) = (𝑥 ∈ ℝ ↦ 0))
178		ioossre 13325	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ ℝ
179	178	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
180		eqid 2736	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
181	180	tgioo2 24166	. . . . . 6 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
182		iooretop 24129	. . . . . . 7 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
183	182	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
184	2, 175, 176, 177, 179, 181, 180, 183	dvmptres 25327	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 1)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
185	2, 84, 111, 173, 85, 10, 184	dvmptadd 25324	. . . 4 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (((2 log_b 𝑥)↑5) + 1))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)))
186		dfrp2 13313	. . . . . . . 8 ⊢ ℝ⁺ = (0(,)+∞)
187	186	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ⁺ = (0(,)+∞))
188	187	mpteq1d 5200	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ ↦ (2 log_b 𝑦)) = (𝑦 ∈ (0(,)+∞) ↦ (2 log_b 𝑦)))
189	188	oveq2d 7373	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ⁺ ↦ (2 log_b 𝑦))) = (ℝ D (𝑦 ∈ (0(,)+∞) ↦ (2 log_b 𝑦))))
190	90	rexrd 11205	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ^*)
191		pnfxr 11209	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
192	191	a1i 11	. . . . . . 7 ⊢ (𝜑 → +∞ ∈ ℝ^*)
193	90	leidd 11721	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 0)
194		0lepnf 13053	. . . . . . . 8 ⊢ 0 ≤ +∞
195	194	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ≤ +∞)
196		eqid 2736	. . . . . . 7 ⊢ (𝑦 ∈ (0(,)+∞) ↦ (2 log_b 𝑦)) = (𝑦 ∈ (0(,)+∞) ↦ (2 log_b 𝑦))
197		eqid 2736	. . . . . . 7 ⊢ (𝑦 ∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))) = (𝑦 ∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2))))
198	190, 192, 193, 195, 196, 197	dvrelog2b 40523	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (0(,)+∞) ↦ (2 log_b 𝑦))) = (𝑦 ∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))))
199	187	eqcomd 2742	. . . . . . 7 ⊢ (𝜑 → (0(,)+∞) = ℝ⁺)
200	199	mpteq1d 5200	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))) = (𝑦 ∈ ℝ⁺ ↦ (1 / (𝑦 · (log‘2)))))
201	198, 200	eqtrd 2776	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (0(,)+∞) ↦ (2 log_b 𝑦))) = (𝑦 ∈ ℝ⁺ ↦ (1 / (𝑦 · (log‘2)))))
202	189, 201	eqtrd 2776	. . . 4 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ⁺ ↦ (2 log_b 𝑦))) = (𝑦 ∈ ℝ⁺ ↦ (1 / (𝑦 · (log‘2)))))
203		oveq2 7365	. . . 4 ⊢ (𝑦 = (((2 log_b 𝑥)↑5) + 1) → (2 log_b 𝑦) = (2 log_b (((2 log_b 𝑥)↑5) + 1)))
204		oveq1 7364	. . . . 5 ⊢ (𝑦 = (((2 log_b 𝑥)↑5) + 1) → (𝑦 · (log‘2)) = ((((2 log_b 𝑥)↑5) + 1) · (log‘2)))
205	204	oveq2d 7373	. . . 4 ⊢ (𝑦 = (((2 log_b 𝑥)↑5) + 1) → (1 / (𝑦 · (log‘2))) = (1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))))
206	2, 2, 115, 112, 127, 141, 185, 202, 203, 205	dvmptco 25336	. . 3 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 log_b (((2 log_b 𝑥)↑5) + 1)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))))
207	4	a1i 11	. . . 4 ⊢ (𝜑 → 2 ∈ ℝ)
208	207	recnd 11183	. . 3 ⊢ (𝜑 → 2 ∈ ℂ)
209	2, 78, 113, 206, 208	dvmptcmul 25328	. 2 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 · ((1 / ((((2 log_b 𝑥)↑5) + 1) · (log‘2))) · (((5 · ((2 log_b 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)))))
210	144	sqcld 14049	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 log_b 𝑥)↑2) ∈ ℂ)
211	82	resqcld 14030	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘2)↑2) ∈ ℝ)
212	81	rpne0d 12962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
213	3, 212	logcld 25926	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈ ℂ)
214	213, 97, 63	expne0d 14057	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘2)↑2) ≠ 0)
215	5, 211, 214	redivcld 11983	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 / ((log‘2)↑2)) ∈ ℝ)
216	67	relogcld 25978	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘𝑥) ∈ ℝ)
217		2m1e1 12279	. . . . . . 7 ⊢ (2 − 1) = 1
218		1nn0 12429	. . . . . . 7 ⊢ 1 ∈ ℕ₀
219	217, 218	eqeltri 2834	. . . . . 6 ⊢ (2 − 1) ∈ ℕ₀
220	219	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 − 1) ∈ ℕ₀)
221	216, 220	reexpcld 14068	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘𝑥)↑(2 − 1)) ∈ ℝ)
222	67	rpne0d 12962	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 0)
223	221, 9, 222	redivcld 11983	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ)
224	215, 223	remulcld 11185	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ)
225		eqid 2736	. . 3 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 log_b 𝑥)↑2)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 log_b 𝑥)↑2))
226		eqid 2736	. . 3 ⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))
227		eqid 2736	. . 3 ⊢ (2 / ((log‘2)↑2)) = (2 / ((log‘2)↑2))
228		2nn 12226	. . . 4 ⊢ 2 ∈ ℕ
229	228	a1i 11	. . 3 ⊢ (𝜑 → 2 ∈ ℕ)
230	11, 23, 155, 157, 225, 226, 227, 229	dvrelogpow2b 40525	. 2 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 log_b 𝑥)↑2))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))))
231	2, 79, 114, 209, 210, 224, 230	dvmptadd 25324	1 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · (2 log_b (((2 log_b 𝑥)↑5) + 1))) + ((2 log_b 𝑥)↑2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((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)) / 𝑥)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ⊤wtru 1542 ∈ wcel 2106 ≠ wne 2943 ⊆ wss 3910 {cpr 4588 class class class wbr 5105 ↦ cmpt 5188 ran crn 5634 ‘cfv 6496 (class class class)co 7357 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 +∞cpnf 11186 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 ℕcn 12153 2c2 12208 3c3 12209 4c4 12210 5c5 12211 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 (,)cioo 13264 ↑cexp 13967 TopOpenctopn 17303 topGenctg 17319 ℂ_fldccnfld 20796 D cdv 25227 logclog 25910 log_b clogb 26114

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-addf 11130 ax-mulf 11131

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ioc 13269 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-fl 13697 df-mod 13775 df-seq 13907 df-exp 13968 df-fac 14174 df-bc 14203 df-hash 14231 df-shft 14952 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-limsup 15353 df-clim 15370 df-rlim 15371 df-sum 15571 df-ef 15950 df-sin 15952 df-cos 15953 df-pi 15955 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-rest 17304 df-topn 17305 df-0g 17323 df-gsum 17324 df-topgen 17325 df-pt 17326 df-prds 17329 df-xrs 17384 df-qtop 17389 df-imas 17390 df-xps 17392 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-submnd 18602 df-mulg 18873 df-cntz 19097 df-cmn 19564 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-fbas 20793 df-fg 20794 df-cnfld 20797 df-top 22243 df-topon 22260 df-topsp 22282 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-perf 22488 df-cn 22578 df-cnp 22579 df-haus 22666 df-cmp 22738 df-tx 22913 df-hmeo 23106 df-fil 23197 df-fm 23289 df-flim 23290 df-flf 23291 df-xms 23673 df-ms 23674 df-tms 23675 df-cncf 24241 df-limc 25230 df-dv 25231 df-log 25912 df-logb 26115

This theorem is referenced by: aks4d1p1p5 40532

W3C validator