Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
โข (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))) = (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))) |
2 | | 1cnd 11157 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โ) |
3 | | 2cnd 12238 |
. . . . . . . 8
โข (๐ โ โ โ 2 โ
โ) |
4 | | nncn 12168 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
5 | 3, 4 | mulcld 11182 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
6 | 5, 2 | addcld 11181 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
7 | | elnnuz 12814 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
8 | 7 | biimpi 215 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
9 | | eqidd 2738 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))) = (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2)))) |
10 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โ (1...๐) โง ๐ = ๐) โ ๐ = ๐) |
11 | 10 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((๐ โ (1...๐) โง ๐ = ๐) โ (2 ยท ๐) = (2 ยท ๐)) |
12 | 11 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ โ (1...๐) โง ๐ = ๐) โ ((2 ยท ๐)โ4) = ((2 ยท ๐)โ4)) |
13 | 11 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข ((๐ โ (1...๐) โง ๐ = ๐) โ ((2 ยท ๐) โ 1) = ((2 ยท ๐) โ 1)) |
14 | 11, 13 | oveq12d 7380 |
. . . . . . . . . . . 12
โข ((๐ โ (1...๐) โง ๐ = ๐) โ ((2 ยท ๐) ยท ((2 ยท ๐) โ 1)) = ((2 ยท ๐) ยท ((2 ยท ๐) โ 1))) |
15 | 14 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ โ (1...๐) โง ๐ = ๐) โ (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2) = (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)) |
16 | 12, 15 | oveq12d 7380 |
. . . . . . . . . 10
โข ((๐ โ (1...๐) โง ๐ = ๐) โ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)) = (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))) |
17 | | elfznn 13477 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ๐ โ โ) |
18 | | 2cnd 12238 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ 2 โ โ) |
19 | 17 | nncnd 12176 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โ) |
20 | 18, 19 | mulcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ (2 ยท ๐) โ โ) |
21 | | 4nn0 12439 |
. . . . . . . . . . . . 13
โข 4 โ
โ0 |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ 4 โ
โ0) |
23 | 20, 22 | expcld 14058 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ ((2 ยท ๐)โ4) โ โ) |
24 | | 1cnd 11157 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ 1 โ โ) |
25 | 20, 24 | subcld 11519 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ((2 ยท ๐) โ 1) โ โ) |
26 | 20, 25 | mulcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ((2 ยท ๐) ยท ((2 ยท ๐) โ 1)) โ
โ) |
27 | 26 | sqcld 14056 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2) โ
โ) |
28 | | 2ne0 12264 |
. . . . . . . . . . . . . . 15
โข 2 โ
0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ 2 โ 0) |
30 | 17 | nnne0d 12210 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ ๐ โ 0) |
31 | 18, 19, 29, 30 | mulne0d 11814 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ (2 ยท ๐) โ 0) |
32 | | 1red 11163 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1...๐) โ 1 โ โ) |
33 | | 2re 12234 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ 2 โ โ) |
35 | 34, 32 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ (2 ยท 1) โ
โ) |
36 | 17 | nnred 12175 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ ๐ โ โ) |
37 | 34, 36 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ (2 ยท ๐) โ โ) |
38 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . 18
โข 1 <
2 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ 1 < 2) |
40 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . 17
โข (2
ยท 1) = 2 |
41 | 39, 40 | breqtrrdi 5152 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ 1 < (2 ยท
1)) |
42 | | 0le2 12262 |
. . . . . . . . . . . . . . . . . 18
โข 0 โค
2 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ 0 โค 2) |
44 | | elfzle1 13451 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ 1 โค ๐) |
45 | 32, 36, 34, 43, 44 | lemul2ad 12102 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ (2 ยท 1) โค (2 ยท
๐)) |
46 | 32, 35, 37, 41, 45 | ltletrd 11322 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1...๐) โ 1 < (2 ยท ๐)) |
47 | 32, 46 | gtned 11297 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ (2 ยท ๐) โ 1) |
48 | 20, 24, 47 | subne0d 11528 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ((2 ยท ๐) โ 1) โ 0) |
49 | 20, 25, 31, 48 | mulne0d 11814 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ((2 ยท ๐) ยท ((2 ยท ๐) โ 1)) โ 0) |
50 | | 2z 12542 |
. . . . . . . . . . . . 13
โข 2 โ
โค |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ 2 โ โค) |
52 | 26, 49, 51 | expne0d 14064 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2) โ
0) |
53 | 23, 27, 52 | divcld 11938 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)) โ
โ) |
54 | 9, 16, 17, 53 | fvmptd 6960 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ๐) =
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))) |
55 | 54, 53 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ๐)
โ โ) |
56 | 55 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ๐)
โ โ) |
57 | | mulcl 11142 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ค โ โ) โ (๐ ยท ๐ค) โ โ) |
58 | 57 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง (๐ โ โ โง ๐ค โ โ)) โ (๐ ยท ๐ค) โ โ) |
59 | 8, 56, 58 | seqcl 13935 |
. . . . . 6
โข (๐ โ โ โ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐) โ
โ) |
60 | | 2nn 12233 |
. . . . . . . . . 10
โข 2 โ
โ |
61 | 60 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ 2 โ
โ) |
62 | | id 22 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
63 | 61, 62 | nnmulcld 12213 |
. . . . . . . 8
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
64 | 63 | peano2nnd 12177 |
. . . . . . 7
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
65 | 64 | nnne0d 12210 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
66 | 2, 6, 59, 65 | div32d 11961 |
. . . . 5
โข (๐ โ โ โ ((1 / ((2
ยท ๐) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐)) = (1 ยท ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐) / ((2 ยท ๐) + 1)))) |
67 | 59, 6, 65 | divcld 11938 |
. . . . . 6
โข (๐ โ โ โ ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐) / ((2 ยท ๐) + 1)) โ
โ) |
68 | 67 | mulid2d 11180 |
. . . . 5
โข (๐ โ โ โ (1
ยท ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐) /
((2 ยท ๐) + 1))) =
((seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐) / ((2 ยท ๐) + 1))) |
69 | | wallispi2lem2 44387 |
. . . . . 6
โข (๐ โ โ โ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐) = (((2โ(4 ยท ๐)) ยท ((!โ๐)โ4)) / ((!โ(2
ยท ๐))โ2))) |
70 | 69 | oveq1d 7377 |
. . . . 5
โข (๐ โ โ โ ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐) / ((2 ยท ๐) + 1)) = ((((2โ(4 ยท
๐)) ยท
((!โ๐)โ4)) /
((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1))) |
71 | 66, 68, 70 | 3eqtrd 2781 |
. . . 4
โข (๐ โ โ โ ((1 / ((2
ยท ๐) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐)) = ((((2โ(4 ยท
๐)) ยท
((!โ๐)โ4)) /
((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1))) |
72 | 71 | mpteq2ia 5213 |
. . 3
โข (๐ โ โ โฆ ((1 /
((2 ยท ๐) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐))) =
(๐ โ โ โฆ
((((2โ(4 ยท ๐))
ยท ((!โ๐)โ4)) / ((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1))) |
73 | | wallispi2lem1 44386 |
. . . 4
โข (๐ โ โ โ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐) = ((1 / ((2 ยท ๐) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐))) |
74 | 73 | mpteq2ia 5213 |
. . 3
โข (๐ โ โ โฆ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐)) = (๐ โ โ โฆ ((1 / ((2 ยท
๐) + 1)) ยท (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐))) |
75 | | wallispi2.1 |
. . 3
โข ๐ = (๐ โ โ โฆ ((((2โ(4
ยท ๐)) ยท
((!โ๐)โ4)) /
((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1))) |
76 | 72, 74, 75 | 3eqtr4ri 2776 |
. 2
โข ๐ = (๐ โ โ โฆ (seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1)))))โ๐)) |
77 | 1, 76 | wallispi 44385 |
1
โข ๐ โ (ฯ /
2) |