opnmbllem0 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > opnmbllem0		Structured version Visualization version GIF version

Theorem opnmbllem0 35813

Description: Lemma for ismblfin 35818; could also be used to shorten proof of opnmbllem 24765. (Contributed by Brendan Leahy, 13-Jul-2018.)

**Assertion**
Ref	Expression
opnmbllem0	⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)

Distinct variable group: 𝑥,𝑦,𝑧,𝐴

Proof of Theorem opnmbllem0 Dummy variables 𝑛 𝑟 𝑠 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6774	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → ([,]‘𝑧) = ([,]‘𝑤))
2	1	sseq1d 3952	. . . . . . 7 ⊢ (𝑧 = 𝑤 → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴))
3	2	elrab 3624	. . . . . 6 ⊢ (𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘𝑤) ⊆ 𝐴))
4		simprr 770	. . . . . . 7 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ⊆ 𝐴)
5		fvex 6787	. . . . . . . 8 ⊢ ([,]‘𝑤) ∈ V
6	5	elpw 4537	. . . . . . 7 ⊢ (([,]‘𝑤) ∈ 𝒫 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴)
7	4, 6	sylibr 233	. . . . . 6 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ∈ 𝒫 𝐴)
8	3, 7	sylan2b 594	. . . . 5 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) → ([,]‘𝑤) ∈ 𝒫 𝐴)
9	8	ralrimiva 3103	. . . 4 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)
10		iccf 13180	. . . . . 6 ⊢ [,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^
11		ffun 6603	. . . . . 6 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → Fun [,])
12	10, 11	ax-mp 5	. . . . 5 ⊢ Fun [,]
13		ssrab2 4013	. . . . . . 7 ⊢ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
14		oveq1 7282	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑟 → (𝑥 / (2↑𝑦)) = (𝑟 / (2↑𝑦)))
15		oveq1 7282	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → (𝑥 + 1) = (𝑟 + 1))
16	15	oveq1d 7290	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑟 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑟 + 1) / (2↑𝑦)))
17	14, 16	opeq12d 4812	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑟 → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ = ⟨(𝑟 / (2↑𝑦)), ((𝑟 + 1) / (2↑𝑦))⟩)
18		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑠 → (2↑𝑦) = (2↑𝑠))
19	18	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑠 → (𝑟 / (2↑𝑦)) = (𝑟 / (2↑𝑠)))
20	18	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑠 → ((𝑟 + 1) / (2↑𝑦)) = ((𝑟 + 1) / (2↑𝑠)))
21	19, 20	opeq12d 4812	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑠 → ⟨(𝑟 / (2↑𝑦)), ((𝑟 + 1) / (2↑𝑦))⟩ = ⟨(𝑟 / (2↑𝑠)), ((𝑟 + 1) / (2↑𝑠))⟩)
22	17, 21	cbvmpov 7370	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑟 ∈ ℤ, 𝑠 ∈ ℕ₀ ↦ ⟨(𝑟 / (2↑𝑠)), ((𝑟 + 1) / (2↑𝑠))⟩)
23	22	dyadf 24755	. . . . . . . . 9 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶( ≤ ∩ (ℝ × ℝ))
24		frn 6607	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶( ≤ ∩ (ℝ × ℝ)) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ ( ≤ ∩ (ℝ × ℝ)))
25	23, 24	ax-mp 5	. . . . . . . 8 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ ( ≤ ∩ (ℝ × ℝ))
26		inss2 4163	. . . . . . . . 9 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
27		rexpssxrxp 11020	. . . . . . . . 9 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
28	26, 27	sstri 3930	. . . . . . . 8 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
29	25, 28	sstri 3930	. . . . . . 7 ⊢ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ^* × ℝ^*)
30	13, 29	sstri 3930	. . . . . 6 ⊢ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ (ℝ^* × ℝ^*)
31	10	fdmi 6612	. . . . . 6 ⊢ dom [,] = (ℝ^* × ℝ^*)
32	30, 31	sseqtrri 3958	. . . . 5 ⊢ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]
33		funimass4 6834	. . . . 5 ⊢ ((Fun [,] ∧ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴))
34	12, 32, 33	mp2an 689	. . . 4 ⊢ (([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)
35	9, 34	sylibr 233	. . 3 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴)
36		sspwuni 5029	. . 3 ⊢ (([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴)
37	35, 36	sylib 217	. 2 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴)
38		eqid 2738	. . . . 5 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
39	38	rexmet 23954	. . . 4 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
40		eqid 2738	. . . . . 6 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
41	38, 40	tgioo 23959	. . . . 5 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
42	41	mopni2 23649	. . . 4 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ⁺ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴)
43	39, 42	mp3an1 1447	. . 3 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ⁺ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴)
44		elssuni 4871	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ⊆ ∪ (topGen‘ran (,)))
45		uniretop 23926	. . . . . . . . 9 ⊢ ℝ = ∪ (topGen‘ran (,))
46	44, 45	sseqtrrdi 3972	. . . . . . . 8 ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ⊆ ℝ)
47	46	sselda 3921	. . . . . . 7 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ)
48		rpre 12738	. . . . . . 7 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
49	38	bl2ioo 23955	. . . . . . 7 ⊢ ((𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
50	47, 48, 49	syl2an 596	. . . . . 6 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
51	50	sseq1d 3952	. . . . 5 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → ((𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 ↔ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴))
52		2re 12047	. . . . . . . . 9 ⊢ 2 ∈ ℝ
53		1lt2 12144	. . . . . . . . 9 ⊢ 1 < 2
54		expnlbnd 13948	. . . . . . . . 9 ⊢ ((𝑟 ∈ ℝ⁺ ∧ 2 ∈ ℝ ∧ 1 < 2) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
55	52, 53, 54	mp3an23 1452	. . . . . . . 8 ⊢ (𝑟 ∈ ℝ⁺ → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
56	55	ad2antrl 725	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
57	47	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ℝ)
58		2nn 12046	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
59		nnnn0 12240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
60	59	ad2antrl 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑛 ∈ ℕ₀)
61		nnexpcl 13795	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
62	58, 60, 61	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℕ)
63	62	nnred 11988	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℝ)
64	57, 63	remulcld 11005	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) ∈ ℝ)
65		fllelt 13517	. . . . . . . . . . . . 13 ⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)))
66	64, 65	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)))
67	66	simpld 495	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))
68		reflcl 13516	. . . . . . . . . . . . 13 ⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ)
69	64, 68	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ)
70	62	nngt0d 12022	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 0 < (2↑𝑛))
71		ledivmul2 11854	. . . . . . . . . . . 12 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))))
72	69, 57, 63, 70, 71	syl112anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))))
73	67, 72	mpbird 256	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤)
74		peano2re 11148	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ)
75	69, 74	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ)
76	75, 62	nndivred 12027	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈ ℝ)
77	66	simprd 496	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))
78		ltmuldiv 11848	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
79	57, 75, 63, 70, 78	syl112anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
80	77, 79	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))
81	57, 76, 80	ltled 11123	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))
82	69, 62	nndivred 12027	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ)
83		elicc2 13144	. . . . . . . . . . 11 ⊢ ((((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈ ℝ) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))))
84	82, 76, 83	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))))
85	57, 73, 81, 84	mpbir3and 1341	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
86	64	flcld 13518	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ)
87	22	dyadval 24756	. . . . . . . . . . . 12 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) = ⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
88	86, 60, 87	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) = ⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
89	88	fveq2d 6778	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) = ([,]‘⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩))
90		df-ov 7278	. . . . . . . . . 10 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) = ([,]‘⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
91	89, 90	eqtr4di 2796	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
92	85, 91	eleqtrrd 2842	. . . . . . . 8 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)))
93		ffn 6600	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ₀)⟶( ≤ ∩ (ℝ × ℝ)) → (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) Fn (ℤ × ℕ₀))
94	23, 93	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) Fn (ℤ × ℕ₀)
95		fnovrn 7447	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) Fn (ℤ × ℕ₀) ∧ (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
96	94, 95	mp3an1 1447	. . . . . . . . . . 11 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
97	86, 60, 96	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
98		simplrl 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ⁺)
99	98	rpred 12772	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ)
100	57, 99	resubcld 11403	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈ ℝ)
101	100	rexrd 11025	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈ ℝ^*)
102	57, 99	readdcld 11004	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ)
103	102	rexrd 11025	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ^*)
104	82, 99	readdcld 11004	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟) ∈ ℝ)
105	69	recnd 11003	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℂ)
106		1cnd 10970	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 1 ∈ ℂ)
107	63	recnd 11003	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℂ)
108	62	nnne0d 12023	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ≠ 0)
109	105, 106, 107, 108	divdird 11789	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))))
110	62	nnrecred 12024	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) ∈ ℝ)
111		simprr 770	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) < 𝑟)
112	110, 99, 82, 111	ltadd2dd 11134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
113	109, 112	eqbrtrd 5096	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
114	57, 76, 104, 80, 113	lttrd 11136	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
115	57, 99, 82	ltsubaddd 11571	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)))
116	114, 115	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)))
117	57, 110	readdcld 11004	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) ∈ ℝ)
118	82, 57, 110, 73	leadd1dd 11589	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) ≤ (𝑤 + (1 / (2↑𝑛))))
119	109, 118	eqbrtrd 5096	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ≤ (𝑤 + (1 / (2↑𝑛))))
120	110, 99, 57, 111	ltadd2dd 11134	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) < (𝑤 + 𝑟))
121	76, 117, 102, 119, 120	lelttrd 11133	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))
122		iccssioo 13148	. . . . . . . . . . . . 13 ⊢ ((((𝑤 − 𝑟) ∈ ℝ^* ∧ (𝑤 + 𝑟) ∈ ℝ^*) ∧ ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
123	101, 103, 116, 121, 122	syl22anc 836	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
124	91, 123	eqsstrd 3959	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
125		simplrr 775	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)
126	124, 125	sstrd 3931	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ 𝐴)
127		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) → ([,]‘𝑧) = ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)))
128	127	sseq1d 3952	. . . . . . . . . . 11 ⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ 𝐴))
129	128	elrab 3624	. . . . . . . . . 10 ⊢ (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ 𝐴))
130	97, 126, 129	sylanbrc 583	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})
131		funfvima2 7107	. . . . . . . . . 10 ⊢ ((Fun [,] ∧ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
132	12, 32, 131	mp2an 689	. . . . . . . . 9 ⊢ (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
133	130, 132	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
134		elunii 4844	. . . . . . . 8 ⊢ ((𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
135	92, 133, 134	syl2anc 584	. . . . . . 7 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
136	56, 135	rexlimddv 3220	. . . . . 6 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
137	136	expr 457	. . . . 5 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → (((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
138	51, 137	sylbid 239	. . . 4 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → ((𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
139	138	rexlimdva 3213	. . 3 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → (∃𝑟 ∈ ℝ⁺ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
140	43, 139	mpd 15	. 2 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
141	37, 140	eqelssd 3942	1 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 {crab 3068 ∩ cin 3886 ⊆ wss 3887 𝒫 cpw 4533 ⟨cop 4567 ∪ cuni 4839 class class class wbr 5074 × cxp 5587 dom cdm 5589 ran crn 5590 ↾ cres 5591 “ cima 5592 ∘ ccom 5593 Fun wfun 6427 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ∈ cmpo 7277 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 ℕcn 11973 2c2 12028 ℕ₀cn0 12233 ℤcz 12319 ℝ⁺crp 12730 (,)cioo 13079 [,]cicc 13082 ⌊cfl 13510 ↑cexp 13782 abscabs 14945 topGenctg 17148 ∞Metcxmet 20582 ballcbl 20584 MetOpencmopn 20587

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-icc 13086 df-fl 13512 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-topgen 17154 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-top 22043 df-topon 22060 df-bases 22096

This theorem is referenced by: mblfinlem1 35814 mblfinlem2 35815

W3C validator