Step |
Hyp |
Ref |
Expression |
1 |
|
nn0re |
|- ( C e. NN0 -> C e. RR ) |
2 |
1
|
adantl |
|- ( ( Y e. NN /\ C e. NN0 ) -> C e. RR ) |
3 |
2
|
adantr |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> C e. RR ) |
4 |
|
simpr |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> N e. NN0 ) |
5 |
|
simpr |
|- ( ( Y e. NN /\ C e. NN0 ) -> C e. NN0 ) |
6 |
5
|
adantr |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> C e. NN0 ) |
7 |
4 6
|
nn0addcld |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( N + C ) e. NN0 ) |
8 |
7
|
nn0red |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( N + C ) e. RR ) |
9 |
|
nnnn0 |
|- ( Y e. NN -> Y e. NN0 ) |
10 |
9
|
ad2antrr |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> Y e. NN0 ) |
11 |
7 10
|
nn0mulcld |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( N + C ) x. Y ) e. NN0 ) |
12 |
11
|
nn0red |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( N + C ) x. Y ) e. RR ) |
13 |
|
nn0ge0 |
|- ( N e. NN0 -> 0 <_ N ) |
14 |
13
|
adantl |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> 0 <_ N ) |
15 |
6
|
nn0red |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> C e. RR ) |
16 |
4
|
nn0red |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> N e. RR ) |
17 |
15 16
|
addge02d |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( 0 <_ N <-> C <_ ( N + C ) ) ) |
18 |
14 17
|
mpbid |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> C <_ ( N + C ) ) |
19 |
|
simpll |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> Y e. NN ) |
20 |
19
|
nnred |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> Y e. RR ) |
21 |
7
|
nn0ge0d |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> 0 <_ ( N + C ) ) |
22 |
|
nnge1 |
|- ( Y e. NN -> 1 <_ Y ) |
23 |
22
|
ad2antrr |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> 1 <_ Y ) |
24 |
8 20 21 23
|
lemulge11d |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( N + C ) <_ ( ( N + C ) x. Y ) ) |
25 |
3 8 12 18 24
|
letrd |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> C <_ ( ( N + C ) x. Y ) ) |
26 |
|
nn0sub |
|- ( ( C e. NN0 /\ ( ( N + C ) x. Y ) e. NN0 ) -> ( C <_ ( ( N + C ) x. Y ) <-> ( ( ( N + C ) x. Y ) - C ) e. NN0 ) ) |
27 |
6 11 26
|
syl2anc |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( C <_ ( ( N + C ) x. Y ) <-> ( ( ( N + C ) x. Y ) - C ) e. NN0 ) ) |
28 |
25 27
|
mpbid |
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( ( N + C ) x. Y ) - C ) e. NN0 ) |