caucvgrlem2

Description: Lemma for caucvgr . (Contributed by NM, 4-Apr-2005) (Proof shortened by Mario Carneiro, 8-May-2016)

	Ref	Expression
Hypotheses	caucvgr.1	$⊢ φ \to A \subseteq ℝ$
	caucvgr.2	$⊢ φ \to F : A ⟶ ℂ$
	caucvgr.3	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
	caucvgr.4	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in A \forall k \in A (j \leq k \to \|F (k) - F (j)\| < x)$
	caucvgrlem2.5	$⊢ H : ℂ ⟶ ℝ$
	caucvgrlem2.6	$⊢ (F (k) \in ℂ \land F (j) \in ℂ) \to \|H (F (k)) - H (F (j))\| \leq \|F (k) - F (j)\|$
Assertion	caucvgrlem2	$⊢ φ \to (n \in A ⟼ H (F (n))) \underset{ℝ}{⇝} \underset{ℝ}{⇝} (H \circ F)$

Proof

Step	Hyp	Ref	Expression
1		caucvgr.1	$⊢ φ \to A \subseteq ℝ$
2		caucvgr.2	$⊢ φ \to F : A ⟶ ℂ$
3		caucvgr.3	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
4		caucvgr.4	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in A \forall k \in A (j \leq k \to \|F (k) - F (j)\| < x)$
5		caucvgrlem2.5	$⊢ H : ℂ ⟶ ℝ$
6		caucvgrlem2.6	$⊢ (F (k) \in ℂ \land F (j) \in ℂ) \to \|H (F (k)) - H (F (j))\| \leq \|F (k) - F (j)\|$
7		fcompt	$⊢ (H : ℂ ⟶ ℝ \land F : A ⟶ ℂ) \to H \circ F = (n \in A ⟼ H (F (n)))$
8	5 2 7	sylancr	$⊢ φ \to H \circ F = (n \in A ⟼ H (F (n)))$
9		fco	$⊢ (H : ℂ ⟶ ℝ \land F : A ⟶ ℂ) \to (H \circ F) : A ⟶ ℝ$
10	5 2 9	sylancr	$⊢ φ \to (H \circ F) : A ⟶ ℝ$
11	2	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to F : A ⟶ ℂ$
12		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to k \in A$
13	11 12	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to F (k) \in ℂ$
14		simprl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to j \in A$
15	11 14	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to F (j) \in ℂ$
16	13 15 6	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to \|H (F (k)) - H (F (j))\| \leq \|F (k) - F (j)\|$
17	5	ffvelrni	$⊢ F (k) \in ℂ \to H (F (k)) \in ℝ$
18	13 17	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to H (F (k)) \in ℝ$
19	5	ffvelrni	$⊢ F (j) \in ℂ \to H (F (j)) \in ℝ$
20	15 19	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to H (F (j)) \in ℝ$
21	18 20	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to H (F (k)) - H (F (j)) \in ℝ$
22	21	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to H (F (k)) - H (F (j)) \in ℂ$
23	22	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to \|H (F (k)) - H (F (j))\| \in ℝ$
24	13 15	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to F (k) - F (j) \in ℂ$
25	24	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to \|F (k) - F (j)\| \in ℝ$
26		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
27	26	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to x \in ℝ$
28		lelttr	$⊢ (\|H (F (k)) - H (F (j))\| \in ℝ \land \|F (k) - F (j)\| \in ℝ \land x \in ℝ) \to ((\|H (F (k)) - H (F (j))\| \leq \|F (k) - F (j)\| \land \|F (k) - F (j)\| < x) \to \|H (F (k)) - H (F (j))\| < x)$
29	23 25 27 28	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to ((\|H (F (k)) - H (F (j))\| \leq \|F (k) - F (j)\| \land \|F (k) - F (j)\| < x) \to \|H (F (k)) - H (F (j))\| < x)$
30	16 29	mpand	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to (\|F (k) - F (j)\| < x \to \|H (F (k)) - H (F (j))\| < x)$
31		fvco3	$⊢ (F : A ⟶ ℂ \land k \in A) \to (H \circ F) (k) = H (F (k))$
32	11 12 31	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to (H \circ F) (k) = H (F (k))$
33		fvco3	$⊢ (F : A ⟶ ℂ \land j \in A) \to (H \circ F) (j) = H (F (j))$
34	11 14 33	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to (H \circ F) (j) = H (F (j))$
35	32 34	oveq12d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to (H \circ F) (k) - (H \circ F) (j) = H (F (k)) - H (F (j))$
36	35	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to \|(H \circ F) (k) - (H \circ F) (j)\| = \|H (F (k)) - H (F (j))\|$
37	36	breq1d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to (\|(H \circ F) (k) - (H \circ F) (j)\| < x \leftrightarrow \|H (F (k)) - H (F (j))\| < x)$
38	30 37	sylibrd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to (\|F (k) - F (j)\| < x \to \|(H \circ F) (k) - (H \circ F) (j)\| < x)$
39	38	imim2d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in A \land k \in A)) \to ((j \leq k \to \|F (k) - F (j)\| < x) \to (j \leq k \to \|(H \circ F) (k) - (H \circ F) (j)\| < x))$
40	39	anassrs	$⊢ (((φ \land x \in ℝ^{+}) \land j \in A) \land k \in A) \to ((j \leq k \to \|F (k) - F (j)\| < x) \to (j \leq k \to \|(H \circ F) (k) - (H \circ F) (j)\| < x))$
41	40	ralimdva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in A) \to (\forall k \in A (j \leq k \to \|F (k) - F (j)\| < x) \to \forall k \in A (j \leq k \to \|(H \circ F) (k) - (H \circ F) (j)\| < x))$
42	41	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in A \forall k \in A (j \leq k \to \|F (k) - F (j)\| < x) \to \exists j \in A \forall k \in A (j \leq k \to \|(H \circ F) (k) - (H \circ F) (j)\| < x))$
43	42	ralimdva	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in A \forall k \in A (j \leq k \to \|F (k) - F (j)\| < x) \to \forall x \in ℝ^{+} \exists j \in A \forall k \in A (j \leq k \to \|(H \circ F) (k) - (H \circ F) (j)\| < x))$
44	4 43	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in A \forall k \in A (j \leq k \to \|(H \circ F) (k) - (H \circ F) (j)\| < x)$
45	1 10 3 44	caurcvgr	$⊢ φ \to (H \circ F) \underset{ℝ}{⇝} lim sup (H \circ F)$
46		rlimrel	$⊢ Rel \underset{ℝ}{⇝}$
47	46	releldmi	$⊢ (H \circ F) \underset{ℝ}{⇝} lim sup (H \circ F) \to H \circ F \in dom \underset{ℝ}{⇝}$
48	45 47	syl	$⊢ φ \to H \circ F \in dom \underset{ℝ}{⇝}$
49		ax-resscn	$⊢ ℝ \subseteq ℂ$
50		fss	$⊢ ((H \circ F) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (H \circ F) : A ⟶ ℂ$
51	10 49 50	sylancl	$⊢ φ \to (H \circ F) : A ⟶ ℂ$
52	51 3	rlimdm	$⊢ φ \to (H \circ F \in dom \underset{ℝ}{⇝} \leftrightarrow (H \circ F) \underset{ℝ}{⇝} \underset{ℝ}{⇝} (H \circ F))$
53	48 52	mpbid	$⊢ φ \to (H \circ F) \underset{ℝ}{⇝} \underset{ℝ}{⇝} (H \circ F)$
54	8 53	eqbrtrrd	$⊢ φ \to (n \in A ⟼ H (F (n))) \underset{ℝ}{⇝} \underset{ℝ}{⇝} (H \circ F)$

Metamath Proof Explorer

Theorem caucvgrlem2

Proof