limcimolemlt - Intuitionistic Logic Explorer

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

Theorem limcimolemlt 14900

Description: Lemma for limcimo 14901. (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 14767	. . . 4 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		ax-resscn 7971	. . . . . . 7 ⊢ ℝ ⊆ ℂ
3		sseq1 3206	. . . . . . 7 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 168	. . . . . 6 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5	4	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℝ) → 𝑆 ⊆ ℂ)
6		eqimss 3237	. . . . . 6 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
7	6	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
8		limcimo.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
9		elpri 3645	. . . . . 6 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ))
11	5, 7, 10	mpjaodan 799	. . . 4 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
12		xmetres2 14615	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
13	1, 11, 12	sylancr 414	. . 3 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
14		limcimo.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾_t 𝑆))
15		eqid 2196	. . . . . 6 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
16		limcflfcntop.k	. . . . . 6 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
17		eqid 2196	. . . . . 6 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
18	15, 16, 17	metrest 14742	. . . . 5 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
19	1, 11, 18	sylancr 414	. . . 4 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
20	14, 19	eleqtrd 2275	. . 3 ⊢ (𝜑 → 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
21		limcimo.bc	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
22		limcimo.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
23		limcimo.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ℝ⁺)
24		rpmincl 11403	. . . 4 ⊢ ((𝐷 ∈ ℝ⁺ ∧ 𝐺 ∈ ℝ⁺) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
25	22, 23, 24	syl2anc 411	. . 3 ⊢ (𝜑 → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
26	17	mopni3 14720	. . 3 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) ∧ 𝐵 ∈ 𝐶) ∧ inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺) → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
27	13, 20, 21, 25, 26	syl31anc 1252	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
28		limcimo.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝐹 lim_ℂ 𝐵))
29		limcrcl 14894	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐹 lim_ℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
30	28, 29	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
31	30	simp1d 1011	. . . . . . 7 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
32	30	simp2d 1012	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
33		limcimo.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
34	31, 32, 33	ellimc3ap 14897	. . . . . 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 14897	. . . . . 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 4036	. . . . . 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 2275	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ ℝ)
52		simprl 529	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ⁺)
53	52	rphalfcld 9784	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ⁺)
54	53	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ⁺)
55	54	rpred 9771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ)
56	51, 55	readdcld 8056	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ ℝ)
57	56, 50	eleqtrrd 2276	. . . . . . . . . . . 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 9773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℂ)
61	58, 60	addcld 8046	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
62		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝑆 = ℂ)
63	61, 62	eleqtrrd 2276	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
64	10	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑆 = ℝ ∨ 𝑆 = ℂ))
65	57, 63, 64	mpjaodan 799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
66	48, 65	ovresd 6064	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))))
67	33	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ ℂ)
68	53	rpcnd 9773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℂ)
69	67, 68	addcld 8046	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
70		eqid 2196	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) = (abs ∘ − )
71	70	cnmetdval 14765	. . . . . . . . . . 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 8368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (𝐵 − (𝐵 + (𝑟 / 2))))
74	67	subidd 8325	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − 𝐵) = 0)
75	74	oveq1d 5937	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (0 − (𝑟 / 2)))
76	73, 75	eqtr3d 2231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − (𝐵 + (𝑟 / 2))) = (0 − (𝑟 / 2)))
77	76	fveq2d 5562	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘(0 − (𝑟 / 2))))
78		0cnd 8019	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ∈ ℂ)
79	78, 68	abssubd 11358	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(0 − (𝑟 / 2))) = (abs‘((𝑟 / 2) − 0)))
80	77, 79	eqtrd 2229	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘((𝑟 / 2) − 0)))
81	68	subid1d 8326	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝑟 / 2) − 0) = (𝑟 / 2))
82	81	fveq2d 5562	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝑟 / 2) − 0)) = (abs‘(𝑟 / 2)))
83	53	rpred 9771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ)
84	53	rpge0d 9775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ≤ (𝑟 / 2))
85	83, 84	absidd 11332	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
86	80, 82, 85	3eqtrd 2233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (𝑟 / 2))
87	66, 72, 86	3eqtrd 2233	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝑟 / 2))
88		rphalflt 9758	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
89	88	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) < 𝑟)
90	87, 89	eqbrtrd 4055	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟)
91	13	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
92		rpxr 9736	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
93	92	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ^*)
94		elbl2 14629	. . . . . . . . 9 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑟 ∈ ℝ^*) ∧ (𝐵 ∈ 𝑆 ∧ (𝐵 + (𝑟 / 2)) ∈ 𝑆)) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
95	91, 93, 48, 65, 94	syl22anc 1250	. . . . . . . 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 3184	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐶)
98	53	rpap0d 9777	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) # 0)
99	67, 67	negsubdid 8352	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = (-𝐵 + 𝐵))
100	74	negeqd 8221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = -0)
101		neg0 8272	. . . . . . . . . . . 12 ⊢ -0 = 0
102	100, 101	eqtrdi 2245	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = 0)
103	99, 102	eqtr3d 2231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + 𝐵) = 0)
104	103	oveq1d 5937	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (0 + (𝑟 / 2)))
105	67	negcld 8324	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -𝐵 ∈ ℂ)
106	105, 67, 68	addassd 8049	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (-𝐵 + (𝐵 + (𝑟 / 2))))
107	68	addlidd 8176	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (0 + (𝑟 / 2)) = (𝑟 / 2))
108	104, 106, 107	3eqtr3d 2237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) = (𝑟 / 2))
109	98, 108, 103	3brtr4d 4065	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵))
110		apadd2 8636	. . . . . . . 8 ⊢ (((𝐵 + (𝑟 / 2)) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℂ) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
111	69, 67, 105, 110	syl3anc 1249	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
112	109, 111	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) # 𝐵)
113	45, 97, 112	elrabd 2922	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵})
114		limcimo.ca	. . . . . . 7 ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
115	114	sseld 3182	. . . . . 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 5698	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐹‘(𝐵 + (𝑟 / 2))) ∈ ℂ)
119	37, 42	subcld 8337	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑋 − 𝑌) ∈ ℂ)
120	119	abscld 11346	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) ∈ ℝ)
121	37, 118	abssubd 11358	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) = (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)))
122	69, 67	subcld 8337	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) ∈ ℂ)
123	122	abscld 11346	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) ∈ ℝ)
124	52	rpred 9771	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ)
125	22	rpred 9771	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
126	125	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐷 ∈ ℝ)
127	67, 68	pncan2d 8339	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) = (𝑟 / 2))
128	127	fveq2d 5562	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (abs‘(𝑟 / 2)))
129	128, 85	eqtrd 2229	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (𝑟 / 2))
130	129, 89	eqbrtrd 4055	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝑟)
131	23	rpred 9771	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℝ)
132	131	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐺 ∈ ℝ)
133		mincl 11396	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
134	126, 132, 133	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
135		simprrl 539	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < inf({𝐷, 𝐺}, ℝ, < ))
136		min1inf 11397	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
137	126, 132, 136	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
138	124, 134, 126, 135, 137	ltletrd 8450	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐷)
139	123, 124, 126, 130, 138	lttrd 8152	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)
140		breq1 4036	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (𝑧 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
141		fvoveq1 5945	. . . . . . . . 9 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑧 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
142	141	breq1d 4043	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑧 − 𝐵)) < 𝐷 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷))
143	140, 142	anbi12d 473	. . . . . . 7 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)))
144	143	imbrov2fvoveq 5947	. . . . . 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 2873	. . . . 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 4055	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) < ((abs‘(𝑋 − 𝑌)) / 2))
150		min2inf 11398	. . . . . . 7 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
151	126, 132, 150	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
152	124, 134, 132, 135, 151	ltletrd 8450	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐺)
153	123, 124, 132, 130, 152	lttrd 8152	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)
154		breq1 4036	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (𝑤 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
155		fvoveq1 5945	. . . . . . . 8 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑤 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
156	155	breq1d 4043	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑤 − 𝐵)) < 𝐺 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺))
157	154, 156	anbi12d 473	. . . . . 6 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)))
158	157	imbrov2fvoveq 5947	. . . . 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 2873	. . . 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 11366	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
164	27, 163	rexlimddv 2619	1 ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ∀wral 2475 ∃wrex 2476 {crab 2479 ⊆ wss 3157 {cpr 3623 class class class wbr 4033 × cxp 4661 dom cdm 4663 ↾ cres 4665 ∘ ccom 4667 ⟶wf 5254 ‘cfv 5258 (class class class)co 5922 infcinf 7049 ℂcc 7877 ℝcr 7878 0cc0 7879 + caddc 7882 ℝ^*cxr 8060 < clt 8061 ≤ cle 8062 − cmin 8197 -cneg 8198 # cap 8608 / cdiv 8699 2c2 9041 ℝ⁺crp 9728 abscabs 11162 ↾_t crest 12910 ∞Metcxmet 14092 ballcbl 14094 MetOpencmopn 14097 lim_ℂ climc 14890

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-map 6709 df-pm 6710 df-sup 7050 df-inf 7051 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-xneg 9847 df-xadd 9848 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-rest 12912 df-topgen 12931 df-psmet 14099 df-xmet 14100 df-met 14101 df-bl 14102 df-mopn 14103 df-top 14234 df-topon 14247 df-bases 14279 df-limced 14892

This theorem is referenced by: limcimo 14901

W3C validator