Step |
Hyp |
Ref |
Expression |
1 |
|
fvoveq1 |
|
2 |
1
|
oveq1d |
|
3 |
2
|
oveq2d |
|
4 |
|
rpre |
|
5 |
|
ssrab2 |
|
6 |
|
simprr |
|
7 |
5 6
|
sseldi |
|
8 |
|
mucl |
|
9 |
7 8
|
syl |
|
10 |
9
|
zcnd |
|
11 |
|
elfznn |
|
12 |
11
|
nnrpd |
|
13 |
12
|
ad2antrl |
|
14 |
7
|
nnrpd |
|
15 |
13 14
|
rpdivcld |
|
16 |
|
relogcl |
|
17 |
16
|
recnd |
|
18 |
15 17
|
syl |
|
19 |
18
|
sqcld |
|
20 |
10 19
|
mulcld |
|
21 |
3 4 20
|
dvdsflsumcom |
|
22 |
|
elfznn |
|
23 |
22
|
3ad2ant3 |
|
24 |
23
|
nncnd |
|
25 |
|
elfznn |
|
26 |
25
|
3ad2ant2 |
|
27 |
26
|
nncnd |
|
28 |
26
|
nnne0d |
|
29 |
24 27 28
|
divcan3d |
|
30 |
29
|
fveq2d |
|
31 |
30
|
oveq1d |
|
32 |
31
|
oveq2d |
|
33 |
32
|
2sumeq2dv |
|
34 |
21 33
|
eqtrd |
|
35 |
34
|
oveq1d |
|
36 |
35
|
oveq1d |
|
37 |
36
|
mpteq2ia |
|
38 |
|
eqid |
|
39 |
38
|
selberglem2 |
|
40 |
37 39
|
eqeltri |
|