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 
|- X = ( Base ` R )
nrginvrcn.u 
|- U = ( Unit ` R )
nrginvrcn.i 
|- I = ( invr ` R )
nrginvrcn.n 
|- N = ( norm ` R )
nrginvrcn.d 
|- D = ( dist ` R )
nrginvrcn.r 
|- ( ph -> R e. NrmRing )
nrginvrcn.z 
|- ( ph -> R e. NzRing )
nrginvrcn.a 
|- ( ph -> A e. U )
nrginvrcn.b 
|- ( ph -> B e. RR+ )
nrginvrcn.t 
|- T = ( if ( 1 <_ ( ( N ` A ) x. B ) , 1 , ( ( N ` A ) x. B ) ) x. ( ( N ` A ) / 2 ) )
Assertion nrginvrcnlem 
|- ( ph -> E. x e. RR+ A. y e. U ( ( A D y ) < x -> ( ( I ` A ) D ( I ` y ) ) < B ) )

Proof

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