Step | Hyp | Ref
| Expression |
1 | | sq2 14107 |
. . . . . 6
โข
(2โ2) = 4 |
2 | | 2t2e4 12322 |
. . . . . 6
โข (2
ยท 2) = 4 |
3 | 1, 2 | eqtr4i 2764 |
. . . . 5
โข
(2โ2) = (2 ยท 2) |
4 | 3 | oveq2i 7369 |
. . . 4
โข
((2โ(๐ + 1)) /
(2โ2)) = ((2โ(๐ +
1)) / (2 ยท 2)) |
5 | | 2cn 12233 |
. . . . . 6
โข 2 โ
โ |
6 | | expp1 13980 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ0) โ (2โ(๐ + 1)) = ((2โ๐) ยท 2)) |
7 | 5, 6 | mpan 689 |
. . . . 5
โข (๐ โ โ0
โ (2โ(๐ + 1)) =
((2โ๐) ยท
2)) |
8 | 7 | oveq1d 7373 |
. . . 4
โข (๐ โ โ0
โ ((2โ(๐ + 1)) /
(2 ยท 2)) = (((2โ๐) ยท 2) / (2 ยท
2))) |
9 | 4, 8 | eqtrid 2785 |
. . 3
โข (๐ โ โ0
โ ((2โ(๐ + 1)) /
(2โ2)) = (((2โ๐)
ยท 2) / (2 ยท 2))) |
10 | | expcl 13991 |
. . . . 5
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
11 | 5, 10 | mpan 689 |
. . . 4
โข (๐ โ โ0
โ (2โ๐) โ
โ) |
12 | | 2cnne0 12368 |
. . . . 5
โข (2 โ
โ โง 2 โ 0) |
13 | | divmuldiv 11860 |
. . . . 5
โข
((((2โ๐) โ
โ โง 2 โ โ) โง ((2 โ โ โง 2 โ 0) โง
(2 โ โ โง 2 โ 0))) โ (((2โ๐) / 2) ยท (2 / 2)) = (((2โ๐) ยท 2) / (2 ยท
2))) |
14 | 12, 12, 13 | mpanr12 704 |
. . . 4
โข
(((2โ๐) โ
โ โง 2 โ โ) โ (((2โ๐) / 2) ยท (2 / 2)) = (((2โ๐) ยท 2) / (2 ยท
2))) |
15 | 11, 5, 14 | sylancl 587 |
. . 3
โข (๐ โ โ0
โ (((2โ๐) / 2)
ยท (2 / 2)) = (((2โ๐) ยท 2) / (2 ยท
2))) |
16 | | 2div2e1 12299 |
. . . . 5
โข (2 / 2) =
1 |
17 | 16 | oveq2i 7369 |
. . . 4
โข
(((2โ๐) / 2)
ยท (2 / 2)) = (((2โ๐) / 2) ยท 1) |
18 | 11 | halfcld 12403 |
. . . . 5
โข (๐ โ โ0
โ ((2โ๐) / 2)
โ โ) |
19 | 18 | mulid1d 11177 |
. . . 4
โข (๐ โ โ0
โ (((2โ๐) / 2)
ยท 1) = ((2โ๐) /
2)) |
20 | 17, 19 | eqtrid 2785 |
. . 3
โข (๐ โ โ0
โ (((2โ๐) / 2)
ยท (2 / 2)) = ((2โ๐) / 2)) |
21 | 9, 15, 20 | 3eqtr2rd 2780 |
. 2
โข (๐ โ โ0
โ ((2โ๐) / 2) =
((2โ(๐ + 1)) /
(2โ2))) |
22 | | 2nn0 12435 |
. . . 4
โข 2 โ
โ0 |
23 | | faclbnd 14196 |
. . . 4
โข ((2
โ โ0 โง ๐ โ โ0) โ
(2โ(๐ + 1)) โค
((2โ2) ยท (!โ๐))) |
24 | 22, 23 | mpan 689 |
. . 3
โข (๐ โ โ0
โ (2โ(๐ + 1))
โค ((2โ2) ยท (!โ๐))) |
25 | | 2re 12232 |
. . . . 5
โข 2 โ
โ |
26 | | peano2nn0 12458 |
. . . . 5
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
27 | | reexpcl 13990 |
. . . . 5
โข ((2
โ โ โง (๐ +
1) โ โ0) โ (2โ(๐ + 1)) โ โ) |
28 | 25, 26, 27 | sylancr 588 |
. . . 4
โข (๐ โ โ0
โ (2โ(๐ + 1))
โ โ) |
29 | | faccl 14189 |
. . . . 5
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
30 | 29 | nnred 12173 |
. . . 4
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
31 | | 4re 12242 |
. . . . . . 7
โข 4 โ
โ |
32 | 1, 31 | eqeltri 2830 |
. . . . . 6
โข
(2โ2) โ โ |
33 | | 4pos 12265 |
. . . . . . 7
โข 0 <
4 |
34 | 33, 1 | breqtrri 5133 |
. . . . . 6
โข 0 <
(2โ2) |
35 | 32, 34 | pm3.2i 472 |
. . . . 5
โข
((2โ2) โ โ โง 0 < (2โ2)) |
36 | | ledivmul 12036 |
. . . . 5
โข
(((2โ(๐ + 1))
โ โ โง (!โ๐) โ โ โง ((2โ2) โ
โ โง 0 < (2โ2))) โ (((2โ(๐ + 1)) / (2โ2)) โค (!โ๐) โ (2โ(๐ + 1)) โค ((2โ2) ยท
(!โ๐)))) |
37 | 35, 36 | mp3an3 1451 |
. . . 4
โข
(((2โ(๐ + 1))
โ โ โง (!โ๐) โ โ) โ (((2โ(๐ + 1)) / (2โ2)) โค
(!โ๐) โ
(2โ(๐ + 1)) โค
((2โ2) ยท (!โ๐)))) |
38 | 28, 30, 37 | syl2anc 585 |
. . 3
โข (๐ โ โ0
โ (((2โ(๐ + 1)) /
(2โ2)) โค (!โ๐) โ (2โ(๐ + 1)) โค ((2โ2) ยท
(!โ๐)))) |
39 | 24, 38 | mpbird 257 |
. 2
โข (๐ โ โ0
โ ((2โ(๐ + 1)) /
(2โ2)) โค (!โ๐)) |
40 | 21, 39 | eqbrtrd 5128 |
1
โข (๐ โ โ0
โ ((2โ๐) / 2)
โค (!โ๐)) |