Metamath Proof Explorer


Theorem etransclem45

Description: K is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem45.p φ P
etransclem45.m φ M 0
etransclem45.f F = x x P 1 j = 1 M x j P
etransclem45.a φ A : 0
etransclem45.k K = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
Assertion etransclem45 φ K

Proof

Step Hyp Ref Expression
1 etransclem45.p φ P
2 etransclem45.m φ M 0
3 etransclem45.f F = x x P 1 j = 1 M x j P
4 etransclem45.a φ A : 0
5 etransclem45.k K = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
6 fzfi 0 M Fin
7 fzfi 0 R Fin
8 xpfi 0 M Fin 0 R Fin 0 M × 0 R Fin
9 6 7 8 mp2an 0 M × 0 R Fin
10 9 a1i φ 0 M × 0 R Fin
11 nnm1nn0 P P 1 0
12 1 11 syl φ P 1 0
13 12 faccld φ P 1 !
14 13 nncnd φ P 1 !
15 4 adantr φ k 0 M × 0 R A : 0
16 xp1st k 0 M × 0 R 1 st k 0 M
17 elfznn0 1 st k 0 M 1 st k 0
18 16 17 syl k 0 M × 0 R 1 st k 0
19 18 adantl φ k 0 M × 0 R 1 st k 0
20 15 19 ffvelrnd φ k 0 M × 0 R A 1 st k
21 20 zcnd φ k 0 M × 0 R A 1 st k
22 reelprrecn
23 22 a1i φ k 0 M × 0 R
24 reopn topGen ran .
25 eqid TopOpen fld = TopOpen fld
26 25 tgioo2 topGen ran . = TopOpen fld 𝑡
27 24 26 eleqtri TopOpen fld 𝑡
28 27 a1i φ k 0 M × 0 R TopOpen fld 𝑡
29 1 adantr φ k 0 M × 0 R P
30 2 adantr φ k 0 M × 0 R M 0
31 xp2nd k 0 M × 0 R 2 nd k 0 R
32 elfznn0 2 nd k 0 R 2 nd k 0
33 31 32 syl k 0 M × 0 R 2 nd k 0
34 33 adantl φ k 0 M × 0 R 2 nd k 0
35 23 28 29 30 3 34 etransclem33 φ k 0 M × 0 R D n F 2 nd k :
36 19 nn0red φ k 0 M × 0 R 1 st k
37 35 36 ffvelrnd φ k 0 M × 0 R D n F 2 nd k 1 st k
38 21 37 mulcld φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k
39 13 nnne0d φ P 1 ! 0
40 10 14 38 39 fsumdivc φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 ! = k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
41 14 adantr φ k 0 M × 0 R P 1 !
42 39 adantr φ k 0 M × 0 R P 1 ! 0
43 21 37 41 42 divassd φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 ! = A 1 st k D n F 2 nd k 1 st k P 1 !
44 etransclem5 k 0 M y y k if k = 0 P 1 P = j 0 M x x j if j = 0 P 1 P
45 etransclem11 m 0 d 0 m 0 M | k = 0 M d k = m = n 0 c 0 n 0 M | j = 0 M c j = n
46 16 adantl φ k 0 M × 0 R 1 st k 0 M
47 23 28 29 30 3 34 44 45 46 36 etransclem37 φ k 0 M × 0 R P 1 ! D n F 2 nd k 1 st k
48 13 nnzd φ P 1 !
49 48 adantr φ k 0 M × 0 R P 1 !
50 19 nn0zd φ k 0 M × 0 R 1 st k
51 23 28 29 30 3 34 36 50 etransclem42 φ k 0 M × 0 R D n F 2 nd k 1 st k
52 dvdsval2 P 1 ! P 1 ! 0 D n F 2 nd k 1 st k P 1 ! D n F 2 nd k 1 st k D n F 2 nd k 1 st k P 1 !
53 49 42 51 52 syl3anc φ k 0 M × 0 R P 1 ! D n F 2 nd k 1 st k D n F 2 nd k 1 st k P 1 !
54 47 53 mpbid φ k 0 M × 0 R D n F 2 nd k 1 st k P 1 !
55 20 54 zmulcld φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
56 43 55 eqeltrd φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
57 10 56 fsumzcl φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
58 40 57 eqeltrd φ k 0 M × 0 R A 1 st k D n F 2 nd k 1 st k P 1 !
59 5 58 eqeltrid φ K