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 23423

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 10681	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		rexr 10681	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
3		icc0 12780	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
4	1, 2, 3	syl2an 597	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
5	4	biimpar 480	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅)
6	5	fveq2d 6669	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = ((int‘(topGen‘ran (,)))‘∅))
7		retop 23364	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
8		ntr0 21683	. . . . . . 7 ⊢ ((topGen‘ran (,)) ∈ Top → ((int‘(topGen‘ran (,)))‘∅) = ∅)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ((int‘(topGen‘ran (,)))‘∅) = ∅
10		0ss 4350	. . . . . 6 ⊢ ∅ ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵))
11	9, 10	eqsstri 4001	. . . . 5 ⊢ ((int‘(topGen‘ran (,)))‘∅) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵))
12	6, 11	eqsstrdi 4021	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
13		iccssre 12812	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
14		uniretop 23365	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	ntrss2 21659	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
16	7, 13, 15	sylancr 589	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
17	16	adantr 483	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
18	1, 2	anim12i 614	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
19		uncom 4129	. . . . . . . 8 ⊢ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})
20		prunioo 12861	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
21	19, 20	syl5eq 2868	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
22	21	3expa 1114	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
23	18, 22	sylan 582	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)) = (𝐴[,]𝐵))
24	17, 23	sseqtrrd 4008	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
25		simpr 487	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
26		simpl 485	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
27	12, 24, 25, 26	ltlecasei 10742	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ ({𝐴, 𝐵} ∪ (𝐴(,)𝐵)))
28	14	ntropn 21651	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)))
29	7, 13, 28	sylancr 589	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)))
30		eqid 2821	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	rexmet 23393	. . . . . . . . 9 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32		eqid 2821	. . . . . . . . . . 11 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
33	30, 32	tgioo 23398	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
34	33	mopni2 23097	. . . . . . . . 9 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
35	31, 34	mp3an1 1444	. . . . . . . 8 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
36	29, 35	sylan 582	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
37	26	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
38		rphalfcl 12410	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) ∈ ℝ⁺)
39	38	adantl 484	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
40	37, 39	ltsubrpd 12457	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) < 𝐴)
41	39	rpred 12425	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
42	37, 41	resubcld 11062	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ ℝ)
43	42, 37	ltnled 10781	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) < 𝐴 ↔ ¬ 𝐴 ≤ (𝐴 − (𝑥 / 2))))
44	40, 43	mpbid 234	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ 𝐴 ≤ (𝐴 − (𝑥 / 2)))
45		rpre 12391	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
46	45	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
47		rphalflt 12412	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 / 2) < 𝑥)
48	47	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) < 𝑥)
49	41, 46, 37, 48	ltsub2dd 11247	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)))
50	37, 46	readdcld 10664	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 + 𝑥) ∈ ℝ)
51		ltaddrp 12420	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝑥))
52	37, 51	sylancom 590	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝑥))
53	42, 37, 50, 40, 52	lttrd 10795	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))
54	37, 46	resubcld 11062	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) ∈ ℝ)
55	54	rexrd 10685	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − 𝑥) ∈ ℝ^*)
56	50	rexrd 10685	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 + 𝑥) ∈ ℝ^*)
57		elioo2 12773	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑥) ∈ ℝ^* ∧ (𝐴 + 𝑥) ∈ ℝ^*) → ((𝐴 − (𝑥 / 2)) ∈ ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)) ↔ ((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))))
58	55, 56, 57	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) ∈ ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)) ↔ ((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ (𝐴 − 𝑥) < (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) < (𝐴 + 𝑥))))
59	42, 49, 53, 58	mpbir3and 1338	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
60	30	bl2ioo 23394	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
61	37, 46, 60	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐴 − 𝑥)(,)(𝐴 + 𝑥)))
62	59, 61	eleqtrrd 2916	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐴 − (𝑥 / 2)) ∈ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥))
63		ssel 3961	. . . . . . . . . . 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 724	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
66	65	sseld 3966	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐴 − (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵)))
67		elicc2 12795	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) ≤ 𝐵)))
68		simp2 1133	. . . . . . . . . . . 12 ⊢ (((𝐴 − (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐴 − (𝑥 / 2)) ∧ (𝐴 − (𝑥 / 2)) ≤ 𝐵) → 𝐴 ≤ (𝐴 − (𝑥 / 2)))
69	67, 68	syl6bi 255	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − (𝑥 / 2)) ∈ (𝐴[,]𝐵) → 𝐴 ≤ (𝐴 − (𝑥 / 2))))
70	69	ad2antrr 724	. . . . . . . . . 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 200	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
73	72	nrexdv 3270	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ¬ ∃𝑥 ∈ ℝ⁺ (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
74	36, 73	pm2.65da 815	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
75	33	mopni2 23097	. . . . . . . . 9 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
76	31, 75	mp3an1 1444	. . . . . . . 8 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
77	29, 76	sylan 582	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
78	25	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐵 ∈ ℝ)
79	38	adantl 484	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
80	78, 79	ltaddrpd 12458	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝐵 < (𝐵 + (𝑥 / 2)))
81	79	rpred 12425	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ)
82	78, 81	readdcld 10664	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ ℝ)
83	78, 82	ltnled 10781	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 < (𝐵 + (𝑥 / 2)) ↔ ¬ (𝐵 + (𝑥 / 2)) ≤ 𝐵))
84	80, 83	mpbid 234	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ (𝐵 + (𝑥 / 2)) ≤ 𝐵)
85	45	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
86	78, 85	resubcld 11062	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) ∈ ℝ)
87		ltsubrp 12419	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < 𝐵)
88	78, 87	sylancom 590	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < 𝐵)
89	86, 78, 82, 88, 80	lttrd 10795	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)))
90	47	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) < 𝑥)
91	81, 85, 78, 90	ltadd2dd 10793	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))
92	86	rexrd 10685	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 − 𝑥) ∈ ℝ^*)
93	78, 85	readdcld 10664	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + 𝑥) ∈ ℝ)
94	93	rexrd 10685	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + 𝑥) ∈ ℝ^*)
95		elioo2 12773	. . . . . . . . . . . . . 14 ⊢ (((𝐵 − 𝑥) ∈ ℝ^* ∧ (𝐵 + 𝑥) ∈ ℝ^*) → ((𝐵 + (𝑥 / 2)) ∈ ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)) ↔ ((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))))
96	92, 94, 95	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵 + (𝑥 / 2)) ∈ ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)) ↔ ((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ (𝐵 − 𝑥) < (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) < (𝐵 + 𝑥))))
97	82, 89, 91, 96	mpbir3and 1338	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
98	30	bl2ioo 23394	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
99	78, 85, 98	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) = ((𝐵 − 𝑥)(,)(𝐵 + 𝑥)))
100	97, 99	eleqtrrd 2916	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → (𝐵 + (𝑥 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥))
101		ssel 3961	. . . . . . . . . . 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 724	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴[,]𝐵))
104	103	sseld 3966	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ((𝐵 + (𝑥 / 2)) ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) → (𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵)))
105		elicc2 12795	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) ≤ 𝐵)))
106		simp3 1134	. . . . . . . . . . . 12 ⊢ (((𝐵 + (𝑥 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝐵 + (𝑥 / 2)) ∧ (𝐵 + (𝑥 / 2)) ≤ 𝐵) → (𝐵 + (𝑥 / 2)) ≤ 𝐵)
107	105, 106	syl6bi 255	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 + (𝑥 / 2)) ∈ (𝐴[,]𝐵) → (𝐵 + (𝑥 / 2)) ≤ 𝐵))
108	107	ad2antrr 724	. . . . . . . . . 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 200	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) ∧ 𝑥 ∈ ℝ⁺) → ¬ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
111	110	nrexdv 3270	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) → ¬ ∃𝑥 ∈ ℝ⁺ (𝐵(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑥) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
112	77, 111	pm2.65da 815	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
113		eleq1 2900	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
114	113	notbid 320	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ ¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
115		eleq1 2900	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
116	115	notbid 320	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
117	114, 116	ralprg 4626	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ↔ (¬ 𝐴 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∧ ¬ 𝐵 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))))
118	74, 112, 117	mpbir2and 711	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
119		disjr 4400	. . . . 5 ⊢ ((((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅ ↔ ∀𝑥 ∈ {𝐴, 𝐵} ¬ 𝑥 ∈ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
120	118, 119	sylibr 236	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ∩ {𝐴, 𝐵}) = ∅)
121		disjssun 4417	. . . 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 234	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) ⊆ (𝐴(,)𝐵))
124		iooretop 23368	. . . 4 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
125		ioossicc 12816	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
126	14	ssntr 21660	. . . 4 ⊢ ((((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
127	124, 125, 126	mpanr12 703	. . 3 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → (𝐴(,)𝐵) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
128	7, 13, 127	sylancr 589	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
129	123, 128	eqssd 3984	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 ∪ cun 3934 ∩ cin 3935 ⊆ wss 3936 ∅c0 4291 {cpr 4563 class class class wbr 5059 × cxp 5548 ran crn 5551 ↾ cres 5552 ∘ ccom 5554 ‘cfv 6350 (class class class)co 7150 ℝcr 10530 + caddc 10534 ℝ^*cxr 10668 < clt 10669 ≤ cle 10670 − cmin 10864 / cdiv 11291 2c2 11686 ℝ⁺crp 12383 (,)cioo 12732 [,]cicc 12735 abscabs 14587 topGenctg 16705 ∞Metcxmet 20524 ballcbl 20526 MetOpencmopn 20529 Topctop 21495 intcnt 21619

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-sup 8900 df-inf 8901 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-q 12343 df-rp 12384 df-xneg 12501 df-xadd 12502 df-xmul 12503 df-ioo 12736 df-ico 12738 df-icc 12739 df-seq 13364 df-exp 13424 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-topgen 16711 df-psmet 20531 df-xmet 20532 df-met 20533 df-bl 20534 df-mopn 20535 df-top 21496 df-topon 21513 df-bases 21548 df-ntr 21622

This theorem is referenced by: rolle 24581 cmvth 24582 mvth 24583 dvlip 24584 dvlipcn 24585 dvlip2 24586 c1liplem1 24587 dvgt0lem1 24593 dvle 24598 lhop1lem 24604 dvcnvrelem1 24608 dvcvx 24611 dvfsumabs 24614 ftc1cn 24634 ftc2 24635 ftc2ditglem 24636 itgparts 24638 itgsubstlem 24639 efcvx 25031 pige3ALT 25099 logccv 25240 lgamgulmlem2 25601 ftc2re 31864 ftc1cnnc 34960 ftc2nc 34970 areacirc 34981 itgpowd 39814 lhe4.4ex1a 40654 dvmptresicc 42196 dvbdfbdioolem1 42205 itgsin0pilem1 42227 itgsinexplem1 42231 itgcoscmulx 42246 itgiccshift 42257 itgperiod 42258 itgsbtaddcnst 42259 dirkeritg 42380 fourierdlem39 42424 fourierdlem73 42457 etransclem46 42558

W3C validator