Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = 1 β (seq1( Β· ,
(π β β β¦
(((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β1)) |
2 | | 1z 12538 |
. . . . . . . . . 10
β’ 1 β
β€ |
3 | | seq1 13925 |
. . . . . . . . . 10
β’ (1 β
β€ β (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β1) = ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . 9
β’ (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))β1) = ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1) |
5 | 1, 4 | eqtrdi 2789 |
. . . . . . . 8
β’ (π = 1 β (seq1( Β· ,
(π β β β¦
(((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1)) |
6 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = 1 β (π + 1) = (1 + 1)) |
7 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = 1 β (π + (π + 1)) = (1 + (π + 1))) |
8 | 6, 7 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = 1 β ((π + 1) / (π + (π + 1))) = ((1 + 1) / (1 + (π + 1)))) |
9 | 8 | oveq2d 7374 |
. . . . . . . 8
β’ (π = 1 β ((π + 1) Β· ((π + 1) / (π + (π + 1)))) = ((π + 1) Β· ((1 + 1) / (1 + (π + 1))))) |
10 | 5, 9 | eqeq12d 2749 |
. . . . . . 7
β’ (π = 1 β ((seq1( Β· ,
(π β β β¦
(((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1) = ((π + 1) Β· ((1 + 1) / (1 + (π + 1)))))) |
11 | 10 | imbi2d 341 |
. . . . . 6
β’ (π = 1 β ((π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (π β β0 β ((π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1) = ((π + 1) Β· ((1 + 1) / (1 + (π + 1))))))) |
12 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ)) |
13 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π + 1) = (π + 1)) |
14 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π + (π + 1)) = (π + (π + 1))) |
15 | 13, 14 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β ((π + 1) / (π + (π + 1))) = ((π + 1) / (π + (π + 1)))) |
16 | 15 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β ((π + 1) Β· ((π + 1) / (π + (π + 1)))) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) |
17 | 12, 16 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))))) |
18 | 17 | imbi2d 341 |
. . . . . 6
β’ (π = π β ((π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))))) |
19 | | fveq2 6843 |
. . . . . . . 8
β’ (π = (π + 1) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1))) |
20 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π + 1) = ((π + 1) + 1)) |
21 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π + (π + 1)) = ((π + 1) + (π + 1))) |
22 | 20, 21 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = (π + 1) β ((π + 1) / (π + (π + 1))) = (((π + 1) + 1) / ((π + 1) + (π + 1)))) |
23 | 22 | oveq2d 7374 |
. . . . . . . 8
β’ (π = (π + 1) β ((π + 1) Β· ((π + 1) / (π + (π + 1)))) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))) |
24 | 19, 23 | eqeq12d 2749 |
. . . . . . 7
β’ (π = (π + 1) β ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1)))))) |
25 | 24 | imbi2d 341 |
. . . . . 6
β’ (π = (π + 1) β ((π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))))) |
26 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ)) |
27 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π + 1) = (π + 1)) |
28 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π + (π + 1)) = (π + (π + 1))) |
29 | 27, 28 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β ((π + 1) / (π + (π + 1))) = ((π + 1) / (π + (π + 1)))) |
30 | 29 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β ((π + 1) Β· ((π + 1) / (π + (π + 1)))) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) |
31 | 26, 30 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π β ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))))) |
32 | 31 | imbi2d 341 |
. . . . . 6
β’ (π = π β ((π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))))) |
33 | | 1nn 12169 |
. . . . . . . 8
β’ 1 β
β |
34 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π = 1 β (π / π) = (π / 1)) |
35 | 34 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = 1 β (1 + (π / π)) = (1 + (π / 1))) |
36 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π = 1 β (1 / π) = (1 / 1)) |
37 | 36 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = 1 β (1 + (1 / π)) = (1 + (1 /
1))) |
38 | 35, 37 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π = 1 β ((1 + (π / π)) Β· (1 + (1 / π))) = ((1 + (π / 1)) Β· (1 + (1 /
1)))) |
39 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = 1 β ((π + 1) / π) = ((π + 1) / 1)) |
40 | 39 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π = 1 β (1 + ((π + 1) / π)) = (1 + ((π + 1) / 1))) |
41 | 38, 40 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = 1 β (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))) = (((1 + (π / 1)) Β· (1 + (1 / 1))) / (1 +
((π + 1) /
1)))) |
42 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))) = (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))) |
43 | | ovex 7391 |
. . . . . . . . 9
β’ (((1 +
(π / 1)) Β· (1 + (1 /
1))) / (1 + ((π + 1) / 1)))
β V |
44 | 41, 42, 43 | fvmpt 6949 |
. . . . . . . 8
β’ (1 β
β β ((π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π))))β1) = (((1 + (π / 1)) Β· (1 + (1 / 1))) / (1 +
((π + 1) /
1)))) |
45 | 33, 44 | ax-mp 5 |
. . . . . . 7
β’ ((π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1) = (((1 + (π / 1)) Β· (1 + (1 / 1))) / (1 +
((π + 1) /
1))) |
46 | | nn0cn 12428 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
47 | 46 | div1d 11928 |
. . . . . . . . . . 11
β’ (π β β0
β (π / 1) = π) |
48 | 47 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β β0
β (1 + (π / 1)) = (1 +
π)) |
49 | | 1div1e1 11850 |
. . . . . . . . . . . 12
β’ (1 / 1) =
1 |
50 | 49 | oveq2i 7369 |
. . . . . . . . . . 11
β’ (1 + (1 /
1)) = (1 + 1) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
β’ (π β β0
β (1 + (1 / 1)) = (1 + 1)) |
52 | 48, 51 | oveq12d 7376 |
. . . . . . . . 9
β’ (π β β0
β ((1 + (π / 1))
Β· (1 + (1 / 1))) = ((1 + π) Β· (1 + 1))) |
53 | | nn0p1nn 12457 |
. . . . . . . . . . . 12
β’ (π β β0
β (π + 1) β
β) |
54 | 53 | nncnd 12174 |
. . . . . . . . . . 11
β’ (π β β0
β (π + 1) β
β) |
55 | 54 | div1d 11928 |
. . . . . . . . . 10
β’ (π β β0
β ((π + 1) / 1) =
(π + 1)) |
56 | 55 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β β0
β (1 + ((π + 1) / 1))
= (1 + (π +
1))) |
57 | 52, 56 | oveq12d 7376 |
. . . . . . . 8
β’ (π β β0
β (((1 + (π / 1))
Β· (1 + (1 / 1))) / (1 + ((π + 1) / 1))) = (((1 + π) Β· (1 + 1)) / (1 + (π + 1)))) |
58 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (π β β0
β 1 β β) |
59 | 58, 46 | addcomd 11362 |
. . . . . . . . . 10
β’ (π β β0
β (1 + π) = (π + 1)) |
60 | 59 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β β0
β ((1 + π) Β· (1
+ 1)) = ((π + 1) Β·
(1 + 1))) |
61 | 60 | oveq1d 7373 |
. . . . . . . 8
β’ (π β β0
β (((1 + π) Β·
(1 + 1)) / (1 + (π + 1))) =
(((π + 1) Β· (1 + 1))
/ (1 + (π +
1)))) |
62 | | ax-1cn 11114 |
. . . . . . . . . . 11
β’ 1 β
β |
63 | 62, 62 | addcli 11166 |
. . . . . . . . . 10
β’ (1 + 1)
β β |
64 | 63 | a1i 11 |
. . . . . . . . 9
β’ (π β β0
β (1 + 1) β β) |
65 | 33 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β0
β 1 β β) |
66 | 65, 53 | nnaddcld 12210 |
. . . . . . . . . 10
β’ (π β β0
β (1 + (π + 1)) β
β) |
67 | 66 | nncnd 12174 |
. . . . . . . . 9
β’ (π β β0
β (1 + (π + 1)) β
β) |
68 | 66 | nnne0d 12208 |
. . . . . . . . 9
β’ (π β β0
β (1 + (π + 1)) β
0) |
69 | 54, 64, 67, 68 | divassd 11971 |
. . . . . . . 8
β’ (π β β0
β (((π + 1) Β·
(1 + 1)) / (1 + (π + 1))) =
((π + 1) Β· ((1 + 1)
/ (1 + (π +
1))))) |
70 | 57, 61, 69 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β β0
β (((1 + (π / 1))
Β· (1 + (1 / 1))) / (1 + ((π + 1) / 1))) = ((π + 1) Β· ((1 + 1) / (1 + (π + 1))))) |
71 | 45, 70 | eqtrid 2785 |
. . . . . 6
β’ (π β β0
β ((π β β
β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β1) = ((π + 1) Β· ((1 + 1) / (1 + (π + 1))))) |
72 | | seqp1 13927 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β1) β (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)))) |
73 | | nnuz 12811 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
74 | 72, 73 | eleq2s 2852 |
. . . . . . . . . . 11
β’ (π β β β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)))) |
75 | 74 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ π β β0)
β (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)))) |
76 | 75 | adantr 482 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)))) |
77 | | oveq1 7365 |
. . . . . . . . . 10
β’ ((seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1))) = (((π + 1) Β· ((π + 1) / (π + (π + 1)))) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)))) |
78 | 77 | adantl 483 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β ((seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1))) = (((π + 1) Β· ((π + 1) / (π + (π + 1)))) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)))) |
79 | | peano2nn 12170 |
. . . . . . . . . . . . . 14
β’ (π β β β (π + 1) β
β) |
80 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (π / π) = (π / (π + 1))) |
81 | 80 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (1 + (π / π)) = (1 + (π / (π + 1)))) |
82 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (1 / π) = (1 / (π + 1))) |
83 | 82 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (1 + (1 / π)) = (1 + (1 / (π + 1)))) |
84 | 81, 83 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β ((1 + (π / π)) Β· (1 + (1 / π))) = ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1))))) |
85 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β ((π + 1) / π) = ((π + 1) / (π + 1))) |
86 | 85 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (1 + ((π + 1) / π)) = (1 + ((π + 1) / (π + 1)))) |
87 | 84, 86 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))) = (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1))))) |
88 | | ovex 7391 |
. . . . . . . . . . . . . . 15
β’ (((1 +
(π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1)))) β V |
89 | 87, 42, 88 | fvmpt 6949 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β β
((π β β β¦
(((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)) = (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1))))) |
90 | 79, 89 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β ((π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1)) = (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1))))) |
91 | 90 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π β β β (((π + 1) Β· ((π + 1) / (π + (π + 1)))) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1))) = (((π + 1) Β· ((π + 1) / (π + (π + 1)))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1)))))) |
92 | 91 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
((π + 1) / (π + (π + 1)))) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1))) = (((π + 1) Β· ((π + 1) / (π + (π + 1)))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1)))))) |
93 | 53 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (π + 1) β
β) |
94 | 93 | nncnd 12174 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β0)
β (π + 1) β
β) |
95 | 79 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (π + 1) β
β) |
96 | 95 | nnrpd 12960 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (π + 1) β
β+) |
97 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β π β
β) |
98 | 97 | nnrpd 12960 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β π β
β+) |
99 | 93 | nnrpd 12960 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (π + 1) β
β+) |
100 | 98, 99 | rpaddcld 12977 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (π + (π + 1)) β
β+) |
101 | 96, 100 | rpdivcld 12979 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β ((π + 1) / (π + (π + 1))) β
β+) |
102 | 101 | rpcnd 12964 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β0)
β ((π + 1) / (π + (π + 1))) β β) |
103 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β 1 β β) |
104 | | nn0re 12427 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
β) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β0)
β π β
β) |
106 | 105, 95 | nndivred 12212 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β (π / (π + 1)) β
β) |
107 | 106 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β (π / (π + 1)) β
β) |
108 | 103, 107 | addcomd 11362 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β (1 + (π / (π + 1))) = ((π / (π + 1)) + 1)) |
109 | | nn0ge0 12443 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β 0 β€ π) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β 0 β€ π) |
111 | 105, 96, 110 | divge0d 13002 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β 0 β€ (π / (π + 1))) |
112 | 106, 111 | ge0p1rpd 12992 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((π / (π + 1)) + 1) β
β+) |
113 | 108, 112 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (1 + (π / (π + 1))) β
β+) |
114 | | 1rp 12924 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β+ |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β 1 β β+) |
116 | 96 | rpreccld 12972 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β (1 / (π + 1)) β
β+) |
117 | 115, 116 | rpaddcld 12977 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (1 + (1 / (π + 1)))
β β+) |
118 | 113, 117 | rpmulcld 12978 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β ((1 + (π / (π + 1))) Β· (1 + (1 /
(π + 1)))) β
β+) |
119 | 99, 96 | rpdivcld 12979 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β ((π + 1) / (π + 1)) β
β+) |
120 | 115, 119 | rpaddcld 12977 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (1 + ((π + 1) /
(π + 1))) β
β+) |
121 | 118, 120 | rpdivcld 12979 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (((1 + (π / (π + 1))) Β· (1 + (1 /
(π + 1)))) / (1 + ((π + 1) / (π + 1)))) β
β+) |
122 | 121 | rpcnd 12964 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β0)
β (((1 + (π / (π + 1))) Β· (1 + (1 /
(π + 1)))) / (1 + ((π + 1) / (π + 1)))) β β) |
123 | 94, 102, 122 | mulassd 11183 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
((π + 1) / (π + (π + 1)))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1))))) = ((π + 1) Β· (((π + 1) / (π + (π + 1))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1))))))) |
124 | 101, 118 | rpmulcld 12978 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1))))) β
β+) |
125 | 124 | rpcnd 12964 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1))))) β
β) |
126 | 120 | rpcnd 12964 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (1 + ((π + 1) /
(π + 1))) β
β) |
127 | 95 | nncnd 12174 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (π + 1) β
β) |
128 | 120 | rpne0d 12967 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (1 + ((π + 1) /
(π + 1))) β
0) |
129 | 95 | nnne0d 12208 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (π + 1) β
0) |
130 | 125, 126,
127, 128, 129 | divcan5d 11962 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
(((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))))) / ((π + 1) Β· (1 + ((π + 1) / (π + 1))))) = ((((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1))))) / (1 + ((π + 1) / (π + 1))))) |
131 | 118 | rpcnd 12964 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((1 + (π / (π + 1))) Β· (1 + (1 /
(π + 1)))) β
β) |
132 | 127, 102,
131 | mul12d 11369 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β ((π + 1) Β·
(((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))))) = (((π + 1) / (π + (π + 1))) Β· ((π + 1) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1))))))) |
133 | 113 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β (1 + (π / (π + 1))) β
β) |
134 | 117 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β (1 + (1 / (π + 1)))
β β) |
135 | 127, 133,
134 | mulassd 11183 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
(1 + (π / (π + 1)))) Β· (1 + (1 /
(π + 1)))) = ((π + 1) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))))) |
136 | 127, 103,
107 | adddid 11184 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β0)
β ((π + 1) Β· (1
+ (π / (π + 1)))) = (((π + 1) Β· 1) + ((π + 1) Β· (π / (π + 1))))) |
137 | 127 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β0)
β ((π + 1) Β· 1)
= (π + 1)) |
138 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β β0)
β π β
β0) |
139 | 138 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β0)
β π β
β) |
140 | 139, 127,
129 | divcan2d 11938 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β0)
β ((π + 1) Β·
(π / (π + 1))) = π) |
141 | 137, 140 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
1) + ((π + 1) Β·
(π / (π + 1)))) = ((π + 1) + π)) |
142 | 97 | nncnd 12174 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β0)
β π β
β) |
143 | 142, 103,
139 | addassd 11182 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β0)
β ((π + 1) + π) = (π + (1 + π))) |
144 | 103, 139 | addcomd 11362 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β0)
β (1 + π) = (π + 1)) |
145 | 144 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β0)
β (π + (1 + π)) = (π + (π + 1))) |
146 | 143, 145 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β0)
β ((π + 1) + π) = (π + (π + 1))) |
147 | 136, 141,
146 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β ((π + 1) Β· (1
+ (π / (π + 1)))) = (π + (π + 1))) |
148 | 147 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
(1 + (π / (π + 1)))) Β· (1 + (1 /
(π + 1)))) = ((π + (π + 1)) Β· (1 + (1 / (π + 1))))) |
149 | 135, 148 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((π + 1) Β·
((1 + (π / (π + 1))) Β· (1 + (1 /
(π + 1))))) = ((π + (π + 1)) Β· (1 + (1 / (π + 1))))) |
150 | 149 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (((π + 1) / (π + (π + 1))) Β· ((π + 1) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))))) = (((π + 1) / (π + (π + 1))) Β· ((π + (π + 1)) Β· (1 + (1 / (π + 1)))))) |
151 | 100 | rpcnd 12964 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β (π + (π + 1)) β
β) |
152 | 102, 151,
134 | mulassd 11183 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((((π + 1) / (π + (π + 1))) Β· (π + (π + 1))) Β· (1 + (1 / (π + 1)))) = (((π + 1) / (π + (π + 1))) Β· ((π + (π + 1)) Β· (1 + (1 / (π + 1)))))) |
153 | 100 | rpne0d 12967 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β0)
β (π + (π + 1)) β 0) |
154 | 127, 151,
153 | divcan1d 11937 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β (((π + 1) / (π + (π + 1))) Β· (π + (π + 1))) = (π + 1)) |
155 | 154 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β ((((π + 1) / (π + (π + 1))) Β· (π + (π + 1))) Β· (1 + (1 / (π + 1)))) = ((π + 1) Β· (1 + (1 / (π + 1))))) |
156 | 116 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β (1 / (π + 1)) β
β) |
157 | 127, 103,
156 | adddid 11184 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β ((π + 1) Β· (1
+ (1 / (π + 1)))) =
(((π + 1) Β· 1) +
((π + 1) Β· (1 /
(π +
1))))) |
158 | 103, 127,
129 | divcan2d 11938 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β ((π + 1) Β· (1
/ (π + 1))) =
1) |
159 | 137, 158 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
1) + ((π + 1) Β· (1 /
(π + 1)))) = ((π + 1) + 1)) |
160 | 155, 157,
159 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((((π + 1) / (π + (π + 1))) Β· (π + (π + 1))) Β· (1 + (1 / (π + 1)))) = ((π + 1) + 1)) |
161 | 152, 160 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (((π + 1) / (π + (π + 1))) Β· ((π + (π + 1)) Β· (1 + (1 / (π + 1))))) = ((π + 1) + 1)) |
162 | 132, 150,
161 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β ((π + 1) Β·
(((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))))) = ((π + 1) + 1)) |
163 | 119 | rpcnd 12964 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((π + 1) / (π + 1)) β
β) |
164 | 127, 103,
163 | adddid 11184 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β ((π + 1) Β· (1
+ ((π + 1) / (π + 1)))) = (((π + 1) Β· 1) + ((π + 1) Β· ((π + 1) / (π + 1))))) |
165 | 94, 127, 129 | divcan2d 11938 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((π + 1) Β·
((π + 1) / (π + 1))) = (π + 1)) |
166 | 137, 165 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
1) + ((π + 1) Β·
((π + 1) / (π + 1)))) = ((π + 1) + (π + 1))) |
167 | 164, 166 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β ((π + 1) Β· (1
+ ((π + 1) / (π + 1)))) = ((π + 1) + (π + 1))) |
168 | 162, 167 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
(((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))))) / ((π + 1) Β· (1 + ((π + 1) / (π + 1))))) = (((π + 1) + 1) / ((π + 1) + (π + 1)))) |
169 | 102, 131,
126, 128 | divassd 11971 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β ((((π + 1) / (π + (π + 1))) Β· ((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1))))) / (1 + ((π + 1) / (π + 1)))) = (((π + 1) / (π + (π + 1))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1)))))) |
170 | 130, 168,
169 | 3eqtr3rd 2782 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β0)
β (((π + 1) / (π + (π + 1))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1))))) = (((π + 1) + 1) / ((π + 1) + (π + 1)))) |
171 | 170 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β ((π + 1) Β·
(((π + 1) / (π + (π + 1))) Β· (((1 + (π / (π + 1))) Β· (1 + (1 / (π + 1)))) / (1 + ((π + 1) / (π + 1)))))) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))) |
172 | 92, 123, 171 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β β β§ π β β0)
β (((π + 1) Β·
((π + 1) / (π + (π + 1)))) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1))) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))) |
173 | 172 | adantr 482 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (((π + 1) Β· ((π + 1) / (π + (π + 1)))) Β· ((π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))β(π + 1))) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))) |
174 | 76, 78, 173 | 3eqtrd 2777 |
. . . . . . . 8
β’ (((π β β β§ π β β0)
β§ (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))) |
175 | 174 | exp31 421 |
. . . . . . 7
β’ (π β β β (π β β0
β ((seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))))) |
176 | 175 | a2d 29 |
. . . . . 6
β’ (π β β β ((π β β0
β (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) β (π β β0 β (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π)))))β(π + 1)) = ((π + 1) Β· (((π + 1) + 1) / ((π + 1) + (π + 1))))))) |
177 | 11, 18, 25, 32, 71, 176 | nnind 12176 |
. . . . 5
β’ (π β β β (π β β0
β (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1)))))) |
178 | 177 | impcom 409 |
. . . 4
β’ ((π β β0
β§ π β β)
β (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) |
179 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = π β (π₯ + 1) = (π + 1)) |
180 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = π β (π₯ + (π + 1)) = (π + (π + 1))) |
181 | 179, 180 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π β ((π₯ + 1) / (π₯ + (π + 1))) = ((π + 1) / (π + (π + 1)))) |
182 | 181 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = π β ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) |
183 | | eqid 2733 |
. . . . . 6
β’ (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1))))) = (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1))))) |
184 | | ovex 7391 |
. . . . . 6
β’ ((π + 1) Β· ((π + 1) / (π + (π + 1)))) β V |
185 | 182, 183,
184 | fvmpt 6949 |
. . . . 5
β’ (π β β β ((π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) |
186 | 185 | adantl 483 |
. . . 4
β’ ((π β β0
β§ π β β)
β ((π₯ β β
β¦ ((π + 1) Β·
((π₯ + 1) / (π₯ + (π + 1)))))βπ) = ((π + 1) Β· ((π + 1) / (π + (π + 1))))) |
187 | 178, 186 | eqtr4d 2776 |
. . 3
β’ ((π β β0
β§ π β β)
β (seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))βπ)) |
188 | 187 | ralrimiva 3140 |
. 2
β’ (π β β0
β βπ β
β (seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))βπ)) |
189 | | seqfn 13924 |
. . . . 5
β’ (1 β
β€ β seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) Fn
(β€β₯β1)) |
190 | 2, 189 | ax-mp 5 |
. . . 4
β’ seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π))))) Fn
(β€β₯β1) |
191 | 73 | fneq2i 6601 |
. . . 4
β’ (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π))))) Fn β β seq1( Β· ,
(π β β β¦
(((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) Fn
(β€β₯β1)) |
192 | 190, 191 | mpbir 230 |
. . 3
β’ seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π))))) Fn β |
193 | | ovex 7391 |
. . . 4
β’ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))) β V |
194 | 193, 183 | fnmpti 6645 |
. . 3
β’ (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1))))) Fn β |
195 | | eqfnfv 6983 |
. . 3
β’ ((seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π))))) Fn β β§ (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1))))) Fn β) β (seq1( Β·
, (π β β β¦
(((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) = (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1))))) β βπ β β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))βπ))) |
196 | 192, 194,
195 | mp2an 691 |
. 2
β’ (seq1(
Β· , (π β
β β¦ (((1 + (π /
π)) Β· (1 + (1 /
π))) / (1 + ((π + 1) / π))))) = (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1))))) β βπ β β (seq1( Β· , (π β β β¦ (((1 +
(π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π)))))βπ) = ((π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))βπ)) |
197 | 188, 196 | sylibr 233 |
1
β’ (π β β0
β seq1( Β· , (π
β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) = (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))) |