limcimolemlt - Intuitionistic Logic Explorer

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

Theorem limcimolemlt 15169

Description: Lemma for limcimo 15170. (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 15036	. . . 4 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		ax-resscn 8019	. . . . . . 7 ⊢ ℝ ⊆ ℂ
3		sseq1 3216	. . . . . . 7 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 168	. . . . . 6 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5	4	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℝ) → 𝑆 ⊆ ℂ)
6		eqimss 3247	. . . . . 6 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
7	6	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
8		limcimo.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
9		elpri 3656	. . . . . 6 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ))
11	5, 7, 10	mpjaodan 800	. . . 4 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
12		xmetres2 14884	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
13	1, 11, 12	sylancr 414	. . 3 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
14		limcimo.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾_t 𝑆))
15		eqid 2205	. . . . . 6 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
16		limcflfcntop.k	. . . . . 6 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
17		eqid 2205	. . . . . 6 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
18	15, 16, 17	metrest 15011	. . . . 5 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
19	1, 11, 18	sylancr 414	. . . 4 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
20	14, 19	eleqtrd 2284	. . 3 ⊢ (𝜑 → 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
21		limcimo.bc	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
22		limcimo.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
23		limcimo.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ℝ⁺)
24		rpmincl 11582	. . . 4 ⊢ ((𝐷 ∈ ℝ⁺ ∧ 𝐺 ∈ ℝ⁺) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
25	22, 23, 24	syl2anc 411	. . 3 ⊢ (𝜑 → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
26	17	mopni3 14989	. . 3 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) ∧ 𝐵 ∈ 𝐶) ∧ inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺) → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
27	13, 20, 21, 25, 26	syl31anc 1253	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
28		limcimo.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝐹 lim_ℂ 𝐵))
29		limcrcl 15163	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐹 lim_ℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
30	28, 29	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
31	30	simp1d 1012	. . . . . . 7 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
32	30	simp2d 1013	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
33		limcimo.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
34	31, 32, 33	ellimc3ap 15166	. . . . . 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 15166	. . . . . 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 4048	. . . . . 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 2284	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ ℝ)
52		simprl 529	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ⁺)
53	52	rphalfcld 9833	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ⁺)
54	53	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ⁺)
55	54	rpred 9820	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ)
56	51, 55	readdcld 8104	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ ℝ)
57	56, 50	eleqtrrd 2285	. . . . . . . . . . . 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 9822	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℂ)
61	58, 60	addcld 8094	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
62		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝑆 = ℂ)
63	61, 62	eleqtrrd 2285	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
64	10	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑆 = ℝ ∨ 𝑆 = ℂ))
65	57, 63, 64	mpjaodan 800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
66	48, 65	ovresd 6089	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))))
67	33	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ ℂ)
68	53	rpcnd 9822	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℂ)
69	67, 68	addcld 8094	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
70		eqid 2205	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) = (abs ∘ − )
71	70	cnmetdval 15034	. . . . . . . . . . 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 8416	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (𝐵 − (𝐵 + (𝑟 / 2))))
74	67	subidd 8373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − 𝐵) = 0)
75	74	oveq1d 5961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (0 − (𝑟 / 2)))
76	73, 75	eqtr3d 2240	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − (𝐵 + (𝑟 / 2))) = (0 − (𝑟 / 2)))
77	76	fveq2d 5582	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘(0 − (𝑟 / 2))))
78		0cnd 8067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ∈ ℂ)
79	78, 68	abssubd 11537	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(0 − (𝑟 / 2))) = (abs‘((𝑟 / 2) − 0)))
80	77, 79	eqtrd 2238	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘((𝑟 / 2) − 0)))
81	68	subid1d 8374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝑟 / 2) − 0) = (𝑟 / 2))
82	81	fveq2d 5582	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝑟 / 2) − 0)) = (abs‘(𝑟 / 2)))
83	53	rpred 9820	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ)
84	53	rpge0d 9824	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ≤ (𝑟 / 2))
85	83, 84	absidd 11511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
86	80, 82, 85	3eqtrd 2242	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (𝑟 / 2))
87	66, 72, 86	3eqtrd 2242	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝑟 / 2))
88		rphalflt 9807	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
89	88	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) < 𝑟)
90	87, 89	eqbrtrd 4067	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟)
91	13	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
92		rpxr 9785	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
93	92	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ^*)
94		elbl2 14898	. . . . . . . . 9 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑟 ∈ ℝ^*) ∧ (𝐵 ∈ 𝑆 ∧ (𝐵 + (𝑟 / 2)) ∈ 𝑆)) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
95	91, 93, 48, 65, 94	syl22anc 1251	. . . . . . . 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 3194	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐶)
98	53	rpap0d 9826	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) # 0)
99	67, 67	negsubdid 8400	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = (-𝐵 + 𝐵))
100	74	negeqd 8269	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = -0)
101		neg0 8320	. . . . . . . . . . . 12 ⊢ -0 = 0
102	100, 101	eqtrdi 2254	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = 0)
103	99, 102	eqtr3d 2240	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + 𝐵) = 0)
104	103	oveq1d 5961	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (0 + (𝑟 / 2)))
105	67	negcld 8372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -𝐵 ∈ ℂ)
106	105, 67, 68	addassd 8097	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (-𝐵 + (𝐵 + (𝑟 / 2))))
107	68	addlidd 8224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (0 + (𝑟 / 2)) = (𝑟 / 2))
108	104, 106, 107	3eqtr3d 2246	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) = (𝑟 / 2))
109	98, 108, 103	3brtr4d 4077	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵))
110		apadd2 8684	. . . . . . . 8 ⊢ (((𝐵 + (𝑟 / 2)) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℂ) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
111	69, 67, 105, 110	syl3anc 1250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
112	109, 111	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) # 𝐵)
113	45, 97, 112	elrabd 2931	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵})
114		limcimo.ca	. . . . . . 7 ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
115	114	sseld 3192	. . . . . 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 5718	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐹‘(𝐵 + (𝑟 / 2))) ∈ ℂ)
119	37, 42	subcld 8385	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑋 − 𝑌) ∈ ℂ)
120	119	abscld 11525	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) ∈ ℝ)
121	37, 118	abssubd 11537	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) = (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)))
122	69, 67	subcld 8385	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) ∈ ℂ)
123	122	abscld 11525	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) ∈ ℝ)
124	52	rpred 9820	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ)
125	22	rpred 9820	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
126	125	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐷 ∈ ℝ)
127	67, 68	pncan2d 8387	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) = (𝑟 / 2))
128	127	fveq2d 5582	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (abs‘(𝑟 / 2)))
129	128, 85	eqtrd 2238	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (𝑟 / 2))
130	129, 89	eqbrtrd 4067	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝑟)
131	23	rpred 9820	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℝ)
132	131	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐺 ∈ ℝ)
133		mincl 11575	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
134	126, 132, 133	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
135		simprrl 539	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < inf({𝐷, 𝐺}, ℝ, < ))
136		min1inf 11576	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
137	126, 132, 136	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
138	124, 134, 126, 135, 137	ltletrd 8498	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐷)
139	123, 124, 126, 130, 138	lttrd 8200	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)
140		breq1 4048	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (𝑧 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
141		fvoveq1 5969	. . . . . . . . 9 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑧 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
142	141	breq1d 4055	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑧 − 𝐵)) < 𝐷 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷))
143	140, 142	anbi12d 473	. . . . . . 7 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)))
144	143	imbrov2fvoveq 5971	. . . . . 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 2882	. . . . 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 4067	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) < ((abs‘(𝑋 − 𝑌)) / 2))
150		min2inf 11577	. . . . . . 7 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
151	126, 132, 150	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
152	124, 134, 132, 135, 151	ltletrd 8498	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐺)
153	123, 124, 132, 130, 152	lttrd 8200	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)
154		breq1 4048	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (𝑤 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
155		fvoveq1 5969	. . . . . . . 8 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑤 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
156	155	breq1d 4055	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑤 − 𝐵)) < 𝐺 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺))
157	154, 156	anbi12d 473	. . . . . 6 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)))
158	157	imbrov2fvoveq 5971	. . . . 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 2882	. . . 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 11545	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
164	27, 163	rexlimddv 2628	1 ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 ∧ w3a 981 = wceq 1373 ∈ wcel 2176 ∀wral 2484 ∃wrex 2485 {crab 2488 ⊆ wss 3166 {cpr 3634 class class class wbr 4045 × cxp 4674 dom cdm 4676 ↾ cres 4678 ∘ ccom 4680 ⟶wf 5268 ‘cfv 5272 (class class class)co 5946 infcinf 7087 ℂcc 7925 ℝcr 7926 0cc0 7927 + caddc 7930 ℝ^*cxr 8108 < clt 8109 ≤ cle 8110 − cmin 8245 -cneg 8246 # cap 8656 / cdiv 8747 2c2 9089 ℝ⁺crp 9777 abscabs 11341 ↾_t crest 13104 ∞Metcxmet 14331 ballcbl 14333 MetOpencmopn 14336 lim_ℂ climc 15159

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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4160 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-iinf 4637 ax-cnex 8018 ax-resscn 8019 ax-1cn 8020 ax-1re 8021 ax-icn 8022 ax-addcl 8023 ax-addrcl 8024 ax-mulcl 8025 ax-mulrcl 8026 ax-addcom 8027 ax-mulcom 8028 ax-addass 8029 ax-mulass 8030 ax-distr 8031 ax-i2m1 8032 ax-0lt1 8033 ax-1rid 8034 ax-0id 8035 ax-rnegex 8036 ax-precex 8037 ax-cnre 8038 ax-pre-ltirr 8039 ax-pre-ltwlin 8040 ax-pre-lttrn 8041 ax-pre-apti 8042 ax-pre-ltadd 8043 ax-pre-mulgt0 8044 ax-pre-mulext 8045 ax-arch 8046 ax-caucvg 8047

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4046 df-opab 4107 df-mpt 4108 df-tr 4144 df-id 4341 df-po 4344 df-iso 4345 df-iord 4414 df-on 4416 df-ilim 4417 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-isom 5281 df-riota 5901 df-ov 5949 df-oprab 5950 df-mpo 5951 df-1st 6228 df-2nd 6229 df-recs 6393 df-frec 6479 df-map 6739 df-pm 6740 df-sup 7088 df-inf 7089 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114 df-le 8115 df-sub 8247 df-neg 8248 df-reap 8650 df-ap 8657 df-div 8748 df-inn 9039 df-2 9097 df-3 9098 df-4 9099 df-n0 9298 df-z 9375 df-uz 9651 df-q 9743 df-rp 9778 df-xneg 9896 df-xadd 9897 df-seqfrec 10595 df-exp 10686 df-cj 11186 df-re 11187 df-im 11188 df-rsqrt 11342 df-abs 11343 df-rest 13106 df-topgen 13125 df-psmet 14338 df-xmet 14339 df-met 14340 df-bl 14341 df-mopn 14342 df-top 14503 df-topon 14516 df-bases 14548 df-limced 15161

This theorem is referenced by: limcimo 15170

W3C validator