Metamath Proof Explorer


Theorem itcovalt2lem2lem1

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

Ref Expression
Assertion itcovalt2lem2lem1 Y C 0 N 0 N + C Y C 0

Proof

Step Hyp Ref Expression
1 nn0re C 0 C
2 1 adantl Y C 0 C
3 2 adantr Y C 0 N 0 C
4 simpr Y C 0 N 0 N 0
5 simpr Y C 0 C 0
6 5 adantr Y C 0 N 0 C 0
7 4 6 nn0addcld Y C 0 N 0 N + C 0
8 7 nn0red Y C 0 N 0 N + C
9 nnnn0 Y Y 0
10 9 ad2antrr Y C 0 N 0 Y 0
11 7 10 nn0mulcld Y C 0 N 0 N + C Y 0
12 11 nn0red Y C 0 N 0 N + C Y
13 nn0ge0 N 0 0 N
14 13 adantl Y C 0 N 0 0 N
15 6 nn0red Y C 0 N 0 C
16 4 nn0red Y C 0 N 0 N
17 15 16 addge02d Y C 0 N 0 0 N C N + C
18 14 17 mpbid Y C 0 N 0 C N + C
19 simpll Y C 0 N 0 Y
20 19 nnred Y C 0 N 0 Y
21 7 nn0ge0d Y C 0 N 0 0 N + C
22 nnge1 Y 1 Y
23 22 ad2antrr Y C 0 N 0 1 Y
24 8 20 21 23 lemulge11d Y C 0 N 0 N + C N + C Y
25 3 8 12 18 24 letrd Y C 0 N 0 C N + C Y
26 nn0sub C 0 N + C Y 0 C N + C Y N + C Y C 0
27 6 11 26 syl2anc Y C 0 N 0 C N + C Y N + C Y C 0
28 25 27 mpbid Y C 0 N 0 N + C Y C 0