limcimolemlt - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > limcimolemlt		GIF version

Theorem limcimolemlt 13702

Description: Lemma for limcimo 13703. (Contributed by Jim Kingdon, 3-Jul-2023.)

**Hypotheses**
Ref	Expression
limcflf.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
limcflf.a	⊢ (𝜑 → 𝐴 ⊆ ℂ)
limcimo.b	⊢ (𝜑 → 𝐵 ∈ ℂ)
limcimo.bc	⊢ (𝜑 → 𝐵 ∈ 𝐶)
limcimo.bs	⊢ (𝜑 → 𝐵 ∈ 𝑆)
limcimo.c	⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾_t 𝑆))
limcimo.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
limcimo.ca	⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
limcflfcntop.k	⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
limcimo.d	⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
limcimo.x	⊢ (𝜑 → 𝑋 ∈ (𝐹 lim_ℂ 𝐵))
limcimo.y	⊢ (𝜑 → 𝑌 ∈ (𝐹 lim_ℂ 𝐵))
limcimo.z	⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
limcimo.g	⊢ (𝜑 → 𝐺 ∈ ℝ⁺)
limcimo.w	⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))

**Assertion**
Ref	Expression
limcimolemlt	⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))

Distinct variable groups: 𝑤,𝐴 𝑧,𝐴 𝐵,𝑞 𝑤,𝐵 𝑧,𝐵 𝐶,𝑞 𝑧,𝐷 𝑤,𝐹 𝑧,𝐹 𝑤,𝐺 𝑤,𝑋 𝑧,𝑋 𝑤,𝑌 𝑧,𝑌 Allowed substitution hints: 𝜑(𝑧,𝑤,𝑞) 𝐴(𝑞) 𝐶(𝑧,𝑤) 𝐷(𝑤,𝑞) 𝑆(𝑧,𝑤,𝑞) 𝐹(𝑞) 𝐺(𝑧,𝑞) 𝐾(𝑧,𝑤,𝑞) 𝑋(𝑞) 𝑌(𝑞)

