Step | Hyp | Ref
| Expression |
1 | | axsegconlem8.3 |
. 2
โข ๐น = (๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) |
2 | | axsegconlem2.1 |
. . . . . . . . . . 11
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) |
3 | 2 | axsegconlem4 28167 |
. . . . . . . . . 10
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (โโ๐) โ โ) |
4 | 3 | 3adant3 1132 |
. . . . . . . . 9
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ (โโ๐) โ โ) |
5 | 4 | ad2antrr 724 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ โ) |
6 | | axsegconlem7.2 |
. . . . . . . . . 10
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) |
7 | 6 | axsegconlem4 28167 |
. . . . . . . . 9
โข ((๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โ (โโ๐) โ โ) |
8 | 7 | ad2antlr 725 |
. . . . . . . 8
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ โ) |
9 | 5, 8 | readdcld 11239 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) + (โโ๐)) โ โ) |
10 | | simpl2 1192 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐ต โ (๐ผโ๐)) |
11 | | fveere 28148 |
. . . . . . . 8
โข ((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
12 | 10, 11 | sylan 580 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
13 | 9, 12 | remulcld 11240 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ โ) |
14 | | simpl1 1191 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐ด โ (๐ผโ๐)) |
15 | | fveere 28148 |
. . . . . . . 8
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
16 | 14, 15 | sylan 580 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
17 | 8, 16 | remulcld 11240 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((โโ๐) ยท (๐ดโ๐)) โ โ) |
18 | 13, 17 | resubcld 11638 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) โ โ) |
19 | 2 | axsegconlem6 28169 |
. . . . . . 7
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ 0 < (โโ๐)) |
20 | 19 | gt0ne0d 11774 |
. . . . . 6
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ (โโ๐) โ 0) |
21 | 20 | ad2antrr 724 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (โโ๐) โ 0) |
22 | 18, 5, 21 | redivcld 12038 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)) โ โ) |
23 | 22 | ralrimiva 3146 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ โ (1...๐)(((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)) โ โ) |
24 | | eleenn 28143 |
. . . . 5
โข (๐ท โ (๐ผโ๐) โ ๐ โ โ) |
25 | 24 | ad2antll 727 |
. . . 4
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐ โ โ) |
26 | | mptelee 28142 |
. . . 4
โข (๐ โ โ โ ((๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) โ (๐ผโ๐) โ โ๐ โ (1...๐)(((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)) โ โ)) |
27 | 25, 26 | syl 17 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ((๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) โ (๐ผโ๐) โ โ๐ โ (1...๐)(((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐)) โ โ)) |
28 | 23, 27 | mpbird 256 |
. 2
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) โ (๐ผโ๐)) |
29 | 1, 28 | eqeltrid 2837 |
1
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐น โ (๐ผโ๐)) |