Step | Hyp | Ref
| Expression |
1 | | relin01 11734 |
. . 3
โข (๐พ โ โ โ (๐พ โค 0 โจ (0 โค ๐พ โง ๐พ โค 1) โจ 1 โค ๐พ)) |
2 | 1 | adantl 482 |
. 2
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ (๐พ โค 0 โจ (0 โค ๐พ โง ๐พ โค 1) โจ 1 โค ๐พ)) |
3 | | fveere 28148 |
. . . . . . . . 9
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
4 | 3 | adantlr 713 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
5 | | fveere 28148 |
. . . . . . . . 9
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
6 | 5 | adantll 712 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
7 | 4, 6 | jca 512 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ ((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ)) |
8 | | simprl 769 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ๐พ โ โ) |
9 | 8 | recnd 11238 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ๐พ โ โ) |
10 | | resubcl 11520 |
. . . . . . . . . . . . 13
โข (((๐ถโ๐) โ โ โง (๐ดโ๐) โ โ) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
11 | 10 | ancoms 459 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
12 | 11 | adantr 481 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
13 | 12 | recnd 11238 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
14 | 9, 13, 13 | mulassd 11233 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (๐พ ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
15 | 8, 12 | remulcld 11240 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
16 | 15 | recnd 11238 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
17 | | recn 11196 |
. . . . . . . . . . . 12
โข ((๐ดโ๐) โ โ โ (๐ดโ๐) โ โ) |
18 | 17 | ad2antrr 724 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (๐ดโ๐) โ โ) |
19 | 16, 18 | pncand 11568 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) = (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
20 | 19 | oveq1d 7420 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
21 | 13 | sqvald 14104 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (((๐ถโ๐) โ (๐ดโ๐))โ2) = (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
22 | 21 | oveq2d 7421 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (๐พ ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) = (๐พ ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
23 | 14, 20, 22 | 3eqtr4d 2782 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (๐พ ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
24 | | simprr 771 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ๐พ โค 0) |
25 | 12 | sqge0d 14098 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2)) |
26 | 24, 25 | jca 512 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (๐พ โค 0 โง 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
27 | 26 | orcd 871 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((๐พ โค 0 โง 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2)) โจ (0 โค ๐พ โง (((๐ถโ๐) โ (๐ดโ๐))โ2) โค 0))) |
28 | 12 | resqcld 14086 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (((๐ถโ๐) โ (๐ดโ๐))โ2) โ โ) |
29 | | mulle0b 12081 |
. . . . . . . . . 10
โข ((๐พ โ โ โง (((๐ถโ๐) โ (๐ดโ๐))โ2) โ โ) โ ((๐พ ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โค 0 โ ((๐พ โค 0 โง 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2)) โจ (0 โค ๐พ โง (((๐ถโ๐) โ (๐ดโ๐))โ2) โค 0)))) |
30 | 8, 28, 29 | syl2anc 584 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((๐พ ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โค 0 โ ((๐พ โค 0 โง 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2)) โจ (0 โค ๐พ โง (((๐ถโ๐) โ (๐ดโ๐))โ2) โค 0)))) |
31 | 27, 30 | mpbird 256 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ (๐พ ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โค 0) |
32 | 23, 31 | eqbrtrd 5169 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง ๐พ โค 0)) โ ((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0) |
33 | 7, 32 | sylan 580 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โง (๐พ โ โ โง ๐พ โค 0)) โ ((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0) |
34 | 33 | an32s 650 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐พ โ โ โง ๐พ โค 0)) โง ๐ โ (1...๐)) โ ((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0) |
35 | 34 | ralrimiva 3146 |
. . . 4
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐พ โ โ โง ๐พ โค 0)) โ โ๐ โ (1...๐)((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0) |
36 | 35 | expr 457 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ (๐พ โค 0 โ โ๐ โ (1...๐)((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
37 | | recn 11196 |
. . . . . . . . . . . . 13
โข ((๐ถโ๐) โ โ โ (๐ถโ๐) โ โ) |
38 | 37 | ad2antlr 725 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (๐ถโ๐) โ โ) |
39 | 17 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (๐ดโ๐) โ โ) |
40 | | simprl 769 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ๐พ โ โ) |
41 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
42 | 40, 41 | remulcld 11240 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
43 | 42 | recnd 11238 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
44 | 38, 39, 43 | sub32d 11599 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ (๐ดโ๐)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (((๐ถโ๐) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (๐ดโ๐))) |
45 | | ax-1cn 11164 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
46 | 40 | recnd 11238 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ๐พ โ โ) |
47 | 41 | recnd 11238 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
48 | | subdir 11644 |
. . . . . . . . . . . . 13
โข ((1
โ โ โง ๐พ
โ โ โง ((๐ถโ๐) โ (๐ดโ๐)) โ โ) โ ((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((1 ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
49 | 45, 46, 47, 48 | mp3an2i 1466 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((1 ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
50 | 47 | mullidd 11228 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (1 ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((๐ถโ๐) โ (๐ดโ๐))) |
51 | 50 | oveq1d 7420 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((1 ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (((๐ถโ๐) โ (๐ดโ๐)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
52 | 49, 51 | eqtr2d 2773 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ (๐ดโ๐)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = ((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
53 | 38, 43, 39 | subsub4d 11598 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (๐ดโ๐)) = ((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) |
54 | 44, 52, 53 | 3eqtr3rd 2781 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) = ((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
55 | 39, 39, 43 | sub32d 11599 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ดโ๐) โ (๐ดโ๐)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (((๐ดโ๐) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (๐ดโ๐))) |
56 | 39 | subidd 11555 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((๐ดโ๐) โ (๐ดโ๐)) = 0) |
57 | 56 | oveq1d 7420 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ดโ๐) โ (๐ดโ๐)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (0 โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
58 | | df-neg 11443 |
. . . . . . . . . . . 12
โข -(๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) = (0 โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
59 | 57, 58 | eqtr4di 2790 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ดโ๐) โ (๐ดโ๐)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = -(๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
60 | 39, 43, 39 | subsub4d 11598 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ดโ๐) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (๐ดโ๐)) = ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) |
61 | 55, 59, 60 | 3eqtr3rd 2781 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) = -(๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
62 | 54, 61 | oveq12d 7423 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) = (((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท -(๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
63 | | 1re 11210 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
64 | | resubcl 11520 |
. . . . . . . . . . . . . 14
โข ((1
โ โ โง ๐พ
โ โ) โ (1 โ ๐พ) โ โ) |
65 | 63, 64 | mpan 688 |
. . . . . . . . . . . . 13
โข (๐พ โ โ โ (1
โ ๐พ) โ
โ) |
66 | 65 | ad2antrl 726 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (1 โ ๐พ) โ
โ) |
67 | 66, 41 | remulcld 11240 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
68 | 67 | recnd 11238 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
69 | 68, 43 | mulneg2d 11664 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท -(๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = -(((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
70 | 66 | recnd 11238 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (1 โ ๐พ) โ
โ) |
71 | 70, 47, 46, 47 | mul4d 11422 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
72 | 71 | negeqd 11450 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ -(((1 โ ๐พ) ยท ((๐ถโ๐) โ (๐ดโ๐))) ยท (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐)))) = -(((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
73 | 62, 69, 72 | 3eqtrd 2776 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) = -(((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
74 | 66, 40 | remulcld 11240 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ ((1 โ ๐พ) ยท ๐พ) โ โ) |
75 | 41 | resqcld 14086 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ (๐ดโ๐))โ2) โ โ) |
76 | | simpl 483 |
. . . . . . . . . . . . . 14
โข ((๐พ โ โ โง (0 โค
๐พ โง ๐พ โค 1)) โ ๐พ โ โ) |
77 | 63, 76, 64 | sylancr 587 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง (0 โค
๐พ โง ๐พ โค 1)) โ (1 โ ๐พ) โ
โ) |
78 | | subge0 11723 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ๐พ
โ โ) โ (0 โค (1 โ ๐พ) โ ๐พ โค 1)) |
79 | 63, 78 | mpan 688 |
. . . . . . . . . . . . . . 15
โข (๐พ โ โ โ (0 โค
(1 โ ๐พ) โ ๐พ โค 1)) |
80 | 79 | biimpar 478 |
. . . . . . . . . . . . . 14
โข ((๐พ โ โ โง ๐พ โค 1) โ 0 โค (1
โ ๐พ)) |
81 | 80 | adantrl 714 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง (0 โค
๐พ โง ๐พ โค 1)) โ 0 โค (1 โ ๐พ)) |
82 | | simprl 769 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง (0 โค
๐พ โง ๐พ โค 1)) โ 0 โค ๐พ) |
83 | 77, 76, 81, 82 | mulge0d 11787 |
. . . . . . . . . . . 12
โข ((๐พ โ โ โง (0 โค
๐พ โง ๐พ โค 1)) โ 0 โค ((1 โ ๐พ) ยท ๐พ)) |
84 | 83 | adantl 482 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ 0 โค ((1 โ ๐พ) ยท ๐พ)) |
85 | 41 | sqge0d 14098 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2)) |
86 | 74, 75, 84, 85 | mulge0d 11787 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ 0 โค (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
87 | 47 | sqvald 14104 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ (๐ดโ๐))โ2) = (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
88 | 87 | oveq2d 7421 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) = (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
89 | 86, 88 | breqtrd 5173 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ 0 โค (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
90 | 41, 41 | remulcld 11240 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
91 | 74, 90 | remulcld 11240 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ โ) |
92 | 91 | le0neg2d 11782 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (0 โค (((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ -(((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โค 0)) |
93 | 89, 92 | mpbid 231 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ -(((1 โ ๐พ) ยท ๐พ) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โค 0) |
94 | 73, 93 | eqbrtrd 5169 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0) |
95 | 7, 94 | sylan 580 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ (((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0) |
96 | 95 | an32s 650 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โง ๐ โ (1...๐)) โ (((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0) |
97 | 96 | ralrimiva 3146 |
. . . 4
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐พ โ โ โง (0 โค ๐พ โง ๐พ โค 1))) โ โ๐ โ (1...๐)(((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0) |
98 | 97 | expr 457 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ ((0 โค ๐พ โง ๐พ โค 1) โ โ๐ โ (1...๐)(((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0)) |
99 | 37 | ad2antlr 725 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐ถโ๐) โ โ) |
100 | 17 | ad2antrr 724 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐ดโ๐) โ โ) |
101 | 99, 100 | negsubdi2d 11583 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ -((๐ถโ๐) โ (๐ดโ๐)) = ((๐ดโ๐) โ (๐ถโ๐))) |
102 | 101 | oveq1d 7420 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (-((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
103 | | simplr 767 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐ถโ๐) โ โ) |
104 | | simpll 765 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐ดโ๐) โ โ) |
105 | 103, 104,
10 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
106 | 105 | recnd 11238 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
107 | | peano2rem 11523 |
. . . . . . . . . . . . . 14
โข (๐พ โ โ โ (๐พ โ 1) โ
โ) |
108 | 107 | ad2antrl 726 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐พ โ 1) โ โ) |
109 | 108, 105 | remulcld 11240 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
110 | 109 | recnd 11238 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
111 | 106, 110 | mulneg1d 11663 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (-((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = -(((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
112 | 108 | recnd 11238 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐พ โ 1) โ โ) |
113 | 106, 112,
106 | mul12d 11419 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
114 | 106 | sqvald 14104 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ถโ๐) โ (๐ดโ๐))โ2) = (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
115 | 114 | oveq2d 7421 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) = ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
116 | 113, 115 | eqtr4d 2775 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
117 | 116 | negeqd 11450 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ -(((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = -((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
118 | 111, 117 | eqtrd 2772 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (-((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = -((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
119 | | simprl 769 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ๐พ โ โ) |
120 | 119 | recnd 11238 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ๐พ โ โ) |
121 | | subdir 11644 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง 1 โ
โ โง ((๐ถโ๐) โ (๐ดโ๐)) โ โ) โ ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (1 ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
122 | 45, 121 | mp3an2 1449 |
. . . . . . . . . . . 12
โข ((๐พ โ โ โง ((๐ถโ๐) โ (๐ดโ๐)) โ โ) โ ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (1 ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
123 | 120, 106,
122 | syl2anc 584 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (1 ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
124 | 106 | mullidd 11228 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (1 ยท ((๐ถโ๐) โ (๐ดโ๐))) = ((๐ถโ๐) โ (๐ดโ๐))) |
125 | 124 | oveq2d 7421 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (1 ยท ((๐ถโ๐) โ (๐ดโ๐)))) = ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ ((๐ถโ๐) โ (๐ดโ๐)))) |
126 | 119, 105 | remulcld 11240 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
127 | 126 | recnd 11238 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
128 | 127, 99, 100 | subsub3d 11597 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) โ ((๐ถโ๐) โ (๐ดโ๐))) = (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) |
129 | 123, 125,
128 | 3eqtrd 2776 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) |
130 | 129 | oveq2d 7421 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐พ โ 1) ยท ((๐ถโ๐) โ (๐ดโ๐)))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐)))) |
131 | 102, 118,
130 | 3eqtr3rd 2781 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) = -((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
132 | 105 | resqcld 14086 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ถโ๐) โ (๐ดโ๐))โ2) โ โ) |
133 | | simprr 771 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ 1 โค ๐พ) |
134 | | subge0 11723 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง 1 โ
โ) โ (0 โค (๐พ
โ 1) โ 1 โค ๐พ)) |
135 | 63, 134 | mpan2 689 |
. . . . . . . . . . . 12
โข (๐พ โ โ โ (0 โค
(๐พ โ 1) โ 1 โค
๐พ)) |
136 | 135 | ad2antrl 726 |
. . . . . . . . . . 11
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (0 โค (๐พ โ 1) โ 1 โค ๐พ)) |
137 | 133, 136 | mpbird 256 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ 0 โค (๐พ โ 1)) |
138 | 105 | sqge0d 14098 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ 0 โค (((๐ถโ๐) โ (๐ดโ๐))โ2)) |
139 | 108, 132,
137, 138 | mulge0d 11787 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ 0 โค ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2))) |
140 | 108, 132 | remulcld 11240 |
. . . . . . . . . 10
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โ โ) |
141 | 140 | le0neg2d 11782 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (0 โค ((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โ -((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โค 0)) |
142 | 139, 141 | mpbid 231 |
. . . . . . . 8
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ -((๐พ โ 1) ยท (((๐ถโ๐) โ (๐ดโ๐))โ2)) โค 0) |
143 | 131, 142 | eqbrtrd 5169 |
. . . . . . 7
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0) |
144 | 7, 143 | sylan 580 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โง (๐พ โ โ โง 1 โค ๐พ)) โ (((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0) |
145 | 144 | an32s 650 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐พ โ โ โง 1 โค ๐พ)) โง ๐ โ (1...๐)) โ (((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0) |
146 | 145 | ralrimiva 3146 |
. . . 4
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐พ โ โ โง 1 โค ๐พ)) โ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0) |
147 | 146 | expr 457 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ (1 โค ๐พ โ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |
148 | 36, 98, 147 | 3orim123d 1444 |
. 2
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ ((๐พ โค 0 โจ (0 โค ๐พ โง ๐พ โค 1) โจ 1 โค ๐พ) โ (โ๐ โ (1...๐)((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0))) |
149 | 2, 148 | mpd 15 |
1
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ (โ๐ โ (1...๐)((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |