Metamath Proof Explorer

Theorem rlimcnp2

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses rlimcnp2.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,) +∞ ) )
rlimcnp2.0 ⊢ ( 𝜑 → 0 ∈ 𝐴 )
rlimcnp2.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
rlimcnp2.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
rlimcnp2.r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑆 ∈ ℂ )
rlimcnp2.d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 ∈ 𝐵 ↔ ( 1 / 𝑦 ) ∈ 𝐴 ) )
rlimcnp2.s ⊢ ( 𝑦 = ( 1 / 𝑥 ) → 𝑆 = 𝑅 )
rlimcnp2.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
rlimcnp2.k ⊢ 𝐾 = ( 𝐽 ↾t 𝐴 )
Assertion rlimcnp2 ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 rlimcnp2.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,) +∞ ) )
2 rlimcnp2.0 ⊢ ( 𝜑 → 0 ∈ 𝐴 )
3 rlimcnp2.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
4 rlimcnp2.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 rlimcnp2.r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑆 ∈ ℂ )
6 rlimcnp2.d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 ∈ 𝐵 ↔ ( 1 / 𝑦 ) ∈ 𝐴 ) )
7 rlimcnp2.s ⊢ ( 𝑦 = ( 1 / 𝑥 ) → 𝑆 = 𝑅 )
8 rlimcnp2.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
9 rlimcnp2.k ⊢ 𝐾 = ( 𝐽 ↾t 𝐴 )
10 inss1 ⊢ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ⊆ 𝐵
11 resmpt ⊢ ( ( 𝐵 ∩ ( 1 [,) +∞ ) ) ⊆ 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ) = ( 𝑦 ∈ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ↦ 𝑆 ) )
12 10 11 mp1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ) = ( 𝑦 ∈ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ↦ 𝑆 ) )
13 0xr ⊢ 0 ∈ ℝ*
14 0lt1 ⊢ 0 < 1
15 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
16 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
17 xrltletr ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 0 < 1 ∧ 1 ≤ 𝑤 ) → 0 < 𝑤 ) )
18 15 16 17 ixxss1 ⊢ ( ( 0 ∈ ℝ* ∧ 0 < 1 ) → ( 1 [,) +∞ ) ⊆ ( 0 (,) +∞ ) )
19 13 14 18 mp2an ⊢ ( 1 [,) +∞ ) ⊆ ( 0 (,) +∞ )
20 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
21 19 20 sseqtri ⊢ ( 1 [,) +∞ ) ⊆ ℝ+
22 sslin ⊢ ( ( 1 [,) +∞ ) ⊆ ℝ+ → ( 𝐵 ∩ ( 1 [,) +∞ ) ) ⊆ ( 𝐵 ∩ ℝ+ ) )
23 21 22 ax-mp ⊢ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ⊆ ( 𝐵 ∩ ℝ+ )
24 resmpt ⊢ ( ( 𝐵 ∩ ( 1 [,) +∞ ) ) ⊆ ( 𝐵 ∩ ℝ+ ) → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ) = ( 𝑦 ∈ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ↦ 𝑆 ) )
25 23 24 mp1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ) = ( 𝑦 ∈ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ↦ 𝑆 ) )
26 12 25 eqtr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ) = ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) ) )
27 resres ⊢ ( ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ 𝐵 ) ↾ ( 1 [,) +∞ ) ) = ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) )
28 resres ⊢ ( ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ 𝐵 ) ↾ ( 1 [,) +∞ ) ) = ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 𝐵 ∩ ( 1 [,) +∞ ) ) )
29 26 27 28 3eqtr4g ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ 𝐵 ) ↾ ( 1 [,) +∞ ) ) = ( ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ 𝐵 ) ↾ ( 1 [,) +∞ ) ) )
30 5 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) : 𝐵 ⟶ ℂ )
31 30 ffnd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) Fn 𝐵 )
32 fnresdm ⊢ ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) Fn 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
33 31 32 syl ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
34 33 reseq1d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ 𝐵 ) ↾ ( 1 [,) +∞ ) ) = ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) )
35 elinel1 ⊢ ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) → 𝑦 ∈ 𝐵 )
36 35 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → 𝑆 ∈ ℂ )
37 36 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) : ( 𝐵 ∩ ℝ+ ) ⟶ ℂ )
38 frel ⊢ ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) : ( 𝐵 ∩ ℝ+ ) ⟶ ℂ → Rel ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) )
39 37 38 syl ⊢ ( 𝜑 → Rel ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) )
40 eqid ⊢ ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) = ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 )
41 40 36 dmmptd ⊢ ( 𝜑 → dom ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) = ( 𝐵 ∩ ℝ+ ) )
42 inss1 ⊢ ( 𝐵 ∩ ℝ+ ) ⊆ 𝐵
43 41 42 eqsstrdi ⊢ ( 𝜑 → dom ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ⊆ 𝐵 )
44 relssres ⊢ ( ( Rel ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ∧ dom ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ⊆ 𝐵 ) → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ 𝐵 ) = ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) )
45 39 43 44 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ 𝐵 ) = ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) )
46 45 reseq1d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ 𝐵 ) ↾ ( 1 [,) +∞ ) ) = ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) )
47 29 34 46 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) = ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) )
48 47 breq1d ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) ⇝𝑟 𝐶 ↔ ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) ⇝𝑟 𝐶 ) )
49 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
50 30 3 49 rlimresb ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) ⇝𝑟 𝐶 ) )
51 42 3 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ ℝ+ ) ⊆ ℝ )
52 37 51 49 rlimresb ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ↾ ( 1 [,) +∞ ) ) ⇝𝑟 𝐶 ) )
53 48 50 52 3bitr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ⇝𝑟 𝐶 ) )
54 inss2 ⊢ ( 𝐵 ∩ ℝ+ ) ⊆ ℝ+
55 54 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ ℝ+ ) ⊆ ℝ+ )
56 55 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → 𝑦 ∈ ℝ+ )
57 56 rpreccld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → ( 1 / 𝑦 ) ∈ ℝ+ )
58 57 rpne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → ( 1 / 𝑦 ) ≠ 0 )
59 58 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → ¬ ( 1 / 𝑦 ) = 0 )
60 59 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) = ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 )
61 oveq2 ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( 1 / 𝑥 ) = ( 1 / ( 1 / 𝑦 ) ) )
62 rpcnne0 ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
63 recrec ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 1 / ( 1 / 𝑦 ) ) = 𝑦 )
64 56 62 63 3syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → ( 1 / ( 1 / 𝑦 ) ) = 𝑦 )
65 61 64 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) ∧ 𝑥 = ( 1 / 𝑦 ) ) → ( 1 / 𝑥 ) = 𝑦 )
66 65 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) ∧ 𝑥 = ( 1 / 𝑦 ) ) → 𝑦 = ( 1 / 𝑥 ) )
67 66 7 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) ∧ 𝑥 = ( 1 / 𝑦 ) ) → 𝑆 = 𝑅 )
68 67 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) ∧ 𝑥 = ( 1 / 𝑦 ) ) → 𝑅 = 𝑆 )
69 57 68 csbied ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 = 𝑆 )
70 60 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) = 𝑆 )
71 70 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) ) = ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) )
72 71 breq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) ) ⇝𝑟 𝐶 ↔ ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ 𝑆 ) ⇝𝑟 𝐶 ) )
73 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑤 = 0 ) → 𝐶 ∈ ℂ )
74 1 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ( 0 [,) +∞ ) )
75 0re ⊢ 0 ∈ ℝ
76 pnfxr ⊢ +∞ ∈ ℝ*
77 elico2 ⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑤 ∈ ( 0 [,) +∞ ) ↔ ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞ ) ) )
78 75 76 77 mp2an ⊢ ( 𝑤 ∈ ( 0 [,) +∞ ) ↔ ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞ ) )
79 74 78 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞ ) )
80 79 simp1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ℝ )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → 𝑤 ∈ ℝ )
82 79 simp2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 0 ≤ 𝑤 )
83 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( 0 ≤ 𝑤 ↔ ( 0 < 𝑤 ∨ 0 = 𝑤 ) ) )
84 75 80 83 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 0 ≤ 𝑤 ↔ ( 0 < 𝑤 ∨ 0 = 𝑤 ) ) )
85 82 84 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 0 < 𝑤 ∨ 0 = 𝑤 ) )
86 85 ord ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ 0 < 𝑤 → 0 = 𝑤 ) )
87 eqcom ⊢ ( 0 = 𝑤 ↔ 𝑤 = 0 )
88 86 87 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ 0 < 𝑤 → 𝑤 = 0 ) )
89 88 con1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ 𝑤 = 0 → 0 < 𝑤 ) )
90 89 imp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → 0 < 𝑤 )
91 81 90 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → 𝑤 ∈ ℝ+ )
92 rpcnne0 ⊢ ( 𝑤 ∈ ℝ+ → ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) )
93 recrec ⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) → ( 1 / ( 1 / 𝑤 ) ) = 𝑤 )
94 92 93 syl ⊢ ( 𝑤 ∈ ℝ+ → ( 1 / ( 1 / 𝑤 ) ) = 𝑤 )
95 91 94 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ( 1 / ( 1 / 𝑤 ) ) = 𝑤 )
96 95 csbeq1d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ⦋ ( 1 / ( 1 / 𝑤 ) ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑤 / 𝑥 ⦌ 𝑅 )
97 oveq2 ⊢ ( 𝑦 = ( 1 / 𝑤 ) → ( 1 / 𝑦 ) = ( 1 / ( 1 / 𝑤 ) ) )
98 97 csbeq1d ⊢ ( 𝑦 = ( 1 / 𝑤 ) → ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 = ⦋ ( 1 / ( 1 / 𝑤 ) ) / 𝑥 ⦌ 𝑅 )
99 98 eleq1d ⊢ ( 𝑦 = ( 1 / 𝑤 ) → ( ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ∈ ℂ ↔ ⦋ ( 1 / ( 1 / 𝑤 ) ) / 𝑥 ⦌ 𝑅 ∈ ℂ ) )
100 69 36 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ) → ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ∈ ℂ )
101 100 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ∈ ℂ )
102 101 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ∀ 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ∈ ℂ )
103 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → 𝑤 ∈ 𝐴 )
104 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → 𝜑 )
105 eleq1 ⊢ ( 𝑦 = ( 1 / 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ ( 1 / 𝑤 ) ∈ 𝐵 ) )
106 97 eleq1d ⊢ ( 𝑦 = ( 1 / 𝑤 ) → ( ( 1 / 𝑦 ) ∈ 𝐴 ↔ ( 1 / ( 1 / 𝑤 ) ) ∈ 𝐴 ) )
107 105 106 bibi12d ⊢ ( 𝑦 = ( 1 / 𝑤 ) → ( ( 𝑦 ∈ 𝐵 ↔ ( 1 / 𝑦 ) ∈ 𝐴 ) ↔ ( ( 1 / 𝑤 ) ∈ 𝐵 ↔ ( 1 / ( 1 / 𝑤 ) ) ∈ 𝐴 ) ) )
108 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( 𝑦 ∈ 𝐵 ↔ ( 1 / 𝑦 ) ∈ 𝐴 ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∀ 𝑦 ∈ ℝ+ ( 𝑦 ∈ 𝐵 ↔ ( 1 / 𝑦 ) ∈ 𝐴 ) )
110 rpreccl ⊢ ( 𝑤 ∈ ℝ+ → ( 1 / 𝑤 ) ∈ ℝ+ )
111 110 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( 1 / 𝑤 ) ∈ ℝ+ )
112 107 109 111 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ( 1 / 𝑤 ) ∈ 𝐵 ↔ ( 1 / ( 1 / 𝑤 ) ) ∈ 𝐴 ) )
113 94 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( 1 / ( 1 / 𝑤 ) ) = 𝑤 )
114 113 eleq1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ( 1 / ( 1 / 𝑤 ) ) ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
115 112 114 bitr2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 ∈ 𝐴 ↔ ( 1 / 𝑤 ) ∈ 𝐵 ) )
116 104 91 115 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ( 𝑤 ∈ 𝐴 ↔ ( 1 / 𝑤 ) ∈ 𝐵 ) )
117 103 116 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ( 1 / 𝑤 ) ∈ 𝐵 )
118 91 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ( 1 / 𝑤 ) ∈ ℝ+ )
119 117 118 elind ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ( 1 / 𝑤 ) ∈ ( 𝐵 ∩ ℝ+ ) )
120 99 102 119 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ⦋ ( 1 / ( 1 / 𝑤 ) ) / 𝑥 ⦌ 𝑅 ∈ ℂ )
121 96 120 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ¬ 𝑤 = 0 ) → ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ∈ ℂ )
122 73 121 ifclda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) ∈ ℂ )
123 111 biantrud ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ( 1 / 𝑤 ) ∈ 𝐵 ↔ ( ( 1 / 𝑤 ) ∈ 𝐵 ∧ ( 1 / 𝑤 ) ∈ ℝ+ ) ) )
124 115 123 bitrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 ∈ 𝐴 ↔ ( ( 1 / 𝑤 ) ∈ 𝐵 ∧ ( 1 / 𝑤 ) ∈ ℝ+ ) ) )
125 elin ⊢ ( ( 1 / 𝑤 ) ∈ ( 𝐵 ∩ ℝ+ ) ↔ ( ( 1 / 𝑤 ) ∈ 𝐵 ∧ ( 1 / 𝑤 ) ∈ ℝ+ ) )
126 124 125 bitr4di ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 ∈ 𝐴 ↔ ( 1 / 𝑤 ) ∈ ( 𝐵 ∩ ℝ+ ) ) )
127 iftrue ⊢ ( 𝑤 = 0 → if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) = 𝐶 )
128 eqeq1 ⊢ ( 𝑤 = ( 1 / 𝑦 ) → ( 𝑤 = 0 ↔ ( 1 / 𝑦 ) = 0 ) )
129 csbeq1 ⊢ ( 𝑤 = ( 1 / 𝑦 ) → ⦋ 𝑤 / 𝑥 ⦌ 𝑅 = ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 )
130 128 129 ifbieq2d ⊢ ( 𝑤 = ( 1 / 𝑦 ) → if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) = if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) )
131 1 2 55 122 126 127 130 8 9 rlimcnp ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) ) ⇝𝑟 𝐶 ↔ ( 𝑤 ∈ 𝐴 ↦ if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )
132 nfcv ⊢ Ⅎ 𝑤 if ( 𝑥 = 0 , 𝐶 , 𝑅 )
133 nfv ⊢ Ⅎ 𝑥 𝑤 = 0
134 nfcv ⊢ Ⅎ 𝑥 𝐶
135 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝑅
136 133 134 135 nfif ⊢ Ⅎ 𝑥 if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 )
137 eqeq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 0 ↔ 𝑤 = 0 ) )
138 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝑅 = ⦋ 𝑤 / 𝑥 ⦌ 𝑅 )
139 137 138 ifbieq2d ⊢ ( 𝑥 = 𝑤 → if ( 𝑥 = 0 , 𝐶 , 𝑅 ) = if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) )
140 132 136 139 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) = ( 𝑤 ∈ 𝐴 ↦ if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) )
141 140 eleq1i ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ↔ ( 𝑤 ∈ 𝐴 ↦ if ( 𝑤 = 0 , 𝐶 , ⦋ 𝑤 / 𝑥 ⦌ 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) )
142 131 141 bitr4di ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝐵 ∩ ℝ+ ) ↦ if ( ( 1 / 𝑦 ) = 0 , 𝐶 , ⦋ ( 1 / 𝑦 ) / 𝑥 ⦌ 𝑅 ) ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )
143 53 72 142 3bitr2d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )