Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . . 7
โข (๐ โ (0...๐) โ Fin) |
2 | | elfznn0 13541 |
. . . . . . . 8
โข (๐ โ (0...๐) โ ๐ โ โ0) |
3 | | eirr.1 |
. . . . . . . . . . . 12
โข ๐น = (๐ โ โ0 โฆ (1 /
(!โ๐))) |
4 | | nn0z 12531 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ๐ โ
โค) |
5 | | 1exp 14004 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ
(1โ๐) =
1) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (1โ๐) =
1) |
7 | 6 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ((1โ๐) /
(!โ๐)) = (1 /
(!โ๐))) |
8 | 7 | mpteq2ia 5213 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โฆ ((1โ๐) /
(!โ๐))) = (๐ โ โ0
โฆ (1 / (!โ๐))) |
9 | 3, 8 | eqtr4i 2768 |
. . . . . . . . . . 11
โข ๐น = (๐ โ โ0 โฆ
((1โ๐) /
(!โ๐))) |
10 | 9 | eftval 15966 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐นโ๐) = ((1โ๐) / (!โ๐))) |
11 | 10 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ((1โ๐) / (!โ๐))) |
12 | | ax-1cn 11116 |
. . . . . . . . . . 11
โข 1 โ
โ |
13 | 12 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
14 | | eftcl 15963 |
. . . . . . . . . 10
โข ((1
โ โ โง ๐
โ โ0) โ ((1โ๐) / (!โ๐)) โ โ) |
15 | 13, 14 | sylan 581 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
((1โ๐) /
(!โ๐)) โ
โ) |
16 | 11, 15 | eqeltrd 2838 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) โ โ) |
17 | 2, 16 | sylan2 594 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ (๐นโ๐) โ โ) |
18 | 1, 17 | fsumcl 15625 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (0...๐)(๐นโ๐) โ โ) |
19 | | nn0uz 12812 |
. . . . . . . . 9
โข
โ0 = (โคโฅโ0) |
20 | | eqid 2737 |
. . . . . . . . 9
โข
(โคโฅโ(๐ + 1)) =
(โคโฅโ(๐ + 1)) |
21 | | eirr.3 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
22 | 21 | peano2nnd 12177 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โ) |
23 | 22 | nnnn0d 12480 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ
โ0) |
24 | | eqidd 2738 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = (๐นโ๐)) |
25 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (1 / (!โ๐)) = (1 / (!โ๐))) |
27 | | ovex 7395 |
. . . . . . . . . . . 12
โข (1 /
(!โ๐)) โ
V |
28 | 26, 3, 27 | fvmpt 6953 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐นโ๐) = (1 / (!โ๐))) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = (1 / (!โ๐))) |
30 | | faccl 14190 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
31 | 30 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
32 | 31 | nnrpd 12962 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ+) |
33 | 32 | rpreccld 12974 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ (1 /
(!โ๐)) โ
โ+) |
34 | 29, 33 | eqeltrd 2838 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) โ
โ+) |
35 | 9 | efcllem 15967 |
. . . . . . . . . 10
โข (1 โ
โ โ seq0( + , ๐น)
โ dom โ ) |
36 | 13, 35 | syl 17 |
. . . . . . . . 9
โข (๐ โ seq0( + , ๐น) โ dom โ
) |
37 | 19, 20, 23, 24, 34, 36 | isumrpcl 15735 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) โ
โ+) |
38 | 37 | rpred 12964 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) โ โ) |
39 | 38 | recnd 11190 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) โ โ) |
40 | | esum 15970 |
. . . . . . . . 9
โข e =
ฮฃ๐ โ
โ0 (1 / (!โ๐)) |
41 | 28 | sumeq2i 15591 |
. . . . . . . . 9
โข
ฮฃ๐ โ
โ0 (๐นโ๐) = ฮฃ๐ โ โ0 (1 /
(!โ๐)) |
42 | 40, 41 | eqtr4i 2768 |
. . . . . . . 8
โข e =
ฮฃ๐ โ
โ0 (๐นโ๐) |
43 | 19, 20, 23, 24, 16, 36 | isumsplit 15732 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ โ0 (๐นโ๐) = (ฮฃ๐ โ (0...((๐ + 1) โ 1))(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐))) |
44 | 42, 43 | eqtrid 2789 |
. . . . . . 7
โข (๐ โ e = (ฮฃ๐ โ (0...((๐ + 1) โ 1))(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐))) |
45 | 21 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
46 | | pncan 11414 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
47 | 45, 12, 46 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1) โ 1) = ๐) |
48 | 47 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (0...((๐ + 1) โ 1)) = (0...๐)) |
49 | 48 | sumeq1d 15593 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (0...((๐ + 1) โ 1))(๐นโ๐) = ฮฃ๐ โ (0...๐)(๐นโ๐)) |
50 | 49 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ (0...((๐ + 1) โ 1))(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐)) = (ฮฃ๐ โ (0...๐)(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐))) |
51 | 44, 50 | eqtrd 2777 |
. . . . . 6
โข (๐ โ e = (ฮฃ๐ โ (0...๐)(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐))) |
52 | 18, 39, 51 | mvrladdd 11575 |
. . . . 5
โข (๐ โ (e โ ฮฃ๐ โ (0...๐)(๐นโ๐)) = ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐)) |
53 | 52 | oveq2d 7378 |
. . . 4
โข (๐ โ ((!โ๐) ยท (e โ
ฮฃ๐ โ (0...๐)(๐นโ๐))) = ((!โ๐) ยท ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐))) |
54 | 21 | nnnn0d 12480 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
55 | 54 | faccld 14191 |
. . . . . 6
โข (๐ โ (!โ๐) โ โ) |
56 | 55 | nncnd 12176 |
. . . . 5
โข (๐ โ (!โ๐) โ โ) |
57 | | ere 15978 |
. . . . . . 7
โข e โ
โ |
58 | 57 | recni 11176 |
. . . . . 6
โข e โ
โ |
59 | 58 | a1i 11 |
. . . . 5
โข (๐ โ e โ
โ) |
60 | 56, 59, 18 | subdid 11618 |
. . . 4
โข (๐ โ ((!โ๐) ยท (e โ
ฮฃ๐ โ (0...๐)(๐นโ๐))) = (((!โ๐) ยท e) โ ((!โ๐) ยท ฮฃ๐ โ (0...๐)(๐นโ๐)))) |
61 | 53, 60 | eqtr3d 2779 |
. . 3
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) = (((!โ๐) ยท e) โ ((!โ๐) ยท ฮฃ๐ โ (0...๐)(๐นโ๐)))) |
62 | | eirr.4 |
. . . . . . 7
โข (๐ โ e = (๐ / ๐)) |
63 | 62 | oveq2d 7378 |
. . . . . 6
โข (๐ โ ((!โ๐) ยท e) = ((!โ๐) ยท (๐ / ๐))) |
64 | | eirr.2 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
65 | 64 | zcnd 12615 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
66 | 21 | nnne0d 12210 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
67 | 56, 65, 45, 66 | div12d 11974 |
. . . . . 6
โข (๐ โ ((!โ๐) ยท (๐ / ๐)) = (๐ ยท ((!โ๐) / ๐))) |
68 | 63, 67 | eqtrd 2777 |
. . . . 5
โข (๐ โ ((!โ๐) ยท e) = (๐ ยท ((!โ๐) / ๐))) |
69 | 21 | nnred 12175 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
70 | 69 | leidd 11728 |
. . . . . . . 8
โข (๐ โ ๐ โค ๐) |
71 | | facdiv 14194 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ
โง ๐ โค ๐) โ ((!โ๐) / ๐) โ โ) |
72 | 54, 21, 70, 71 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ ((!โ๐) / ๐) โ โ) |
73 | 72 | nnzd 12533 |
. . . . . 6
โข (๐ โ ((!โ๐) / ๐) โ โค) |
74 | 64, 73 | zmulcld 12620 |
. . . . 5
โข (๐ โ (๐ ยท ((!โ๐) / ๐)) โ โค) |
75 | 68, 74 | eqeltrd 2838 |
. . . 4
โข (๐ โ ((!โ๐) ยท e) โ
โค) |
76 | 1, 56, 17 | fsummulc2 15676 |
. . . . 5
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ (0...๐)(๐นโ๐)) = ฮฃ๐ โ (0...๐)((!โ๐) ยท (๐นโ๐))) |
77 | 2 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ ๐ โ โ0) |
78 | 77, 28 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (๐นโ๐) = (1 / (!โ๐))) |
79 | 78 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((!โ๐) ยท (๐นโ๐)) = ((!โ๐) ยท (1 / (!โ๐)))) |
80 | 56 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (!โ๐) โ โ) |
81 | 2, 31 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...๐)) โ (!โ๐) โ โ) |
82 | 81 | nncnd 12176 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (!โ๐) โ โ) |
83 | | facne0 14193 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (!โ๐) โ
0) |
84 | 77, 83 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ (!โ๐) โ 0) |
85 | 80, 82, 84 | divrecd 11941 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ ((!โ๐) / (!โ๐)) = ((!โ๐) ยท (1 / (!โ๐)))) |
86 | 79, 85 | eqtr4d 2780 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ ((!โ๐) ยท (๐นโ๐)) = ((!โ๐) / (!โ๐))) |
87 | | permnn 14233 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ ((!โ๐) / (!โ๐)) โ โ) |
88 | 87 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ ((!โ๐) / (!โ๐)) โ โ) |
89 | 86, 88 | eqeltrd 2838 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ ((!โ๐) ยท (๐นโ๐)) โ โ) |
90 | 89 | nnzd 12533 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ ((!โ๐) ยท (๐นโ๐)) โ โค) |
91 | 1, 90 | fsumzcl 15627 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...๐)((!โ๐) ยท (๐นโ๐)) โ โค) |
92 | 76, 91 | eqeltrd 2838 |
. . . 4
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ (0...๐)(๐นโ๐)) โ โค) |
93 | 75, 92 | zsubcld 12619 |
. . 3
โข (๐ โ (((!โ๐) ยท e) โ
((!โ๐) ยท
ฮฃ๐ โ (0...๐)(๐นโ๐))) โ โค) |
94 | 61, 93 | eqeltrd 2838 |
. 2
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) โ โค) |
95 | | 0zd 12518 |
. . 3
โข (๐ โ 0 โ
โค) |
96 | 55 | nnrpd 12962 |
. . . . 5
โข (๐ โ (!โ๐) โ
โ+) |
97 | 96, 37 | rpmulcld 12980 |
. . . 4
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) โ
โ+) |
98 | 97 | rpgt0d 12967 |
. . 3
โข (๐ โ 0 < ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐))) |
99 | 22 | peano2nnd 12177 |
. . . . . . . 8
โข (๐ โ ((๐ + 1) + 1) โ โ) |
100 | 99 | nnred 12175 |
. . . . . . 7
โข (๐ โ ((๐ + 1) + 1) โ โ) |
101 | 23 | faccld 14191 |
. . . . . . . 8
โข (๐ โ (!โ(๐ + 1)) โ
โ) |
102 | 101, 22 | nnmulcld 12213 |
. . . . . . 7
โข (๐ โ ((!โ(๐ + 1)) ยท (๐ + 1)) โ
โ) |
103 | 100, 102 | nndivred 12214 |
. . . . . 6
โข (๐ โ (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1))) โ โ) |
104 | 55 | nnrecred 12211 |
. . . . . 6
โข (๐ โ (1 / (!โ๐)) โ
โ) |
105 | | abs1 15189 |
. . . . . . . . . . . 12
โข
(absโ1) = 1 |
106 | 105 | oveq1i 7372 |
. . . . . . . . . . 11
โข
((absโ1)โ๐) = (1โ๐) |
107 | 106 | oveq1i 7372 |
. . . . . . . . . 10
โข
(((absโ1)โ๐) / (!โ๐)) = ((1โ๐) / (!โ๐)) |
108 | 107 | mpteq2i 5215 |
. . . . . . . . 9
โข (๐ โ โ0
โฆ (((absโ1)โ๐) / (!โ๐))) = (๐ โ โ0 โฆ
((1โ๐) /
(!โ๐))) |
109 | 9, 108 | eqtr4i 2768 |
. . . . . . . 8
โข ๐น = (๐ โ โ0 โฆ
(((absโ1)โ๐) /
(!โ๐))) |
110 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ โ0
โฆ ((((absโ1)โ(๐ + 1)) / (!โ(๐ + 1))) ยท ((1 / ((๐ + 1) + 1))โ๐))) = (๐ โ โ0 โฆ
((((absโ1)โ(๐ +
1)) / (!โ(๐ + 1)))
ยท ((1 / ((๐ + 1) +
1))โ๐))) |
111 | | 1le1 11790 |
. . . . . . . . . 10
โข 1 โค
1 |
112 | 105, 111 | eqbrtri 5131 |
. . . . . . . . 9
โข
(absโ1) โค 1 |
113 | 112 | a1i 11 |
. . . . . . . 8
โข (๐ โ (absโ1) โค
1) |
114 | 9, 109, 110, 22, 13, 113 | eftlub 15998 |
. . . . . . 7
โข (๐ โ (absโฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) โค (((absโ1)โ(๐ + 1)) ยท (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1))))) |
115 | 37 | rprege0d 12971 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) โ โ โง 0 โค ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐))) |
116 | | absid 15188 |
. . . . . . . 8
โข
((ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐) โ โ โง 0 โค ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) โ (absโฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) = ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐)) |
117 | 115, 116 | syl 17 |
. . . . . . 7
โข (๐ โ (absโฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) = ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐)) |
118 | 105 | oveq1i 7372 |
. . . . . . . . . 10
โข
((absโ1)โ(๐ + 1)) = (1โ(๐ + 1)) |
119 | 22 | nnzd 12533 |
. . . . . . . . . . 11
โข (๐ โ (๐ + 1) โ โค) |
120 | | 1exp 14004 |
. . . . . . . . . . 11
โข ((๐ + 1) โ โค โ
(1โ(๐ + 1)) =
1) |
121 | 119, 120 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (1โ(๐ + 1)) = 1) |
122 | 118, 121 | eqtrid 2789 |
. . . . . . . . 9
โข (๐ โ ((absโ1)โ(๐ + 1)) = 1) |
123 | 122 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ
(((absโ1)โ(๐ +
1)) ยท (((๐ + 1) + 1)
/ ((!โ(๐ + 1))
ยท (๐ + 1)))) = (1
ยท (((๐ + 1) + 1) /
((!โ(๐ + 1)) ยท
(๐ +
1))))) |
124 | 103 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1))) โ โ) |
125 | 124 | mulid2d 11180 |
. . . . . . . 8
โข (๐ โ (1 ยท (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1)))) = (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1)))) |
126 | 123, 125 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ
(((absโ1)โ(๐ +
1)) ยท (((๐ + 1) + 1)
/ ((!โ(๐ + 1))
ยท (๐ + 1)))) =
(((๐ + 1) + 1) /
((!โ(๐ + 1)) ยท
(๐ + 1)))) |
127 | 114, 117,
126 | 3brtr3d 5141 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) โค (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1)))) |
128 | 22 | nnred 12175 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โ) |
129 | 128, 128 | readdcld 11191 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) + (๐ + 1)) โ โ) |
130 | 128, 128 | remulcld 11192 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) ยท (๐ + 1)) โ โ) |
131 | | 1red 11163 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
132 | 21 | nnge1d 12208 |
. . . . . . . . . . 11
โข (๐ โ 1 โค ๐) |
133 | | 1nn 12171 |
. . . . . . . . . . . 12
โข 1 โ
โ |
134 | | nnleltp1 12565 |
. . . . . . . . . . . 12
โข ((1
โ โ โง ๐
โ โ) โ (1 โค ๐ โ 1 < (๐ + 1))) |
135 | 133, 21, 134 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (1 โค ๐ โ 1 < (๐ + 1))) |
136 | 132, 135 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ 1 < (๐ + 1)) |
137 | 131, 128,
128, 136 | ltadd2dd 11321 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) + 1) < ((๐ + 1) + (๐ + 1))) |
138 | 22 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ (๐ + 1) โ โ) |
139 | 138 | 2timesd 12403 |
. . . . . . . . . 10
โข (๐ โ (2 ยท (๐ + 1)) = ((๐ + 1) + (๐ + 1))) |
140 | | df-2 12223 |
. . . . . . . . . . . 12
โข 2 = (1 +
1) |
141 | 131, 69, 131, 132 | leadd1dd 11776 |
. . . . . . . . . . . 12
โข (๐ โ (1 + 1) โค (๐ + 1)) |
142 | 140, 141 | eqbrtrid 5145 |
. . . . . . . . . . 11
โข (๐ โ 2 โค (๐ + 1)) |
143 | | 2re 12234 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
144 | 143 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
145 | 22 | nngt0d 12209 |
. . . . . . . . . . . 12
โข (๐ โ 0 < (๐ + 1)) |
146 | | lemul1 12014 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (๐ +
1) โ โ โง ((๐
+ 1) โ โ โง 0 < (๐ + 1))) โ (2 โค (๐ + 1) โ (2 ยท (๐ + 1)) โค ((๐ + 1) ยท (๐ + 1)))) |
147 | 144, 128,
128, 145, 146 | syl112anc 1375 |
. . . . . . . . . . 11
โข (๐ โ (2 โค (๐ + 1) โ (2 ยท (๐ + 1)) โค ((๐ + 1) ยท (๐ + 1)))) |
148 | 142, 147 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (2 ยท (๐ + 1)) โค ((๐ + 1) ยท (๐ + 1))) |
149 | 139, 148 | eqbrtrrd 5134 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) + (๐ + 1)) โค ((๐ + 1) ยท (๐ + 1))) |
150 | 100, 129,
130, 137, 149 | ltletrd 11322 |
. . . . . . . 8
โข (๐ โ ((๐ + 1) + 1) < ((๐ + 1) ยท (๐ + 1))) |
151 | | facp1 14185 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
152 | 54, 151 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
153 | 152 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((!โ(๐ + 1)) / (!โ๐)) = (((!โ๐) ยท (๐ + 1)) / (!โ๐))) |
154 | 101 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ (!โ(๐ + 1)) โ
โ) |
155 | 55 | nnne0d 12210 |
. . . . . . . . . . . 12
โข (๐ โ (!โ๐) โ 0) |
156 | 154, 56, 155 | divrecd 11941 |
. . . . . . . . . . 11
โข (๐ โ ((!โ(๐ + 1)) / (!โ๐)) = ((!โ(๐ + 1)) ยท (1 /
(!โ๐)))) |
157 | 138, 56, 155 | divcan3d 11943 |
. . . . . . . . . . 11
โข (๐ โ (((!โ๐) ยท (๐ + 1)) / (!โ๐)) = (๐ + 1)) |
158 | 153, 156,
157 | 3eqtr3rd 2786 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) = ((!โ(๐ + 1)) ยท (1 / (!โ๐)))) |
159 | 158 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) ยท (๐ + 1)) = (((!โ(๐ + 1)) ยท (1 / (!โ๐))) ยท (๐ + 1))) |
160 | 104 | recnd 11190 |
. . . . . . . . . 10
โข (๐ โ (1 / (!โ๐)) โ
โ) |
161 | 154, 160,
138 | mul32d 11372 |
. . . . . . . . 9
โข (๐ โ (((!โ(๐ + 1)) ยท (1 /
(!โ๐))) ยท
(๐ + 1)) =
(((!โ(๐ + 1))
ยท (๐ + 1)) ยท
(1 / (!โ๐)))) |
162 | 159, 161 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((๐ + 1) ยท (๐ + 1)) = (((!โ(๐ + 1)) ยท (๐ + 1)) ยท (1 / (!โ๐)))) |
163 | 150, 162 | breqtrd 5136 |
. . . . . . 7
โข (๐ โ ((๐ + 1) + 1) < (((!โ(๐ + 1)) ยท (๐ + 1)) ยท (1 /
(!โ๐)))) |
164 | 102 | nnred 12175 |
. . . . . . . 8
โข (๐ โ ((!โ(๐ + 1)) ยท (๐ + 1)) โ
โ) |
165 | 102 | nngt0d 12209 |
. . . . . . . 8
โข (๐ โ 0 < ((!โ(๐ + 1)) ยท (๐ + 1))) |
166 | | ltdivmul 12037 |
. . . . . . . 8
โข ((((๐ + 1) + 1) โ โ โง
(1 / (!โ๐)) โ
โ โง (((!โ(๐
+ 1)) ยท (๐ + 1))
โ โ โง 0 < ((!โ(๐ + 1)) ยท (๐ + 1)))) โ ((((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1))) < (1 / (!โ๐)) โ ((๐ + 1) + 1) < (((!โ(๐ + 1)) ยท (๐ + 1)) ยท (1 /
(!โ๐))))) |
167 | 100, 104,
164, 165, 166 | syl112anc 1375 |
. . . . . . 7
โข (๐ โ ((((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1))) < (1 / (!โ๐)) โ ((๐ + 1) + 1) < (((!โ(๐ + 1)) ยท (๐ + 1)) ยท (1 /
(!โ๐))))) |
168 | 163, 167 | mpbird 257 |
. . . . . 6
โข (๐ โ (((๐ + 1) + 1) / ((!โ(๐ + 1)) ยท (๐ + 1))) < (1 / (!โ๐))) |
169 | 38, 103, 104, 127, 168 | lelttrd 11320 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) < (1 / (!โ๐))) |
170 | 38, 131, 96 | ltmuldiv2d 13012 |
. . . . 5
โข (๐ โ (((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) < 1 โ ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐) < (1 / (!โ๐)))) |
171 | 169, 170 | mpbird 257 |
. . . 4
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) < 1) |
172 | | 0p1e1 12282 |
. . . 4
โข (0 + 1) =
1 |
173 | 171, 172 | breqtrrdi 5152 |
. . 3
โข (๐ โ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) < (0 + 1)) |
174 | | btwnnz 12586 |
. . 3
โข ((0
โ โค โง 0 < ((!โ๐) ยท ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐)) โง ((!โ๐) ยท ฮฃ๐ โ (โคโฅโ(๐ + 1))(๐นโ๐)) < (0 + 1)) โ ยฌ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) โ โค) |
175 | 95, 98, 173, 174 | syl3anc 1372 |
. 2
โข (๐ โ ยฌ ((!โ๐) ยท ฮฃ๐ โ
(โคโฅโ(๐ + 1))(๐นโ๐)) โ โค) |
176 | 94, 175 | pm2.65i 193 |
1
โข ยฌ
๐ |