Metamath Proof Explorer


Theorem itcovalt2lem2lem2

Description: Lemma 2 for itcovalt2lem2 . (Contributed by AV, 7-May-2024)

Ref Expression
Assertion itcovalt2lem2lem2 Y 0 C 0 N 0 2 N + C 2 Y C + C = N + C 2 Y + 1 C

Proof

Step Hyp Ref Expression
1 2cnd Y 0 C 0 N 0 2
2 simpr Y 0 C 0 N 0 N 0
3 simpr Y 0 C 0 C 0
4 3 adantr Y 0 C 0 N 0 C 0
5 2 4 nn0addcld Y 0 C 0 N 0 N + C 0
6 5 nn0cnd Y 0 C 0 N 0 N + C
7 2nn0 2 0
8 7 a1i Y 0 2 0
9 id Y 0 Y 0
10 8 9 nn0expcld Y 0 2 Y 0
11 10 nn0cnd Y 0 2 Y
12 11 ad2antrr Y 0 C 0 N 0 2 Y
13 6 12 mulcld Y 0 C 0 N 0 N + C 2 Y
14 nn0cn C 0 C
15 14 ad2antlr Y 0 C 0 N 0 C
16 1 13 15 subdid Y 0 C 0 N 0 2 N + C 2 Y C = 2 N + C 2 Y 2 C
17 16 oveq1d Y 0 C 0 N 0 2 N + C 2 Y C + C = 2 N + C 2 Y - 2 C + C
18 7 a1i Y 0 C 0 N 0 2 0
19 10 ad2antrr Y 0 C 0 N 0 2 Y 0
20 5 19 nn0mulcld Y 0 C 0 N 0 N + C 2 Y 0
21 18 20 nn0mulcld Y 0 C 0 N 0 2 N + C 2 Y 0
22 21 nn0cnd Y 0 C 0 N 0 2 N + C 2 Y
23 7 a1i Y 0 C 0 2 0
24 23 3 nn0mulcld Y 0 C 0 2 C 0
25 24 adantr Y 0 C 0 N 0 2 C 0
26 25 nn0cnd Y 0 C 0 N 0 2 C
27 4 nn0cnd Y 0 C 0 N 0 C
28 22 26 27 subsubd Y 0 C 0 N 0 2 N + C 2 Y 2 C C = 2 N + C 2 Y - 2 C + C
29 1 6 12 mul12d Y 0 C 0 N 0 2 N + C 2 Y = N + C 2 2 Y
30 2cnd Y 0 2
31 30 11 mulcomd Y 0 2 2 Y = 2 Y 2
32 30 9 expp1d Y 0 2 Y + 1 = 2 Y 2
33 31 32 eqtr4d Y 0 2 2 Y = 2 Y + 1
34 33 ad2antrr Y 0 C 0 N 0 2 2 Y = 2 Y + 1
35 34 oveq2d Y 0 C 0 N 0 N + C 2 2 Y = N + C 2 Y + 1
36 29 35 eqtrd Y 0 C 0 N 0 2 N + C 2 Y = N + C 2 Y + 1
37 2txmxeqx C 2 C C = C
38 14 37 syl C 0 2 C C = C
39 38 ad2antlr Y 0 C 0 N 0 2 C C = C
40 36 39 oveq12d Y 0 C 0 N 0 2 N + C 2 Y 2 C C = N + C 2 Y + 1 C
41 17 28 40 3eqtr2d Y 0 C 0 N 0 2 N + C 2 Y C + C = N + C 2 Y + 1 C