This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )