Theorem nrginvrcnlem 23297

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

Hypotheses

Ref	Expression
nrginvrcn.x	⊢ 𝑋 = (Base‘𝑅)
nrginvrcn.u	⊢ 𝑈 = (Unit‘𝑅)
nrginvrcn.i	⊢ 𝐼 = (invr‘𝑅)
nrginvrcn.n	⊢ 𝑁 = (norm‘𝑅)
nrginvrcn.d	⊢ 𝐷 = (dist‘𝑅)
nrginvrcn.r	⊢ (𝜑 → 𝑅 ∈ NrmRing)
nrginvrcn.z	⊢ (𝜑 → 𝑅 ∈ NzRing)
nrginvrcn.a	⊢ (𝜑 → 𝐴 ∈ 𝑈)
nrginvrcn.b	⊢ (𝜑 → 𝐵 ∈ ℝ+)
nrginvrcn.t	⊢ 𝑇 = (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2))

Assertion

Ref	Expression
nrginvrcnlem	⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))

Distinct variable groups:   𝑥,𝑦,𝐼   𝜑,𝑦   𝑥,𝑅,𝑦   𝑥,𝑇,𝑦   𝑥,𝑈,𝑦   𝑥,𝐴   𝑥,𝐵   𝑥,𝐷

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑦)   𝐵(𝑦)   𝐷(𝑦)   𝑁(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem nrginvrcnlem

Step	Hyp	Ref	Expression
1		nrginvrcn.t	. . 3 ⊢ 𝑇 = (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2))
2		1rp 12381	. . . . 5 ⊢ 1 ∈ ℝ+
3		nrginvrcn.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NrmRing)
4		nrgngp 23268	. . . . . . . 8 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ NrmGrp)
6		nrginvrcn.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
7		nrginvrcn.u	. . . . . . . . 9 ⊢ 𝑈 = (Unit‘𝑅)
8	6, 7	unitss 19406	. . . . . . . 8 ⊢ 𝑈 ⊆ 𝑋
9		nrginvrcn.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	8, 9	sseldi 3913	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
11		nrginvrcn.z	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NzRing)
12		eqid 2798	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
13	7, 12	nzrunit 20033	. . . . . . . 8 ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ (0g‘𝑅))
14	11, 9, 13	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅))
15		nrginvrcn.n	. . . . . . . 8 ⊢ 𝑁 = (norm‘𝑅)
16	6, 15, 12	nmrpcl 23226	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0g‘𝑅)) → (𝑁‘𝐴) ∈ ℝ+)
17	5, 10, 14, 16	syl3anc 1368	. . . . . 6 ⊢ (𝜑 → (𝑁‘𝐴) ∈ ℝ+)
18		nrginvrcn.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
19	17, 18	rpmulcld 12435	. . . . 5 ⊢ (𝜑 → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
20		ifcl 4469	. . . . 5 ⊢ ((1 ∈ ℝ+ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ+) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
21	2, 19, 20	sylancr 590	. . . 4 ⊢ (𝜑 → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
22	17	rphalfcld 12431	. . . 4 ⊢ (𝜑 → ((𝑁‘𝐴) / 2) ∈ ℝ+)
23	21, 22	rpmulcld 12435	. . 3 ⊢ (𝜑 → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
24	1, 23	eqeltrid 2894	. 2 ⊢ (𝜑 → 𝑇 ∈ ℝ+)
25	5	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmGrp)
26	9	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑈)
27	6, 7	unitcl 19405	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝑋)
28	26, 27	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑋)
29	6, 15	nmcl 23222	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
30	25, 28, 29	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ)
31	30	recnd 10658	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℂ)
32		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑈)
33	8, 32	sseldi 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑋)
34	6, 15	nmcl 23222	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
35	25, 33, 34	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ)
36	35	recnd 10658	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℂ)
37		ngpgrp 23205	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp)
38	25, 37	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Grp)
39		nrgring 23269	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
40	3, 39	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Ring)
41	40	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Ring)
42		nrginvrcn.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (invr‘𝑅)
43	7, 42, 6	ringinvcl 19422	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐼‘𝐴) ∈ 𝑋)
44	41, 26, 43	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝐴) ∈ 𝑋)
45	7, 42, 6	ringinvcl 19422	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑋)
46	41, 32, 45	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝑦) ∈ 𝑋)
47		eqid 2798	. . . . . . . . . . . . 13 ⊢ (-g‘𝑅) = (-g‘𝑅)
48	6, 47	grpsubcl 18171	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Grp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
49	38, 44, 46, 48	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
50	6, 15	nmcl 23222	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
51	25, 49, 50	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
52	51	recnd 10658	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℂ)
53	31, 36, 52	mul32d 10839	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
54	3	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmRing)
55		eqid 2798	. . . . . . . . . . . 12 ⊢ (.r‘𝑅) = (.r‘𝑅)
56	6, 15, 55	nmmul 23270	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
57	54, 28, 49, 56	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
58	6, 55, 47, 41, 28, 44, 46	ringsubdi 19345	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
59		eqid 2798	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝑅) = (1r‘𝑅)
60	7, 42, 55, 59	unitrinv 19424	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
61	41, 26, 60	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
62	61	oveq1d 7150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
63	58, 62	eqtrd 2833	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
64	63	fveq2d 6649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
65	57, 64	eqtr3d 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
66	65	oveq1d 7150	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
67	6, 59	ringidcl 19314	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝑋)
68	41, 67	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1r‘𝑅) ∈ 𝑋)
69	6, 55	ringcl 19307	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
70	41, 28, 46, 69	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
71	6, 47	grpsubcl 18171	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ (1r‘𝑅) ∈ 𝑋 ∧ (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
72	38, 68, 70, 71	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
73	6, 15, 55	nmmul 23270	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmRing ∧ ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
74	54, 72, 33, 73	syl3anc 1368	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
75	6, 55, 47, 41, 68, 70, 33	rngsubdir 19346	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)))
76	6, 55, 59	ringlidm 19317	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑋) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
77	41, 33, 76	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
78	6, 55	ringass 19310	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
79	41, 28, 46, 33, 78	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
80	7, 42, 55, 59	unitlinv 19423	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
81	41, 32, 80	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
82	81	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)) = (𝐴(.r‘𝑅)(1r‘𝑅)))
83	6, 55, 59	ringridm 19318	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
84	41, 28, 83	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
85	79, 82, 84	3eqtrd 2837	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = 𝐴)
86	77, 85	oveq12d 7153	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)) = (𝑦(-g‘𝑅)𝐴))
87	75, 86	eqtrd 2833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (𝑦(-g‘𝑅)𝐴))
88	87	fveq2d 6649	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
89	74, 88	eqtr3d 2835	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
90	53, 66, 89	3eqtrd 2837	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
91	6, 47	grpsubcl 18171	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
92	38, 33, 28, 91	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
93	6, 15	nmcl 23222	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
94	25, 92, 93	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
95	94	recnd 10658	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℂ)
96	17	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ+)
97	11	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NzRing)
98	7, 12	nzrunit 20033	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ NzRing ∧ 𝑦 ∈ 𝑈) → 𝑦 ≠ (0g‘𝑅))
99	97, 32, 98	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ≠ (0g‘𝑅))
100	6, 15, 12	nmrpcl 23226	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ (0g‘𝑅)) → (𝑁‘𝑦) ∈ ℝ+)
101	25, 33, 99, 100	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ+)
102	96, 101	rpmulcld 12435	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ+)
103	102	rpred 12419	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ)
104	103	recnd 10658	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℂ)
105	102	rpne0d 12424	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ≠ 0)
106	95, 104, 52, 105	divmuld 11427	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ↔ (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴))))
107	90, 106	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
108		nrginvrcn.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝑅)
109	15, 6, 47, 108	ngpdsr 23211	. . . . . . . 8 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
110	25, 28, 33, 109	syl3anc 1368	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
111	110	oveq1d 7150	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
112	15, 6, 47, 108	ngpds 23210	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
113	25, 44, 46, 112	syl3anc 1368	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
114	107, 111, 113	3eqtr4rd 2844	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
115	110, 94	eqeltrd 2890	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) ∈ ℝ)
116	24	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ+)
117	116	rpred 12419	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ)
118	18	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ+)
119	118	rpred 12419	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ)
120	103, 119	remulcld 10660	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) ∈ ℝ)
121		simprr 772	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < 𝑇)
122	19	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
123	96	rphalfcld 12431	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ+)
124	122, 123	rpmulcld 12435	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
125	124	rpred 12419	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ)
126		1re 10630	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
127	122	rpred 12419	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ)
128		min2 12571	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
129	126, 127, 128	sylancr 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
130	21	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
131	130	rpred 12419	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ)
132	131, 127, 123	lemul1d 12462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵) ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2))))
133	129, 132	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
134	1, 133	eqbrtrid 5065	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
135	123	rpred 12419	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ)
136	31	2halvesd 11871	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) = (𝑁‘𝐴))
137	30, 35	resubcld 11057	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ∈ ℝ)
138	6, 15, 47	nm2dif 23231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
139	25, 28, 33, 138	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
140	15, 6, 47, 108	ngpds 23210	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
141	25, 28, 33, 140	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
142	139, 141	breqtrrd 5058	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝐴𝐷𝑦))
143		min1 12570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
144	126, 127, 143	sylancr 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
145		1red 10631	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 1 ∈ ℝ)
146	131, 145, 123	lemul1d 12462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1 ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2))))
147	144, 146	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2)))
148	1, 147	eqbrtrid 5065	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (1 · ((𝑁‘𝐴) / 2)))
149	135	recnd 10658	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℂ)
150	149	mulid2d 10648	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1 · ((𝑁‘𝐴) / 2)) = ((𝑁‘𝐴) / 2))
151	148, 150	breqtrd 5056	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ ((𝑁‘𝐴) / 2))
152	115, 117, 135, 121, 151	ltletrd 10789	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < ((𝑁‘𝐴) / 2))
153	137, 115, 135, 142, 152	lelttrd 10787	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2))
154	30, 35, 135	ltsubadd2d 11227	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2) ↔ (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
155	153, 154	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
156	136, 155	eqbrtrd 5052	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
157	135, 35, 135	ltadd1d 11222	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) < (𝑁‘𝑦) ↔ (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
158	156, 157	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) < (𝑁‘𝑦))
159	135, 35, 122, 158	ltmul2dd 12475	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
160	119	recnd 10658	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℂ)
161	31, 36, 160	mul32d 10839	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) = (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
162	159, 161	breqtrrd 5058	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
163	117, 125, 120, 134, 162	lelttrd 10787	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
164	115, 117, 120, 121, 163	lttrd 10790	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
165	115, 119, 102	ltdivmuld 12470	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵 ↔ (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)))
166	164, 165	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵)
167	114, 166	eqbrtrd 5052	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)
168	167	expr 460	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑈) → ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
169	168	ralrimiva 3149	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
170		breq2 5034	. . 3 ⊢ (𝑥 = 𝑇 → ((𝐴𝐷𝑦) < 𝑥 ↔ (𝐴𝐷𝑦) < 𝑇))
171	170	rspceaimv 3576	. 2 ⊢ ((𝑇 ∈ ℝ+ ∧ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
172	24, 169, 171	syl2anc 587	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  ifcif 4425   class class class wbr 5030  ‘cfv 6324  (class class class)co 7135  ℝcr 10525  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664   ≤ cle 10665   − cmin 10859   / cdiv 11286  2c2 11680  ℝ⁺crp 12377  Basecbs 16475  ._rcmulr 16558  distcds 16566  0_gc0g 16705  Grpcgrp 18095  -_gcsg 18097  1_rcur 19244  Ringcrg 19290  Unitcui 19385  inv_rcinvr 19417  NzRingcnzr 20023  normcnm 23183  NrmGrpcngp 23184  NrmRingcnrg 23186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-tpos 7875  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-sup 8890  df-inf 8891  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-fz 12886  df-seq 13365  df-exp 13426  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-tset 16576  df-ple 16577  df-ds 16579  df-0g 16707  df-topgen 16709  df-xrs 16767  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-grp 18098  df-minusg 18099  df-sbg 18100  df-mgp 19233  df-ur 19245  df-ring 19292  df-oppr 19369  df-dvdsr 19387  df-unit 19388  df-invr 19418  df-abv 19581  df-nzr 20024  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-xms 22927  df-ms 22928  df-nm 23189  df-ngp 23190  df-nrg 23192

This theorem is referenced by:  nrginvrcn  23298