Step | Hyp | Ref
| Expression |
1 | | 1rp 12943 |
. . . . . . . 8
โข 1 โ
โ+ |
2 | 1 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ต โ โ)
โ 1 โ โ+) |
3 | | nnrp 12950 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต โ
โ+) |
4 | 3 | rpreccld 12991 |
. . . . . . . 8
โข (๐ต โ โ โ (1 /
๐ต) โ
โ+) |
5 | 4 | adantl 482 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 / ๐ต) โ
โ+) |
6 | 2, 5 | rpaddcld 12996 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + (1 / ๐ต)) โ
โ+) |
7 | 6 | rpcnd 12983 |
. . . . 5
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + (1 / ๐ต)) โ
โ) |
8 | | simpl 483 |
. . . . 5
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ๐ โ
โ0) |
9 | 7, 8 | expp1d 14077 |
. . . 4
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((1 + (1 / ๐ต))โ(๐ + 1)) = (((1 + (1 / ๐ต))โ๐) ยท (1 + (1 / ๐ต)))) |
10 | 1 | a1i 11 |
. . . . . . . . 9
โข (๐ต โ โ โ 1 โ
โ+) |
11 | 10, 4 | rpaddcld 12996 |
. . . . . . . 8
โข (๐ต โ โ โ (1 + (1 /
๐ต)) โ
โ+) |
12 | | nn0z 12548 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โค) |
13 | | rpexpcl 14011 |
. . . . . . . 8
โข (((1 + (1
/ ๐ต)) โ
โ+ โง ๐
โ โค) โ ((1 + (1 / ๐ต))โ๐) โ
โ+) |
14 | 11, 12, 13 | syl2anr 597 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((1 + (1 / ๐ต))โ๐) โ
โ+) |
15 | 14 | rpcnd 12983 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((1 + (1 / ๐ต))โ๐) โ โ) |
16 | | 1cnd 11174 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ต โ โ)
โ 1 โ โ) |
17 | | nn0nndivcl 12508 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (๐ / ๐ต) โ
โ) |
18 | 17 | recnd 11207 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (๐ / ๐ต) โ
โ) |
19 | 16, 18 | addcomd 11381 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + (๐ / ๐ต)) = ((๐ / ๐ต) + 1)) |
20 | | nn0ge0div 12596 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ต โ โ)
โ 0 โค (๐ / ๐ต)) |
21 | 17, 20 | ge0p1rpd 13011 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((๐ / ๐ต) + 1) โ
โ+) |
22 | 19, 21 | eqeltrd 2832 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + (๐ / ๐ต)) โ
โ+) |
23 | 22 | rpcnd 12983 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + (๐ / ๐ต)) โ
โ) |
24 | 22 | rpne0d 12986 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + (๐ / ๐ต)) โ 0) |
25 | 15, 23, 24 | divcan1d 11956 |
. . . . 5
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท (1 + (๐ / ๐ต))) = ((1 + (1 / ๐ต))โ๐)) |
26 | 25 | oveq1d 7392 |
. . . 4
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท (1 + (๐ / ๐ต))) ยท (1 + (1 / ๐ต))) = (((1 + (1 / ๐ต))โ๐) ยท (1 + (1 / ๐ต)))) |
27 | 14, 22 | rpdivcld 12998 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) โ
โ+) |
28 | 27 | rpcnd 12983 |
. . . . 5
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) โ โ) |
29 | 28, 23, 7 | mulassd 11202 |
. . . 4
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท (1 + (๐ / ๐ต))) ยท (1 + (1 / ๐ต))) = ((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท ((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต))))) |
30 | 9, 26, 29 | 3eqtr2d 2777 |
. . 3
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((1 + (1 / ๐ต))โ(๐ + 1)) = ((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท ((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต))))) |
31 | 30 | oveq1d 7392 |
. 2
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((1 + (1 / ๐ต))โ(๐ + 1)) / (1 + ((๐ + 1) / ๐ต))) = (((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท ((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต)))) / (1 + ((๐ + 1) / ๐ต)))) |
32 | 22, 6 | rpmulcld 12997 |
. . . 4
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต))) โ
โ+) |
33 | 32 | rpcnd 12983 |
. . 3
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต))) โ
โ) |
34 | | nn0p1nn 12476 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
35 | 34 | nnrpd 12979 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + 1) โ
โ+) |
36 | 35 | adantr 481 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (๐ + 1) โ
โ+) |
37 | 3 | adantl 482 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ๐ต โ
โ+) |
38 | 36, 37 | rpdivcld 12998 |
. . . . 5
โข ((๐ โ โ0
โง ๐ต โ โ)
โ ((๐ + 1) / ๐ต) โ
โ+) |
39 | 2, 38 | rpaddcld 12996 |
. . . 4
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + ((๐ + 1) /
๐ต)) โ
โ+) |
40 | 39 | rpcnd 12983 |
. . 3
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + ((๐ + 1) /
๐ต)) โ
โ) |
41 | 39 | rpne0d 12986 |
. . 3
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (1 + ((๐ + 1) /
๐ต)) โ
0) |
42 | 28, 33, 40, 41 | divassd 11990 |
. 2
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท ((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต)))) / (1 + ((๐ + 1) / ๐ต))) = ((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท (((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต))) / (1 + ((๐ + 1) / ๐ต))))) |
43 | 31, 42 | eqtrd 2771 |
1
โข ((๐ โ โ0
โง ๐ต โ โ)
โ (((1 + (1 / ๐ต))โ(๐ + 1)) / (1 + ((๐ + 1) / ๐ต))) = ((((1 + (1 / ๐ต))โ๐) / (1 + (๐ / ๐ต))) ยท (((1 + (๐ / ๐ต)) ยท (1 + (1 / ๐ต))) / (1 + ((๐ + 1) / ๐ต))))) |