Step | Hyp | Ref
| Expression |
1 | | 0nn0 9191 |
. . . . . . . . 9
โข 0 โ
โ0 |
2 | | nn0uz 9562 |
. . . . . . . . 9
โข
โ0 = (โคโฅโ0) |
3 | 1, 2 | eleqtri 2252 |
. . . . . . . 8
โข 0 โ
(โคโฅโ0) |
4 | 3 | a1i 9 |
. . . . . . 7
โข (โค
โ 0 โ (โคโฅโ0)) |
5 | | elnn0uz 9565 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ0)) |
6 | 5 | biimpri 133 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ0) โ ๐ โ โ0) |
7 | | faccl 10715 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
8 | 7 | nnrecred 8966 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (1 / (!โ๐))
โ โ) |
9 | | fveq2 5516 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
10 | 9 | oveq2d 5891 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (1 / (!โ๐)) = (1 / (!โ๐))) |
11 | | erelem1.2 |
. . . . . . . . . . . 12
โข ๐บ = (๐ โ โ0 โฆ (1 /
(!โ๐))) |
12 | 10, 11 | fvmptg 5593 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง (1 / (!โ๐))
โ โ) โ (๐บโ๐) = (1 / (!โ๐))) |
13 | 8, 12 | mpdan 421 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐บโ๐) = (1 / (!โ๐))) |
14 | 13, 8 | eqeltrd 2254 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐บโ๐) โ
โ) |
15 | 6, 14 | syl 14 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ0) โ (๐บโ๐) โ โ) |
16 | 15 | adantl 277 |
. . . . . . 7
โข
((โค โง ๐
โ (โคโฅโ0)) โ (๐บโ๐) โ โ) |
17 | | readdcl 7937 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ฆ โ โ) โ (๐ + ๐ฆ) โ โ) |
18 | 17 | adantl 277 |
. . . . . . 7
โข
((โค โง (๐
โ โ โง ๐ฆ
โ โ)) โ (๐
+ ๐ฆ) โ
โ) |
19 | 4, 16, 18 | seq3p1 10462 |
. . . . . 6
โข (โค
โ (seq0( + , ๐บ)โ(0 + 1)) = ((seq0( + , ๐บ)โ0) + (๐บโ(0 + 1)))) |
20 | | 0zd 9265 |
. . . . . . . . 9
โข (โค
โ 0 โ โค) |
21 | 20, 16, 18 | seq3-1 10460 |
. . . . . . . 8
โข (โค
โ (seq0( + , ๐บ)โ0) = (๐บโ0)) |
22 | | fveq2 5516 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (!โ๐) =
(!โ0)) |
23 | | fac0 10708 |
. . . . . . . . . . . . 13
โข
(!โ0) = 1 |
24 | 22, 23 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (!โ๐) = 1) |
25 | 24 | oveq2d 5891 |
. . . . . . . . . . 11
โข (๐ = 0 โ (1 / (!โ๐)) = (1 / 1)) |
26 | | ax-1cn 7904 |
. . . . . . . . . . . 12
โข 1 โ
โ |
27 | 26 | div1i 8697 |
. . . . . . . . . . 11
โข (1 / 1) =
1 |
28 | 25, 27 | eqtrdi 2226 |
. . . . . . . . . 10
โข (๐ = 0 โ (1 / (!โ๐)) = 1) |
29 | | 1ex 7952 |
. . . . . . . . . 10
โข 1 โ
V |
30 | 28, 11, 29 | fvmpt 5594 |
. . . . . . . . 9
โข (0 โ
โ0 โ (๐บโ0) = 1) |
31 | 1, 30 | mp1i 10 |
. . . . . . . 8
โข (โค
โ (๐บโ0) =
1) |
32 | 21, 31 | eqtrd 2210 |
. . . . . . 7
โข (โค
โ (seq0( + , ๐บ)โ0) = 1) |
33 | | 1e0p1 9425 |
. . . . . . . . 9
โข 1 = (0 +
1) |
34 | 33 | fveq2i 5519 |
. . . . . . . 8
โข (๐บโ1) = (๐บโ(0 + 1)) |
35 | | 1nn0 9192 |
. . . . . . . . 9
โข 1 โ
โ0 |
36 | | fveq2 5516 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ (!โ๐) =
(!โ1)) |
37 | | fac1 10709 |
. . . . . . . . . . . . 13
โข
(!โ1) = 1 |
38 | 36, 37 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (!โ๐) = 1) |
39 | 38 | oveq2d 5891 |
. . . . . . . . . . 11
โข (๐ = 1 โ (1 / (!โ๐)) = (1 / 1)) |
40 | 39, 27 | eqtrdi 2226 |
. . . . . . . . . 10
โข (๐ = 1 โ (1 / (!โ๐)) = 1) |
41 | 40, 11, 29 | fvmpt 5594 |
. . . . . . . . 9
โข (1 โ
โ0 โ (๐บโ1) = 1) |
42 | 35, 41 | mp1i 10 |
. . . . . . . 8
โข (โค
โ (๐บโ1) =
1) |
43 | 34, 42 | eqtr3id 2224 |
. . . . . . 7
โข (โค
โ (๐บโ(0 + 1)) =
1) |
44 | 32, 43 | oveq12d 5893 |
. . . . . 6
โข (โค
โ ((seq0( + , ๐บ)โ0) + (๐บโ(0 + 1))) = (1 + 1)) |
45 | 19, 44 | eqtrd 2210 |
. . . . 5
โข (โค
โ (seq0( + , ๐บ)โ(0 + 1)) = (1 + 1)) |
46 | 33 | fveq2i 5519 |
. . . . 5
โข (seq0( +
, ๐บ)โ1) = (seq0( + ,
๐บ)โ(0 +
1)) |
47 | | df-2 8978 |
. . . . 5
โข 2 = (1 +
1) |
48 | 45, 46, 47 | 3eqtr4g 2235 |
. . . 4
โข (โค
โ (seq0( + , ๐บ)โ1) = 2) |
49 | 35 | a1i 9 |
. . . . 5
โข (โค
โ 1 โ โ0) |
50 | | nn0z 9273 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โค) |
51 | | 1exp 10549 |
. . . . . . . . . . . 12
โข (๐ โ โค โ
(1โ๐) =
1) |
52 | 50, 51 | syl 14 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (1โ๐) =
1) |
53 | 52 | oveq1d 5890 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((1โ๐) /
(!โ๐)) = (1 /
(!โ๐))) |
54 | 53 | mpteq2ia 4090 |
. . . . . . . . 9
โข (๐ โ โ0
โฆ ((1โ๐) /
(!โ๐))) = (๐ โ โ0
โฆ (1 / (!โ๐))) |
55 | 11, 54 | eqtr4i 2201 |
. . . . . . . 8
โข ๐บ = (๐ โ โ0 โฆ
((1โ๐) /
(!โ๐))) |
56 | 55 | efcvg 11674 |
. . . . . . 7
โข (1 โ
โ โ seq0( + , ๐บ)
โ (expโ1)) |
57 | 26, 56 | mp1i 10 |
. . . . . 6
โข (โค
โ seq0( + , ๐บ) โ
(expโ1)) |
58 | | df-e 11657 |
. . . . . 6
โข e =
(expโ1) |
59 | 57, 58 | breqtrrdi 4046 |
. . . . 5
โข (โค
โ seq0( + , ๐บ) โ
e) |
60 | 13 | adantl 277 |
. . . . . 6
โข
((โค โง ๐
โ โ0) โ (๐บโ๐) = (1 / (!โ๐))) |
61 | 7 | adantl 277 |
. . . . . . 7
โข
((โค โง ๐
โ โ0) โ (!โ๐) โ โ) |
62 | 61 | nnrecred 8966 |
. . . . . 6
โข
((โค โง ๐
โ โ0) โ (1 / (!โ๐)) โ โ) |
63 | 60, 62 | eqeltrd 2254 |
. . . . 5
โข
((โค โง ๐
โ โ0) โ (๐บโ๐) โ โ) |
64 | 61 | nnred 8932 |
. . . . . . 7
โข
((โค โง ๐
โ โ0) โ (!โ๐) โ โ) |
65 | 61 | nngt0d 8963 |
. . . . . . 7
โข
((โค โง ๐
โ โ0) โ 0 < (!โ๐)) |
66 | | 1re 7956 |
. . . . . . . 8
โข 1 โ
โ |
67 | | 0le1 8438 |
. . . . . . . 8
โข 0 โค
1 |
68 | | divge0 8830 |
. . . . . . . 8
โข (((1
โ โ โง 0 โค 1) โง ((!โ๐) โ โ โง 0 < (!โ๐))) โ 0 โค (1 /
(!โ๐))) |
69 | 66, 67, 68 | mpanl12 436 |
. . . . . . 7
โข
(((!โ๐) โ
โ โง 0 < (!โ๐)) โ 0 โค (1 / (!โ๐))) |
70 | 64, 65, 69 | syl2anc 411 |
. . . . . 6
โข
((โค โง ๐
โ โ0) โ 0 โค (1 / (!โ๐))) |
71 | 70, 60 | breqtrrd 4032 |
. . . . 5
โข
((โค โง ๐
โ โ0) โ 0 โค (๐บโ๐)) |
72 | 2, 49, 59, 63, 71 | climserle 11353 |
. . . 4
โข (โค
โ (seq0( + , ๐บ)โ1) โค e) |
73 | 48, 72 | eqbrtrrd 4028 |
. . 3
โข (โค
โ 2 โค e) |
74 | 73 | mptru 1362 |
. 2
โข 2 โค
e |
75 | | nnuz 9563 |
. . . . . 6
โข โ =
(โคโฅโ1) |
76 | | 1zzd 9280 |
. . . . . 6
โข (โค
โ 1 โ โค) |
77 | 1 | a1i 9 |
. . . . . . . 8
โข (โค
โ 0 โ โ0) |
78 | 63 | recnd 7986 |
. . . . . . . 8
โข
((โค โง ๐
โ โ0) โ (๐บโ๐) โ โ) |
79 | 2, 77, 78, 59 | clim2ser 11345 |
. . . . . . 7
โข (โค
โ seq(0 + 1)( + , ๐บ)
โ (e โ (seq0( + , ๐บ)โ0))) |
80 | | 0p1e1 9033 |
. . . . . . . 8
โข (0 + 1) =
1 |
81 | | seqeq1 10448 |
. . . . . . . 8
โข ((0 + 1)
= 1 โ seq(0 + 1)( + , ๐บ) = seq1( + , ๐บ)) |
82 | 80, 81 | ax-mp 5 |
. . . . . . 7
โข seq(0 +
1)( + , ๐บ) = seq1( + ,
๐บ) |
83 | 32 | mptru 1362 |
. . . . . . . 8
โข (seq0( +
, ๐บ)โ0) =
1 |
84 | 83 | oveq2i 5886 |
. . . . . . 7
โข (e
โ (seq0( + , ๐บ)โ0)) = (e โ 1) |
85 | 79, 82, 84 | 3brtr3g 4037 |
. . . . . 6
โข (โค
โ seq1( + , ๐บ) โ
(e โ 1)) |
86 | | 2cnd 8992 |
. . . . . . . 8
โข (โค
โ 2 โ โ) |
87 | | halfre 9132 |
. . . . . . . . . . . . . . 15
โข (1 / 2)
โ โ |
88 | 87 | a1i 9 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (1 / 2) โ โ) |
89 | | id 19 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ ๐ โ
โ0) |
90 | 88, 89 | reexpcld 10671 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ((1 / 2)โ๐)
โ โ) |
91 | | oveq2 5883 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((1 / 2)โ๐) = ((1 / 2)โ๐)) |
92 | | eqid 2177 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โฆ ((1 / 2)โ๐)) =
(๐ โ
โ0 โฆ ((1 / 2)โ๐)) |
93 | 91, 92 | fvmptg 5593 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ((1 / 2)โ๐)
โ โ) โ ((๐
โ โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
94 | 90, 93 | mpdan 421 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
95 | 94 | adantl 277 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) = ((1 / 2)โ๐)) |
96 | | simpr 110 |
. . . . . . . . . . . . 13
โข
((โค โง ๐
โ โ0) โ ๐ โ โ0) |
97 | | reexpcl 10537 |
. . . . . . . . . . . . 13
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
98 | 87, 96, 97 | sylancr 414 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
99 | 98 | recnd 7986 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
100 | 95, 99 | eqeltrd 2254 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) โ
โ) |
101 | | 1lt2 9088 |
. . . . . . . . . . . . . 14
โข 1 <
2 |
102 | | 2re 8989 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
103 | | 0le2 9009 |
. . . . . . . . . . . . . . 15
โข 0 โค
2 |
104 | | absid 11080 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ โง 0 โค 2) โ (absโ2) = 2) |
105 | 102, 103,
104 | mp2an 426 |
. . . . . . . . . . . . . 14
โข
(absโ2) = 2 |
106 | 101, 105 | breqtrri 4031 |
. . . . . . . . . . . . 13
โข 1 <
(absโ2) |
107 | 106 | a1i 9 |
. . . . . . . . . . . 12
โข (โค
โ 1 < (absโ2)) |
108 | 86, 107, 95 | georeclim 11521 |
. . . . . . . . . . 11
โข (โค
โ seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) โ (2 / (2 โ
1))) |
109 | | 2m1e1 9037 |
. . . . . . . . . . . . 13
โข (2
โ 1) = 1 |
110 | 109 | oveq2i 5886 |
. . . . . . . . . . . 12
โข (2 / (2
โ 1)) = (2 / 1) |
111 | | 2cn 8990 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
112 | 111 | div1i 8697 |
. . . . . . . . . . . 12
โข (2 / 1) =
2 |
113 | 110, 112 | eqtri 2198 |
. . . . . . . . . . 11
โข (2 / (2
โ 1)) = 2 |
114 | 108, 113 | breqtrdi 4045 |
. . . . . . . . . 10
โข (โค
โ seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) โ 2) |
115 | 2, 77, 100, 114 | clim2ser 11345 |
. . . . . . . . 9
โข (โค
โ seq(0 + 1)( + , (๐
โ โ0 โฆ ((1 / 2)โ๐))) โ (2 โ (seq0( + , (๐ โ โ0
โฆ ((1 / 2)โ๐)))โ0))) |
116 | | seqeq1 10448 |
. . . . . . . . . 10
โข ((0 + 1)
= 1 โ seq(0 + 1)( + , (๐ โ โ0 โฆ ((1 /
2)โ๐))) = seq1( + ,
(๐ โ
โ0 โฆ ((1 / 2)โ๐)))) |
117 | 80, 116 | ax-mp 5 |
. . . . . . . . 9
โข seq(0 +
1)( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) = seq1( + , (๐ โ โ0 โฆ ((1 /
2)โ๐))) |
118 | 6 | adantl 277 |
. . . . . . . . . . . . . . 15
โข
((โค โง ๐
โ (โคโฅโ0)) โ ๐ โ โ0) |
119 | 94, 90 | eqeltrd 2254 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((1 / 2)โ๐))โ๐) โ โ) |
120 | 118, 119 | syl 14 |
. . . . . . . . . . . . . 14
โข
((โค โง ๐
โ (โคโฅโ0)) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) โ
โ) |
121 | 20, 120, 18 | seq3-1 10460 |
. . . . . . . . . . . . 13
โข (โค
โ (seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐)))โ0) = ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ0)) |
122 | | halfcn 9133 |
. . . . . . . . . . . . . . . . 17
โข (1 / 2)
โ โ |
123 | | exp0 10524 |
. . . . . . . . . . . . . . . . 17
โข ((1 / 2)
โ โ โ ((1 / 2)โ0) = 1) |
124 | 122, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข ((1 /
2)โ0) = 1 |
125 | 124, 35 | eqeltri 2250 |
. . . . . . . . . . . . . . 15
โข ((1 /
2)โ0) โ โ0 |
126 | | oveq2 5883 |
. . . . . . . . . . . . . . . 16
โข (๐ = 0 โ ((1 / 2)โ๐) = ((1 /
2)โ0)) |
127 | 126, 92 | fvmptg 5593 |
. . . . . . . . . . . . . . 15
โข ((0
โ โ0 โง ((1 / 2)โ0) โ โ0)
โ ((๐ โ
โ0 โฆ ((1 / 2)โ๐))โ0) = ((1 /
2)โ0)) |
128 | 1, 125, 127 | mp2an 426 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ0) = ((1 /
2)โ0) |
129 | 128, 124 | eqtri 2198 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ0) = 1 |
130 | 121, 129 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข (โค
โ (seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐)))โ0) = 1) |
131 | 130 | mptru 1362 |
. . . . . . . . . . 11
โข (seq0( +
, (๐ โ
โ0 โฆ ((1 / 2)โ๐)))โ0) = 1 |
132 | 131 | oveq2i 5886 |
. . . . . . . . . 10
โข (2
โ (seq0( + , (๐
โ โ0 โฆ ((1 / 2)โ๐)))โ0)) = (2 โ
1) |
133 | 132, 109 | eqtri 2198 |
. . . . . . . . 9
โข (2
โ (seq0( + , (๐
โ โ0 โฆ ((1 / 2)โ๐)))โ0)) = 1 |
134 | 115, 117,
133 | 3brtr3g 4037 |
. . . . . . . 8
โข (โค
โ seq1( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) โ 1) |
135 | | nnnn0 9183 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
136 | 135, 100 | sylan2 286 |
. . . . . . . 8
โข
((โค โง ๐
โ โ) โ ((๐
โ โ0 โฆ ((1 / 2)โ๐))โ๐) โ โ) |
137 | 102 | a1i 9 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 2 โ
โ) |
138 | 135, 90 | syl 14 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1 /
2)โ๐) โ
โ) |
139 | 137, 138 | remulcld 7988 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ((1 / 2)โ๐))
โ โ) |
140 | 91 | oveq2d 5891 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (2 ยท ((1 / 2)โ๐)) = (2 ยท ((1 /
2)โ๐))) |
141 | | erelem1.1 |
. . . . . . . . . . . 12
โข ๐น = (๐ โ โ โฆ (2 ยท ((1 /
2)โ๐))) |
142 | 140, 141 | fvmptg 5593 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (2
ยท ((1 / 2)โ๐))
โ โ) โ (๐นโ๐) = (2 ยท ((1 / 2)โ๐))) |
143 | 139, 142 | mpdan 421 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐นโ๐) = (2 ยท ((1 / 2)โ๐))) |
144 | 143 | adantl 277 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ) โ (๐นโ๐) = (2 ยท ((1 / 2)โ๐))) |
145 | 135, 95 | sylan2 286 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ) โ ((๐
โ โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
146 | 145 | oveq2d 5891 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ) โ (2 ยท ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐)) = (2 ยท ((1 /
2)โ๐))) |
147 | 144, 146 | eqtr4d 2213 |
. . . . . . . 8
โข
((โค โง ๐
โ โ) โ (๐นโ๐) = (2 ยท ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐))) |
148 | 75, 76, 86, 134, 136, 147 | isermulc2 11348 |
. . . . . . 7
โข (โค
โ seq1( + , ๐น) โ
(2 ยท 1)) |
149 | | 2t1e2 9072 |
. . . . . . 7
โข (2
ยท 1) = 2 |
150 | 148, 149 | breqtrdi 4045 |
. . . . . 6
โข (โค
โ seq1( + , ๐น) โ
2) |
151 | 135, 63 | sylan2 286 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (๐บโ๐) โ โ) |
152 | | remulcl 7939 |
. . . . . . . . 9
โข ((2
โ โ โง ((1 / 2)โ๐) โ โ) โ (2 ยท ((1 /
2)โ๐)) โ
โ) |
153 | 102, 98, 152 | sylancr 414 |
. . . . . . . 8
โข
((โค โง ๐
โ โ0) โ (2 ยท ((1 / 2)โ๐)) โ โ) |
154 | 135, 153 | sylan2 286 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (2 ยท ((1 / 2)โ๐)) โ โ) |
155 | 144, 154 | eqeltrd 2254 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (๐นโ๐) โ โ) |
156 | | faclbnd2 10722 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ((2โ๐) / 2)
โค (!โ๐)) |
157 | 156 | adantl 277 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ ((2โ๐) / 2) โค (!โ๐)) |
158 | | 2nn 9080 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
159 | | nnexpcl 10533 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
160 | 158, 96, 159 | sylancr 414 |
. . . . . . . . . . . . 13
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ โ) |
161 | 160 | nnrpd 9694 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ
โ+) |
162 | 161 | rphalfcld 9709 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((2โ๐) / 2) โ
โ+) |
163 | 61 | nnrpd 9694 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ (!โ๐) โ
โ+) |
164 | 162, 163 | lerecd 9716 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (((2โ๐) / 2) โค (!โ๐) โ (1 / (!โ๐)) โค (1 / ((2โ๐) / 2)))) |
165 | 157, 164 | mpbid 147 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ0) โ (1 / (!โ๐)) โค (1 / ((2โ๐) / 2))) |
166 | | 2cnd 8992 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ 2 โ โ) |
167 | 160 | nncnd 8933 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ โ) |
168 | 160 | nnap0d 8965 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ (2โ๐) # 0) |
169 | 166, 167,
168 | divrecapd 8750 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (2 / (2โ๐)) = (2 ยท (1 / (2โ๐)))) |
170 | | 2ap0 9012 |
. . . . . . . . . . . 12
โข 2 #
0 |
171 | 170 | a1i 9 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ 2 # 0) |
172 | 167, 166,
168, 171 | recdivapd 8764 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (1 / ((2โ๐) / 2)) = (2 / (2โ๐))) |
173 | | nn0z 9273 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ๐ โ
โค) |
174 | 173 | adantl 277 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ ๐ โ โค) |
175 | 166, 171,
174 | exprecapd 10662 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((1 / 2)โ๐) = (1 / (2โ๐))) |
176 | 175 | oveq2d 5891 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (2 ยท ((1 / 2)โ๐)) = (2 ยท (1 / (2โ๐)))) |
177 | 169, 172,
176 | 3eqtr4rd 2221 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ0) โ (2 ยท ((1 / 2)โ๐)) = (1 / ((2โ๐) / 2))) |
178 | 165, 177 | breqtrrd 4032 |
. . . . . . . 8
โข
((โค โง ๐
โ โ0) โ (1 / (!โ๐)) โค (2 ยท ((1 / 2)โ๐))) |
179 | 135, 178 | sylan2 286 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (1 / (!โ๐)) โค (2 ยท ((1 / 2)โ๐))) |
180 | 135, 60 | sylan2 286 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (๐บโ๐) = (1 / (!โ๐))) |
181 | 179, 180,
144 | 3brtr4d 4036 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (๐บโ๐) โค (๐นโ๐)) |
182 | 75, 76, 85, 150, 151, 155, 181 | iserle 11350 |
. . . . 5
โข (โค
โ (e โ 1) โค 2) |
183 | 182 | mptru 1362 |
. . . 4
โข (e
โ 1) โค 2 |
184 | | ere 11678 |
. . . . 5
โข e โ
โ |
185 | 184, 66, 102 | lesubaddi 8463 |
. . . 4
โข ((e
โ 1) โค 2 โ e โค (2 + 1)) |
186 | 183, 185 | mpbi 145 |
. . 3
โข e โค (2
+ 1) |
187 | | df-3 8979 |
. . 3
โข 3 = (2 +
1) |
188 | 186, 187 | breqtrri 4031 |
. 2
โข e โค
3 |
189 | 74, 188 | pm3.2i 272 |
1
โข (2 โค e
โง e โค 3) |