Metamath Proof Explorer

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 sseldi ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
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 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ ( 𝐴 𝐷 𝑦 ) < 𝑇 ) ) → 𝑦 ∈ 𝑋 )
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 rngsubdir ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ ( 𝐴 𝐷 𝑦 ) < 𝑇 ) ) → ( ( ( 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 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑈 ∧ ( 𝐴 𝐷 𝑦 ) < 𝑇 ) ) → ( 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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑈 ( ( 𝐴 𝐷 𝑦 ) < 𝑥 → ( ( 𝐼 ‘ 𝐴 ) 𝐷 ( 𝐼 ‘ 𝑦 ) ) < 𝐵 ) )