Step |
Hyp |
Ref |
Expression |
1 |
|
fprodle.kph |
|- F/ k ph |
2 |
|
fprodle.a |
|- ( ph -> A e. Fin ) |
3 |
|
fprodle.b |
|- ( ( ph /\ k e. A ) -> B e. RR ) |
4 |
|
fprodle.0l3b |
|- ( ( ph /\ k e. A ) -> 0 <_ B ) |
5 |
|
fprodle.c |
|- ( ( ph /\ k e. A ) -> C e. RR ) |
6 |
|
fprodle.blec |
|- ( ( ph /\ k e. A ) -> B <_ C ) |
7 |
|
1red |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> 1 e. RR ) |
8 |
|
nfra1 |
|- F/ k A. k e. A B =/= 0 |
9 |
1 8
|
nfan |
|- F/ k ( ph /\ A. k e. A B =/= 0 ) |
10 |
2
|
adantr |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> A e. Fin ) |
11 |
5
|
adantlr |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> C e. RR ) |
12 |
3
|
adantlr |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B e. RR ) |
13 |
|
rspa |
|- ( ( A. k e. A B =/= 0 /\ k e. A ) -> B =/= 0 ) |
14 |
13
|
adantll |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B =/= 0 ) |
15 |
11 12 14
|
redivcld |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> ( C / B ) e. RR ) |
16 |
9 10 15
|
fprodreclf |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A ( C / B ) e. RR ) |
17 |
1 2 3
|
fprodreclf |
|- ( ph -> prod_ k e. A B e. RR ) |
18 |
17
|
adantr |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B e. RR ) |
19 |
1 2 3 4
|
fprodge0 |
|- ( ph -> 0 <_ prod_ k e. A B ) |
20 |
19
|
adantr |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> 0 <_ prod_ k e. A B ) |
21 |
4
|
adantlr |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> 0 <_ B ) |
22 |
12 21 14
|
ne0gt0d |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> 0 < B ) |
23 |
12 22
|
elrpd |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B e. RR+ ) |
24 |
6
|
adantlr |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B <_ C ) |
25 |
|
divge1 |
|- ( ( B e. RR+ /\ C e. RR /\ B <_ C ) -> 1 <_ ( C / B ) ) |
26 |
23 11 24 25
|
syl3anc |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> 1 <_ ( C / B ) ) |
27 |
9 10 15 26
|
fprodge1 |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> 1 <_ prod_ k e. A ( C / B ) ) |
28 |
7 16 18 20 27
|
lemul2ad |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. 1 ) <_ ( prod_ k e. A B x. prod_ k e. A ( C / B ) ) ) |
29 |
3
|
recnd |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
30 |
1 2 29
|
fprodclf |
|- ( ph -> prod_ k e. A B e. CC ) |
31 |
30
|
mulid1d |
|- ( ph -> ( prod_ k e. A B x. 1 ) = prod_ k e. A B ) |
32 |
31
|
adantr |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. 1 ) = prod_ k e. A B ) |
33 |
5
|
recnd |
|- ( ( ph /\ k e. A ) -> C e. CC ) |
34 |
33
|
adantlr |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> C e. CC ) |
35 |
29
|
adantlr |
|- ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B e. CC ) |
36 |
9 10 34 35 14
|
fproddivf |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A ( C / B ) = ( prod_ k e. A C / prod_ k e. A B ) ) |
37 |
36
|
oveq2d |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. prod_ k e. A ( C / B ) ) = ( prod_ k e. A B x. ( prod_ k e. A C / prod_ k e. A B ) ) ) |
38 |
1 2 33
|
fprodclf |
|- ( ph -> prod_ k e. A C e. CC ) |
39 |
38
|
adantr |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A C e. CC ) |
40 |
30
|
adantr |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B e. CC ) |
41 |
9 10 35 14
|
fprodn0f |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B =/= 0 ) |
42 |
39 40 41
|
divcan2d |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. ( prod_ k e. A C / prod_ k e. A B ) ) = prod_ k e. A C ) |
43 |
37 42
|
eqtrd |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. prod_ k e. A ( C / B ) ) = prod_ k e. A C ) |
44 |
28 32 43
|
3brtr3d |
|- ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B <_ prod_ k e. A C ) |
45 |
|
nne |
|- ( -. B =/= 0 <-> B = 0 ) |
46 |
45
|
rexbii |
|- ( E. k e. A -. B =/= 0 <-> E. k e. A B = 0 ) |
47 |
|
rexnal |
|- ( E. k e. A -. B =/= 0 <-> -. A. k e. A B =/= 0 ) |
48 |
|
nfv |
|- F/ j B = 0 |
49 |
|
nfcsb1v |
|- F/_ k [_ j / k ]_ B |
50 |
49
|
nfeq1 |
|- F/ k [_ j / k ]_ B = 0 |
51 |
|
csbeq1a |
|- ( k = j -> B = [_ j / k ]_ B ) |
52 |
51
|
eqeq1d |
|- ( k = j -> ( B = 0 <-> [_ j / k ]_ B = 0 ) ) |
53 |
48 50 52
|
cbvrexw |
|- ( E. k e. A B = 0 <-> E. j e. A [_ j / k ]_ B = 0 ) |
54 |
46 47 53
|
3bitr3i |
|- ( -. A. k e. A B =/= 0 <-> E. j e. A [_ j / k ]_ B = 0 ) |
55 |
|
nfv |
|- F/ k j e. A |
56 |
1 55 50
|
nf3an |
|- F/ k ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) |
57 |
2
|
3ad2ant1 |
|- ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) -> A e. Fin ) |
58 |
29
|
3ad2antl1 |
|- ( ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) /\ k e. A ) -> B e. CC ) |
59 |
|
simp2 |
|- ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) -> j e. A ) |
60 |
52
|
biimparc |
|- ( ( [_ j / k ]_ B = 0 /\ k = j ) -> B = 0 ) |
61 |
60
|
3ad2antl3 |
|- ( ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) /\ k = j ) -> B = 0 ) |
62 |
56 57 58 59 61
|
fprodeq0g |
|- ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) -> prod_ k e. A B = 0 ) |
63 |
62
|
rexlimdv3a |
|- ( ph -> ( E. j e. A [_ j / k ]_ B = 0 -> prod_ k e. A B = 0 ) ) |
64 |
63
|
imp |
|- ( ( ph /\ E. j e. A [_ j / k ]_ B = 0 ) -> prod_ k e. A B = 0 ) |
65 |
|
0red |
|- ( ( ph /\ k e. A ) -> 0 e. RR ) |
66 |
65 3 5 4 6
|
letrd |
|- ( ( ph /\ k e. A ) -> 0 <_ C ) |
67 |
1 2 5 66
|
fprodge0 |
|- ( ph -> 0 <_ prod_ k e. A C ) |
68 |
67
|
adantr |
|- ( ( ph /\ E. j e. A [_ j / k ]_ B = 0 ) -> 0 <_ prod_ k e. A C ) |
69 |
64 68
|
eqbrtrd |
|- ( ( ph /\ E. j e. A [_ j / k ]_ B = 0 ) -> prod_ k e. A B <_ prod_ k e. A C ) |
70 |
54 69
|
sylan2b |
|- ( ( ph /\ -. A. k e. A B =/= 0 ) -> prod_ k e. A B <_ prod_ k e. A C ) |
71 |
44 70
|
pm2.61dan |
|- ( ph -> prod_ k e. A B <_ prod_ k e. A C ) |