Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem7 Unicode version

Theorem basellem7 20547
 Description: Lemma for basel 20550. The function for any fixed goes to . (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
basel.g
basellem7.2
Assertion
Ref Expression
basellem7

Proof of Theorem basellem7
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10414 . . . 4
2 1z 10204 . . . . 5
32a1i 10 . . . 4
4 ax-1cn 8942 . . . . 5
51eqimss2i 3319 . . . . . 6
6 nnex 9899 . . . . . 6
75, 6climconst2 12229 . . . . 5
84, 3, 7sylancr 644 . . . 4
9 ovex 6006 . . . . 5
109a1i 10 . . . 4
11 basellem7.2 . . . . . . 7
125, 6climconst2 12229 . . . . . . 7
1311, 3, 12sylancr 644 . . . . . 6
14 ovex 6006 . . . . . . 7
1514a1i 10 . . . . . 6
16 basel.g . . . . . . . 8
1716basellem6 20546 . . . . . . 7
1817a1i 10 . . . . . 6
1911elexi 2882 . . . . . . . . 9
2019fconst 5533 . . . . . . . 8
2111a1i 10 . . . . . . . . 9
2221snssd 3858 . . . . . . . 8
23 fss 5503 . . . . . . . 8
2420, 22, 23sylancr 644 . . . . . . 7
25 ffvelrn 5770 . . . . . . 7
2624, 25sylan 457 . . . . . 6
27 2nn 10026 . . . . . . . . . . . . 13
2827a1i 10 . . . . . . . . . . . 12
29 nnmulcl 9916 . . . . . . . . . . . 12
3028, 29sylan 457 . . . . . . . . . . 11
3130peano2nnd 9910 . . . . . . . . . 10
3231nnrecred 9938 . . . . . . . . 9
3332recnd 9008 . . . . . . . 8
3433, 16fmptd 5795 . . . . . . 7
35 ffvelrn 5770 . . . . . . 7
3634, 35sylan 457 . . . . . 6
37 ffn 5495 . . . . . . . 8
3824, 37syl 15 . . . . . . 7
39 ffn 5495 . . . . . . . 8
4034, 39syl 15 . . . . . . 7
416a1i 10 . . . . . . 7
42 inidm 3466 . . . . . . 7
43 eqidd 2367 . . . . . . 7
44 eqidd 2367 . . . . . . 7
4538, 40, 41, 41, 42, 43, 44ofval 6214 . . . . . 6
461, 3, 13, 15, 18, 26, 36, 45climmul 12313 . . . . 5
4711mul01i 9149 . . . . 5
4846, 47syl6breq 4164 . . . 4
49 1ex 8980 . . . . . . 7
5049fconst 5533 . . . . . 6
514a1i 10 . . . . . . 7
5251snssd 3858 . . . . . 6
53 fss 5503 . . . . . 6
5450, 52, 53sylancr 644 . . . . 5
55 ffvelrn 5770 . . . . 5
5654, 55sylan 457 . . . 4
57 mulcl 8968 . . . . . . 7
5857adantl 452 . . . . . 6
5958, 24, 34, 41, 41, 42off 6220 . . . . 5
60 ffvelrn 5770 . . . . 5
6159, 60sylan 457 . . . 4
6250a1i 10 . . . . . 6
63 ffn 5495 . . . . . 6
6462, 63syl 15 . . . . 5
65 ffn 5495 . . . . . 6
6659, 65syl 15 . . . . 5
67 eqidd 2367 . . . . 5
68 eqidd 2367 . . . . 5
6964, 66, 41, 41, 42, 67, 68ofval 6214 . . . 4
701, 3, 8, 10, 48, 56, 61, 69climadd 12312 . . 3
7170trud 1328 . 2