Step |
Hyp |
Ref |
Expression |
1 |
|
nn0readdcl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. RR ) |
2 |
1
|
rehalfcld |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M + N ) / 2 ) e. RR ) |
3 |
|
flle |
|- ( ( ( M + N ) / 2 ) e. RR -> ( |_ ` ( ( M + N ) / 2 ) ) <_ ( ( M + N ) / 2 ) ) |
4 |
2 3
|
syl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( |_ ` ( ( M + N ) / 2 ) ) <_ ( ( M + N ) / 2 ) ) |
5 |
|
reflcl |
|- ( ( ( M + N ) / 2 ) e. RR -> ( |_ ` ( ( M + N ) / 2 ) ) e. RR ) |
6 |
2 5
|
syl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( |_ ` ( ( M + N ) / 2 ) ) e. RR ) |
7 |
|
nn0re |
|- ( M e. NN0 -> M e. RR ) |
8 |
7
|
adantr |
|- ( ( M e. NN0 /\ N e. NN0 ) -> M e. RR ) |
9 |
|
letr |
|- ( ( ( |_ ` ( ( M + N ) / 2 ) ) e. RR /\ ( ( M + N ) / 2 ) e. RR /\ M e. RR ) -> ( ( ( |_ ` ( ( M + N ) / 2 ) ) <_ ( ( M + N ) / 2 ) /\ ( ( M + N ) / 2 ) <_ M ) -> ( |_ ` ( ( M + N ) / 2 ) ) <_ M ) ) |
10 |
6 2 8 9
|
syl3anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( |_ ` ( ( M + N ) / 2 ) ) <_ ( ( M + N ) / 2 ) /\ ( ( M + N ) / 2 ) <_ M ) -> ( |_ ` ( ( M + N ) / 2 ) ) <_ M ) ) |
11 |
4 10
|
mpand |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( M + N ) / 2 ) <_ M -> ( |_ ` ( ( M + N ) / 2 ) ) <_ M ) ) |
12 |
|
nn0addcl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. NN0 ) |
13 |
12
|
nn0ge0d |
|- ( ( M e. NN0 /\ N e. NN0 ) -> 0 <_ ( M + N ) ) |
14 |
|
halfnneg2 |
|- ( ( M + N ) e. RR -> ( 0 <_ ( M + N ) <-> 0 <_ ( ( M + N ) / 2 ) ) ) |
15 |
1 14
|
syl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 <_ ( M + N ) <-> 0 <_ ( ( M + N ) / 2 ) ) ) |
16 |
13 15
|
mpbid |
|- ( ( M e. NN0 /\ N e. NN0 ) -> 0 <_ ( ( M + N ) / 2 ) ) |
17 |
|
flge0nn0 |
|- ( ( ( ( M + N ) / 2 ) e. RR /\ 0 <_ ( ( M + N ) / 2 ) ) -> ( |_ ` ( ( M + N ) / 2 ) ) e. NN0 ) |
18 |
2 16 17
|
syl2anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( |_ ` ( ( M + N ) / 2 ) ) e. NN0 ) |
19 |
|
simpl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> M e. NN0 ) |
20 |
|
facwordi |
|- ( ( ( |_ ` ( ( M + N ) / 2 ) ) e. NN0 /\ M e. NN0 /\ ( |_ ` ( ( M + N ) / 2 ) ) <_ M ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` M ) ) |
21 |
20
|
3exp |
|- ( ( |_ ` ( ( M + N ) / 2 ) ) e. NN0 -> ( M e. NN0 -> ( ( |_ ` ( ( M + N ) / 2 ) ) <_ M -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` M ) ) ) ) |
22 |
18 19 21
|
sylc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( |_ ` ( ( M + N ) / 2 ) ) <_ M -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` M ) ) ) |
23 |
|
faccl |
|- ( M e. NN0 -> ( ! ` M ) e. NN ) |
24 |
23
|
nncnd |
|- ( M e. NN0 -> ( ! ` M ) e. CC ) |
25 |
24
|
mulid1d |
|- ( M e. NN0 -> ( ( ! ` M ) x. 1 ) = ( ! ` M ) ) |
26 |
25
|
adantr |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` M ) x. 1 ) = ( ! ` M ) ) |
27 |
|
faccl |
|- ( N e. NN0 -> ( ! ` N ) e. NN ) |
28 |
27
|
nnred |
|- ( N e. NN0 -> ( ! ` N ) e. RR ) |
29 |
28
|
adantl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` N ) e. RR ) |
30 |
23
|
nnred |
|- ( M e. NN0 -> ( ! ` M ) e. RR ) |
31 |
23
|
nnnn0d |
|- ( M e. NN0 -> ( ! ` M ) e. NN0 ) |
32 |
31
|
nn0ge0d |
|- ( M e. NN0 -> 0 <_ ( ! ` M ) ) |
33 |
30 32
|
jca |
|- ( M e. NN0 -> ( ( ! ` M ) e. RR /\ 0 <_ ( ! ` M ) ) ) |
34 |
33
|
adantr |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` M ) e. RR /\ 0 <_ ( ! ` M ) ) ) |
35 |
27
|
nnge1d |
|- ( N e. NN0 -> 1 <_ ( ! ` N ) ) |
36 |
35
|
adantl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> 1 <_ ( ! ` N ) ) |
37 |
|
1re |
|- 1 e. RR |
38 |
|
lemul2a |
|- ( ( ( 1 e. RR /\ ( ! ` N ) e. RR /\ ( ( ! ` M ) e. RR /\ 0 <_ ( ! ` M ) ) ) /\ 1 <_ ( ! ` N ) ) -> ( ( ! ` M ) x. 1 ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
39 |
37 38
|
mp3anl1 |
|- ( ( ( ( ! ` N ) e. RR /\ ( ( ! ` M ) e. RR /\ 0 <_ ( ! ` M ) ) ) /\ 1 <_ ( ! ` N ) ) -> ( ( ! ` M ) x. 1 ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
40 |
29 34 36 39
|
syl21anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` M ) x. 1 ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
41 |
26 40
|
eqbrtrrd |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` M ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
42 |
18
|
faccld |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) e. NN ) |
43 |
42
|
nnred |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) e. RR ) |
44 |
30
|
adantr |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` M ) e. RR ) |
45 |
|
remulcl |
|- ( ( ( ! ` M ) e. RR /\ ( ! ` N ) e. RR ) -> ( ( ! ` M ) x. ( ! ` N ) ) e. RR ) |
46 |
30 28 45
|
syl2an |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` M ) x. ( ! ` N ) ) e. RR ) |
47 |
|
letr |
|- ( ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) e. RR /\ ( ! ` M ) e. RR /\ ( ( ! ` M ) x. ( ! ` N ) ) e. RR ) -> ( ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` M ) /\ ( ! ` M ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
48 |
43 44 46 47
|
syl3anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` M ) /\ ( ! ` M ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
49 |
41 48
|
mpan2d |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` M ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
50 |
11 22 49
|
3syld |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( M + N ) / 2 ) <_ M -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
51 |
|
nn0re |
|- ( N e. NN0 -> N e. RR ) |
52 |
51
|
adantl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> N e. RR ) |
53 |
|
letr |
|- ( ( ( |_ ` ( ( M + N ) / 2 ) ) e. RR /\ ( ( M + N ) / 2 ) e. RR /\ N e. RR ) -> ( ( ( |_ ` ( ( M + N ) / 2 ) ) <_ ( ( M + N ) / 2 ) /\ ( ( M + N ) / 2 ) <_ N ) -> ( |_ ` ( ( M + N ) / 2 ) ) <_ N ) ) |
54 |
6 2 52 53
|
syl3anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( |_ ` ( ( M + N ) / 2 ) ) <_ ( ( M + N ) / 2 ) /\ ( ( M + N ) / 2 ) <_ N ) -> ( |_ ` ( ( M + N ) / 2 ) ) <_ N ) ) |
55 |
4 54
|
mpand |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( M + N ) / 2 ) <_ N -> ( |_ ` ( ( M + N ) / 2 ) ) <_ N ) ) |
56 |
|
simpr |
|- ( ( M e. NN0 /\ N e. NN0 ) -> N e. NN0 ) |
57 |
|
facwordi |
|- ( ( ( |_ ` ( ( M + N ) / 2 ) ) e. NN0 /\ N e. NN0 /\ ( |_ ` ( ( M + N ) / 2 ) ) <_ N ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` N ) ) |
58 |
57
|
3exp |
|- ( ( |_ ` ( ( M + N ) / 2 ) ) e. NN0 -> ( N e. NN0 -> ( ( |_ ` ( ( M + N ) / 2 ) ) <_ N -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` N ) ) ) ) |
59 |
18 56 58
|
sylc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( |_ ` ( ( M + N ) / 2 ) ) <_ N -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` N ) ) ) |
60 |
27
|
nncnd |
|- ( N e. NN0 -> ( ! ` N ) e. CC ) |
61 |
60
|
mulid2d |
|- ( N e. NN0 -> ( 1 x. ( ! ` N ) ) = ( ! ` N ) ) |
62 |
61
|
adantl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 1 x. ( ! ` N ) ) = ( ! ` N ) ) |
63 |
27
|
nnnn0d |
|- ( N e. NN0 -> ( ! ` N ) e. NN0 ) |
64 |
63
|
nn0ge0d |
|- ( N e. NN0 -> 0 <_ ( ! ` N ) ) |
65 |
28 64
|
jca |
|- ( N e. NN0 -> ( ( ! ` N ) e. RR /\ 0 <_ ( ! ` N ) ) ) |
66 |
65
|
adantl |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` N ) e. RR /\ 0 <_ ( ! ` N ) ) ) |
67 |
23
|
nnge1d |
|- ( M e. NN0 -> 1 <_ ( ! ` M ) ) |
68 |
67
|
adantr |
|- ( ( M e. NN0 /\ N e. NN0 ) -> 1 <_ ( ! ` M ) ) |
69 |
|
lemul1a |
|- ( ( ( 1 e. RR /\ ( ! ` M ) e. RR /\ ( ( ! ` N ) e. RR /\ 0 <_ ( ! ` N ) ) ) /\ 1 <_ ( ! ` M ) ) -> ( 1 x. ( ! ` N ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
70 |
37 69
|
mp3anl1 |
|- ( ( ( ( ! ` M ) e. RR /\ ( ( ! ` N ) e. RR /\ 0 <_ ( ! ` N ) ) ) /\ 1 <_ ( ! ` M ) ) -> ( 1 x. ( ! ` N ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
71 |
44 66 68 70
|
syl21anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 1 x. ( ! ` N ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
72 |
62 71
|
eqbrtrrd |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` N ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |
73 |
|
letr |
|- ( ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) e. RR /\ ( ! ` N ) e. RR /\ ( ( ! ` M ) x. ( ! ` N ) ) e. RR ) -> ( ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` N ) /\ ( ! ` N ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
74 |
43 29 46 73
|
syl3anc |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` N ) /\ ( ! ` N ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
75 |
72 74
|
mpan2d |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ! ` N ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
76 |
55 59 75
|
3syld |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( M + N ) / 2 ) <_ N -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) ) |
77 |
|
avgle |
|- ( ( M e. RR /\ N e. RR ) -> ( ( ( M + N ) / 2 ) <_ M \/ ( ( M + N ) / 2 ) <_ N ) ) |
78 |
7 51 77
|
syl2an |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( M + N ) / 2 ) <_ M \/ ( ( M + N ) / 2 ) <_ N ) ) |
79 |
50 76 78
|
mpjaod |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) ) |