iccntr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > iccntr		Structured version Visualization version GIF version

Theorem iccntr 24743

Description: The interior of a closed interval in the standard topology on ℝ is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.)

**Assertion**
Ref	Expression
iccntr	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))

Proof of Theorem iccntr Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexr 11196	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		rexr 11196	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
3		icc0 13330	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
5	4	biimpar 477	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅)
6	5	fveq2d 6844	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = ((int‘(topGen‘ran (,)))‘∅))
7		retop 24682	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
8		ntr0 23001	. . . . . . 7 ⊢ ((topGen‘ran (,)) ∈ Top → ((int‘(topGen‘ran (,)))‘∅) = ∅)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ((int‘(topGen‘ran (,)))‘∅) = ∅
10		0ss 4359	. . . . . 6 ⊢ ∅ ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵))
11	9, 10	eqsstri 3990	. . . . 5 ⊢ ((int‘(topGen‘ran (,)))‘∅) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵))
12	6, 11	eqsstrdi 3988	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
13		iccssre 13366	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
14		uniretop 24683	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	ntrss2 22977	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
16	7, 13, 15	sylancr 587	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
17	16	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
18	1, 2	anim12i 613	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
19		uncom 4117	. . . . . . . 8 ⊢ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})
20		prunioo 13418	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
21	19, 20	eqtrid 2776	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
22	21	3expa 1118	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
23	18, 22	sylan 580	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
24	17, 23	sseqtrrd 3981	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
25		simpr 484	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
26		simpl 482	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
27	12, 24, 25, 26	ltlecasei 11258	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
28	14	ntropn 22969	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)))
29	7, 13, 28	sylancr 587	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)))
30		eqid 2729	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	rexmet 24712	. . . . . . . . 9 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32		eqid 2729	. . . . . . . . . . 11 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
33	30, 32	tgioo 24717	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
34	33	mopni2 24414	. . . . . . . . 9 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
35	31, 34	mp3an1 1450	. . . . . . . 8 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
36	29, 35	sylan 580	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
37	26	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
38		rphalfcl 12956	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ⁺)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
40	37, 39	ltsubrpd 13003	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) < 𝐴)
41	39	rpred 12971	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
42	37, 41	resubcld 11582	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ ℝ)
43	42, 37	ltnled 11297	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐴 − (𝑥 / 2))))
44	40, 43	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ 𝐴 ≤ (𝐴 − (𝑥 / 2)))
45		rpre 12936	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
46	45	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
47		rphalflt 12958	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
48	47	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) < 𝑥)
49	41, 46, 37, 48	ltsub2dd 11767	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)))
50	37, 46	readdcld 11179	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 + 𝑥) ∈ ℝ)
51		ltaddrp 12966	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝑥))
52	37, 51	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝑥))
53	42, 37, 50, 40, 52	lttrd 11311	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))
54	37, 46	resubcld 11582	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) ∈ ℝ)
55	54	rexrd 11200	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) ∈ ℝ^*)
56	50	rexrd 11200	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 + 𝑥) ∈ ℝ^*)
57		elioo2 13323	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑥) ∈ ℝ^* ∧ (𝐴 + 𝑥) ∈ ℝ^*) → ((𝐴 − (𝑥 / 2)) ∈ ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)) ↔ ((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))))
58	55, 56, 57	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) ∈ ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)) ↔ ((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))))
59	42, 49, 53, 58	mpbir3and 1343	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
60	30	bl2ioo 24713	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
61	37, 46, 60	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
62	59, 61	eleqtrrd 2831	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥))
63		ssel 3937	. . . . . . . . . . 11 ⊢ ((𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → ((𝐴 − (𝑥 / 2)) ∈ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) → (𝐴 − (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
64	62, 63	syl5com 31	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐴 − (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
65	16	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
66	65	sseld 3942	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵)))
67		elicc2 13348	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) ≤ 𝐵)))
68		simp2 1137	. . . . . . . . . . . 12 ⊢ (((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) ≤ 𝐵) → 𝐴 ≤ (𝐴 − (𝑥 / 2)))
69	67, 68	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵) → 𝐴 ≤ (𝐴 − (𝑥 / 2))))
70	69	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵) → 𝐴 ≤ (𝐴 − (𝑥 / 2))))
71	64, 66, 70	3syld 60	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → 𝐴 ≤ (𝐴 − (𝑥 / 2))))
72	44, 71	mtod 198	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
73	72	nrexdv 3128	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ¬ ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
74	36, 73	pm2.65da 816	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
75	33	mopni2 24414	. . . . . . . . 9 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
76	31, 75	mp3an1 1450	. . . . . . . 8 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
77	29, 76	sylan 580	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
78	25	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐵 ∈ ℝ)
79	38	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
80	78, 79	ltaddrpd 13004	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐵 < (𝐵 + (𝑥 / 2)))
81	79	rpred 12971	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
82	78, 81	readdcld 11179	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ ℝ)
83	78, 82	ltnled 11297	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 < (𝐵 + (𝑥 / 2)) ↔ ¬ (𝐵 + (𝑥 / 2)) ≤ 𝐵))
84	80, 83	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ (𝐵 + (𝑥 / 2)) ≤ 𝐵)
85	45	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
86	78, 85	resubcld 11582	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) ∈ ℝ)
87		ltsubrp 12965	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < 𝐵)
88	78, 87	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < 𝐵)
89	86, 78, 82, 88, 80	lttrd 11311	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)))
90	47	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) < 𝑥)
91	81, 85, 78, 90	ltadd2dd 11309	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))
92	86	rexrd 11200	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) ∈ ℝ^*)
93	78, 85	readdcld 11179	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + 𝑥) ∈ ℝ)
94	93	rexrd 11200	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + 𝑥) ∈ ℝ^*)
95		elioo2 13323	. . . . . . . . . . . . . 14 ⊢ (((𝐵 − 𝑥) ∈ ℝ^* ∧ (𝐵 + 𝑥) ∈ ℝ^*) → ((𝐵 + (𝑥 / 2)) ∈ ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)) ↔ ((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))))
96	92, 94, 95	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵 + (𝑥 / 2)) ∈ ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)) ↔ ((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))))
97	82, 89, 91, 96	mpbir3and 1343	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
98	30	bl2ioo 24713	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
99	78, 85, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
100	97, 99	eleqtrrd 2831	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥))
101		ssel 3937	. . . . . . . . . . 11 ⊢ ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → ((𝐵 + (𝑥 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) → (𝐵 + (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
102	100, 101	syl5com 31	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐵 + (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
103	16	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
104	103	sseld 3942	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵 + (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵)))
105		elicc2 13348	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) ≤ 𝐵)))
106		simp3 1138	. . . . . . . . . . . 12 ⊢ (((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) ≤ 𝐵) → (𝐵 + (𝑥 / 2)) ≤ 𝐵)
107	105, 106	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵) → (𝐵 + (𝑥 / 2)) ≤ 𝐵))
108	107	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵) → (𝐵 + (𝑥 / 2)) ≤ 𝐵))
109	102, 104, 108	3syld 60	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐵 + (𝑥 / 2)) ≤ 𝐵))
110	84, 109	mtod 198	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
111	110	nrexdv 3128	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ¬ ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
112	77, 111	pm2.65da 816	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
113		eleq1 2816	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
114	113	notbid 318	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ ¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
115		eleq1 2816	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
116	115	notbid 318	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
117	114, 116	ralprg 4656	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ (¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∧ ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))))
118	74, 112, 117	mpbir2and 713	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
119		disjr 4410	. . . . 5 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅ ↔ ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
120	118, 119	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅)
121		disjssun 4427	. . . 4 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅ → (((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) ↔ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴(,)𝐵)))
122	120, 121	syl 17	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) ↔ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴(,)𝐵)))
123	27, 122	mpbid 232	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴(,)𝐵))
124		iooretop 24686	. . . 4 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
125		ioossicc 13370	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
126	14	ssntr 22978	. . . 4 ⊢ ((((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
127	124, 125, 126	mpanr12 705	. . 3 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → (𝐴(,)𝐵) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
128	7, 13, 127	sylancr 587	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
129	123, 128	eqssd 3961	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 {cpr 4587 class class class wbr 5102 × cxp 5629 ran crn 5632 ↾ cres 5633 ∘ ccom 5635 ‘cfv 6499 (class class class)co 7369 ℝcr 11043 + caddc 11047 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 − cmin 11381 / cdiv 11811 2c2 12217 ℝ⁺crp 12927 (,)cioo 13282 [,]cicc 13285 abscabs 15176 topGenctg 17376 ∞Metcxmet 21281 ballcbl 21283 MetOpencmopn 21286 Topctop 22813 intcnt 22937

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-sup 9369 df-inf 9370 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ico 13288 df-icc 13289 df-seq 13943 df-exp 14003 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-topgen 17382 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-top 22814 df-topon 22831 df-bases 22866 df-ntr 22940

This theorem is referenced by: dvmptresicc 25850 rolle 25927 cmvth 25928 cmvthOLD 25929 mvth 25930 dvlip 25931 dvlipcn 25932 dvlip2 25933 c1liplem1 25934 dvgt0lem1 25940 dvle 25945 lhop1lem 25951 dvcnvrelem1 25955 dvcvx 25958 dvfsumabs 25962 ftc1cn 25983 ftc2 25984 ftc2ditglem 25985 itgparts 25987 itgsubstlem 25988 itgpowd 25990 efcvx 26392 pige3ALT 26462 logccv 26605 lgamgulmlem2 26973 ftc2re 34582 ftc1cnnc 37679 ftc2nc 37689 areacirc 37700 dvrelog2 42045 lhe4.4ex1a 44311 dvbdfbdioolem1 45919 itgsin0pilem1 45941 itgsinexplem1 45945 itgcoscmulx 45960 itgiccshift 45971 itgperiod 45972 itgsbtaddcnst 45973 dirkeritg 46093 fourierdlem39 46137 fourierdlem73 46170 etransclem46 46271

W3C validator