limcimolemlt - Intuitionistic Logic Explorer

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

Theorem limcimolemlt 12802

Description: Lemma for limcimo 12803. (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 12700	. . . 4 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		ax-resscn 7712	. . . . . . 7 ⊢ ℝ ⊆ ℂ
3		sseq1 3120	. . . . . . 7 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 167	. . . . . 6 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5	4	adantl 275	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℝ) → 𝑆 ⊆ ℂ)
6		eqimss 3151	. . . . . 6 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
7	6	adantl 275	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
8		limcimo.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
9		elpri 3550	. . . . . 6 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ))
11	5, 7, 10	mpjaodan 787	. . . 4 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
12		xmetres2 12548	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
13	1, 11, 12	sylancr 410	. . 3 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
14		limcimo.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾_t 𝑆))
15		eqid 2139	. . . . . 6 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
16		limcflfcntop.k	. . . . . 6 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
17		eqid 2139	. . . . . 6 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
18	15, 16, 17	metrest 12675	. . . . 5 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
19	1, 11, 18	sylancr 410	. . . 4 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
20	14, 19	eleqtrd 2218	. . 3 ⊢ (𝜑 → 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
21		limcimo.bc	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
22		limcimo.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
23		limcimo.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ℝ⁺)
24		rpmincl 11009	. . . 4 ⊢ ((𝐷 ∈ ℝ⁺ ∧ 𝐺 ∈ ℝ⁺) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
25	22, 23, 24	syl2anc 408	. . 3 ⊢ (𝜑 → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
26	17	mopni3 12653	. . 3 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) ∧ 𝐵 ∈ 𝐶) ∧ inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺) → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
27	13, 20, 21, 25, 26	syl31anc 1219	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
28		limcimo.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝐹 lim_ℂ 𝐵))
29		limcrcl 12796	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐹 lim_ℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
30	28, 29	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
31	30	simp1d 993	. . . . . . 7 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
32	30	simp2d 994	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
33		limcimo.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
34	31, 32, 33	ellimc3ap 12799	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝑋 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑋)) < 𝑎))))
35	28, 34	mpbid 146	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑋)) < 𝑎)))
36	35	simpld 111	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
37	36	adantr 274	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑋 ∈ ℂ)
38		limcimo.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝐹 lim_ℂ 𝐵))
39	31, 32, 33	ellimc3ap 12799	. . . . . 6 ⊢ (𝜑 → (𝑌 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝑌 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑌)) < 𝑎))))
40	38, 39	mpbid 146	. . . . 5 ⊢ (𝜑 → (𝑌 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ dom 𝐹((𝑐 # 𝐵 ∧ (abs‘(𝑐 − 𝐵)) < 𝑏) → (abs‘((𝐹‘𝑐) − 𝑌)) < 𝑎)))
41	40	simpld 111	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℂ)
42	41	adantr 274	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑌 ∈ ℂ)
43		limcflf.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
44	43	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐹:𝐴⟶ℂ)
45		breq1 3932	. . . . . 6 ⊢ (𝑞 = (𝐵 + (𝑟 / 2)) → (𝑞 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
46		simprrr 529	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶)
47		limcimo.bs	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
48	47	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ 𝑆)
49	47	ad2antrr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ 𝑆)
50		simpr 109	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝑆 = ℝ)
51	49, 50	eleqtrd 2218	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ ℝ)
52		simprl 520	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ⁺)
53	52	rphalfcld 9496	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ⁺)
54	53	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ⁺)
55	54	rpred 9483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ)
56	51, 55	readdcld 7795	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ ℝ)
57	56, 50	eleqtrrd 2219	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
58	33	ad2antrr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝐵 ∈ ℂ)
59	53	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℝ⁺)
60	59	rpcnd 9485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℂ)
61	58, 60	addcld 7785	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
62		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝑆 = ℂ)
63	61, 62	eleqtrrd 2219	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
64	10	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑆 = ℝ ∨ 𝑆 = ℂ))
65	57, 63, 64	mpjaodan 787	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
66	48, 65	ovresd 5911	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))))
67	33	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ ℂ)
68	53	rpcnd 9485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℂ)
69	67, 68	addcld 7785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
70		eqid 2139	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) = (abs ∘ − )
71	70	cnmetdval 12698	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℂ ∧ (𝐵 + (𝑟 / 2)) ∈ ℂ) → (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))) = (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))))
72	67, 69, 71	syl2anc 408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))) = (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))))
73	67, 67, 68	subsub4d 8104	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (𝐵 − (𝐵 + (𝑟 / 2))))
74	67	subidd 8061	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − 𝐵) = 0)
75	74	oveq1d 5789	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (0 − (𝑟 / 2)))
76	73, 75	eqtr3d 2174	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − (𝐵 + (𝑟 / 2))) = (0 − (𝑟 / 2)))
77	76	fveq2d 5425	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘(0 − (𝑟 / 2))))
78		0cnd 7759	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ∈ ℂ)
79	78, 68	abssubd 10965	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(0 − (𝑟 / 2))) = (abs‘((𝑟 / 2) − 0)))
80	77, 79	eqtrd 2172	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘((𝑟 / 2) − 0)))
81	68	subid1d 8062	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝑟 / 2) − 0) = (𝑟 / 2))
82	81	fveq2d 5425	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝑟 / 2) − 0)) = (abs‘(𝑟 / 2)))
83	53	rpred 9483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ)
84	53	rpge0d 9487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ≤ (𝑟 / 2))
85	83, 84	absidd 10939	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
86	80, 82, 85	3eqtrd 2176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (𝑟 / 2))
87	66, 72, 86	3eqtrd 2176	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝑟 / 2))
88		rphalflt 9471	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
89	88	ad2antrl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) < 𝑟)
90	87, 89	eqbrtrd 3950	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟)
91	13	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
92		rpxr 9449	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
93	92	ad2antrl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ^*)
94		elbl2 12562	. . . . . . . . 9 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑟 ∈ ℝ^*) ∧ (𝐵 ∈ 𝑆 ∧ (𝐵 + (𝑟 / 2)) ∈ 𝑆)) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
95	91, 93, 48, 65, 94	syl22anc 1217	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
96	90, 95	mpbird 166	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟))
97	46, 96	sseldd 3098	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐶)
98	53	rpap0d 9489	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) # 0)
99	67, 67	negsubdid 8088	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = (-𝐵 + 𝐵))
100	74	negeqd 7957	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = -0)
101		neg0 8008	. . . . . . . . . . . 12 ⊢ -0 = 0
102	100, 101	syl6eq 2188	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = 0)
103	99, 102	eqtr3d 2174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + 𝐵) = 0)
104	103	oveq1d 5789	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (0 + (𝑟 / 2)))
105	67	negcld 8060	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -𝐵 ∈ ℂ)
106	105, 67, 68	addassd 7788	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (-𝐵 + (𝐵 + (𝑟 / 2))))
107	68	addid2d 7912	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (0 + (𝑟 / 2)) = (𝑟 / 2))
108	104, 106, 107	3eqtr3d 2180	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) = (𝑟 / 2))
109	98, 108, 103	3brtr4d 3960	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵))
110		apadd2 8371	. . . . . . . 8 ⊢ (((𝐵 + (𝑟 / 2)) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℂ) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
111	69, 67, 105, 110	syl3anc 1216	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
112	109, 111	mpbird 166	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) # 𝐵)
113	45, 97, 112	elrabd 2842	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵})
114		limcimo.ca	. . . . . . 7 ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
115	114	sseld 3096	. . . . . 6 ⊢ (𝜑 → ((𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} → (𝐵 + (𝑟 / 2)) ∈ 𝐴))
116	115	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} → (𝐵 + (𝑟 / 2)) ∈ 𝐴))
117	113, 116	mpd 13	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐴)
118	44, 117	ffvelrnd 5556	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐹‘(𝐵 + (𝑟 / 2))) ∈ ℂ)
119	37, 42	subcld 8073	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑋 − 𝑌) ∈ ℂ)
120	119	abscld 10953	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) ∈ ℝ)
121	37, 118	abssubd 10965	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) = (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)))
122	69, 67	subcld 8073	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) ∈ ℂ)
123	122	abscld 10953	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) ∈ ℝ)
124	52	rpred 9483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ)
125	22	rpred 9483	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
126	125	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐷 ∈ ℝ)
127	67, 68	pncan2d 8075	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) = (𝑟 / 2))
128	127	fveq2d 5425	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (abs‘(𝑟 / 2)))
129	128, 85	eqtrd 2172	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (𝑟 / 2))
130	129, 89	eqbrtrd 3950	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝑟)
131	23	rpred 9483	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℝ)
132	131	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐺 ∈ ℝ)
133		mincl 11002	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
134	126, 132, 133	syl2anc 408	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
135		simprrl 528	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < inf({𝐷, 𝐺}, ℝ, < ))
136		min1inf 11003	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
137	126, 132, 136	syl2anc 408	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
138	124, 134, 126, 135, 137	ltletrd 8185	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐷)
139	123, 124, 126, 130, 138	lttrd 7888	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)
140		breq1 3932	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (𝑧 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
141		fvoveq1 5797	. . . . . . . . 9 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑧 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
142	141	breq1d 3939	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑧 − 𝐵)) < 𝐷 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷))
143	140, 142	anbi12d 464	. . . . . . 7 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)))
144	143	imbrov2fvoveq 5799	. . . . . 6 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)) ↔ (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2))))
145		limcimo.z	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
146	145	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) → (abs‘((𝐹‘𝑧) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
147	144, 146, 117	rspcdva 2794	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
148	112, 139, 147	mp2and 429	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2))
149	121, 148	eqbrtrd 3950	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) < ((abs‘(𝑋 − 𝑌)) / 2))
150		min2inf 11004	. . . . . . 7 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
151	126, 132, 150	syl2anc 408	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
152	124, 134, 132, 135, 151	ltletrd 8185	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐺)
153	123, 124, 132, 130, 152	lttrd 7888	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)
154		breq1 3932	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (𝑤 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
155		fvoveq1 5797	. . . . . . . 8 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑤 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
156	155	breq1d 3939	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑤 − 𝐵)) < 𝐺 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺))
157	154, 156	anbi12d 464	. . . . . 6 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)))
158	157	imbrov2fvoveq 5799	. . . . 5 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)) ↔ (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2))))
159		limcimo.w	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
160	159	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) → (abs‘((𝐹‘𝑤) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
161	158, 160, 117	rspcdva 2794	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
162	112, 153, 161	mp2and 429	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2))
163	37, 42, 118, 120, 149, 162	abs3lemd 10973	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
164	27, 163	rexlimddv 2554	1 ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 697 ∧ w3a 962 = wceq 1331 ∈ wcel 1480 ∀wral 2416 ∃wrex 2417 {crab 2420 ⊆ wss 3071 {cpr 3528 class class class wbr 3929 × cxp 4537 dom cdm 4539 ↾ cres 4541 ∘ ccom 4543 ⟶wf 5119 ‘cfv 5123 (class class class)co 5774 infcinf 6870 ℂcc 7618 ℝcr 7619 0cc0 7620 + caddc 7623 ℝ^*cxr 7799 < clt 7800 ≤ cle 7801 − cmin 7933 -cneg 7934 # cap 8343 / cdiv 8432 2c2 8771 ℝ⁺crp 9441 abscabs 10769 ↾_t crest 12120 ∞Metcxmet 12149 ballcbl 12151 MetOpencmopn 12154 lim_ℂ climc 12792

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-mulrcl 7719 ax-addcom 7720 ax-mulcom 7721 ax-addass 7722 ax-mulass 7723 ax-distr 7724 ax-i2m1 7725 ax-0lt1 7726 ax-1rid 7727 ax-0id 7728 ax-rnegex 7729 ax-precex 7730 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-apti 7735 ax-pre-ltadd 7736 ax-pre-mulgt0 7737 ax-pre-mulext 7738 ax-arch 7739 ax-caucvg 7740

This theorem depends on definitions: df-bi 116 df-stab 816 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-if 3475 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-isom 5132 df-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-recs 6202 df-frec 6288 df-map 6544 df-pm 6545 df-sup 6871 df-inf 6872 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806 df-sub 7935 df-neg 7936 df-reap 8337 df-ap 8344 df-div 8433 df-inn 8721 df-2 8779 df-3 8780 df-4 8781 df-n0 8978 df-z 9055 df-uz 9327 df-q 9412 df-rp 9442 df-xneg 9559 df-xadd 9560 df-seqfrec 10219 df-exp 10293 df-cj 10614 df-re 10615 df-im 10616 df-rsqrt 10770 df-abs 10771 df-rest 12122 df-topgen 12141 df-psmet 12156 df-xmet 12157 df-met 12158 df-bl 12159 df-mopn 12160 df-top 12165 df-topon 12178 df-bases 12210 df-limced 12794

This theorem is referenced by: limcimo 12803

W3C validator