Theorem 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	⊢ 𝑋 = ( 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	nrginvrcnlem	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑈 ( ( 𝐴 𝐷 𝑦 ) < 𝑥 → ( ( 𝐼 ‘ 𝐴 ) 𝐷 ( 𝐼 ‘ 𝑦 ) ) < 𝐵 ) )

Proof

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