Theorem nrginvrcnlem 24055

Description: Lemma for nrginvrcn 24056. Compare this proof with reccn2 15479, 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 12919	. . . . 5 ⊢ 1 ∈ ℝ+
3		nrginvrcn.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NrmRing)
4		nrgngp 24026	. . . . . . . 8 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ NrmGrp)
6		nrginvrcn.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
7		nrginvrcn.u	. . . . . . . . 9 ⊢ 𝑈 = (Unit‘𝑅)
8	6, 7	unitss 20089	. . . . . . . 8 ⊢ 𝑈 ⊆ 𝑋
9		nrginvrcn.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	8, 9	sselid 3942	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
11		nrginvrcn.z	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NzRing)
12		eqid 2736	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
13	7, 12	nzrunit 20737	. . . . . . . 8 ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ (0g‘𝑅))
14	11, 9, 13	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅))
15		nrginvrcn.n	. . . . . . . 8 ⊢ 𝑁 = (norm‘𝑅)
16	6, 15, 12	nmrpcl 23976	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0g‘𝑅)) → (𝑁‘𝐴) ∈ ℝ+)
17	5, 10, 14, 16	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (𝑁‘𝐴) ∈ ℝ+)
18		nrginvrcn.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
19	17, 18	rpmulcld 12973	. . . . 5 ⊢ (𝜑 → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
20		ifcl 4531	. . . . 5 ⊢ ((1 ∈ ℝ+ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ+) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
21	2, 19, 20	sylancr 587	. . . 4 ⊢ (𝜑 → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
22	17	rphalfcld 12969	. . . 4 ⊢ (𝜑 → ((𝑁‘𝐴) / 2) ∈ ℝ+)
23	21, 22	rpmulcld 12973	. . 3 ⊢ (𝜑 → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
24	1, 23	eqeltrid 2842	. 2 ⊢ (𝜑 → 𝑇 ∈ ℝ+)
25	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmGrp)
26	9	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑈)
27	6, 7	unitcl 20088	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝑋)
28	26, 27	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑋)
29	6, 15	nmcl 23972	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
30	25, 28, 29	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ)
31	30	recnd 11183	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℂ)
32		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑈)
33	8, 32	sselid 3942	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑋)
34	6, 15	nmcl 23972	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
35	25, 33, 34	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ)
36	35	recnd 11183	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℂ)
37		ngpgrp 23955	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp)
38	25, 37	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Grp)
39		nrgring 24027	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
40	3, 39	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Ring)
41	40	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Ring)
42		nrginvrcn.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (invr‘𝑅)
43	7, 42, 6	ringinvcl 20105	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐼‘𝐴) ∈ 𝑋)
44	41, 26, 43	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝐴) ∈ 𝑋)
45	7, 42, 6	ringinvcl 20105	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑋)
46	41, 32, 45	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝑦) ∈ 𝑋)
47		eqid 2736	. . . . . . . . . . . . 13 ⊢ (-g‘𝑅) = (-g‘𝑅)
48	6, 47	grpsubcl 18827	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Grp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
49	38, 44, 46, 48	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
50	6, 15	nmcl 23972	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
51	25, 49, 50	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
52	51	recnd 11183	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℂ)
53	31, 36, 52	mul32d 11365	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
54	3	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmRing)
55		eqid 2736	. . . . . . . . . . . 12 ⊢ (.r‘𝑅) = (.r‘𝑅)
56	6, 15, 55	nmmul 24028	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
57	54, 28, 49, 56	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
58	6, 55, 47, 41, 28, 44, 46	ringsubdi 20023	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
59		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝑅) = (1r‘𝑅)
60	7, 42, 55, 59	unitrinv 20107	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
61	41, 26, 60	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
62	61	oveq1d 7372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
63	58, 62	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
64	63	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
65	57, 64	eqtr3d 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
66	65	oveq1d 7372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
67	6, 59	ringidcl 19989	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝑋)
68	41, 67	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1r‘𝑅) ∈ 𝑋)
69	6, 55	ringcl 19981	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
70	41, 28, 46, 69	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
71	6, 47	grpsubcl 18827	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ (1r‘𝑅) ∈ 𝑋 ∧ (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
72	38, 68, 70, 71	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
73	6, 15, 55	nmmul 24028	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmRing ∧ ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
74	54, 72, 33, 73	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
75	6, 55, 47, 41, 68, 70, 33	ringsubdir 20024	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)))
76	6, 55, 59	ringlidm 19992	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑋) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
77	41, 33, 76	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
78	6, 55	ringass 19984	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
79	41, 28, 46, 33, 78	syl13anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
80	7, 42, 55, 59	unitlinv 20106	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
81	41, 32, 80	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
82	81	oveq2d 7373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)) = (𝐴(.r‘𝑅)(1r‘𝑅)))
83	6, 55, 59	ringridm 19993	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
84	41, 28, 83	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
85	79, 82, 84	3eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = 𝐴)
86	77, 85	oveq12d 7375	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)) = (𝑦(-g‘𝑅)𝐴))
87	75, 86	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (𝑦(-g‘𝑅)𝐴))
88	87	fveq2d 6846	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
89	74, 88	eqtr3d 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
90	53, 66, 89	3eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
91	6, 47	grpsubcl 18827	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
92	38, 33, 28, 91	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
93	6, 15	nmcl 23972	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
94	25, 92, 93	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
95	94	recnd 11183	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℂ)
96	17	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ+)
97	11	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NzRing)
98	7, 12	nzrunit 20737	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ NzRing ∧ 𝑦 ∈ 𝑈) → 𝑦 ≠ (0g‘𝑅))
99	97, 32, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ≠ (0g‘𝑅))
100	6, 15, 12	nmrpcl 23976	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ (0g‘𝑅)) → (𝑁‘𝑦) ∈ ℝ+)
101	25, 33, 99, 100	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ+)
102	96, 101	rpmulcld 12973	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ+)
103	102	rpred 12957	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ)
104	103	recnd 11183	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℂ)
105	102	rpne0d 12962	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ≠ 0)
106	95, 104, 52, 105	divmuld 11953	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ↔ (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴))))
107	90, 106	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
108		nrginvrcn.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝑅)
109	15, 6, 47, 108	ngpdsr 23961	. . . . . . . 8 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
110	25, 28, 33, 109	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
111	110	oveq1d 7372	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
112	15, 6, 47, 108	ngpds 23960	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
113	25, 44, 46, 112	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
114	107, 111, 113	3eqtr4rd 2787	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
115	110, 94	eqeltrd 2838	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) ∈ ℝ)
116	24	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ+)
117	116	rpred 12957	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ)
118	18	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ+)
119	118	rpred 12957	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ)
120	103, 119	remulcld 11185	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) ∈ ℝ)
121		simprr 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < 𝑇)
122	19	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
123	96	rphalfcld 12969	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ+)
124	122, 123	rpmulcld 12973	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
125	124	rpred 12957	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ)
126		1re 11155	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
127	122	rpred 12957	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ)
128		min2 13109	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
129	126, 127, 128	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
130	21	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
131	130	rpred 12957	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ)
132	131, 127, 123	lemul1d 13000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵) ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2))))
133	129, 132	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
134	1, 133	eqbrtrid 5140	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
135	123	rpred 12957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ)
136	31	2halvesd 12399	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) = (𝑁‘𝐴))
137	30, 35	resubcld 11583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ∈ ℝ)
138	6, 15, 47	nm2dif 23981	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
139	25, 28, 33, 138	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
140	15, 6, 47, 108	ngpds 23960	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
141	25, 28, 33, 140	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
142	139, 141	breqtrrd 5133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝐴𝐷𝑦))
143		min1 13108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
144	126, 127, 143	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
145		1red 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 1 ∈ ℝ)
146	131, 145, 123	lemul1d 13000	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1 ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2))))
147	144, 146	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2)))
148	1, 147	eqbrtrid 5140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (1 · ((𝑁‘𝐴) / 2)))
149	135	recnd 11183	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℂ)
150	149	mulid2d 11173	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1 · ((𝑁‘𝐴) / 2)) = ((𝑁‘𝐴) / 2))
151	148, 150	breqtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ ((𝑁‘𝐴) / 2))
152	115, 117, 135, 121, 151	ltletrd 11315	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < ((𝑁‘𝐴) / 2))
153	137, 115, 135, 142, 152	lelttrd 11313	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2))
154	30, 35, 135	ltsubadd2d 11753	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2) ↔ (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
155	153, 154	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
156	136, 155	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
157	135, 35, 135	ltadd1d 11748	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) < (𝑁‘𝑦) ↔ (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
158	156, 157	mpbird 256	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) < (𝑁‘𝑦))
159	135, 35, 122, 158	ltmul2dd 13013	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
160	119	recnd 11183	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℂ)
161	31, 36, 160	mul32d 11365	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) = (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
162	159, 161	breqtrrd 5133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
163	117, 125, 120, 134, 162	lelttrd 11313	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
164	115, 117, 120, 121, 163	lttrd 11316	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
165	115, 119, 102	ltdivmuld 13008	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵 ↔ (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)))
166	164, 165	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵)
167	114, 166	eqbrtrd 5127	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)
168	167	expr 457	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑈) → ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
169	168	ralrimiva 3143	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
170		breq2 5109	. . 3 ⊢ (𝑥 = 𝑇 → ((𝐴𝐷𝑦) < 𝑥 ↔ (𝐴𝐷𝑦) < 𝑇))
171	170	rspceaimv 3585	. 2 ⊢ ((𝑇 ∈ ℝ+ ∧ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
172	24, 169, 171	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  ifcif 4486   class class class wbr 5105  ‘cfv 6496  (class class class)co 7357  ℝcr 11050  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189   ≤ cle 11190   − cmin 11385   / cdiv 11812  2c2 12208  ℝ⁺crp 12915  Basecbs 17083  ._rcmulr 17134  distcds 17142  0_gc0g 17321  Grpcgrp 18748  -_gcsg 18750  1_rcur 19913  Ringcrg 19964  Unitcui 20068  inv_rcinvr 20100  NzRingcnzr 20727  normcnm 23932  NrmGrpcngp 23933  NrmRingcnrg 23935

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-fz 13425  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-tset 17152  df-ple 17153  df-ds 17155  df-0g 17323  df-topgen 17325  df-xrs 17384  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mgp 19897  df-ur 19914  df-ring 19966  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-abv 20276  df-nzr 20728  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-xms 23673  df-ms 23674  df-nm 23938  df-ngp 23939  df-nrg 23941

This theorem is referenced by:  nrginvrcn  24056