nrginvrcnlem

Description: Lemma for nrginvrcn . Compare this proof with reccn2 , the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	nrginvrcn.x	$⊢ X = {Base}_{R}$
	nrginvrcn.u	$⊢ U = Unit (R)$
	nrginvrcn.i	$⊢ I = {inv}_{r} (R)$
	nrginvrcn.n	$⊢ N = norm (R)$
	nrginvrcn.d	$⊢ D = dist (R)$
	nrginvrcn.r	$⊢ φ \to R \in NrmRing$
	nrginvrcn.z	$⊢ φ \to R \in NzRing$
	nrginvrcn.a	$⊢ φ \to A \in U$
	nrginvrcn.b	$⊢ φ \to B \in ℝ^{+}$
	nrginvrcn.t	$⊢ T = if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2})$
Assertion	nrginvrcnlem	$⊢ φ \to \exists x \in ℝ^{+} \forall y \in U (A D y < x \to I (A) D I (y) < B)$

Proof

Step	Hyp	Ref	Expression
1		nrginvrcn.x	$⊢ X = {Base}_{R}$
2		nrginvrcn.u	$⊢ U = Unit (R)$
3		nrginvrcn.i	$⊢ I = {inv}_{r} (R)$
4		nrginvrcn.n	$⊢ N = norm (R)$
5		nrginvrcn.d	$⊢ D = dist (R)$
6		nrginvrcn.r	$⊢ φ \to R \in NrmRing$
7		nrginvrcn.z	$⊢ φ \to R \in NzRing$
8		nrginvrcn.a	$⊢ φ \to A \in U$
9		nrginvrcn.b	$⊢ φ \to B \in ℝ^{+}$
10		nrginvrcn.t	$⊢ T = if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2})$
11		1rp	$⊢ 1 \in ℝ^{+}$
12		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
13	6 12	syl	$⊢ φ \to R \in NrmGrp$
14	1 2	unitss	$⊢ U \subseteq X$
15	14 8	sselid	$⊢ φ \to A \in X$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	2 16	nzrunit	$⊢ (R \in NzRing \land A \in U) \to A \neq 0_{R}$
18	7 8 17	syl2anc	$⊢ φ \to A \neq 0_{R}$
19	1 4 16	nmrpcl	$⊢ (R \in NrmGrp \land A \in X \land A \neq 0_{R}) \to N (A) \in ℝ^{+}$
20	13 15 18 19	syl3anc	$⊢ φ \to N (A) \in ℝ^{+}$
21	20 9	rpmulcld	$⊢ φ \to N (A) B \in ℝ^{+}$
22		ifcl	$⊢ (1 \in ℝ^{+} \land N (A) B \in ℝ^{+}) \to if (1 \leq N (A) B, 1, N (A) B) \in ℝ^{+}$
23	11 21 22	sylancr	$⊢ φ \to if (1 \leq N (A) B, 1, N (A) B) \in ℝ^{+}$
24	20	rphalfcld	$⊢ φ \to \frac{N (A)}{2} \in ℝ^{+}$
25	23 24	rpmulcld	$⊢ φ \to if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2}) \in ℝ^{+}$
26	10 25	eqeltrid	$⊢ φ \to T \in ℝ^{+}$
27	13	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to R \in NrmGrp$
28	8	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to A \in U$
29	1 2	unitcl	$⊢ A \in U \to A \in X$
30	28 29	syl	$⊢ (φ \land (y \in U \land A D y < T)) \to A \in X$
31	1 4	nmcl	$⊢ (R \in NrmGrp \land A \in X) \to N (A) \in ℝ$
32	27 30 31	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) \in ℝ$
33	32	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) \in ℂ$
34		simprl	$⊢ (φ \land (y \in U \land A D y < T)) \to y \in U$
35	14 34	sselid	$⊢ (φ \land (y \in U \land A D y < T)) \to y \in X$
36	1 4	nmcl	$⊢ (R \in NrmGrp \land y \in X) \to N (y) \in ℝ$
37	27 35 36	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (y) \in ℝ$
38	37	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (y) \in ℂ$
39		ngpgrp	$⊢ R \in NrmGrp \to R \in Grp$
40	27 39	syl	$⊢ (φ \land (y \in U \land A D y < T)) \to R \in Grp$
41		nrgring	$⊢ R \in NrmRing \to R \in Ring$
42	6 41	syl	$⊢ φ \to R \in Ring$
43	42	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to R \in Ring$
44	2 3 1	ringinvcl	$⊢ (R \in Ring \land A \in U) \to I (A) \in X$
45	43 28 44	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to I (A) \in X$
46	2 3 1	ringinvcl	$⊢ (R \in Ring \land y \in U) \to I (y) \in X$
47	43 34 46	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to I (y) \in X$
48		eqid	$⊢ -_{R} = -_{R}$
49	1 48	grpsubcl	$⊢ (R \in Grp \land I (A) \in X \land I (y) \in X) \to I (A) -_{R} I (y) \in X$
50	40 45 47 49	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to I (A) -_{R} I (y) \in X$
51	1 4	nmcl	$⊢ (R \in NrmGrp \land I (A) -_{R} I (y) \in X) \to N (I (A) -_{R} I (y)) \in ℝ$
52	27 50 51	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (I (A) -_{R} I (y)) \in ℝ$
53	52	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (I (A) -_{R} I (y)) \in ℂ$
54	33 38 53	mul32d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) N (I (A) -_{R} I (y)) = N (A) N (I (A) -_{R} I (y)) N (y)$
55	6	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to R \in NrmRing$
56		eqid	$⊢ \cdot_{R} = \cdot_{R}$
57	1 4 56	nmmul	$⊢ (R \in NrmRing \land A \in X \land I (A) -_{R} I (y) \in X) \to N (A \cdot_{R} (I (A) -_{R} I (y))) = N (A) N (I (A) -_{R} I (y))$
58	55 30 50 57	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A \cdot_{R} (I (A) -_{R} I (y))) = N (A) N (I (A) -_{R} I (y))$
59	1 56 48 43 30 45 47	ringsubdi	$⊢ (φ \land (y \in U \land A D y < T)) \to A \cdot_{R} (I (A) -_{R} I (y)) = (A \cdot_{R} I (A)) -_{R} (A \cdot_{R} I (y))$
60		eqid	$⊢ 1_{R} = 1_{R}$
61	2 3 56 60	unitrinv	$⊢ (R \in Ring \land A \in U) \to A \cdot_{R} I (A) = 1_{R}$
62	43 28 61	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to A \cdot_{R} I (A) = 1_{R}$
63	62	oveq1d	$⊢ (φ \land (y \in U \land A D y < T)) \to (A \cdot_{R} I (A)) -_{R} (A \cdot_{R} I (y)) = 1_{R} -_{R} (A \cdot_{R} I (y))$
64	59 63	eqtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to A \cdot_{R} (I (A) -_{R} I (y)) = 1_{R} -_{R} (A \cdot_{R} I (y))$
65	64	fveq2d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A \cdot_{R} (I (A) -_{R} I (y))) = N (1_{R} -_{R} (A \cdot_{R} I (y)))$
66	58 65	eqtr3d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (I (A) -_{R} I (y)) = N (1_{R} -_{R} (A \cdot_{R} I (y)))$
67	66	oveq1d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (I (A) -_{R} I (y)) N (y) = N (1_{R} -_{R} (A \cdot_{R} I (y))) N (y)$
68	1 60	ringidcl	$⊢ R \in Ring \to 1_{R} \in X$
69	43 68	syl	$⊢ (φ \land (y \in U \land A D y < T)) \to 1_{R} \in X$
70	1 56	ringcl	$⊢ (R \in Ring \land A \in X \land I (y) \in X) \to A \cdot_{R} I (y) \in X$
71	43 30 47 70	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to A \cdot_{R} I (y) \in X$
72	1 48	grpsubcl	$⊢ (R \in Grp \land 1_{R} \in X \land A \cdot_{R} I (y) \in X) \to 1_{R} -_{R} (A \cdot_{R} I (y)) \in X$
73	40 69 71 72	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to 1_{R} -_{R} (A \cdot_{R} I (y)) \in X$
74	1 4 56	nmmul	$⊢ (R \in NrmRing \land 1_{R} -_{R} (A \cdot_{R} I (y)) \in X \land y \in X) \to N ((1_{R} -_{R} (A \cdot_{R} I (y))) \cdot_{R} y) = N (1_{R} -_{R} (A \cdot_{R} I (y))) N (y)$
75	55 73 35 74	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N ((1_{R} -_{R} (A \cdot_{R} I (y))) \cdot_{R} y) = N (1_{R} -_{R} (A \cdot_{R} I (y))) N (y)$
76	1 56 48 43 69 71 35	rngsubdir	$⊢ (φ \land (y \in U \land A D y < T)) \to (1_{R} -_{R} (A \cdot_{R} I (y))) \cdot_{R} y = (1_{R} \cdot_{R} y) -_{R} ((A \cdot_{R} I (y)) \cdot_{R} y)$
77	1 56 60	ringlidm	$⊢ (R \in Ring \land y \in X) \to 1_{R} \cdot_{R} y = y$
78	43 35 77	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to 1_{R} \cdot_{R} y = y$
79	1 56	ringass	$⊢ (R \in Ring \land (A \in X \land I (y) \in X \land y \in X)) \to (A \cdot_{R} I (y)) \cdot_{R} y = A \cdot_{R} (I (y) \cdot_{R} y)$
80	43 30 47 35 79	syl13anc	$⊢ (φ \land (y \in U \land A D y < T)) \to (A \cdot_{R} I (y)) \cdot_{R} y = A \cdot_{R} (I (y) \cdot_{R} y)$
81	2 3 56 60	unitlinv	$⊢ (R \in Ring \land y \in U) \to I (y) \cdot_{R} y = 1_{R}$
82	43 34 81	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to I (y) \cdot_{R} y = 1_{R}$
83	82	oveq2d	$⊢ (φ \land (y \in U \land A D y < T)) \to A \cdot_{R} (I (y) \cdot_{R} y) = A \cdot_{R} 1_{R}$
84	1 56 60	ringridm	$⊢ (R \in Ring \land A \in X) \to A \cdot_{R} 1_{R} = A$
85	43 30 84	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to A \cdot_{R} 1_{R} = A$
86	80 83 85	3eqtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to (A \cdot_{R} I (y)) \cdot_{R} y = A$
87	78 86	oveq12d	$⊢ (φ \land (y \in U \land A D y < T)) \to (1_{R} \cdot_{R} y) -_{R} ((A \cdot_{R} I (y)) \cdot_{R} y) = y -_{R} A$
88	76 87	eqtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to (1_{R} -_{R} (A \cdot_{R} I (y))) \cdot_{R} y = y -_{R} A$
89	88	fveq2d	$⊢ (φ \land (y \in U \land A D y < T)) \to N ((1_{R} -_{R} (A \cdot_{R} I (y))) \cdot_{R} y) = N (y -_{R} A)$
90	75 89	eqtr3d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (1_{R} -_{R} (A \cdot_{R} I (y))) N (y) = N (y -_{R} A)$
91	54 67 90	3eqtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) N (I (A) -_{R} I (y)) = N (y -_{R} A)$
92	1 48	grpsubcl	$⊢ (R \in Grp \land y \in X \land A \in X) \to y -_{R} A \in X$
93	40 35 30 92	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to y -_{R} A \in X$
94	1 4	nmcl	$⊢ (R \in NrmGrp \land y -_{R} A \in X) \to N (y -_{R} A) \in ℝ$
95	27 93 94	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (y -_{R} A) \in ℝ$
96	95	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (y -_{R} A) \in ℂ$
97	20	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) \in ℝ^{+}$
98	7	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to R \in NzRing$
99	2 16	nzrunit	$⊢ (R \in NzRing \land y \in U) \to y \neq 0_{R}$
100	98 34 99	syl2anc	$⊢ (φ \land (y \in U \land A D y < T)) \to y \neq 0_{R}$
101	1 4 16	nmrpcl	$⊢ (R \in NrmGrp \land y \in X \land y \neq 0_{R}) \to N (y) \in ℝ^{+}$
102	27 35 100 101	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (y) \in ℝ^{+}$
103	97 102	rpmulcld	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) \in ℝ^{+}$
104	103	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) \in ℝ$
105	104	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) \in ℂ$
106	103	rpne0d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) \neq 0$
107	96 105 53 106	divmuld	$⊢ (φ \land (y \in U \land A D y < T)) \to (\frac{N (y -_{R} A)}{N (A) N (y)} = N (I (A) -_{R} I (y)) \leftrightarrow N (A) N (y) N (I (A) -_{R} I (y)) = N (y -_{R} A))$
108	91 107	mpbird	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{N (y -_{R} A)}{N (A) N (y)} = N (I (A) -_{R} I (y))$
109	4 1 48 5	ngpdsr	$⊢ (R \in NrmGrp \land A \in X \land y \in X) \to A D y = N (y -_{R} A)$
110	27 30 35 109	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to A D y = N (y -_{R} A)$
111	110	oveq1d	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{A D y}{N (A) N (y)} = \frac{N (y -_{R} A)}{N (A) N (y)}$
112	4 1 48 5	ngpds	$⊢ (R \in NrmGrp \land I (A) \in X \land I (y) \in X) \to I (A) D I (y) = N (I (A) -_{R} I (y))$
113	27 45 47 112	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to I (A) D I (y) = N (I (A) -_{R} I (y))$
114	108 111 113	3eqtr4rd	$⊢ (φ \land (y \in U \land A D y < T)) \to I (A) D I (y) = \frac{A D y}{N (A) N (y)}$
115	110 95	eqeltrd	$⊢ (φ \land (y \in U \land A D y < T)) \to A D y \in ℝ$
116	26	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to T \in ℝ^{+}$
117	116	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to T \in ℝ$
118	9	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to B \in ℝ^{+}$
119	118	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to B \in ℝ$
120	104 119	remulcld	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) B \in ℝ$
121		simprr	$⊢ (φ \land (y \in U \land A D y < T)) \to A D y < T$
122	21	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) B \in ℝ^{+}$
123	97	rphalfcld	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{N (A)}{2} \in ℝ^{+}$
124	122 123	rpmulcld	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) B (\frac{N (A)}{2}) \in ℝ^{+}$
125	124	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) B (\frac{N (A)}{2}) \in ℝ$
126		1re	$⊢ 1 \in ℝ$
127	122	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) B \in ℝ$
128		min2	$⊢ (1 \in ℝ \land N (A) B \in ℝ) \to if (1 \leq N (A) B, 1, N (A) B) \leq N (A) B$
129	126 127 128	sylancr	$⊢ (φ \land (y \in U \land A D y < T)) \to if (1 \leq N (A) B, 1, N (A) B) \leq N (A) B$
130	23	adantr	$⊢ (φ \land (y \in U \land A D y < T)) \to if (1 \leq N (A) B, 1, N (A) B) \in ℝ^{+}$
131	130	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to if (1 \leq N (A) B, 1, N (A) B) \in ℝ$
132	131 127 123	lemul1d	$⊢ (φ \land (y \in U \land A D y < T)) \to (if (1 \leq N (A) B, 1, N (A) B) \leq N (A) B \leftrightarrow if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2}) \leq N (A) B (\frac{N (A)}{2}))$
133	129 132	mpbid	$⊢ (φ \land (y \in U \land A D y < T)) \to if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2}) \leq N (A) B (\frac{N (A)}{2})$
134	10 133	eqbrtrid	$⊢ (φ \land (y \in U \land A D y < T)) \to T \leq N (A) B (\frac{N (A)}{2})$
135	123	rpred	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{N (A)}{2} \in ℝ$
136	33	2halvesd	$⊢ (φ \land (y \in U \land A D y < T)) \to (\frac{N (A)}{2}) + (\frac{N (A)}{2}) = N (A)$
137	32 37	resubcld	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) - N (y) \in ℝ$
138	1 4 48	nm2dif	$⊢ (R \in NrmGrp \land A \in X \land y \in X) \to N (A) - N (y) \leq N (A -_{R} y)$
139	27 30 35 138	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) - N (y) \leq N (A -_{R} y)$
140	4 1 48 5	ngpds	$⊢ (R \in NrmGrp \land A \in X \land y \in X) \to A D y = N (A -_{R} y)$
141	27 30 35 140	syl3anc	$⊢ (φ \land (y \in U \land A D y < T)) \to A D y = N (A -_{R} y)$
142	139 141	breqtrrd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) - N (y) \leq A D y$
143		min1	$⊢ (1 \in ℝ \land N (A) B \in ℝ) \to if (1 \leq N (A) B, 1, N (A) B) \leq 1$
144	126 127 143	sylancr	$⊢ (φ \land (y \in U \land A D y < T)) \to if (1 \leq N (A) B, 1, N (A) B) \leq 1$
145		1red	$⊢ (φ \land (y \in U \land A D y < T)) \to 1 \in ℝ$
146	131 145 123	lemul1d	$⊢ (φ \land (y \in U \land A D y < T)) \to (if (1 \leq N (A) B, 1, N (A) B) \leq 1 \leftrightarrow if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2}) \leq 1 (\frac{N (A)}{2}))$
147	144 146	mpbid	$⊢ (φ \land (y \in U \land A D y < T)) \to if (1 \leq N (A) B, 1, N (A) B) (\frac{N (A)}{2}) \leq 1 (\frac{N (A)}{2})$
148	10 147	eqbrtrid	$⊢ (φ \land (y \in U \land A D y < T)) \to T \leq 1 (\frac{N (A)}{2})$
149	135	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{N (A)}{2} \in ℂ$
150	149	mulid2d	$⊢ (φ \land (y \in U \land A D y < T)) \to 1 (\frac{N (A)}{2}) = \frac{N (A)}{2}$
151	148 150	breqtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to T \leq \frac{N (A)}{2}$
152	115 117 135 121 151	ltletrd	$⊢ (φ \land (y \in U \land A D y < T)) \to A D y < \frac{N (A)}{2}$
153	137 115 135 142 152	lelttrd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) - N (y) < \frac{N (A)}{2}$
154	32 37 135	ltsubadd2d	$⊢ (φ \land (y \in U \land A D y < T)) \to (N (A) - N (y) < \frac{N (A)}{2} \leftrightarrow N (A) < N (y) + (\frac{N (A)}{2}))$
155	153 154	mpbid	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) < N (y) + (\frac{N (A)}{2})$
156	136 155	eqbrtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to (\frac{N (A)}{2}) + (\frac{N (A)}{2}) < N (y) + (\frac{N (A)}{2})$
157	135 37 135	ltadd1d	$⊢ (φ \land (y \in U \land A D y < T)) \to (\frac{N (A)}{2} < N (y) \leftrightarrow (\frac{N (A)}{2}) + (\frac{N (A)}{2}) < N (y) + (\frac{N (A)}{2}))$
158	156 157	mpbird	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{N (A)}{2} < N (y)$
159	135 37 122 158	ltmul2dd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) B (\frac{N (A)}{2}) < N (A) B N (y)$
160	119	recnd	$⊢ (φ \land (y \in U \land A D y < T)) \to B \in ℂ$
161	33 38 160	mul32d	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) N (y) B = N (A) B N (y)$
162	159 161	breqtrrd	$⊢ (φ \land (y \in U \land A D y < T)) \to N (A) B (\frac{N (A)}{2}) < N (A) N (y) B$
163	117 125 120 134 162	lelttrd	$⊢ (φ \land (y \in U \land A D y < T)) \to T < N (A) N (y) B$
164	115 117 120 121 163	lttrd	$⊢ (φ \land (y \in U \land A D y < T)) \to A D y < N (A) N (y) B$
165	115 119 103	ltdivmuld	$⊢ (φ \land (y \in U \land A D y < T)) \to (\frac{A D y}{N (A) N (y)} < B \leftrightarrow A D y < N (A) N (y) B)$
166	164 165	mpbird	$⊢ (φ \land (y \in U \land A D y < T)) \to \frac{A D y}{N (A) N (y)} < B$
167	114 166	eqbrtrd	$⊢ (φ \land (y \in U \land A D y < T)) \to I (A) D I (y) < B$
168	167	expr	$⊢ (φ \land y \in U) \to (A D y < T \to I (A) D I (y) < B)$
169	168	ralrimiva	$⊢ φ \to \forall y \in U (A D y < T \to I (A) D I (y) < B)$
170		breq2	$⊢ x = T \to (A D y < x \leftrightarrow A D y < T)$
171	170	rspceaimv	$⊢ (T \in ℝ^{+} \land \forall y \in U (A D y < T \to I (A) D I (y) < B)) \to \exists x \in ℝ^{+} \forall y \in U (A D y < x \to I (A) D I (y) < B)$
172	26 169 171	syl2anc	$⊢ φ \to \exists x \in ℝ^{+} \forall y \in U (A D y < x \to I (A) D I (y) < B)$

Metamath Proof Explorer

Theorem nrginvrcnlem

Proof