This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )