Theorem nrginvrcnlem 24586

Description: Lemma for nrginvrcn 24587. Compare this proof with reccn2 15570, 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 12962	. . . . 5 ⊢ 1 ∈ ℝ+
3		nrginvrcn.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NrmRing)
4		nrgngp 24557	. . . . . . . 8 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ NrmGrp)
6		nrginvrcn.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
7		nrginvrcn.u	. . . . . . . . 9 ⊢ 𝑈 = (Unit‘𝑅)
8	6, 7	unitss 20292	. . . . . . . 8 ⊢ 𝑈 ⊆ 𝑋
9		nrginvrcn.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	8, 9	sselid 3947	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
11		nrginvrcn.z	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NzRing)
12		eqid 2730	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
13	7, 12	nzrunit 20440	. . . . . . . 8 ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ (0g‘𝑅))
14	11, 9, 13	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅))
15		nrginvrcn.n	. . . . . . . 8 ⊢ 𝑁 = (norm‘𝑅)
16	6, 15, 12	nmrpcl 24515	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0g‘𝑅)) → (𝑁‘𝐴) ∈ ℝ+)
17	5, 10, 14, 16	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝑁‘𝐴) ∈ ℝ+)
18		nrginvrcn.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
19	17, 18	rpmulcld 13018	. . . . 5 ⊢ (𝜑 → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
20		ifcl 4537	. . . . 5 ⊢ ((1 ∈ ℝ+ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ+) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
21	2, 19, 20	sylancr 587	. . . 4 ⊢ (𝜑 → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
22	17	rphalfcld 13014	. . . 4 ⊢ (𝜑 → ((𝑁‘𝐴) / 2) ∈ ℝ+)
23	21, 22	rpmulcld 13018	. . 3 ⊢ (𝜑 → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
24	1, 23	eqeltrid 2833	. 2 ⊢ (𝜑 → 𝑇 ∈ ℝ+)
25	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmGrp)
26	9	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑈)
27	6, 7	unitcl 20291	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝑋)
28	26, 27	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑋)
29	6, 15	nmcl 24511	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
30	25, 28, 29	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ)
31	30	recnd 11209	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℂ)
32		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑈)
33	8, 32	sselid 3947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑋)
34	6, 15	nmcl 24511	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
35	25, 33, 34	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ)
36	35	recnd 11209	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℂ)
37		ngpgrp 24494	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp)
38	25, 37	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Grp)
39		nrgring 24558	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
40	3, 39	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Ring)
41	40	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Ring)
42		nrginvrcn.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (invr‘𝑅)
43	7, 42, 6	ringinvcl 20308	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐼‘𝐴) ∈ 𝑋)
44	41, 26, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝐴) ∈ 𝑋)
45	7, 42, 6	ringinvcl 20308	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑋)
46	41, 32, 45	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝑦) ∈ 𝑋)
47		eqid 2730	. . . . . . . . . . . . 13 ⊢ (-g‘𝑅) = (-g‘𝑅)
48	6, 47	grpsubcl 18959	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Grp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
49	38, 44, 46, 48	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
50	6, 15	nmcl 24511	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
51	25, 49, 50	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
52	51	recnd 11209	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℂ)
53	31, 36, 52	mul32d 11391	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
54	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmRing)
55		eqid 2730	. . . . . . . . . . . 12 ⊢ (.r‘𝑅) = (.r‘𝑅)
56	6, 15, 55	nmmul 24559	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
57	54, 28, 49, 56	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
58	6, 55, 47, 41, 28, 44, 46	ringsubdi 20223	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
59		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝑅) = (1r‘𝑅)
60	7, 42, 55, 59	unitrinv 20310	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
61	41, 26, 60	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
62	61	oveq1d 7405	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
63	58, 62	eqtrd 2765	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
64	63	fveq2d 6865	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
65	57, 64	eqtr3d 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
66	65	oveq1d 7405	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
67	6, 59	ringidcl 20181	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝑋)
68	41, 67	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1r‘𝑅) ∈ 𝑋)
69	6, 55	ringcl 20166	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
70	41, 28, 46, 69	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
71	6, 47	grpsubcl 18959	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ (1r‘𝑅) ∈ 𝑋 ∧ (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
72	38, 68, 70, 71	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
73	6, 15, 55	nmmul 24559	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmRing ∧ ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
74	54, 72, 33, 73	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
75	6, 55, 47, 41, 68, 70, 33	ringsubdir 20224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)))
76	6, 55, 59	ringlidm 20185	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑋) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
77	41, 33, 76	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
78	6, 55	ringass 20169	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
79	41, 28, 46, 33, 78	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
80	7, 42, 55, 59	unitlinv 20309	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
81	41, 32, 80	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
82	81	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)) = (𝐴(.r‘𝑅)(1r‘𝑅)))
83	6, 55, 59	ringridm 20186	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
84	41, 28, 83	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
85	79, 82, 84	3eqtrd 2769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = 𝐴)
86	77, 85	oveq12d 7408	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)) = (𝑦(-g‘𝑅)𝐴))
87	75, 86	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (𝑦(-g‘𝑅)𝐴))
88	87	fveq2d 6865	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
89	74, 88	eqtr3d 2767	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
90	53, 66, 89	3eqtrd 2769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
91	6, 47	grpsubcl 18959	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
92	38, 33, 28, 91	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
93	6, 15	nmcl 24511	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
94	25, 92, 93	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
95	94	recnd 11209	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℂ)
96	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ+)
97	11	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NzRing)
98	7, 12	nzrunit 20440	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ NzRing ∧ 𝑦 ∈ 𝑈) → 𝑦 ≠ (0g‘𝑅))
99	97, 32, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ≠ (0g‘𝑅))
100	6, 15, 12	nmrpcl 24515	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ (0g‘𝑅)) → (𝑁‘𝑦) ∈ ℝ+)
101	25, 33, 99, 100	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ+)
102	96, 101	rpmulcld 13018	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ+)
103	102	rpred 13002	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ)
104	103	recnd 11209	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℂ)
105	102	rpne0d 13007	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ≠ 0)
106	95, 104, 52, 105	divmuld 11987	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ↔ (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴))))
107	90, 106	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
108		nrginvrcn.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝑅)
109	15, 6, 47, 108	ngpdsr 24500	. . . . . . . 8 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
110	25, 28, 33, 109	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
111	110	oveq1d 7405	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
112	15, 6, 47, 108	ngpds 24499	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
113	25, 44, 46, 112	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
114	107, 111, 113	3eqtr4rd 2776	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
115	110, 94	eqeltrd 2829	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) ∈ ℝ)
116	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ+)
117	116	rpred 13002	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ)
118	18	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ+)
119	118	rpred 13002	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ)
120	103, 119	remulcld 11211	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) ∈ ℝ)
121		simprr 772	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < 𝑇)
122	19	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
123	96	rphalfcld 13014	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ+)
124	122, 123	rpmulcld 13018	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
125	124	rpred 13002	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ)
126		1re 11181	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
127	122	rpred 13002	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ)
128		min2 13157	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
129	126, 127, 128	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
130	21	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
131	130	rpred 13002	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ)
132	131, 127, 123	lemul1d 13045	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵) ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2))))
133	129, 132	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
134	1, 133	eqbrtrid 5145	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
135	123	rpred 13002	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ)
136	31	2halvesd 12435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) = (𝑁‘𝐴))
137	30, 35	resubcld 11613	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ∈ ℝ)
138	6, 15, 47	nm2dif 24520	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
139	25, 28, 33, 138	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
140	15, 6, 47, 108	ngpds 24499	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
141	25, 28, 33, 140	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
142	139, 141	breqtrrd 5138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝐴𝐷𝑦))
143		min1 13156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
144	126, 127, 143	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
145		1red 11182	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 1 ∈ ℝ)
146	131, 145, 123	lemul1d 13045	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1 ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2))))
147	144, 146	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2)))
148	1, 147	eqbrtrid 5145	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (1 · ((𝑁‘𝐴) / 2)))
149	135	recnd 11209	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℂ)
150	149	mullidd 11199	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1 · ((𝑁‘𝐴) / 2)) = ((𝑁‘𝐴) / 2))
151	148, 150	breqtrd 5136	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ ((𝑁‘𝐴) / 2))
152	115, 117, 135, 121, 151	ltletrd 11341	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < ((𝑁‘𝐴) / 2))
153	137, 115, 135, 142, 152	lelttrd 11339	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2))
154	30, 35, 135	ltsubadd2d 11783	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2) ↔ (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
155	153, 154	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
156	136, 155	eqbrtrd 5132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
157	135, 35, 135	ltadd1d 11778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) < (𝑁‘𝑦) ↔ (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
158	156, 157	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) < (𝑁‘𝑦))
159	135, 35, 122, 158	ltmul2dd 13058	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
160	119	recnd 11209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℂ)
161	31, 36, 160	mul32d 11391	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) = (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
162	159, 161	breqtrrd 5138	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
163	117, 125, 120, 134, 162	lelttrd 11339	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
164	115, 117, 120, 121, 163	lttrd 11342	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
165	115, 119, 102	ltdivmuld 13053	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵 ↔ (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)))
166	164, 165	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵)
167	114, 166	eqbrtrd 5132	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)
168	167	expr 456	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑈) → ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
169	168	ralrimiva 3126	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
170		breq2 5114	. . 3 ⊢ (𝑥 = 𝑇 → ((𝐴𝐷𝑦) < 𝑥 ↔ (𝐴𝐷𝑦) < 𝑇))
171	170	rspceaimv 3597	. 2 ⊢ ((𝑇 ∈ ℝ+ ∧ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
172	24, 169, 171	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  ifcif 4491   class class class wbr 5110  ‘cfv 6514  (class class class)co 7390  ℝcr 11074  1c1 11076   + caddc 11078   · cmul 11080   < clt 11215   ≤ cle 11216   − cmin 11412   / cdiv 11842  2c2 12248  ℝ⁺crp 12958  Basecbs 17186  ._rcmulr 17228  distcds 17236  0_gc0g 17409  Grpcgrp 18872  -_gcsg 18874  1_rcur 20097  Ringcrg 20149  Unitcui 20271  inv_rcinvr 20303  NzRingcnzr 20428  normcnm 24471  NrmGrpcngp 24472  NrmRingcnrg 24474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9400  df-inf 9401  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-z 12537  df-dec 12657  df-uz 12801  df-q 12915  df-rp 12959  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-fz 13476  df-seq 13974  df-exp 14034  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-tset 17246  df-ple 17247  df-ds 17249  df-0g 17411  df-topgen 17413  df-xrs 17472  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875  df-minusg 18876  df-sbg 18877  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-ring 20151  df-oppr 20253  df-dvdsr 20273  df-unit 20274  df-invr 20304  df-nzr 20429  df-abv 20725  df-psmet 21263  df-xmet 21264  df-met 21265  df-bl 21266  df-mopn 21267  df-top 22788  df-topon 22805  df-topsp 22827  df-bases 22840  df-xms 24215  df-ms 24216  df-nm 24477  df-ngp 24478  df-nrg 24480

This theorem is referenced by:  nrginvrcn  24587