Step | Hyp | Ref
| Expression |
1 | | nn0re 12481 |
. . . . . . . . 9
โข (๐ โ โ0
โ ๐ โ
โ) |
2 | | reexpcl 14044 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐พ โ โ0)
โ (๐โ๐พ) โ
โ) |
3 | 1, 2 | sylan 581 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐พ โ
โ0) โ (๐โ๐พ) โ โ) |
4 | 3 | ancoms 460 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ โ
โ0) โ (๐โ๐พ) โ โ) |
5 | | nnre 12219 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
6 | | reexpcl 14044 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
7 | 5, 6 | sylan 581 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
8 | | remulcl 11195 |
. . . . . . 7
โข (((๐โ๐พ) โ โ โง (๐โ๐) โ โ) โ ((๐โ๐พ) ยท (๐โ๐)) โ โ) |
9 | 4, 7, 8 | syl2an 597 |
. . . . . 6
โข (((๐พ โ โ0
โง ๐ โ
โ0) โง (๐ โ โ โง ๐ โ โ0)) โ ((๐โ๐พ) ยท (๐โ๐)) โ โ) |
10 | 9 | anandirs 678 |
. . . . 5
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โ โ) |
11 | | 2nn 12285 |
. . . . . . . . 9
โข 2 โ
โ |
12 | | nn0sqcl 14055 |
. . . . . . . . 9
โข (๐พ โ โ0
โ (๐พโ2) โ
โ0) |
13 | | nnexpcl 14040 |
. . . . . . . . 9
โข ((2
โ โ โง (๐พโ2) โ โ0) โ
(2โ(๐พโ2)) โ
โ) |
14 | 11, 12, 13 | sylancr 588 |
. . . . . . . 8
โข (๐พ โ โ0
โ (2โ(๐พโ2))
โ โ) |
15 | | nnnn0 12479 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
16 | | nn0addcl 12507 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐พ โ
โ0) โ (๐ + ๐พ) โ
โ0) |
17 | 16 | ancoms 460 |
. . . . . . . . . . 11
โข ((๐พ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐พ) โ
โ0) |
18 | 15, 17 | sylan2 594 |
. . . . . . . . . 10
โข ((๐พ โ โ0
โง ๐ โ โ)
โ (๐ + ๐พ) โ
โ0) |
19 | | nnexpcl 14040 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ + ๐พ) โ โ0) โ (๐โ(๐ + ๐พ)) โ โ) |
20 | 18, 19 | sylan2 594 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐พ โ โ0
โง ๐ โ โ))
โ (๐โ(๐ + ๐พ)) โ โ) |
21 | 20 | anabss7 672 |
. . . . . . . 8
โข ((๐พ โ โ0
โง ๐ โ โ)
โ (๐โ(๐ + ๐พ)) โ โ) |
22 | | nnmulcl 12236 |
. . . . . . . 8
โข
(((2โ(๐พโ2)) โ โ โง (๐โ(๐ + ๐พ)) โ โ) โ ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) โ โ) |
23 | 14, 21, 22 | syl2an2r 684 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ โ โ)
โ ((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) โ โ) |
24 | 23 | nnred 12227 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ โ โ)
โ ((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) โ โ) |
25 | | faccl 14243 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
26 | 25 | nnred 12227 |
. . . . . 6
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
27 | | remulcl 11195 |
. . . . . 6
โข
((((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) โ โ โง (!โ๐) โ โ) โ
(((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ) |
28 | 24, 26, 27 | syl2an 597 |
. . . . 5
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ) |
29 | | 2re 12286 |
. . . . . 6
โข 2 โ
โ |
30 | | remulcl 11195 |
. . . . . 6
โข ((2
โ โ โง (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ) โ (2 ยท
(((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) โ โ) |
31 | 29, 28, 30 | sylancr 588 |
. . . . 5
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) โ โ) |
32 | | faclbnd4 14257 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐พ โ
โ0 โง ๐
โ โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
33 | 15, 32 | syl3an3 1166 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐พ โ
โ0 โง ๐
โ โ) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
34 | 33 | 3coml 1128 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ โ โ
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
35 | 34 | 3expa 1119 |
. . . . 5
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
36 | | 1lt2 12383 |
. . . . . 6
โข 1 <
2 |
37 | | nnmulcl 12236 |
. . . . . . . . 9
โข
((((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) โ โ โง (!โ๐) โ โ) โ
(((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ) |
38 | 23, 25, 37 | syl2an 597 |
. . . . . . . 8
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ) |
39 | 38 | nngt0d 12261 |
. . . . . . 7
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ 0 < (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
40 | | ltmulgt12 12075 |
. . . . . . . 8
โข
(((((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ โง 2 โ โ
โง 0 < (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) โ (1 < 2 โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) < (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))))) |
41 | 29, 40 | mp3an2 1450 |
. . . . . . 7
โข
(((((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ โ โง 0 <
(((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) โ (1 < 2 โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) < (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))))) |
42 | 28, 39, 41 | syl2anc 585 |
. . . . . 6
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ (1 < 2 โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) < (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))))) |
43 | 36, 42 | mpbii 232 |
. . . . 5
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) < (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
44 | 10, 28, 31, 35, 43 | lelttrd 11372 |
. . . 4
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) < (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
45 | | 2cn 12287 |
. . . . 5
โข 2 โ
โ |
46 | 23 | nncnd 12228 |
. . . . 5
โข ((๐พ โ โ0
โง ๐ โ โ)
โ ((2โ(๐พโ2))
ยท (๐โ(๐ + ๐พ))) โ โ) |
47 | 25 | nncnd 12228 |
. . . . 5
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
48 | | mulass 11198 |
. . . . 5
โข ((2
โ โ โง ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) โ โ โง (!โ๐) โ โ) โ ((2
ยท ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) ยท (!โ๐)) = (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
49 | 45, 46, 47, 48 | mp3an3an 1468 |
. . . 4
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ ((2 ยท ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) ยท (!โ๐)) = (2 ยท (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
50 | 44, 49 | breqtrrd 5177 |
. . 3
โข (((๐พ โ โ0
โง ๐ โ โ)
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) < ((2 ยท ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) ยท (!โ๐))) |
51 | 50 | 3impa 1111 |
. 2
โข ((๐พ โ โ0
โง ๐ โ โ
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) < ((2 ยท ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) ยท (!โ๐))) |
52 | 51 | 3comr 1126 |
1
โข ((๐ โ โ0
โง ๐พ โ
โ0 โง ๐
โ โ) โ ((๐โ๐พ) ยท (๐โ๐)) < ((2 ยท ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) ยท (!โ๐))) |