Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . 4
โข (๐ฅ = 4 โ (2โ๐ฅ) = (2โ4)) |
2 | | 2exp4 17018 |
. . . 4
โข
(2โ4) = ;16 |
3 | 1, 2 | eqtrdi 2789 |
. . 3
โข (๐ฅ = 4 โ (2โ๐ฅ) = ;16) |
4 | | fveq2 6892 |
. . . 4
โข (๐ฅ = 4 โ (!โ๐ฅ) =
(!โ4)) |
5 | | fac4 14241 |
. . . 4
โข
(!โ4) = ;24 |
6 | 4, 5 | eqtrdi 2789 |
. . 3
โข (๐ฅ = 4 โ (!โ๐ฅ) = ;24) |
7 | 3, 6 | breq12d 5162 |
. 2
โข (๐ฅ = 4 โ ((2โ๐ฅ) < (!โ๐ฅ) โ ;16 < ;24)) |
8 | | oveq2 7417 |
. . 3
โข (๐ฅ = ๐ โ (2โ๐ฅ) = (2โ๐)) |
9 | | fveq2 6892 |
. . 3
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
10 | 8, 9 | breq12d 5162 |
. 2
โข (๐ฅ = ๐ โ ((2โ๐ฅ) < (!โ๐ฅ) โ (2โ๐) < (!โ๐))) |
11 | | oveq2 7417 |
. . 3
โข (๐ฅ = (๐ + 1) โ (2โ๐ฅ) = (2โ(๐ + 1))) |
12 | | fveq2 6892 |
. . 3
โข (๐ฅ = (๐ + 1) โ (!โ๐ฅ) = (!โ(๐ + 1))) |
13 | 11, 12 | breq12d 5162 |
. 2
โข (๐ฅ = (๐ + 1) โ ((2โ๐ฅ) < (!โ๐ฅ) โ (2โ(๐ + 1)) < (!โ(๐ + 1)))) |
14 | | oveq2 7417 |
. . 3
โข (๐ฅ = ๐ โ (2โ๐ฅ) = (2โ๐)) |
15 | | fveq2 6892 |
. . 3
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
16 | 14, 15 | breq12d 5162 |
. 2
โข (๐ฅ = ๐ โ ((2โ๐ฅ) < (!โ๐ฅ) โ (2โ๐) < (!โ๐))) |
17 | | 1nn0 12488 |
. . 3
โข 1 โ
โ0 |
18 | | 2nn0 12489 |
. . 3
โข 2 โ
โ0 |
19 | | 6nn0 12493 |
. . 3
โข 6 โ
โ0 |
20 | | 4nn0 12491 |
. . 3
โข 4 โ
โ0 |
21 | | 6lt10 12811 |
. . 3
โข 6 <
;10 |
22 | | 1lt2 12383 |
. . 3
โข 1 <
2 |
23 | 17, 18, 19, 20, 21, 22 | decltc 12706 |
. 2
โข ;16 < ;24 |
24 | | 2nn 12285 |
. . . . . . . . 9
โข 2 โ
โ |
25 | 24 | a1i 11 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 2 โ โ) |
26 | | 4nn 12295 |
. . . . . . . . . 10
โข 4 โ
โ |
27 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ๐ โ
(โคโฅโ4)) |
28 | | eluznn 12902 |
. . . . . . . . . 10
โข ((4
โ โ โง ๐
โ (โคโฅโ4)) โ ๐ โ โ) |
29 | 26, 27, 28 | sylancr 588 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ๐ โ โ) |
30 | 29 | nnnn0d 12532 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ๐ โ โ0) |
31 | 25, 30 | nnexpcld 14208 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (2โ๐) โ โ) |
32 | 31 | nnred 12227 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (2โ๐) โ โ) |
33 | | 2re 12286 |
. . . . . . 7
โข 2 โ
โ |
34 | 33 | a1i 11 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 2 โ โ) |
35 | 32, 34 | remulcld 11244 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ((2โ๐) ยท 2) โ
โ) |
36 | 30 | faccld 14244 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (!โ๐) โ โ) |
37 | 36 | nnred 12227 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (!โ๐) โ โ) |
38 | 37, 34 | remulcld 11244 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ((!โ๐) ยท 2) โ
โ) |
39 | 29 | nnred 12227 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ๐ โ โ) |
40 | | 1red 11215 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 1 โ โ) |
41 | 39, 40 | readdcld 11243 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (๐ + 1) โ โ) |
42 | 37, 41 | remulcld 11244 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ((!โ๐) ยท (๐ + 1)) โ โ) |
43 | | 2rp 12979 |
. . . . . . 7
โข 2 โ
โ+ |
44 | 43 | a1i 11 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 2 โ
โ+) |
45 | | simpr 486 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (2โ๐) < (!โ๐)) |
46 | 32, 37, 44, 45 | ltmul1dd 13071 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ((2โ๐) ยท 2) < ((!โ๐) ยท 2)) |
47 | 36 | nnnn0d 12532 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (!โ๐) โ
โ0) |
48 | 47 | nn0ge0d 12535 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 0 โค (!โ๐)) |
49 | | df-2 12275 |
. . . . . . 7
โข 2 = (1 +
1) |
50 | 29 | nnge1d 12260 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 1 โค ๐) |
51 | 40, 39, 40, 50 | leadd1dd 11828 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (1 + 1) โค (๐ + 1)) |
52 | 49, 51 | eqbrtrid 5184 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 2 โค (๐ + 1)) |
53 | 34, 41, 37, 48, 52 | lemul2ad 12154 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ((!โ๐) ยท 2) โค ((!โ๐) ยท (๐ + 1))) |
54 | 35, 38, 42, 46, 53 | ltletrd 11374 |
. . . 4
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ ((2โ๐) ยท 2) < ((!โ๐) ยท (๐ + 1))) |
55 | | 2cnd 12290 |
. . . . 5
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ 2 โ โ) |
56 | 55, 30 | expp1d 14112 |
. . . 4
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (2โ(๐ + 1)) = ((2โ๐) ยท 2)) |
57 | | facp1 14238 |
. . . . 5
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
58 | 30, 57 | syl 17 |
. . . 4
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
59 | 54, 56, 58 | 3brtr4d 5181 |
. . 3
โข ((๐ โ
(โคโฅโ4) โง (2โ๐) < (!โ๐)) โ (2โ(๐ + 1)) < (!โ(๐ + 1))) |
60 | 59 | ex 414 |
. 2
โข (๐ โ
(โคโฅโ4) โ ((2โ๐) < (!โ๐) โ (2โ(๐ + 1)) < (!โ(๐ + 1)))) |
61 | 7, 10, 13, 16, 23, 60 | uzind4i 12894 |
1
โข (๐ โ
(โคโฅโ4) โ (2โ๐) < (!โ๐)) |