Theorem ellimcabssub0

Description: An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ellimcabssub0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	ellimcabssub0.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) )
	ellimcabssub0.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	ellimcabssub0.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	ellimcabssub0.p	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	ellimcabssub0.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	ellimcabssub0	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) ↔ 0 ∈ ( 𝐺 limℂ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ellimcabssub0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		ellimcabssub0.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) )
3		ellimcabssub0.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
4		ellimcabssub0.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		ellimcabssub0.p	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
6		ellimcabssub0.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
7		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
8	6 7	2thd	⊢ ( 𝜑 → ( 𝐶 ∈ ℂ ↔ 0 ∈ ℂ ) )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
10	4 9	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
11	10 2	fmptd	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
12	11	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
13	12	subid1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) − 0 ) = ( 𝐺 ‘ 𝑧 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
15		csbov1g	⊢ ( 𝑧 ∈ V → ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 − 𝐶 ) )
16	15	elv	⊢ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 − 𝐶 )
17		sban	⊢ ( [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ) )
18		nfv	⊢ Ⅎ 𝑥 𝜑
19	18	sbf	⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜑 )
20		clelsb1	⊢ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 )
21	19 20	anbi12i	⊢ ( ( [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) )
22	17 21	bitri	⊢ ( [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) )
23	4	nfth	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
24	23	sbf	⊢ ( [ 𝑧 / 𝑥 ] ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) )
25		sbim	⊢ ( [ 𝑧 / 𝑥 ] ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ) )
26	24 25	sylbb1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) → ( [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ) )
27	22 26	biimtrrid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) → ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ) )
28	4 27	ax-mp	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ )
29		sbsbc	⊢ ( [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ↔ [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ )
30		sbcel1g	⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
31	30	elv	⊢ ( [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℂ )
32	29 31	bitri	⊢ ( [ 𝑧 / 𝑥 ] 𝐵 ∈ ℂ ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℂ )
33	28 32	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℂ )
34	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
35	33 34	subcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 − 𝐶 ) ∈ ℂ )
36	16 35	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) ∈ ℂ )
37	2	fvmpts	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) ∈ ℂ ) → ( 𝐺 ‘ 𝑧 ) = ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) )
38	14 36 37	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) = ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) )
39	1	fvmpts	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
40	14 33 39	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
41	40	oveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 − 𝐶 ) )
42	16 41	eqtr4id	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 − 𝐶 ) = ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) )
43	13 38 42	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) = ( ( 𝐺 ‘ 𝑧 ) − 0 ) )
44	43	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) )
45	44	breq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) )
46	45	imbi2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ) ↔ ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) ) )
47	46	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) ) )
48	47	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ) ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) ) )
49	48	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) ) )
50	8 49	anbi12d	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) ) ) )
51	4 1	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
52	51 3 5	ellimc3	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑦 ) ) ) )
53	11 3 5	ellimc3	⊢ ( 𝜑 → ( 0 ∈ ( 𝐺 limℂ 𝐷 ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 0 ) ) < 𝑦 ) ) ) )
54	50 52 53	3bitr4d	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) ↔ 0 ∈ ( 𝐺 limℂ 𝐷 ) ) )