limcimolemlt - Intuitionistic Logic Explorer

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

Theorem limcimolemlt 15765

Description: Lemma for limcimo 15766. (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 15632	. . . 4 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		ax-resscn 8271	. . . . . . 7 ⊢ ℝ ⊆ ℂ
3		sseq1 3271	. . . . . . 7 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 168	. . . . . 6 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5	4	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℝ) → 𝑆 ⊆ ℂ)
6		eqimss 3302	. . . . . 6 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
7	6	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
8		limcimo.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
9		elpri 3732	. . . . . 6 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ))
11	5, 7, 10	mpjaodan 810	. . . 4 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
12		xmetres2 15480	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
13	1, 11, 12	sylancr 418	. . 3 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
14		limcimo.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾_t 𝑆))
15		eqid 2238	. . . . . 6 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
16		limcflfcntop.k	. . . . . 6 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
17		eqid 2238	. . . . . 6 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
18	15, 16, 17	metrest 15607	. . . . 5 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
19	1, 11, 18	sylancr 418	. . . 4 ⊢ (𝜑 → (𝐾 ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
20	14, 19	eleqtrd 2317	. . 3 ⊢ (𝜑 → 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
21		limcimo.bc	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
22		limcimo.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
23		limcimo.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ℝ⁺)
24		rpmincl 12004	. . . 4 ⊢ ((𝐷 ∈ ℝ⁺ ∧ 𝐺 ∈ ℝ⁺) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
25	22, 23, 24	syl2anc 415	. . 3 ⊢ (𝜑 → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺)
26	17	mopni3 15585	. . 3 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) ∧ 𝐵 ∈ 𝐶) ∧ inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ⁺) → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
27	13, 20, 21, 25, 26	syl31anc 1281	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℝ⁺ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))
28		limcimo.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝐹 lim_ℂ 𝐵))
29		limcrcl 15759	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐹 lim_ℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
30	28, 29	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
31	30	simp1d 1040	. . . . . . 7 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
32	30	simp2d 1041	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
33		limcimo.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
34	31, 32, 33	ellimc3ap 15762	. . . . . 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 15762	. . . . . 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 4133	. . . . . 6 ⊢ (𝑞 = (𝐵 + (𝑟 / 2)) → (𝑞 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
46		simprrr 546	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶)
47		limcimo.bs	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
48	47	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ 𝑆)
49	47	ad2antrr 492	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ 𝑆)
50		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝑆 = ℝ)
51	49, 50	eleqtrd 2317	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → 𝐵 ∈ ℝ)
52		simprl 535	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ⁺)
53	52	rphalfcld 10110	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ⁺)
54	53	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ⁺)
55	54	rpred 10097	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝑟 / 2) ∈ ℝ)
56	51, 55	readdcld 8355	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ ℝ)
57	56, 50	eleqtrrd 2318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℝ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
58	33	ad2antrr 492	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝐵 ∈ ℂ)
59	53	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℝ⁺)
60	59	rpcnd 10099	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝑟 / 2) ∈ ℂ)
61	58, 60	addcld 8345	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
62		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → 𝑆 = ℂ)
63	61, 62	eleqtrrd 2318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) ∧ 𝑆 = ℂ) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
64	10	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑆 = ℝ ∨ 𝑆 = ℂ))
65	57, 63, 64	mpjaodan 810	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝑆)
66	48, 65	ovresd 6230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))))
67	33	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐵 ∈ ℂ)
68	53	rpcnd 10099	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℂ)
69	67, 68	addcld 8345	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ ℂ)
70		eqid 2238	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) = (abs ∘ − )
71	70	cnmetdval 15630	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℂ ∧ (𝐵 + (𝑟 / 2)) ∈ ℂ) → (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))) = (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))))
72	67, 69, 71	syl2anc 415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵(abs ∘ − )(𝐵 + (𝑟 / 2))) = (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))))
73	67, 67, 68	subsub4d 8668	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (𝐵 − (𝐵 + (𝑟 / 2))))
74	67	subidd 8625	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − 𝐵) = 0)
75	74	oveq1d 6100	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 − 𝐵) − (𝑟 / 2)) = (0 − (𝑟 / 2)))
76	73, 75	eqtr3d 2273	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 − (𝐵 + (𝑟 / 2))) = (0 − (𝑟 / 2)))
77	76	fveq2d 5699	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘(0 − (𝑟 / 2))))
78		0cnd 8319	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ∈ ℂ)
79	78, 68	abssubd 11959	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(0 − (𝑟 / 2))) = (abs‘((𝑟 / 2) − 0)))
80	77, 79	eqtrd 2271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (abs‘((𝑟 / 2) − 0)))
81	68	subid1d 8626	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝑟 / 2) − 0) = (𝑟 / 2))
82	81	fveq2d 5699	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝑟 / 2) − 0)) = (abs‘(𝑟 / 2)))
83	53	rpred 10097	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) ∈ ℝ)
84	53	rpge0d 10101	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 0 ≤ (𝑟 / 2))
85	83, 84	absidd 11933	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
86	80, 82, 85	3eqtrd 2275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝐵 − (𝐵 + (𝑟 / 2)))) = (𝑟 / 2))
87	66, 72, 86	3eqtrd 2275	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) = (𝑟 / 2))
88		rphalflt 10084	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
89	88	ad2antrl 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) < 𝑟)
90	87, 89	eqbrtrd 4152	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟)
91	13	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
92		rpxr 10062	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
93	92	ad2antrl 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ^*)
94		elbl2 15494	. . . . . . . . 9 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑟 ∈ ℝ^*) ∧ (𝐵 ∈ 𝑆 ∧ (𝐵 + (𝑟 / 2)) ∈ 𝑆)) → ((𝐵 + (𝑟 / 2)) ∈ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ↔ (𝐵((abs ∘ − ) ↾ (𝑆 × 𝑆))(𝐵 + (𝑟 / 2))) < 𝑟))
95	91, 93, 48, 65, 94	syl22anc 1279	. . . . . . . 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 3249	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ 𝐶)
98	53	rpap0d 10103	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑟 / 2) # 0)
99	67, 67	negsubdid 8652	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = (-𝐵 + 𝐵))
100	74	negeqd 8521	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = -0)
101		neg0 8572	. . . . . . . . . . . 12 ⊢ -0 = 0
102	100, 101	eqtrdi 2287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -(𝐵 − 𝐵) = 0)
103	99, 102	eqtr3d 2273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + 𝐵) = 0)
104	103	oveq1d 6100	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (0 + (𝑟 / 2)))
105	67	negcld 8624	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → -𝐵 ∈ ℂ)
106	105, 67, 68	addassd 8348	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((-𝐵 + 𝐵) + (𝑟 / 2)) = (-𝐵 + (𝐵 + (𝑟 / 2))))
107	68	addlidd 8476	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (0 + (𝑟 / 2)) = (𝑟 / 2))
108	104, 106, 107	3eqtr3d 2279	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) = (𝑟 / 2))
109	98, 108, 103	3brtr4d 4162	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵))
110		apadd2 8937	. . . . . . . 8 ⊢ (((𝐵 + (𝑟 / 2)) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℂ) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
111	69, 67, 105, 110	syl3anc 1278	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) # 𝐵 ↔ (-𝐵 + (𝐵 + (𝑟 / 2))) # (-𝐵 + 𝐵)))
112	109, 111	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) # 𝐵)
113	45, 97, 112	elrabd 2984	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐵 + (𝑟 / 2)) ∈ {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵})
114		limcimo.ca	. . . . . . 7 ⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴)
115	114	sseld 3247	. . . . . 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 5844	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝐹‘(𝐵 + (𝑟 / 2))) ∈ ℂ)
119	37, 42	subcld 8637	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (𝑋 − 𝑌) ∈ ℂ)
120	119	abscld 11947	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) ∈ ℝ)
121	37, 118	abssubd 11959	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) = (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)))
122	69, 67	subcld 8637	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) ∈ ℂ)
123	122	abscld 11947	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) ∈ ℝ)
124	52	rpred 10097	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 ∈ ℝ)
125	22	rpred 10097	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
126	125	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐷 ∈ ℝ)
127	67, 68	pncan2d 8639	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → ((𝐵 + (𝑟 / 2)) − 𝐵) = (𝑟 / 2))
128	127	fveq2d 5699	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (abs‘(𝑟 / 2)))
129	128, 85	eqtrd 2271	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) = (𝑟 / 2))
130	129, 89	eqbrtrd 4152	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝑟)
131	23	rpred 10097	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℝ)
132	131	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝐺 ∈ ℝ)
133		mincl 11997	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
134	126, 132, 133	syl2anc 415	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ∈ ℝ)
135		simprrl 545	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < inf({𝐷, 𝐺}, ℝ, < ))
136		min1inf 11998	. . . . . . . 8 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
137	126, 132, 136	syl2anc 415	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐷)
138	124, 134, 126, 135, 137	ltletrd 8751	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐷)
139	123, 124, 126, 130, 138	lttrd 8452	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)
140		breq1 4133	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (𝑧 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
141		fvoveq1 6108	. . . . . . . . 9 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑧 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
142	141	breq1d 4140	. . . . . . . 8 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑧 − 𝐵)) < 𝐷 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷))
143	140, 142	anbi12d 477	. . . . . . 7 ⊢ (𝑧 = (𝐵 + (𝑟 / 2)) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝐷) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷)))
144	143	imbrov2fvoveq 6110	. . . . . 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 2934	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐷) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2)))
148	112, 139, 147	mp2and 437	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑋)) < ((abs‘(𝑋 − 𝑌)) / 2))
149	121, 148	eqbrtrd 4152	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − (𝐹‘(𝐵 + (𝑟 / 2))))) < ((abs‘(𝑋 − 𝑌)) / 2))
150		min2inf 11999	. . . . . . 7 ⊢ ((𝐷 ∈ ℝ ∧ 𝐺 ∈ ℝ) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
151	126, 132, 150	syl2anc 415	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → inf({𝐷, 𝐺}, ℝ, < ) ≤ 𝐺)
152	124, 134, 132, 135, 151	ltletrd 8751	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → 𝑟 < 𝐺)
153	123, 124, 132, 130, 152	lttrd 8452	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)
154		breq1 4133	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (𝑤 # 𝐵 ↔ (𝐵 + (𝑟 / 2)) # 𝐵))
155		fvoveq1 6108	. . . . . . . 8 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → (abs‘(𝑤 − 𝐵)) = (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)))
156	155	breq1d 4140	. . . . . . 7 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((abs‘(𝑤 − 𝐵)) < 𝐺 ↔ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺))
157	154, 156	anbi12d 477	. . . . . 6 ⊢ (𝑤 = (𝐵 + (𝑟 / 2)) → ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝐺) ↔ ((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺)))
158	157	imbrov2fvoveq 6110	. . . . 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 2934	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (((𝐵 + (𝑟 / 2)) # 𝐵 ∧ (abs‘((𝐵 + (𝑟 / 2)) − 𝐵)) < 𝐺) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2)))
162	112, 153, 161	mp2and 437	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘((𝐹‘(𝐵 + (𝑟 / 2))) − 𝑌)) < ((abs‘(𝑋 − 𝑌)) / 2))
163	37, 42, 118, 120, 149, 162	abs3lemd 11967	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑟 < inf({𝐷, 𝐺}, ℝ, < ) ∧ (𝐵(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑟) ⊆ 𝐶))) → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))
164	27, 163	rexlimddv 2673	1 ⊢ (𝜑 → (abs‘(𝑋 − 𝑌)) < (abs‘(𝑋 − 𝑌)))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ∀wral 2528 ∃wrex 2529 {crab 2532 ⊆ wss 3220 {cpr 3710 class class class wbr 4130 × cxp 4772 dom cdm 4774 ↾ cres 4776 ∘ ccom 4778 ⟶wf 5373 ‘cfv 5377 (class class class)co 6085 infcinf 7323 ℂcc 8177 ℝcr 8178 0cc0 8179 + caddc 8182 ℝ^*cxr 8359 < clt 8360 ≤ cle 8361 − cmin 8497 -cneg 8498 # cap 8909 / cdiv 9002 2c2 9355 ℝ⁺crp 10054 abscabs 11763 ↾_t crest 13593 ∞Metcxmet 14873 ballcbl 14875 MetOpencmopn 14878 lim_ℂ climc 15755

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-map 6924 df-pm 6925 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-2 9363 df-3 9364 df-4 9365 df-n0 9564 df-z 9645 df-uz 9922 df-q 10020 df-rp 10055 df-xneg 10174 df-xadd 10175 df-seqfrec 10885 df-exp 10976 df-cj 11607 df-re 11608 df-im 11609 df-rsqrt 11764 df-abs 11765 df-rest 13595 df-topgen 13614 df-psmet 14880 df-xmet 14881 df-met 14882 df-bl 14883 df-mopn 14884 df-top 15099 df-topon 15112 df-bases 15144 df-limced 15757

This theorem is used by: limcimo 15766

W3C validator