lnconi

Description: Lemma for lnopconi and lnfnconi . (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lncon.1	$⊢ T \in C \to S \in ℝ$
	lncon.2	$⊢ (T \in C \land y \in ℋ) \to N (T (y)) \leq S {norm}_{ℎ} (y)$
	lncon.3	$⊢ T \in C \leftrightarrow \forall x \in ℋ \forall z \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to N (T (w) M T (x)) < z)$
	lncon.4	$⊢ y \in ℋ \to N (T (y)) \in ℝ$
	lncon.5	$⊢ (w \in ℋ \land x \in ℋ) \to T (w -_{ℎ} x) = T (w) M T (x)$
Assertion	lnconi	$⊢ T \in C \leftrightarrow \exists x \in ℝ \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)$

Proof

Step	Hyp	Ref	Expression
1		lncon.1	$⊢ T \in C \to S \in ℝ$
2		lncon.2	$⊢ (T \in C \land y \in ℋ) \to N (T (y)) \leq S {norm}_{ℎ} (y)$
3		lncon.3	$⊢ T \in C \leftrightarrow \forall x \in ℋ \forall z \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to N (T (w) M T (x)) < z)$
4		lncon.4	$⊢ y \in ℋ \to N (T (y)) \in ℝ$
5		lncon.5	$⊢ (w \in ℋ \land x \in ℋ) \to T (w -_{ℎ} x) = T (w) M T (x)$
6	2	ralrimiva	$⊢ T \in C \to \forall y \in ℋ N (T (y)) \leq S {norm}_{ℎ} (y)$
7		oveq1	$⊢ x = S \to x {norm}_{ℎ} (y) = S {norm}_{ℎ} (y)$
8	7	breq2d	$⊢ x = S \to (N (T (y)) \leq x {norm}_{ℎ} (y) \leftrightarrow N (T (y)) \leq S {norm}_{ℎ} (y))$
9	8	ralbidv	$⊢ x = S \to (\forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y) \leftrightarrow \forall y \in ℋ N (T (y)) \leq S {norm}_{ℎ} (y))$
10	9	rspcev	$⊢ (S \in ℝ \land \forall y \in ℋ N (T (y)) \leq S {norm}_{ℎ} (y)) \to \exists x \in ℝ \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)$
11	1 6 10	syl2anc	$⊢ T \in C \to \exists x \in ℝ \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)$
12		arch	$⊢ x \in ℝ \to \exists n \in ℕ x < n$
13	12	adantr	$⊢ (x \in ℝ \land \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)) \to \exists n \in ℕ x < n$
14		nnre	$⊢ n \in ℕ \to n \in ℝ$
15		simplll	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to x \in ℝ$
16		simpllr	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to n \in ℝ$
17		normcl	$⊢ y \in ℋ \to {norm}_{ℎ} (y) \in ℝ$
18	17	adantl	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to {norm}_{ℎ} (y) \in ℝ$
19		normge0	$⊢ y \in ℋ \to 0 \leq {norm}_{ℎ} (y)$
20	19	adantl	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to 0 \leq {norm}_{ℎ} (y)$
21		ltle	$⊢ (x \in ℝ \land n \in ℝ) \to (x < n \to x \leq n)$
22	21	imp	$⊢ ((x \in ℝ \land n \in ℝ) \land x < n) \to x \leq n$
23	22	adantr	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to x \leq n$
24	15 16 18 20 23	lemul1ad	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to x {norm}_{ℎ} (y) \leq n {norm}_{ℎ} (y)$
25	4	adantl	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to N (T (y)) \in ℝ$
26		simpll	$⊢ ((x \in ℝ \land n \in ℝ) \land x < n) \to x \in ℝ$
27		remulcl	$⊢ (x \in ℝ \land {norm}_{ℎ} (y) \in ℝ) \to x {norm}_{ℎ} (y) \in ℝ$
28	26 17 27	syl2an	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to x {norm}_{ℎ} (y) \in ℝ$
29		simplr	$⊢ ((x \in ℝ \land n \in ℝ) \land x < n) \to n \in ℝ$
30		remulcl	$⊢ (n \in ℝ \land {norm}_{ℎ} (y) \in ℝ) \to n {norm}_{ℎ} (y) \in ℝ$
31	29 17 30	syl2an	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to n {norm}_{ℎ} (y) \in ℝ$
32		letr	$⊢ (N (T (y)) \in ℝ \land x {norm}_{ℎ} (y) \in ℝ \land n {norm}_{ℎ} (y) \in ℝ) \to ((N (T (y)) \leq x {norm}_{ℎ} (y) \land x {norm}_{ℎ} (y) \leq n {norm}_{ℎ} (y)) \to N (T (y)) \leq n {norm}_{ℎ} (y))$
33	25 28 31 32	syl3anc	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to ((N (T (y)) \leq x {norm}_{ℎ} (y) \land x {norm}_{ℎ} (y) \leq n {norm}_{ℎ} (y)) \to N (T (y)) \leq n {norm}_{ℎ} (y))$
34	24 33	mpan2d	$⊢ (((x \in ℝ \land n \in ℝ) \land x < n) \land y \in ℋ) \to (N (T (y)) \leq x {norm}_{ℎ} (y) \to N (T (y)) \leq n {norm}_{ℎ} (y))$
35	34	ralimdva	$⊢ ((x \in ℝ \land n \in ℝ) \land x < n) \to (\forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y) \to \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y))$
36	35	impancom	$⊢ ((x \in ℝ \land n \in ℝ) \land \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)) \to (x < n \to \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y))$
37	36	an32s	$⊢ ((x \in ℝ \land \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)) \land n \in ℝ) \to (x < n \to \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y))$
38	14 37	sylan2	$⊢ ((x \in ℝ \land \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)) \land n \in ℕ) \to (x < n \to \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y))$
39	38	reximdva	$⊢ (x \in ℝ \land \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)) \to (\exists n \in ℕ x < n \to \exists n \in ℕ \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y))$
40	13 39	mpd	$⊢ (x \in ℝ \land \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)) \to \exists n \in ℕ \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)$
41	40	rexlimiva	$⊢ \exists x \in ℝ \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y) \to \exists n \in ℕ \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)$
42		simprr	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \to z \in ℝ^{+}$
43		simpll	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \to n \in ℕ$
44	43	nnrpd	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \to n \in ℝ^{+}$
45	42 44	rpdivcld	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \to \frac{z}{n} \in ℝ^{+}$
46		simprr	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to w \in ℋ$
47		simprll	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to x \in ℋ$
48		hvsubcl	$⊢ (w \in ℋ \land x \in ℋ) \to w -_{ℎ} x \in ℋ$
49	46 47 48	syl2anc	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to w -_{ℎ} x \in ℋ$
50		2fveq3	$⊢ y = w -_{ℎ} x \to N (T (y)) = N (T (w -_{ℎ} x))$
51		fveq2	$⊢ y = w -_{ℎ} x \to {norm}_{ℎ} (y) = {norm}_{ℎ} (w -_{ℎ} x)$
52	51	oveq2d	$⊢ y = w -_{ℎ} x \to n {norm}_{ℎ} (y) = n {norm}_{ℎ} (w -_{ℎ} x)$
53	50 52	breq12d	$⊢ y = w -_{ℎ} x \to (N (T (y)) \leq n {norm}_{ℎ} (y) \leftrightarrow N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x))$
54	53	rspcva	$⊢ (w -_{ℎ} x \in ℋ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \to N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x)$
55	49 54	sylan	$⊢ ((n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \to N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x)$
56	55	an32s	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x)$
57	50	eleq1d	$⊢ y = w -_{ℎ} x \to (N (T (y)) \in ℝ \leftrightarrow N (T (w -_{ℎ} x)) \in ℝ)$
58	57 4	vtoclga	$⊢ w -_{ℎ} x \in ℋ \to N (T (w -_{ℎ} x)) \in ℝ$
59	49 58	syl	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to N (T (w -_{ℎ} x)) \in ℝ$
60	14	adantr	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to n \in ℝ$
61		normcl	$⊢ w -_{ℎ} x \in ℋ \to {norm}_{ℎ} (w -_{ℎ} x) \in ℝ$
62	49 61	syl	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to {norm}_{ℎ} (w -_{ℎ} x) \in ℝ$
63		remulcl	$⊢ (n \in ℝ \land {norm}_{ℎ} (w -_{ℎ} x) \in ℝ) \to n {norm}_{ℎ} (w -_{ℎ} x) \in ℝ$
64	60 62 63	syl2anc	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to n {norm}_{ℎ} (w -_{ℎ} x) \in ℝ$
65		simprlr	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to z \in ℝ^{+}$
66	65	rpred	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to z \in ℝ$
67		lelttr	$⊢ (N (T (w -_{ℎ} x)) \in ℝ \land n {norm}_{ℎ} (w -_{ℎ} x) \in ℝ \land z \in ℝ) \to ((N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x) \land n {norm}_{ℎ} (w -_{ℎ} x) < z) \to N (T (w -_{ℎ} x)) < z)$
68	59 64 66 67	syl3anc	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to ((N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x) \land n {norm}_{ℎ} (w -_{ℎ} x) < z) \to N (T (w -_{ℎ} x)) < z)$
69	68	adantlr	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to ((N (T (w -_{ℎ} x)) \leq n {norm}_{ℎ} (w -_{ℎ} x) \land n {norm}_{ℎ} (w -_{ℎ} x) < z) \to N (T (w -_{ℎ} x)) < z)$
70	56 69	mpand	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to (n {norm}_{ℎ} (w -_{ℎ} x) < z \to N (T (w -_{ℎ} x)) < z)$
71		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
72	71	rpregt0d	$⊢ n \in ℕ \to (n \in ℝ \land 0 < n)$
73	72	adantr	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to (n \in ℝ \land 0 < n)$
74		ltmuldiv2	$⊢ ({norm}_{ℎ} (w -_{ℎ} x) \in ℝ \land z \in ℝ \land (n \in ℝ \land 0 < n)) \to (n {norm}_{ℎ} (w -_{ℎ} x) < z \leftrightarrow {norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n})$
75	62 66 73 74	syl3anc	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to (n {norm}_{ℎ} (w -_{ℎ} x) < z \leftrightarrow {norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n})$
76	75	adantlr	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to (n {norm}_{ℎ} (w -_{ℎ} x) < z \leftrightarrow {norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n})$
77	46 47 5	syl2anc	$⊢ (n \in ℕ \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to T (w -_{ℎ} x) = T (w) M T (x)$
78	77	adantlr	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to T (w -_{ℎ} x) = T (w) M T (x)$
79	78	fveq2d	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to N (T (w -_{ℎ} x)) = N (T (w) M T (x))$
80	79	breq1d	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to (N (T (w -_{ℎ} x)) < z \leftrightarrow N (T (w) M T (x)) < z)$
81	70 76 80	3imtr3d	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land ((x \in ℋ \land z \in ℝ^{+}) \land w \in ℋ)) \to ({norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n} \to N (T (w) M T (x)) < z)$
82	81	anassrs	$⊢ (((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \land w \in ℋ) \to ({norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n} \to N (T (w) M T (x)) < z)$
83	82	ralrimiva	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \to \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n} \to N (T (w) M T (x)) < z)$
84		breq2	$⊢ y = \frac{z}{n} \to ({norm}_{ℎ} (w -_{ℎ} x) < y \leftrightarrow {norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n})$
85	84	rspceaimv	$⊢ (\frac{z}{n} \in ℝ^{+} \land \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < \frac{z}{n} \to N (T (w) M T (x)) < z)) \to \exists y \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to N (T (w) M T (x)) < z)$
86	45 83 85	syl2anc	$⊢ ((n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \land (x \in ℋ \land z \in ℝ^{+})) \to \exists y \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to N (T (w) M T (x)) < z)$
87	86	ralrimivva	$⊢ (n \in ℕ \land \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y)) \to \forall x \in ℋ \forall z \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to N (T (w) M T (x)) < z)$
88	87	rexlimiva	$⊢ \exists n \in ℕ \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y) \to \forall x \in ℋ \forall z \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to N (T (w) M T (x)) < z)$
89	88 3	sylibr	$⊢ \exists n \in ℕ \forall y \in ℋ N (T (y)) \leq n {norm}_{ℎ} (y) \to T \in C$
90	41 89	syl	$⊢ \exists x \in ℝ \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y) \to T \in C$
91	11 90	impbii	$⊢ T \in C \leftrightarrow \exists x \in ℝ \forall y \in ℋ N (T (y)) \leq x {norm}_{ℎ} (y)$

Metamath Proof Explorer

Theorem lnconi

Proof