rlim3

Description: Restrict the range of the domain bound to reals greater than some D e. RR . (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlim2.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
	rlim2.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	rlim2.3	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	rlim3.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
Assertion	rlim3	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlim2.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
2		rlim2.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		rlim2.3	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		rlim3.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5	1 2 3	rlim2	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
7	4	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝐷 ∈ ℝ )
8	6 7	ifcld	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ℝ )
9		max1	⊢ ( ( 𝐷 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → 𝐷 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) )
10	4 9	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝐷 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) )
11		elicopnf	⊢ ( 𝐷 ∈ ℝ → ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ( 𝐷 [,) +∞ ) ↔ ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ℝ ∧ 𝐷 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ) ) )
12	7 11	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ( 𝐷 [,) +∞ ) ↔ ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ℝ ∧ 𝐷 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ) ) )
13	8 10 12	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ( 𝐷 [,) +∞ ) )
14	2 4	jca	⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) )
15		max2	⊢ ( ( 𝐷 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → 𝑤 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) )
16	15	ad4ant23	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑤 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) )
17		simplr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑤 ∈ ℝ )
18		simpllr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝐷 ∈ ℝ )
19	17 18	ifcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ℝ )
20		simpll	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) → 𝐴 ⊆ ℝ )
21	20	sselda	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
22		letr	⊢ ( ( 𝑤 ∈ ℝ ∧ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑤 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∧ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 ) → 𝑤 ≤ 𝑧 ) )
23	17 19 21 22	syl3anc	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑤 ≤ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∧ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 ) → 𝑤 ≤ 𝑧 ) )
24	16 23	mpand	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 → 𝑤 ≤ 𝑧 ) )
25	24	imim1d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
26	25	ralimdva	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑤 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
27	14 26	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
28		breq1	⊢ ( 𝑦 = if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) → ( 𝑦 ≤ 𝑧 ↔ if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 ) )
29	28	rspceaimv	⊢ ( ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ∈ ( 𝐷 [,) +∞ ) ∧ ∀ 𝑧 ∈ 𝐴 ( if ( 𝐷 ≤ 𝑤 , 𝑤 , 𝐷 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) )
30	13 27 29	syl6an	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
31	30	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
32	31	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
33	5 32	sylbid	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
34		pnfxr	⊢ +∞ ∈ ℝ^*
35		icossre	⊢ ( ( 𝐷 ∈ ℝ ∧ +∞ ∈ ℝ^* ) → ( 𝐷 [,) +∞ ) ⊆ ℝ )
36	4 34 35	sylancl	⊢ ( 𝜑 → ( 𝐷 [,) +∞ ) ⊆ ℝ )
37		ssrexv	⊢ ( ( 𝐷 [,) +∞ ) ⊆ ℝ → ( ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
38	36 37	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
39	38	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
40	1 2 3	rlim2	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
41	39 40	sylibrd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 ) )
42	33 41	impbid	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )

Metamath Proof Explorer

Theorem rlim3

Proof