Theorem nrginvrcnlem 24990

Description: Lemma for nrginvrcn 24991. Compare this proof with reccn2 15744, 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 13105	. . . . 5 ⊢ 1 ∈ ℝ+
3		nrginvrcn.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NrmRing)
4		nrgngp 24961	. . . . . . . 8 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
5	3, 4	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ NrmGrp)
6		nrginvrcn.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
7		nrginvrcn.u	. . . . . . . . 9 ⊢ 𝑈 = (Unit‘𝑅)
8	6, 7	unitss 20586	. . . . . . . 8 ⊢ 𝑈 ⊆ 𝑋
9		nrginvrcn.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	8, 9	sselid 3929	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
11		nrginvrcn.z	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NzRing)
12		eqid 2761	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
13	7, 12	nzrunit 20755	. . . . . . . 8 ⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ (0g‘𝑅))
14	11, 9, 13	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅))
15		nrginvrcn.n	. . . . . . . 8 ⊢ 𝑁 = (norm‘𝑅)
16	6, 15, 12	nmrpcl 24919	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0g‘𝑅)) → (𝑁‘𝐴) ∈ ℝ+)
17	5, 10, 14, 16	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝑁‘𝐴) ∈ ℝ+)
18		nrginvrcn.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
19	17, 18	rpmulcld 13161	. . . . 5 ⊢ (𝜑 → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
20		ifcl 4528	. . . . 5 ⊢ ((1 ∈ ℝ+ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ+) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
21	2, 19, 20	sylancr 599	. . . 4 ⊢ (𝜑 → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
22	17	rphalfcld 13157	. . . 4 ⊢ (𝜑 → ((𝑁‘𝐴) / 2) ∈ ℝ+)
23	21, 22	rpmulcld 13161	. . 3 ⊢ (𝜑 → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
24	1, 23	eqeltrid 2865	. 2 ⊢ (𝜑 → 𝑇 ∈ ℝ+)
25	5	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmGrp)
26	9	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑈)
27	6, 7	unitcl 20585	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝑋)
28	26, 27	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑋)
29	6, 15	nmcl 24915	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
30	25, 28, 29	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ)
31	30	recnd 11318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℂ)
32		simprl 783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑈)
33	8, 32	sselid 3929	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑋)
34	6, 15	nmcl 24915	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
35	25, 33, 34	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ)
36	35	recnd 11318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℂ)
37		ngpgrp 24898	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp)
38	25, 37	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Grp)
39		nrgring 24962	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
40	3, 39	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Ring)
41	40	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Ring)
42		nrginvrcn.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (invr‘𝑅)
43	7, 42, 6	ringinvcl 20602	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐼‘𝐴) ∈ 𝑋)
44	41, 26, 43	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝐴) ∈ 𝑋)
45	7, 42, 6	ringinvcl 20602	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑋)
46	41, 32, 45	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝑦) ∈ 𝑋)
47		eqid 2761	. . . . . . . . . . . . 13 ⊢ (-g‘𝑅) = (-g‘𝑅)
48	6, 47	grpsubcl 19210	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Grp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
49	38, 44, 46, 48	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
50	6, 15	nmcl 24915	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmGrp ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
51	25, 49, 50	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ)
52	51	recnd 11318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℂ)
53	31, 36, 52	mul32d 11501	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
54	3	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmRing)
55		eqid 2761	. . . . . . . . . . . 12 ⊢ (.r‘𝑅) = (.r‘𝑅)
56	6, 15, 55	nmmul 24963	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
57	54, 28, 49, 56	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))))
58	6, 55, 47, 41, 28, 44, 46	ringsubdi 20518	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
59		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝑅) = (1r‘𝑅)
60	7, 42, 55, 59	unitrinv 20604	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
61	41, 26, 60	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅))
62	61	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
63	58, 62	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))
64	63	fveq2d 6881	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
65	57, 64	eqtr3d 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))))
66	65	oveq1d 7427	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
67	6, 59	ringidcl 20474	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝑋)
68	41, 67	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1r‘𝑅) ∈ 𝑋)
69	6, 55	ringcl 20457	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
70	41, 28, 46, 69	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋)
71	6, 47	grpsubcl 19210	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ (1r‘𝑅) ∈ 𝑋 ∧ (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
72	38, 68, 70, 71	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋)
73	6, 15, 55	nmmul 24963	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmRing ∧ ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
74	54, 72, 33, 73	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)))
75	6, 55, 47, 41, 68, 70, 33	ringsubdir 20519	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)))
76	6, 55, 59	ringlidm 20478	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑋) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
77	41, 33, 76	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦)
78	6, 55	ringass 20460	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
79	41, 28, 46, 33, 78	syl13anc 1399	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)))
80	7, 42, 55, 59	unitlinv 20603	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
81	41, 32, 80	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅))
82	81	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)) = (𝐴(.r‘𝑅)(1r‘𝑅)))
83	6, 55, 59	ringridm 20479	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
84	41, 28, 83	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴)
85	79, 82, 84	3eqtrd 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = 𝐴)
86	77, 85	oveq12d 7430	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)) = (𝑦(-g‘𝑅)𝐴))
87	75, 86	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (𝑦(-g‘𝑅)𝐴))
88	87	fveq2d 6881	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
89	74, 88	eqtr3d 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
90	53, 66, 89	3eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
91	6, 47	grpsubcl 19210	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
92	38, 33, 28, 91	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋)
93	6, 15	nmcl 24915	. . . . . . . . . 10 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
94	25, 92, 93	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ)
95	94	recnd 11318	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℂ)
96	17	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ+)
97	11	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NzRing)
98	7, 12	nzrunit 20755	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ NzRing ∧ 𝑦 ∈ 𝑈) → 𝑦 ≠ (0g‘𝑅))
99	97, 32, 98	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ≠ (0g‘𝑅))
100	6, 15, 12	nmrpcl 24919	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ (0g‘𝑅)) → (𝑁‘𝑦) ∈ ℝ+)
101	25, 33, 99, 100	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ+)
102	96, 101	rpmulcld 13161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ+)
103	102	rpred 13145	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ)
104	103	recnd 11318	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℂ)
105	102	rpne0d 13150	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ≠ 0)
106	95, 104, 52, 105	divmuld 12096	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ↔ (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴))))
107	90, 106	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
108		nrginvrcn.d	. . . . . . . . 9 ⊢ 𝐷 = (dist‘𝑅)
109	15, 6, 47, 108	ngpdsr 24904	. . . . . . . 8 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
110	25, 28, 33, 109	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))
111	110	oveq1d 7427	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
112	15, 6, 47, 108	ngpds 24903	. . . . . . 7 ⊢ ((𝑅 ∈ NrmGrp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
113	25, 44, 46, 112	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))
114	107, 111, 113	3eqtr4rd 2807	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))))
115	110, 94	eqeltrd 2861	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) ∈ ℝ)
116	24	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ+)
117	116	rpred 13145	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ)
118	18	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ+)
119	118	rpred 13145	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ)
120	103, 119	remulcld 11320	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) ∈ ℝ)
121		simprr 785	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < 𝑇)
122	19	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ+)
123	96	rphalfcld 13157	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ+)
124	122, 123	rpmulcld 13161	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ+)
125	124	rpred 13145	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ)
126		1re 11289	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
127	122	rpred 13145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ)
128		min2 13301	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
129	126, 127, 128	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵))
130	21	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ+)
131	130	rpred 13145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ)
132	131, 127, 123	lemul1d 13188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵) ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2))))
133	129, 132	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
134	1, 133	eqbrtrid 5140	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))
135	123	rpred 13145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ)
136	31	2halvesd 12573	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) = (𝑁‘𝐴))
137	30, 35	resubcld 11725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ∈ ℝ)
138	6, 15, 47	nm2dif 24924	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
139	25, 28, 33, 138	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦)))
140	15, 6, 47, 108	ngpds 24903	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
141	25, 28, 33, 140	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦)))
142	139, 141	breqtrrd 5133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝐴𝐷𝑦))
143		min1 13300	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
144	126, 127, 143	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1)
145		1red 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 1 ∈ ℝ)
146	131, 145, 123	lemul1d 13188	. . . . . . . . . . . . . . . . . 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 5140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (1 · ((𝑁‘𝐴) / 2)))
149	135	recnd 11318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℂ)
150	149	mullidd 11308	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1 · ((𝑁‘𝐴) / 2)) = ((𝑁‘𝐴) / 2))
151	148, 150	breqtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ ((𝑁‘𝐴) / 2))
152	115, 117, 135, 121, 151	ltletrd 11451	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < ((𝑁‘𝐴) / 2))
153	137, 115, 135, 142, 152	lelttrd 11449	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2))
154	30, 35, 135	ltsubadd2d 11895	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2) ↔ (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
155	153, 154	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
156	136, 155	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))
157	135, 35, 135	ltadd1d 11890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) < (𝑁‘𝑦) ↔ (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))))
158	156, 157	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) < (𝑁‘𝑦))
159	135, 35, 122, 158	ltmul2dd 13201	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
160	119	recnd 11318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℂ)
161	31, 36, 160	mul32d 11501	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) = (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦)))
162	159, 161	breqtrrd 5133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
163	117, 125, 120, 134, 162	lelttrd 11449	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
164	115, 117, 120, 121, 163	lttrd 11452	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))
165	115, 119, 102	ltdivmuld 13196	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵 ↔ (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)))
166	164, 165	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵)
167	114, 166	eqbrtrd 5127	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)
168	167	expr 462	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑈) → ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
169	168	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
170		breq2 5107	. . 3 ⊢ (𝑥 = 𝑇 → ((𝐴𝐷𝑦) < 𝑥 ↔ (𝐴𝐷𝑦) < 𝑇))
171	170	rspceaimv 3583	. 2 ⊢ ((𝑇 ∈ ℝ+ ∧ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))
172	24, 169, 171	syl2anc 596	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  ifcif 4482   class class class wbr 5103  ‘cfv 6531  (class class class)co 7412  ℝcr 11180  1c1 11182   + caddc 11184   · cmul 11186   < clt 11324   ≤ cle 11325   − cmin 11522   / cdiv 11954  2c2 12378  ℝ⁺crp 13101  Basecbs 17367  ._rcmulr 17409  distcds 17417  0_gc0g 17590  Grpcgrp 19124  -_gcsg 19126  1_rcur 20387  Ringcrg 20439  Unitcui 20565  inv_rcinvr 20597  NzRingcnzr 20742  normcnm 24875  NrmGrpcngp 24876  NrmRingcnrg 24878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-tpos 8227  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-er 8701  df-map 8833  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9418  df-inf 9419  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-5 12389  df-6 12390  df-7 12391  df-8 12392  df-9 12393  df-n0 12588  df-z 12675  df-dec 12796  df-uz 12947  df-q 13057  df-rp 13102  df-xneg 13222  df-xadd 13223  df-xmul 13224  df-fz 13621  df-seq 14125  df-exp 14185  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-struct 17305  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-mulr 17422  df-tset 17427  df-ple 17428  df-ds 17430  df-0g 17592  df-topgen 17594  df-xrs 17654  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-grp 19127  df-minusg 19128  df-sbg 19129  df-cmn 19976  df-abl 19977  df-mgp 20341  df-rng 20355  df-ur 20388  df-ring 20441  df-oppr 20547  df-dvdsr 20567  df-unit 20568  df-invr 20598  df-nzr 20743  df-abv 21046  df-psmet 21650  df-xmet 21651  df-met 21652  df-bl 21653  df-mopn 21654  df-top 23192  df-topon 23209  df-topsp 23231  df-bases 23244  df-xms 24619  df-ms 24620  df-nm 24881  df-ngp 24882  df-nrg 24884

This theorem is used by:  nrginvrcn  24991