Metamath Proof Explorer


Theorem itcovalt2lem2lem1

Description: Lemma 1 for itcovalt2lem2 . (Contributed by AV, 6-May-2024)

Ref Expression
Assertion itcovalt2lem2lem1
|- ( ( ( Y e. NN /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( ( N + C ) x. Y ) - C ) e. NN0 )

Proof

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 )