Proof of Theorem limcimolemlt Dummy variables 𝑎 𝑏 𝑐 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnxmet 13600	. . . 4 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		ax-resscn 7878	. . . . . . 7 ⊢ ℝ ⊆ ℂ
3		sseq1 3176	. . . . . . 7 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 168	. . . . . 6 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5	4	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℝ) → 𝑆 ⊆ ℂ)
6		eqimss 3207	. . . . . 6 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
7	6	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
8		limcimo.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
9		elpri 3612	. . . . . 6 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ))
11	5, 7, 10	mpjaodan 798	. . . 4 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
12		xmetres2 13448	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
13	1, 11, 12	sylancr 414	. . 3 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
14		limcimo.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾_t 𝑆))
15		eqid 2175	. . . . . 6 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
16		limcflfcntop.k	. . . . . 6 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
17		eqid 2175	. . . . . 6 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
18	15, 16, 17	metrest 13575	. . . . 5 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
19	1, 11, 18	sylancr 414	. . . 4 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
20	14, 19	eleqtrd 2254	. . 3 ⊢ (𝜑 → 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
21		limcimo.bc	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
22		limcimo.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
23		limcimo.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ℝ⁺)
24		rpmincl 11212	. . . 4 ⊢ ((𝐷 ∈ ℝ⁺ ∧ 𝐺 ∈ ℝ⁺) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
25	22, 23, 24	syl2anc 411	. . 3 ⊢ (𝜑 → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
26	17	mopni3 13553	. . 3 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) ∧ 𝐵 ∈ 𝐶) ∧ inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺) → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
27	13, 20, 21, 25, 26	syl31anc 1241	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
28		limcimo.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝐹 lim_ℂ 𝐵))
29		limcrcl 13696	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐹 lim_ℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
30	28, 29	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
31	30	simp1d 1009	. . . . . . 7 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
32	30	simp2d 1010	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
33		limcimo.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
34	31, 32, 33	ellimc3ap 13699	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝑋 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑋)) < 𝑎))))
35	28, 34	mpbid 147	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑋)) < 𝑎)))
36	35	simpld 112	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
37	36	adantr 276	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑋 ∈ ℂ)
38		limcimo.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝐹 lim_ℂ 𝐵))
39	31, 32, 33	ellimc3ap 13699	. . . . . 6 ⊢ (𝜑 → (𝑌 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝑌 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑌)) < 𝑎))))
40	38, 39	mpbid 147	. . . . 5 ⊢ (𝜑 → (𝑌 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑌)) < 𝑎)))
41	40	simpld 112	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℂ)
42	41	adantr 276	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑌 ∈ ℂ)
43		limcflf.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
44	43	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐹:𝐴⟶ℂ)
45		breq1 4001	. . . . . 6 ⊢ (𝑞 = (𝐵 + (𝑟 / 2)) → (𝑞 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
46		simprrr 540	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶)
47		limcimo.bs	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
48	47	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ 𝑆)
49	47	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ 𝑆)
50		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝑆 = ℝ)
51	49, 50	eleqtrd 2254	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ ℝ)
52		simprl 529	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ⁺)
53	52	rphalfcld 9678	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ⁺)
54	53	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ⁺)
55	54	rpred 9665	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ)
56	51, 55	readdcld 7961	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ ℝ)
57	56, 50	eleqtrrd 2255	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
58	33	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝐵 ∈ ℂ)
59	53	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℝ⁺)
60	59	rpcnd 9667	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℂ)
61	58, 60	addcld 7951	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
62		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝑆 = ℂ)
63	61, 62	eleqtrrd 2255	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
64	10	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑆 = ℝ ∨ 𝑆 = ℂ))
65	57, 63, 64	mpjaodan 798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
66	48, 65	ovresd 6005	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))))
67	33	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ ℂ)
68	53	rpcnd 9667	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℂ)
69	67, 68	addcld 7951	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
70		eqid 2175	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) = (abs ∘ − )
71	70	cnmetdval 13598	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℂ ∧ (𝐵 + (𝑟 / 2)) ∈ ℂ) → (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))) = (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))))
72	67, 69, 71	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))) = (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))))
73	67, 67, 68	subsub4d 8273	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (𝐵 − (𝐵 + (𝑟 / 2))))
74	67	subidd 8230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − 𝐵) = 0)
75	74	oveq1d 5880	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (0 − (𝑟 / 2)))
76	73, 75	eqtr3d 2210	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − (𝐵 + (𝑟 / 2))) = (0 − (𝑟 / 2)))
77	76	fveq2d 5511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘(0 − (𝑟 / 2))))
78		0cnd 7925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ∈ ℂ)
79	78, 68	abssubd 11168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(0 − (𝑟 / 2))) = (abs‘((𝑟 / 2) − 0)))
80	77, 79	eqtrd 2208	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘((𝑟 / 2) − 0)))
81	68	subid1d 8231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝑟 / 2) − 0) = (𝑟 / 2))
82	81	fveq2d 5511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝑟 / 2) − 0)) = (abs‘(𝑟 / 2)))
83	53	rpred 9665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ)
84	53	rpge0d 9669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ≤ (𝑟 / 2))
85	83, 84	absidd 11142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
86	80, 82, 85	3eqtrd 2212	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (𝑟 / 2))
87	66, 72, 86	3eqtrd 2212	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝑟 / 2))
88		rphalflt 9652	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
89	88	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) < 𝑟)
90	87, 89	eqbrtrd 4020	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟)
91	13	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
92		rpxr 9630	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
93	92	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ^*)
94		elbl2 13462	. . . . . . . . 9 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑟 ∈ ℝ^*) ∧ (𝐵 ∈ 𝑆 ∧ (𝐵 + (𝑟 / 2)) ∈ 𝑆)) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
95	91, 93, 48, 65, 94	syl22anc 1239	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
96	90, 95	mpbird 167	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟))
97	46, 96	sseldd 3154	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐶)
98	53	rpap0d 9671	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) # 0)
99	67, 67	negsubdid 8257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = (-𝐵 + 𝐵))
100	74	negeqd 8126	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = -0)
101		neg0 8177	. . . . . . . . . . . 12 ⊢ -0 = 0
102	100, 101	eqtrdi 2224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = 0)
103	99, 102	eqtr3d 2210	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + 𝐵) = 0)
104	103	oveq1d 5880	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (0 + (𝑟 / 2)))
105	67	negcld 8229	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -𝐵 ∈ ℂ)
106	105, 67, 68	addassd 7954	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (-𝐵 + (𝐵 + (𝑟 / 2))))
107	68	addid2d 8081	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (0 + (𝑟 / 2)) = (𝑟 / 2))
108	104, 106, 107	3eqtr3d 2216	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) = (𝑟 / 2))
109	98, 108, 103	3brtr4d 4030	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵))
110		apadd2 8540	. . . . . . . 8 ⊢ (((𝐵 + (𝑟 / 2)) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℂ) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
111	69, 67, 105, 110	syl3anc 1238	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
112	109, 111	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) # 𝐵)
113	45, 97, 112	elrabd 2893	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵})
114		limcimo.ca	. . . . . . 7 ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
115	114	sseld 3152	. . . . . 6 ⊢ (𝜑 → ((𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} → (𝐵 + (𝑟 / 2)) ∈ 𝐴))
116	115	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} → (𝐵 + (𝑟 / 2)) ∈ 𝐴))
117	113, 116	mpd 13	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐴)
118	44, 117	ffvelcdmd 5644	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐹‘(𝐵 + (𝑟 / 2))) ∈ ℂ)
119	37, 42	subcld 8242	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑋 − 𝑌) ∈ ℂ)
120	119	abscld 11156	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) ∈ ℝ)
121	37, 118	abssubd 11168	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) = (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)))
122	69, 67	subcld 8242	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) ∈ ℂ)
123	122	abscld 11156	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) ∈ ℝ)
124	52	rpred 9665	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ)
125	22	rpred 9665	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
126	125	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐷 ∈ ℝ)
127	67, 68	pncan2d 8244	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) = (𝑟 / 2))
128	127	fveq2d 5511	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (abs‘(𝑟 / 2)))
129	128, 85	eqtrd 2208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (𝑟 / 2))
130	129, 89	eqbrtrd 4020	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝑟)
131	23	rpred 9665	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℝ)
132	131	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐺 ∈ ℝ)
133		mincl 11205	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
134	126, 132, 133	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
135		simprrl 539	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < inf({𝐷, 𝐺}, ℝ, < ))
136		min1inf 11206	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
137	126, 132, 136	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
138	124, 134, 126, 135, 137	ltletrd 8354	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐷)
139	123, 124, 126, 130, 138	lttrd 8057	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)
140		breq1 4001	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (𝑧 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
141		fvoveq1 5888	. . . . . . . . 9 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑧 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
142	141	breq1d 4008	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑧 − 𝐵)) < 𝐷 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷))
143	140, 142	anbi12d 473	. . . . . . 7 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)))
144	143	imbrov2fvoveq 5890	. . . . . 6 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)) ↔ (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2))))
145		limcimo.z	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
146	145	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
147	144, 146, 117	rspcdva 2844	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
148	112, 139, 147	mp2and 433	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2))
149	121, 148	eqbrtrd 4020	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) < ((abs‘(𝑋 − 𝑌)) / 2))
150		min2inf 11207	. . . . . . 7 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
151	126, 132, 150	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
152	124, 134, 132, 135, 151	ltletrd 8354	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐺)
153	123, 124, 132, 130, 152	lttrd 8057	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)
154		breq1 4001	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (𝑤 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
155		fvoveq1 5888	. . . . . . . 8 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑤 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
156	155	breq1d 4008	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑤 − 𝐵)) < 𝐺 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺))
157	154, 156	anbi12d 473	. . . . . 6 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)))
158	157	imbrov2fvoveq 5890	. . . . 5 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)) ↔ (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2))))
159		limcimo.w	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
160	159	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
161	158, 160, 117	rspcdva 2844	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
162	112, 153, 161	mp2and 433	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2))
163	37, 42, 118, 120, 149, 162	abs3lemd 11176	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
164	27, 163	rexlimddv 2597	1 ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 ∧ w3a 978 = wceq 1353 ∈ wcel 2146 ∀wral 2453 ∃wrex 2454 {crab 2457 ⊆ wss 3127 {cpr 3590 class class class wbr 3998 × cxp 4618 dom cdm 4620 ↾ cres 4622 ∘ ccom 4624 ⟶wf 5204 ‘cfv 5208 (class class class)co 5865 infcinf 6972 ℂcc 7784 ℝcr 7785 0cc0 7786 + caddc 7789 ℝ^*cxr 7965 < clt 7966 ≤ cle 7967 − cmin 8102 -cneg 8103 # cap 8512 / cdiv 8601 2c2 8941 ℝ⁺crp 9622 abscabs 10972 ↾_t crest 12608 ∞Metcxmet 13049 ballcbl 13051 MetOpencmopn 13054 lim_ℂ climc 13692

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-13 2148 ax-14 2149 ax-ext 2157 ax-coll 4113 ax-sep 4116 ax-nul 4124 ax-pow 4169 ax-pr 4203 ax-un 4427 ax-setind 4530 ax-iinf 4581 ax-cnex 7877 ax-resscn 7878 ax-1cn 7879 ax-1re 7880 ax-icn 7881 ax-addcl 7882 ax-addrcl 7883 ax-mulcl 7884 ax-mulrcl 7885 ax-addcom 7886 ax-mulcom 7887 ax-addass 7888 ax-mulass 7889 ax-distr 7890 ax-i2m1 7891 ax-0lt1 7892 ax-1rid 7893 ax-0id 7894 ax-rnegex 7895 ax-precex 7896 ax-cnre 7897 ax-pre-ltirr 7898 ax-pre-ltwlin 7899 ax-pre-lttrn 7900 ax-pre-apti 7901 ax-pre-ltadd 7902 ax-pre-mulgt0 7903 ax-pre-mulext 7904 ax-arch 7905 ax-caucvg 7906

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1459 df-sb 1761 df-eu 2027 df-mo 2028 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ne 2346 df-nel 2441 df-ral 2458 df-rex 2459 df-reu 2460 df-rmo 2461 df-rab 2462 df-v 2737 df-sbc 2961 df-csb 3056 df-dif 3129 df-un 3131 df-in 3133 df-ss 3140 df-nul 3421 df-if 3533 df-pw 3574 df-sn 3595 df-pr 3596 df-op 3598 df-uni 3806 df-int 3841 df-iun 3884 df-br 3999 df-opab 4060 df-mpt 4061 df-tr 4097 df-id 4287 df-po 4290 df-iso 4291 df-iord 4360 df-on 4362 df-ilim 4363 df-suc 4365 df-iom 4584 df-xp 4626 df-rel 4627 df-cnv 4628 df-co 4629 df-dm 4630 df-rn 4631 df-res 4632 df-ima 4633 df-iota 5170 df-fun 5210 df-fn 5211 df-f 5212 df-f1 5213 df-fo 5214 df-f1o 5215 df-fv 5216 df-isom 5217 df-riota 5821 df-ov 5868 df-oprab 5869 df-mpo 5870 df-1st 6131 df-2nd 6132 df-recs 6296 df-frec 6382 df-map 6640 df-pm 6641 df-sup 6973 df-inf 6974 df-pnf 7968 df-mnf 7969 df-xr 7970 df-ltxr 7971 df-le 7972 df-sub 8104 df-neg 8105 df-reap 8506 df-ap 8513 df-div 8602 df-inn 8891 df-2 8949 df-3 8950 df-4 8951 df-n0 9148 df-z 9225 df-uz 9500 df-q 9591 df-rp 9623 df-xneg 9741 df-xadd 9742 df-seqfrec 10414 df-exp 10488 df-cj 10817 df-re 10818 df-im 10819 df-rsqrt 10973 df-abs 10974 df-rest 12610 df-topgen 12629 df-psmet 13056 df-xmet 13057 df-met 13058 df-bl 13059 df-mopn 13060 df-top 13065 df-topon 13078 df-bases 13110 df-limced 13694

This theorem is referenced by: limcimo 13703

W3C validator