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 24737

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 11158	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		rexr 11158	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
3		icc0 13293	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
5	4	biimpar 477	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅)
6	5	fveq2d 6826	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = ((int‘(topGen‘ran (,)))‘∅))
7		retop 24676	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
8		ntr0 22996	. . . . . . 7 ⊢ ((topGen‘ran (,)) ∈ Top → ((int‘(topGen‘ran (,)))‘∅) = ∅)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ((int‘(topGen‘ran (,)))‘∅) = ∅
10		0ss 4347	. . . . . 6 ⊢ ∅ ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵))
11	9, 10	eqsstri 3976	. . . . 5 ⊢ ((int‘(topGen‘ran (,)))‘∅) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵))
12	6, 11	eqsstrdi 3974	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
13		iccssre 13329	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
14		uniretop 24677	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	ntrss2 22972	. . . . . . 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 4105	. . . . . . . 8 ⊢ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})
20		prunioo 13381	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
21	19, 20	eqtrid 2778	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
22	21	3expa 1118	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
23	18, 22	sylan 580	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
24	17, 23	sseqtrrd 3967	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
25		simpr 484	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
26		simpl 482	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
27	12, 24, 25, 26	ltlecasei 11221	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
28	14	ntropn 22964	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)))
29	7, 13, 28	sylancr 587	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)))
30		eqid 2731	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	rexmet 24706	. . . . . . . . 9 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32		eqid 2731	. . . . . . . . . . 11 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
33	30, 32	tgioo 24711	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
34	33	mopni2 24408	. . . . . . . . 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 12919	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ⁺)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
40	37, 39	ltsubrpd 12966	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) < 𝐴)
41	39	rpred 12934	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
42	37, 41	resubcld 11545	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ ℝ)
43	42, 37	ltnled 11260	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐴 − (𝑥 / 2))))
44	40, 43	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ 𝐴 ≤ (𝐴 − (𝑥 / 2)))
45		rpre 12899	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
46	45	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
47		rphalflt 12921	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
48	47	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) < 𝑥)
49	41, 46, 37, 48	ltsub2dd 11730	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)))
50	37, 46	readdcld 11141	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 + 𝑥) ∈ ℝ)
51		ltaddrp 12929	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝑥))
52	37, 51	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝑥))
53	42, 37, 50, 40, 52	lttrd 11274	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))
54	37, 46	resubcld 11545	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) ∈ ℝ)
55	54	rexrd 11162	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) ∈ ℝ^*)
56	50	rexrd 11162	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 + 𝑥) ∈ ℝ^*)
57		elioo2 13286	. . . . . . . . . . . . . 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 24707	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
61	37, 46, 60	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
62	59, 61	eleqtrrd 2834	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥))
63		ssel 3923	. . . . . . . . . . 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 3928	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵)))
67		elicc2 13311	. . . . . . . . . . . 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 3127	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ¬ ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
74	36, 73	pm2.65da 816	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
75	33	mopni2 24408	. . . . . . . . 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 12967	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐵 < (𝐵 + (𝑥 / 2)))
81	79	rpred 12934	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
82	78, 81	readdcld 11141	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ ℝ)
83	78, 82	ltnled 11260	. . . . . . . . . 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 11545	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) ∈ ℝ)
87		ltsubrp 12928	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < 𝐵)
88	78, 87	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < 𝐵)
89	86, 78, 82, 88, 80	lttrd 11274	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)))
90	47	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) < 𝑥)
91	81, 85, 78, 90	ltadd2dd 11272	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))
92	86	rexrd 11162	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) ∈ ℝ^*)
93	78, 85	readdcld 11141	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + 𝑥) ∈ ℝ)
94	93	rexrd 11162	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + 𝑥) ∈ ℝ^*)
95		elioo2 13286	. . . . . . . . . . . . . 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 24707	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
99	78, 85, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
100	97, 99	eleqtrrd 2834	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥))
101		ssel 3923	. . . . . . . . . . 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 3928	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵 + (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵)))
105		elicc2 13311	. . . . . . . . . . . 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 3127	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ¬ ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
112	77, 111	pm2.65da 816	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
113		eleq1 2819	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
114	113	notbid 318	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ ¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
115		eleq1 2819	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
116	115	notbid 318	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
117	114, 116	ralprg 4646	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ (¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∧ ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))))
118	74, 112, 117	mpbir2and 713	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
119		disjr 4398	. . . . 5 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅ ↔ ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
120	118, 119	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅)
121		disjssun 4415	. . . 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 24680	. . . 4 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
125		ioossicc 13333	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
126	14	ssntr 22973	. . . 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 3947	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 {cpr 4575 class class class wbr 5089 × cxp 5612 ran crn 5615 ↾ cres 5616 ∘ ccom 5618 ‘cfv 6481 (class class class)co 7346 ℝcr 11005 + caddc 11009 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 − cmin 11344 / cdiv 11774 2c2 12180 ℝ⁺crp 12890 (,)cioo 13245 [,]cicc 13248 abscabs 15141 topGenctg 17341 ∞Metcxmet 21276 ballcbl 21278 MetOpencmopn 21281 Topctop 22808 intcnt 22932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-sup 9326 df-inf 9327 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-q 12847 df-rp 12891 df-xneg 13011 df-xadd 13012 df-xmul 13013 df-ioo 13249 df-ico 13251 df-icc 13252 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-topgen 17347 df-psmet 21283 df-xmet 21284 df-met 21285 df-bl 21286 df-mopn 21287 df-top 22809 df-topon 22826 df-bases 22861 df-ntr 22935

This theorem is referenced by: dvmptresicc 25844 rolle 25921 cmvth 25922 cmvthOLD 25923 mvth 25924 dvlip 25925 dvlipcn 25926 dvlip2 25927 c1liplem1 25928 dvgt0lem1 25934 dvle 25939 lhop1lem 25945 dvcnvrelem1 25949 dvcvx 25952 dvfsumabs 25956 ftc1cn 25977 ftc2 25978 ftc2ditglem 25979 itgparts 25981 itgsubstlem 25982 itgpowd 25984 efcvx 26386 pige3ALT 26456 logccv 26599 lgamgulmlem2 26967 ftc2re 34611 ftc1cnnc 37742 ftc2nc 37752 areacirc 37763 dvrelog2 42167 lhe4.4ex1a 44432 dvbdfbdioolem1 46036 itgsin0pilem1 46058 itgsinexplem1 46062 itgcoscmulx 46077 itgiccshift 46088 itgperiod 46089 itgsbtaddcnst 46090 dirkeritg 46210 fourierdlem39 46254 fourierdlem73 46287 etransclem46 46388

W3C validator