Step |
Hyp |
Ref |
Expression |
1 |
|
dvdivbd.s |
|- ( ph -> S e. { RR , CC } ) |
2 |
|
dvdivbd.a |
|- ( ( ph /\ x e. X ) -> A e. CC ) |
3 |
|
dvdivbd.adv |
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> C ) ) |
4 |
|
dvdivbd.c |
|- ( ( ph /\ x e. X ) -> C e. CC ) |
5 |
|
dvdivbd.b |
|- ( ( ph /\ x e. X ) -> B e. CC ) |
6 |
|
dvdivbd.u |
|- ( ph -> U e. RR ) |
7 |
|
dvdivbd.r |
|- ( ph -> R e. RR ) |
8 |
|
dvdivbd.t |
|- ( ph -> T e. RR ) |
9 |
|
dvdivbd.q |
|- ( ph -> Q e. RR ) |
10 |
|
dvdivbd.cbd |
|- ( ( ph /\ x e. X ) -> ( abs ` C ) <_ U ) |
11 |
|
dvdivbd.bbd |
|- ( ( ph /\ x e. X ) -> ( abs ` B ) <_ R ) |
12 |
|
dvdivbd.dbd |
|- ( ( ph /\ x e. X ) -> ( abs ` D ) <_ T ) |
13 |
|
dvdivbd.abd |
|- ( ( ph /\ x e. X ) -> ( abs ` A ) <_ Q ) |
14 |
|
dvdivbd.bdv |
|- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> D ) ) |
15 |
|
dvdivbd.d |
|- ( ( ph /\ x e. X ) -> D e. CC ) |
16 |
|
dvdivbd.e |
|- ( ph -> E e. RR+ ) |
17 |
|
dvdivbd.ele |
|- ( ph -> A. x e. X E <_ ( abs ` B ) ) |
18 |
|
dvdivbd.f |
|- F = ( S _D ( x e. X |-> ( A / B ) ) ) |
19 |
6 7
|
remulcld |
|- ( ph -> ( U x. R ) e. RR ) |
20 |
8 9
|
remulcld |
|- ( ph -> ( T x. Q ) e. RR ) |
21 |
19 20
|
readdcld |
|- ( ph -> ( ( U x. R ) + ( T x. Q ) ) e. RR ) |
22 |
16
|
rpred |
|- ( ph -> E e. RR ) |
23 |
22
|
resqcld |
|- ( ph -> ( E ^ 2 ) e. RR ) |
24 |
16
|
rpcnd |
|- ( ph -> E e. CC ) |
25 |
16
|
rpgt0d |
|- ( ph -> 0 < E ) |
26 |
25
|
gt0ne0d |
|- ( ph -> E =/= 0 ) |
27 |
|
2z |
|- 2 e. ZZ |
28 |
27
|
a1i |
|- ( ph -> 2 e. ZZ ) |
29 |
24 26 28
|
expne0d |
|- ( ph -> ( E ^ 2 ) =/= 0 ) |
30 |
21 23 29
|
redivcld |
|- ( ph -> ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) e. RR ) |
31 |
|
simpr |
|- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> B = 0 ) |
32 |
31
|
abs00bd |
|- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> ( abs ` B ) = 0 ) |
33 |
|
0red |
|- ( ( ph /\ x e. X ) -> 0 e. RR ) |
34 |
22
|
adantr |
|- ( ( ph /\ x e. X ) -> E e. RR ) |
35 |
5
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` B ) e. RR ) |
36 |
25
|
adantr |
|- ( ( ph /\ x e. X ) -> 0 < E ) |
37 |
17
|
r19.21bi |
|- ( ( ph /\ x e. X ) -> E <_ ( abs ` B ) ) |
38 |
33 34 35 36 37
|
ltletrd |
|- ( ( ph /\ x e. X ) -> 0 < ( abs ` B ) ) |
39 |
38
|
gt0ne0d |
|- ( ( ph /\ x e. X ) -> ( abs ` B ) =/= 0 ) |
40 |
39
|
adantr |
|- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> ( abs ` B ) =/= 0 ) |
41 |
40
|
neneqd |
|- ( ( ( ph /\ x e. X ) /\ B = 0 ) -> -. ( abs ` B ) = 0 ) |
42 |
32 41
|
pm2.65da |
|- ( ( ph /\ x e. X ) -> -. B = 0 ) |
43 |
42
|
neqned |
|- ( ( ph /\ x e. X ) -> B =/= 0 ) |
44 |
|
eldifsn |
|- ( B e. ( CC \ { 0 } ) <-> ( B e. CC /\ B =/= 0 ) ) |
45 |
5 43 44
|
sylanbrc |
|- ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) ) |
46 |
1 2 4 3 45 15 14
|
dvmptdiv |
|- ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) ) |
47 |
18 46
|
syl5eq |
|- ( ph -> F = ( x e. X |-> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) ) |
48 |
4 5
|
mulcld |
|- ( ( ph /\ x e. X ) -> ( C x. B ) e. CC ) |
49 |
15 2
|
mulcld |
|- ( ( ph /\ x e. X ) -> ( D x. A ) e. CC ) |
50 |
48 49
|
subcld |
|- ( ( ph /\ x e. X ) -> ( ( C x. B ) - ( D x. A ) ) e. CC ) |
51 |
5
|
sqcld |
|- ( ( ph /\ x e. X ) -> ( B ^ 2 ) e. CC ) |
52 |
|
sqne0 |
|- ( B e. CC -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) ) |
53 |
5 52
|
syl |
|- ( ( ph /\ x e. X ) -> ( ( B ^ 2 ) =/= 0 <-> B =/= 0 ) ) |
54 |
43 53
|
mpbird |
|- ( ( ph /\ x e. X ) -> ( B ^ 2 ) =/= 0 ) |
55 |
50 51 54
|
divcld |
|- ( ( ph /\ x e. X ) -> ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) e. CC ) |
56 |
47 55
|
fvmpt2d |
|- ( ( ph /\ x e. X ) -> ( F ` x ) = ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) |
57 |
56
|
fveq2d |
|- ( ( ph /\ x e. X ) -> ( abs ` ( F ` x ) ) = ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) ) |
58 |
50 51 54
|
absdivd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) = ( ( abs ` ( ( C x. B ) - ( D x. A ) ) ) / ( abs ` ( B ^ 2 ) ) ) ) |
59 |
50
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) e. RR ) |
60 |
21
|
adantr |
|- ( ( ph /\ x e. X ) -> ( ( U x. R ) + ( T x. Q ) ) e. RR ) |
61 |
16
|
adantr |
|- ( ( ph /\ x e. X ) -> E e. RR+ ) |
62 |
27
|
a1i |
|- ( ( ph /\ x e. X ) -> 2 e. ZZ ) |
63 |
61 62
|
rpexpcld |
|- ( ( ph /\ x e. X ) -> ( E ^ 2 ) e. RR+ ) |
64 |
51
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( B ^ 2 ) ) e. RR ) |
65 |
50
|
absge0d |
|- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` ( ( C x. B ) - ( D x. A ) ) ) ) |
66 |
48
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) e. RR ) |
67 |
49
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) e. RR ) |
68 |
66 67
|
readdcld |
|- ( ( ph /\ x e. X ) -> ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) e. RR ) |
69 |
48 49
|
abs2dif2d |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) <_ ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) ) |
70 |
19
|
adantr |
|- ( ( ph /\ x e. X ) -> ( U x. R ) e. RR ) |
71 |
20
|
adantr |
|- ( ( ph /\ x e. X ) -> ( T x. Q ) e. RR ) |
72 |
4 5
|
absmuld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) = ( ( abs ` C ) x. ( abs ` B ) ) ) |
73 |
4
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` C ) e. RR ) |
74 |
6
|
adantr |
|- ( ( ph /\ x e. X ) -> U e. RR ) |
75 |
7
|
adantr |
|- ( ( ph /\ x e. X ) -> R e. RR ) |
76 |
4
|
absge0d |
|- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` C ) ) |
77 |
5
|
absge0d |
|- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` B ) ) |
78 |
73 74 35 75 76 77 10 11
|
lemul12ad |
|- ( ( ph /\ x e. X ) -> ( ( abs ` C ) x. ( abs ` B ) ) <_ ( U x. R ) ) |
79 |
72 78
|
eqbrtrd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( C x. B ) ) <_ ( U x. R ) ) |
80 |
15 2
|
absmuld |
|- ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) = ( ( abs ` D ) x. ( abs ` A ) ) ) |
81 |
15
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` D ) e. RR ) |
82 |
8
|
adantr |
|- ( ( ph /\ x e. X ) -> T e. RR ) |
83 |
2
|
abscld |
|- ( ( ph /\ x e. X ) -> ( abs ` A ) e. RR ) |
84 |
9
|
adantr |
|- ( ( ph /\ x e. X ) -> Q e. RR ) |
85 |
15
|
absge0d |
|- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` D ) ) |
86 |
2
|
absge0d |
|- ( ( ph /\ x e. X ) -> 0 <_ ( abs ` A ) ) |
87 |
81 82 83 84 85 86 12 13
|
lemul12ad |
|- ( ( ph /\ x e. X ) -> ( ( abs ` D ) x. ( abs ` A ) ) <_ ( T x. Q ) ) |
88 |
80 87
|
eqbrtrd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( D x. A ) ) <_ ( T x. Q ) ) |
89 |
66 67 70 71 79 88
|
le2addd |
|- ( ( ph /\ x e. X ) -> ( ( abs ` ( C x. B ) ) + ( abs ` ( D x. A ) ) ) <_ ( ( U x. R ) + ( T x. Q ) ) ) |
90 |
59 68 60 69 89
|
letrd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( C x. B ) - ( D x. A ) ) ) <_ ( ( U x. R ) + ( T x. Q ) ) ) |
91 |
|
2nn0 |
|- 2 e. NN0 |
92 |
91
|
a1i |
|- ( ( ph /\ x e. X ) -> 2 e. NN0 ) |
93 |
33 34 36
|
ltled |
|- ( ( ph /\ x e. X ) -> 0 <_ E ) |
94 |
|
leexp1a |
|- ( ( ( E e. RR /\ ( abs ` B ) e. RR /\ 2 e. NN0 ) /\ ( 0 <_ E /\ E <_ ( abs ` B ) ) ) -> ( E ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) ) |
95 |
34 35 92 93 37 94
|
syl32anc |
|- ( ( ph /\ x e. X ) -> ( E ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) ) |
96 |
5 92
|
absexpd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( B ^ 2 ) ) = ( ( abs ` B ) ^ 2 ) ) |
97 |
95 96
|
breqtrrd |
|- ( ( ph /\ x e. X ) -> ( E ^ 2 ) <_ ( abs ` ( B ^ 2 ) ) ) |
98 |
59 60 63 64 65 90 97
|
lediv12ad |
|- ( ( ph /\ x e. X ) -> ( ( abs ` ( ( C x. B ) - ( D x. A ) ) ) / ( abs ` ( B ^ 2 ) ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) |
99 |
58 98
|
eqbrtrd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( ( ( C x. B ) - ( D x. A ) ) / ( B ^ 2 ) ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) |
100 |
57 99
|
eqbrtrd |
|- ( ( ph /\ x e. X ) -> ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) |
101 |
100
|
ralrimiva |
|- ( ph -> A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) |
102 |
|
brralrspcev |
|- ( ( ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) e. RR /\ A. x e. X ( abs ` ( F ` x ) ) <_ ( ( ( U x. R ) + ( T x. Q ) ) / ( E ^ 2 ) ) ) -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b ) |
103 |
30 101 102
|
syl2anc |
|- ( ph -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b ) |