Step | Hyp | Ref
| Expression |
1 | | 2cn 12229 |
. . . . 5
โข 2 โ
โ |
2 | | csbrn.1 |
. . . . . . 7
โข (๐ โ ๐ด โ Fin) |
3 | | csbrn.2 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
4 | | csbrn.3 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
5 | 3, 4 | remulcld 11186 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (๐ต ยท ๐ถ) โ โ) |
6 | 2, 5 | fsumrecl 15620 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โ โ) |
7 | 6 | recnd 11184 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โ โ) |
8 | | sqmul 14025 |
. . . . 5
โข ((2
โ โ โง ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โ โ) โ ((2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) = ((2โ2) ยท
(ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2))) |
9 | 1, 7, 8 | sylancr 588 |
. . . 4
โข (๐ โ ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) = ((2โ2) ยท
(ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2))) |
10 | | sq2 14102 |
. . . . 5
โข
(2โ2) = 4 |
11 | 10 | oveq1i 7368 |
. . . 4
โข
((2โ2) ยท (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) = (4 ยท (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) |
12 | 9, 11 | eqtrdi 2793 |
. . 3
โข (๐ โ ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) = (4 ยท (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2))) |
13 | 3 | resqcld 14031 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐ตโ2) โ โ) |
14 | 2, 13 | fsumrecl 15620 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด (๐ตโ2) โ โ) |
15 | | 2re 12228 |
. . . . . 6
โข 2 โ
โ |
16 | | remulcl 11137 |
. . . . . 6
โข ((2
โ โ โง ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โ โ) โ (2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โ โ) |
17 | 15, 6, 16 | sylancr 588 |
. . . . 5
โข (๐ โ (2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โ โ) |
18 | 4 | resqcld 14031 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐ถโ2) โ โ) |
19 | 2, 18 | fsumrecl 15620 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด (๐ถโ2) โ โ) |
20 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ Fin) |
21 | 13 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ตโ2) โ โ) |
22 | | simplr 768 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ๐ฅ โ โ) |
23 | 22 | resqcld 14031 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ฅโ2) โ โ) |
24 | 21, 23 | remulcld 11186 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((๐ตโ2) ยท (๐ฅโ2)) โ โ) |
25 | | remulcl 11137 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (๐ต
ยท ๐ถ) โ โ)
โ (2 ยท (๐ต
ยท ๐ถ)) โ
โ) |
26 | 15, 5, 25 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
27 | 26 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
28 | 27, 22 | remulcld 11186 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ) โ โ) |
29 | 24, 28 | readdcld 11185 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) โ โ) |
30 | 18 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ถโ2) โ โ) |
31 | 29, 30 | readdcld 11185 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2)) โ โ) |
32 | 3 | adantlr 714 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ๐ต โ โ) |
33 | 32, 22 | remulcld 11186 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ต ยท ๐ฅ) โ โ) |
34 | 4 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ๐ถ โ โ) |
35 | 33, 34 | readdcld 11185 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((๐ต ยท ๐ฅ) + ๐ถ) โ โ) |
36 | 35 | sqge0d 14043 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ 0 โค (((๐ต ยท ๐ฅ) + ๐ถ)โ2)) |
37 | 33 | recnd 11184 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ต ยท ๐ฅ) โ โ) |
38 | 34 | recnd 11184 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ๐ถ โ โ) |
39 | | binom2 14122 |
. . . . . . . . . 10
โข (((๐ต ยท ๐ฅ) โ โ โง ๐ถ โ โ) โ (((๐ต ยท ๐ฅ) + ๐ถ)โ2) = ((((๐ต ยท ๐ฅ)โ2) + (2 ยท ((๐ต ยท ๐ฅ) ยท ๐ถ))) + (๐ถโ2))) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (((๐ต ยท ๐ฅ) + ๐ถ)โ2) = ((((๐ต ยท ๐ฅ)โ2) + (2 ยท ((๐ต ยท ๐ฅ) ยท ๐ถ))) + (๐ถโ2))) |
41 | 32 | recnd 11184 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ๐ต โ โ) |
42 | 22 | recnd 11184 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ๐ฅ โ โ) |
43 | 41, 42 | sqmuld 14064 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((๐ต ยท ๐ฅ)โ2) = ((๐ตโ2) ยท (๐ฅโ2))) |
44 | 41, 42, 38 | mul32d 11366 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((๐ต ยท ๐ฅ) ยท ๐ถ) = ((๐ต ยท ๐ถ) ยท ๐ฅ)) |
45 | 44 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (2 ยท ((๐ต ยท ๐ฅ) ยท ๐ถ)) = (2 ยท ((๐ต ยท ๐ถ) ยท ๐ฅ))) |
46 | | 2cnd 12232 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ 2 โ โ) |
47 | 5 | adantlr 714 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ต ยท ๐ถ) โ โ) |
48 | 47 | recnd 11184 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ต ยท ๐ถ) โ โ) |
49 | 46, 48, 42 | mulassd 11179 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ) = (2 ยท ((๐ต ยท ๐ถ) ยท ๐ฅ))) |
50 | 45, 49 | eqtr4d 2780 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (2 ยท ((๐ต ยท ๐ฅ) ยท ๐ถ)) = ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) |
51 | 43, 50 | oveq12d 7376 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (((๐ต ยท ๐ฅ)โ2) + (2 ยท ((๐ต ยท ๐ฅ) ยท ๐ถ))) = (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ))) |
52 | 51 | oveq1d 7373 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((((๐ต ยท ๐ฅ)โ2) + (2 ยท ((๐ต ยท ๐ฅ) ยท ๐ถ))) + (๐ถโ2)) = ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2))) |
53 | 40, 52 | eqtrd 2777 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (((๐ต ยท ๐ฅ) + ๐ถ)โ2) = ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2))) |
54 | 36, 53 | breqtrd 5132 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ 0 โค ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2))) |
55 | 20, 31, 54 | fsumge0 15681 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ 0 โค ฮฃ๐ โ ๐ด ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2))) |
56 | 24 | recnd 11184 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((๐ตโ2) ยท (๐ฅโ2)) โ โ) |
57 | 28 | recnd 11184 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ) โ โ) |
58 | 56, 57 | addcld 11175 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) โ โ) |
59 | 30 | recnd 11184 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ถโ2) โ โ) |
60 | 20, 58, 59 | fsumadd 15626 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ฮฃ๐ โ ๐ด ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2)) = (ฮฃ๐ โ ๐ด (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
61 | 20, 56, 57 | fsumadd 15626 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ ฮฃ๐ โ ๐ด (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) = (ฮฃ๐ โ ๐ด ((๐ตโ2) ยท (๐ฅโ2)) + ฮฃ๐ โ ๐ด ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ))) |
62 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
63 | 62 | recnd 11184 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
64 | 63 | sqcld 14050 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ) โ (๐ฅโ2) โ โ) |
65 | 21 | recnd 11184 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (๐ตโ2) โ โ) |
66 | 20, 64, 65 | fsummulc1 15671 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ) โ (ฮฃ๐ โ ๐ด (๐ตโ2) ยท (๐ฅโ2)) = ฮฃ๐ โ ๐ด ((๐ตโ2) ยท (๐ฅโ2))) |
67 | | 2cnd 12232 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ 2 โ
โ) |
68 | 20, 67, 48 | fsummulc2 15670 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ) โ (2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) = ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ))) |
69 | 68 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ) โ ((2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ) = (ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) |
70 | 26 | recnd 11184 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
71 | 70 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ ๐ด) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
72 | 20, 63, 71 | fsummulc1 15671 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ) โ (ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ) = ฮฃ๐ โ ๐ด ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) |
73 | 69, 72 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ) โ ((2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ) = ฮฃ๐ โ ๐ด ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) |
74 | 66, 73 | oveq12d 7376 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ ((ฮฃ๐ โ ๐ด (๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ)) = (ฮฃ๐ โ ๐ด ((๐ตโ2) ยท (๐ฅโ2)) + ฮฃ๐ โ ๐ด ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ))) |
75 | 61, 74 | eqtr4d 2780 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ ฮฃ๐ โ ๐ด (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) = ((ฮฃ๐ โ ๐ด (๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ))) |
76 | 75 | oveq1d 7373 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ (ฮฃ๐ โ ๐ด (((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + ฮฃ๐ โ ๐ด (๐ถโ2)) = (((ฮฃ๐ โ ๐ด (๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ)) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
77 | 60, 76 | eqtrd 2777 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ ฮฃ๐ โ ๐ด ((((๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท (๐ต ยท ๐ถ)) ยท ๐ฅ)) + (๐ถโ2)) = (((ฮฃ๐ โ ๐ด (๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ)) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
78 | 55, 77 | breqtrd 5132 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ 0 โค
(((ฮฃ๐ โ ๐ด (๐ตโ2) ยท (๐ฅโ2)) + ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) ยท ๐ฅ)) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
79 | 14, 17, 19, 78 | discr 14144 |
. . . 4
โข (๐ โ (((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โ (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) โค 0) |
80 | 17 | resqcld 14031 |
. . . . 5
โข (๐ โ ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โ โ) |
81 | | 4re 12238 |
. . . . . 6
โข 4 โ
โ |
82 | 14, 19 | remulcld 11186 |
. . . . . 6
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ โ) |
83 | | remulcl 11137 |
. . . . . 6
โข ((4
โ โ โง (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ โ) โ (4 ยท
(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ โ) |
84 | 81, 82, 83 | sylancr 588 |
. . . . 5
โข (๐ โ (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ โ) |
85 | 80, 84 | suble0d 11747 |
. . . 4
โข (๐ โ ((((2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โ (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) โค 0 โ ((2 ยท
ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โค (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) |
86 | 79, 85 | mpbid 231 |
. . 3
โข (๐ โ ((2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โค (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) |
87 | 12, 86 | eqbrtrrd 5130 |
. 2
โข (๐ โ (4 ยท (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) โค (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) |
88 | 6 | resqcld 14031 |
. . 3
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2) โ โ) |
89 | 81 | a1i 11 |
. . 3
โข (๐ โ 4 โ
โ) |
90 | | 4pos 12261 |
. . . 4
โข 0 <
4 |
91 | 90 | a1i 11 |
. . 3
โข (๐ โ 0 < 4) |
92 | | lemul2 12009 |
. . 3
โข
(((ฮฃ๐ โ
๐ด (๐ต ยท ๐ถ)โ2) โ โ โง (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ โ โง (4 โ
โ โง 0 < 4)) โ ((ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2) โค (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ (4 ยท (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) โค (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) |
93 | 88, 82, 89, 91, 92 | syl112anc 1375 |
. 2
โข (๐ โ ((ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2) โค (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ (4 ยท (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) โค (4 ยท (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) |
94 | 87, 93 | mpbird 257 |
1
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2) โค (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) |