Step | Hyp | Ref
| Expression |
1 | | axsegconlem7.2 |
. . . . . . . 8
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) |
2 | 1 | axsegconlem4 27932 |
. . . . . . 7
โข ((๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โ (โโ๐) โ โ) |
3 | 2 | ad2antlr 725 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ โ) |
4 | | simpl1 1191 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐ด โ (๐ผโ๐)) |
5 | | fveere 27913 |
. . . . . . 7
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
6 | 4, 5 | sylan 580 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
7 | 3, 6 | remulcld 11194 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐ดโ๐)) โ โ) |
8 | 7 | recnd 11192 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐ดโ๐)) โ โ) |
9 | | axsegconlem2.1 |
. . . . . . . . 9
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) |
10 | 9 | axsegconlem4 27932 |
. . . . . . . 8
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (โโ๐) โ โ) |
11 | 10 | 3adant3 1132 |
. . . . . . 7
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ (โโ๐) โ โ) |
12 | 11 | ad2antrr 724 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ โ) |
13 | | axsegconlem8.3 |
. . . . . . . 8
โข ๐น = (๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) |
14 | 9, 1, 13 | axsegconlem8 27936 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐น โ (๐ผโ๐)) |
15 | | fveere 27913 |
. . . . . . 7
โข ((๐น โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐นโ๐) โ โ) |
16 | 14, 15 | sylan 580 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐นโ๐) โ โ) |
17 | 12, 16 | remulcld 11194 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐นโ๐)) โ โ) |
18 | 17 | recnd 11192 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐นโ๐)) โ โ) |
19 | | readdcl 11143 |
. . . . . . 7
โข
(((โโ๐)
โ โ โง (โโ๐) โ โ) โ
((โโ๐) +
(โโ๐)) โ
โ) |
20 | 11, 2, 19 | syl2an 596 |
. . . . . 6
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ((โโ๐) + (โโ๐)) โ โ) |
21 | 20 | adantr 481 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) + (โโ๐)) โ โ) |
22 | 21 | recnd 11192 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) + (โโ๐)) โ โ) |
23 | | 0red 11167 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ 0 โ
โ) |
24 | 11 | adantr 481 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (โโ๐) โ โ) |
25 | 9 | axsegconlem6 27934 |
. . . . . . . 8
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ 0 < (โโ๐)) |
26 | 25 | adantr 481 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ 0 < (โโ๐)) |
27 | 1 | axsegconlem5 27933 |
. . . . . . . . 9
โข ((๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โ 0 โค (โโ๐)) |
28 | 27 | adantl 482 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ 0 โค (โโ๐)) |
29 | | addge01 11674 |
. . . . . . . . 9
โข
(((โโ๐)
โ โ โง (โโ๐) โ โ) โ (0 โค
(โโ๐) โ
(โโ๐) โค
((โโ๐) +
(โโ๐)))) |
30 | 11, 2, 29 | syl2an 596 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (0 โค (โโ๐) โ (โโ๐) โค ((โโ๐) + (โโ๐)))) |
31 | 28, 30 | mpbid 231 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (โโ๐) โค ((โโ๐) + (โโ๐))) |
32 | 23, 24, 20, 26, 31 | ltletrd 11324 |
. . . . . 6
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ 0 < ((โโ๐) + (โโ๐))) |
33 | 32 | gt0ne0d 11728 |
. . . . 5
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ((โโ๐) + (โโ๐)) โ 0) |
34 | 33 | adantr 481 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) + (โโ๐)) โ 0) |
35 | 8, 18, 22, 34 | divdird 11978 |
. . 3
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) / ((โโ๐) + (โโ๐))) = ((((โโ๐) ยท (๐ดโ๐)) / ((โโ๐) + (โโ๐))) + (((โโ๐) ยท (๐นโ๐)) / ((โโ๐) + (โโ๐))))) |
36 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
37 | 36 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) = (((โโ๐) + (โโ๐)) ยท (๐ตโ๐))) |
38 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
39 | 38 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((โโ๐) ยท (๐ดโ๐)) = ((โโ๐) ยท (๐ดโ๐))) |
40 | 37, 39 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) = ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐)))) |
41 | 40 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)) = (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) |
42 | | ovex 7395 |
. . . . . . . . . 10
โข
(((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)) โ V |
43 | 41, 13, 42 | fvmpt 6953 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ (๐นโ๐) = (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) |
44 | 43 | adantl 482 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐นโ๐) = (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) |
45 | 44 | oveq2d 7378 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐นโ๐)) = ((โโ๐) ยท (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)))) |
46 | | simpl2 1192 |
. . . . . . . . . . . 12
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐ต โ (๐ผโ๐)) |
47 | | fveere 27913 |
. . . . . . . . . . . 12
โข ((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
48 | 46, 47 | sylan 580 |
. . . . . . . . . . 11
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
49 | 21, 48 | remulcld 11194 |
. . . . . . . . . 10
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ โ) |
50 | 49, 7 | resubcld 11592 |
. . . . . . . . 9
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) โ โ) |
51 | 50 | recnd 11192 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) โ โ) |
52 | 12 | recnd 11192 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ โ) |
53 | 25 | gt0ne0d 11728 |
. . . . . . . . 9
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ (โโ๐) โ 0) |
54 | 53 | ad2antrr 724 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ 0) |
55 | 51, 52, 54 | divcan2d 11942 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) = ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐)))) |
56 | 45, 55 | eqtrd 2771 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐นโ๐)) = ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐)))) |
57 | 56 | oveq2d 7378 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) = (((โโ๐) ยท (๐ดโ๐)) + ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))))) |
58 | 49 | recnd 11192 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ โ) |
59 | 8, 58 | pncan3d 11524 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) + ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐)))) = (((โโ๐) + (โโ๐)) ยท (๐ตโ๐))) |
60 | 57, 59 | eqtrd 2771 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) = (((โโ๐) + (โโ๐)) ยท (๐ตโ๐))) |
61 | 7, 17 | readdcld 11193 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) โ โ) |
62 | 61 | recnd 11192 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) โ โ) |
63 | 48 | recnd 11192 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
64 | 62, 63, 22, 34 | divmul2d 11973 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) / ((โโ๐) + (โโ๐))) = (๐ตโ๐) โ (((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) = (((โโ๐) + (โโ๐)) ยท (๐ตโ๐)))) |
65 | 60, 64 | mpbird 256 |
. . 3
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) ยท (๐ดโ๐)) + ((โโ๐) ยท (๐นโ๐))) / ((โโ๐) + (โโ๐))) = (๐ตโ๐)) |
66 | 2 | recnd 11192 |
. . . . . . 7
โข ((๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โ (โโ๐) โ โ) |
67 | 66 | ad2antlr 725 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ โ) |
68 | 6 | recnd 11192 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
69 | 67, 68, 22, 34 | div23d 11977 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) / ((โโ๐) + (โโ๐))) = (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐ดโ๐))) |
70 | 22, 52, 22, 34 | divsubdird 11979 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) + (โโ๐)) โ (โโ๐)) / ((โโ๐) + (โโ๐))) = ((((โโ๐) + (โโ๐)) / ((โโ๐) + (โโ๐))) โ
((โโ๐) /
((โโ๐) +
(โโ๐))))) |
71 | 11 | recnd 11192 |
. . . . . . . . . 10
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ (โโ๐) โ โ) |
72 | | pncan2 11417 |
. . . . . . . . . 10
โข
(((โโ๐)
โ โ โง (โโ๐) โ โ) โ
(((โโ๐) +
(โโ๐)) โ
(โโ๐)) =
(โโ๐)) |
73 | 71, 66, 72 | syl2an 596 |
. . . . . . . . 9
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (((โโ๐) + (โโ๐)) โ (โโ๐)) = (โโ๐)) |
74 | 73 | adantr 481 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) + (โโ๐)) โ (โโ๐)) = (โโ๐)) |
75 | 74 | oveq1d 7377 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) + (โโ๐)) โ (โโ๐)) / ((โโ๐) + (โโ๐))) = ((โโ๐) / ((โโ๐) + (โโ๐)))) |
76 | 22, 34 | dividd 11938 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) + (โโ๐)) / ((โโ๐) + (โโ๐))) = 1) |
77 | 76 | oveq1d 7377 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) + (โโ๐)) / ((โโ๐) + (โโ๐))) โ
((โโ๐) /
((โโ๐) +
(โโ๐)))) = (1
โ ((โโ๐)
/ ((โโ๐) +
(โโ๐))))) |
78 | 70, 75, 77 | 3eqtr3d 2779 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) / ((โโ๐) + (โโ๐))) = (1 โ ((โโ๐) / ((โโ๐) + (โโ๐))))) |
79 | 78 | oveq1d 7377 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐ดโ๐)) = ((1 โ ((โโ๐) / ((โโ๐) + (โโ๐)))) ยท (๐ดโ๐))) |
80 | 69, 79 | eqtrd 2771 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐ดโ๐)) / ((โโ๐) + (โโ๐))) = ((1 โ ((โโ๐) / ((โโ๐) + (โโ๐)))) ยท (๐ดโ๐))) |
81 | 16 | recnd 11192 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐นโ๐) โ โ) |
82 | 52, 81, 22, 34 | div23d 11977 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) ยท (๐นโ๐)) / ((โโ๐) + (โโ๐))) = (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐นโ๐))) |
83 | 80, 82 | oveq12d 7380 |
. . 3
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) ยท (๐ดโ๐)) / ((โโ๐) + (โโ๐))) + (((โโ๐) ยท (๐นโ๐)) / ((โโ๐) + (โโ๐)))) = (((1 โ ((โโ๐) / ((โโ๐) + (โโ๐)))) ยท (๐ดโ๐)) + (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐นโ๐)))) |
84 | 35, 65, 83 | 3eqtr3d 2779 |
. 2
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ตโ๐) = (((1 โ ((โโ๐) / ((โโ๐) + (โโ๐)))) ยท (๐ดโ๐)) + (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐นโ๐)))) |
85 | 84 | ralrimiva 3139 |
1
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ((โโ๐) / ((โโ๐) + (โโ๐)))) ยท (๐ดโ๐)) + (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐นโ๐)))) |