Step | Hyp | Ref
| Expression |
1 | | nn0uz 12810 |
. . . . . 6
โข
โ0 = (โคโฅโ0) |
2 | | 0nn0 12433 |
. . . . . . 7
โข 0 โ
โ0 |
3 | 2 | a1i 11 |
. . . . . 6
โข (โค
โ 0 โ โ0) |
4 | | 1e0p1 12665 |
. . . . . 6
โข 1 = (0 +
1) |
5 | | 0z 12515 |
. . . . . . 7
โข 0 โ
โค |
6 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (!โ๐) =
(!โ0)) |
7 | | fac0 14182 |
. . . . . . . . . . . 12
โข
(!โ0) = 1 |
8 | 6, 7 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ = 0 โ (!โ๐) = 1) |
9 | 8 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = 0 โ (1 / (!โ๐)) = (1 / 1)) |
10 | | ax-1cn 11114 |
. . . . . . . . . . 11
โข 1 โ
โ |
11 | 10 | div1i 11888 |
. . . . . . . . . 10
โข (1 / 1) =
1 |
12 | 9, 11 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ = 0 โ (1 / (!โ๐)) = 1) |
13 | | erelem1.2 |
. . . . . . . . 9
โข ๐บ = (๐ โ โ0 โฆ (1 /
(!โ๐))) |
14 | | 1ex 11156 |
. . . . . . . . 9
โข 1 โ
V |
15 | 12, 13, 14 | fvmpt 6949 |
. . . . . . . 8
โข (0 โ
โ0 โ (๐บโ0) = 1) |
16 | 2, 15 | mp1i 13 |
. . . . . . 7
โข (โค
โ (๐บโ0) =
1) |
17 | 5, 16 | seq1i 13926 |
. . . . . 6
โข (โค
โ (seq0( + , ๐บ)โ0) = 1) |
18 | | 1nn0 12434 |
. . . . . . 7
โข 1 โ
โ0 |
19 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = 1 โ (!โ๐) =
(!โ1)) |
20 | | fac1 14183 |
. . . . . . . . . . 11
โข
(!โ1) = 1 |
21 | 19, 20 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ = 1 โ (!โ๐) = 1) |
22 | 21 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = 1 โ (1 / (!โ๐)) = (1 / 1)) |
23 | 22, 11 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ = 1 โ (1 / (!โ๐)) = 1) |
24 | 23, 13, 14 | fvmpt 6949 |
. . . . . . 7
โข (1 โ
โ0 โ (๐บโ1) = 1) |
25 | 18, 24 | mp1i 13 |
. . . . . 6
โข (โค
โ (๐บโ1) =
1) |
26 | 1, 3, 4, 17, 25 | seqp1d 13929 |
. . . . 5
โข (โค
โ (seq0( + , ๐บ)โ1) = (1 + 1)) |
27 | | df-2 12221 |
. . . . 5
โข 2 = (1 +
1) |
28 | 26, 27 | eqtr4di 2791 |
. . . 4
โข (โค
โ (seq0( + , ๐บ)โ1) = 2) |
29 | 18 | a1i 11 |
. . . . 5
โข (โค
โ 1 โ โ0) |
30 | | nn0z 12529 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โค) |
31 | | 1exp 14003 |
. . . . . . . . . . . 12
โข (๐ โ โค โ
(1โ๐) =
1) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (1โ๐) =
1) |
33 | 32 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((1โ๐) /
(!โ๐)) = (1 /
(!โ๐))) |
34 | 33 | mpteq2ia 5209 |
. . . . . . . . 9
โข (๐ โ โ0
โฆ ((1โ๐) /
(!โ๐))) = (๐ โ โ0
โฆ (1 / (!โ๐))) |
35 | 13, 34 | eqtr4i 2764 |
. . . . . . . 8
โข ๐บ = (๐ โ โ0 โฆ
((1โ๐) /
(!โ๐))) |
36 | 35 | efcvg 15972 |
. . . . . . 7
โข (1 โ
โ โ seq0( + , ๐บ)
โ (expโ1)) |
37 | 10, 36 | mp1i 13 |
. . . . . 6
โข (โค
โ seq0( + , ๐บ) โ
(expโ1)) |
38 | | df-e 15956 |
. . . . . 6
โข e =
(expโ1) |
39 | 37, 38 | breqtrrdi 5148 |
. . . . 5
โข (โค
โ seq0( + , ๐บ) โ
e) |
40 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
41 | 40 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ (1 / (!โ๐)) = (1 / (!โ๐))) |
42 | | ovex 7391 |
. . . . . . . 8
โข (1 /
(!โ๐)) โ
V |
43 | 41, 13, 42 | fvmpt 6949 |
. . . . . . 7
โข (๐ โ โ0
โ (๐บโ๐) = (1 / (!โ๐))) |
44 | 43 | adantl 483 |
. . . . . 6
โข
((โค โง ๐
โ โ0) โ (๐บโ๐) = (1 / (!โ๐))) |
45 | | faccl 14189 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
46 | 45 | adantl 483 |
. . . . . . 7
โข
((โค โง ๐
โ โ0) โ (!โ๐) โ โ) |
47 | 46 | nnrecred 12209 |
. . . . . 6
โข
((โค โง ๐
โ โ0) โ (1 / (!โ๐)) โ โ) |
48 | 44, 47 | eqeltrd 2834 |
. . . . 5
โข
((โค โง ๐
โ โ0) โ (๐บโ๐) โ โ) |
49 | 46 | nnred 12173 |
. . . . . . 7
โข
((โค โง ๐
โ โ0) โ (!โ๐) โ โ) |
50 | 46 | nngt0d 12207 |
. . . . . . 7
โข
((โค โง ๐
โ โ0) โ 0 < (!โ๐)) |
51 | | 1re 11160 |
. . . . . . . 8
โข 1 โ
โ |
52 | | 0le1 11683 |
. . . . . . . 8
โข 0 โค
1 |
53 | | divge0 12029 |
. . . . . . . 8
โข (((1
โ โ โง 0 โค 1) โง ((!โ๐) โ โ โง 0 < (!โ๐))) โ 0 โค (1 /
(!โ๐))) |
54 | 51, 52, 53 | mpanl12 701 |
. . . . . . 7
โข
(((!โ๐) โ
โ โง 0 < (!โ๐)) โ 0 โค (1 / (!โ๐))) |
55 | 49, 50, 54 | syl2anc 585 |
. . . . . 6
โข
((โค โง ๐
โ โ0) โ 0 โค (1 / (!โ๐))) |
56 | 55, 44 | breqtrrd 5134 |
. . . . 5
โข
((โค โง ๐
โ โ0) โ 0 โค (๐บโ๐)) |
57 | 1, 29, 39, 48, 56 | climserle 15553 |
. . . 4
โข (โค
โ (seq0( + , ๐บ)โ1) โค e) |
58 | 28, 57 | eqbrtrrd 5130 |
. . 3
โข (โค
โ 2 โค e) |
59 | 58 | mptru 1549 |
. 2
โข 2 โค
e |
60 | | nnuz 12811 |
. . . . . 6
โข โ =
(โคโฅโ1) |
61 | | 1zzd 12539 |
. . . . . 6
โข (โค
โ 1 โ โค) |
62 | 48 | recnd 11188 |
. . . . . . . 8
โข
((โค โง ๐
โ โ0) โ (๐บโ๐) โ โ) |
63 | 1, 3, 62, 39 | clim2ser 15545 |
. . . . . . 7
โข (โค
โ seq(0 + 1)( + , ๐บ)
โ (e โ (seq0( + , ๐บ)โ0))) |
64 | | 0p1e1 12280 |
. . . . . . . 8
โข (0 + 1) =
1 |
65 | | seqeq1 13915 |
. . . . . . . 8
โข ((0 + 1)
= 1 โ seq(0 + 1)( + , ๐บ) = seq1( + , ๐บ)) |
66 | 64, 65 | ax-mp 5 |
. . . . . . 7
โข seq(0 +
1)( + , ๐บ) = seq1( + ,
๐บ) |
67 | 17 | mptru 1549 |
. . . . . . . 8
โข (seq0( +
, ๐บ)โ0) =
1 |
68 | 67 | oveq2i 7369 |
. . . . . . 7
โข (e
โ (seq0( + , ๐บ)โ0)) = (e โ 1) |
69 | 63, 66, 68 | 3brtr3g 5139 |
. . . . . 6
โข (โค
โ seq1( + , ๐บ) โ
(e โ 1)) |
70 | | 2cnd 12236 |
. . . . . . . 8
โข (โค
โ 2 โ โ) |
71 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((1 / 2)โ๐) = ((1 / 2)โ๐)) |
72 | | eqid 2733 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โฆ ((1 / 2)โ๐)) =
(๐ โ
โ0 โฆ ((1 / 2)โ๐)) |
73 | | ovex 7391 |
. . . . . . . . . . . . 13
โข ((1 /
2)โ๐) โ
V |
74 | 71, 72, 73 | fvmpt 6949 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
75 | 74 | adantl 483 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) = ((1 / 2)โ๐)) |
76 | | halfre 12372 |
. . . . . . . . . . . . 13
โข (1 / 2)
โ โ |
77 | | simpr 486 |
. . . . . . . . . . . . 13
โข
((โค โง ๐
โ โ0) โ ๐ โ โ0) |
78 | | reexpcl 13990 |
. . . . . . . . . . . . 13
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
79 | 76, 77, 78 | sylancr 588 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
80 | 79 | recnd 11188 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
81 | 75, 80 | eqeltrd 2834 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) โ
โ) |
82 | | 1lt2 12329 |
. . . . . . . . . . . . . 14
โข 1 <
2 |
83 | | 2re 12232 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
84 | | 0le2 12260 |
. . . . . . . . . . . . . . 15
โข 0 โค
2 |
85 | | absid 15187 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ โง 0 โค 2) โ (absโ2) = 2) |
86 | 83, 84, 85 | mp2an 691 |
. . . . . . . . . . . . . 14
โข
(absโ2) = 2 |
87 | 82, 86 | breqtrri 5133 |
. . . . . . . . . . . . 13
โข 1 <
(absโ2) |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
โข (โค
โ 1 < (absโ2)) |
89 | 70, 88, 75 | georeclim 15762 |
. . . . . . . . . . 11
โข (โค
โ seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) โ (2 / (2 โ
1))) |
90 | | 2m1e1 12284 |
. . . . . . . . . . . . 13
โข (2
โ 1) = 1 |
91 | 90 | oveq2i 7369 |
. . . . . . . . . . . 12
โข (2 / (2
โ 1)) = (2 / 1) |
92 | | 2cn 12233 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
93 | 92 | div1i 11888 |
. . . . . . . . . . . 12
โข (2 / 1) =
2 |
94 | 91, 93 | eqtri 2761 |
. . . . . . . . . . 11
โข (2 / (2
โ 1)) = 2 |
95 | 89, 94 | breqtrdi 5147 |
. . . . . . . . . 10
โข (โค
โ seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) โ 2) |
96 | 1, 3, 81, 95 | clim2ser 15545 |
. . . . . . . . 9
โข (โค
โ seq(0 + 1)( + , (๐
โ โ0 โฆ ((1 / 2)โ๐))) โ (2 โ (seq0( + , (๐ โ โ0
โฆ ((1 / 2)โ๐)))โ0))) |
97 | | seqeq1 13915 |
. . . . . . . . . 10
โข ((0 + 1)
= 1 โ seq(0 + 1)( + , (๐ โ โ0 โฆ ((1 /
2)โ๐))) = seq1( + ,
(๐ โ
โ0 โฆ ((1 / 2)โ๐)))) |
98 | 64, 97 | ax-mp 5 |
. . . . . . . . 9
โข seq(0 +
1)( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) = seq1( + , (๐ โ โ0 โฆ ((1 /
2)โ๐))) |
99 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 0 โ ((1 / 2)โ๐) = ((1 /
2)โ0)) |
100 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
โข ((1 /
2)โ0) โ V |
101 | 99, 72, 100 | fvmpt 6949 |
. . . . . . . . . . . . . . . 16
โข (0 โ
โ0 โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ0) = ((1
/ 2)โ0)) |
102 | 2, 101 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ0) = ((1 /
2)โ0) |
103 | | halfcn 12373 |
. . . . . . . . . . . . . . . 16
โข (1 / 2)
โ โ |
104 | | exp0 13977 |
. . . . . . . . . . . . . . . 16
โข ((1 / 2)
โ โ โ ((1 / 2)โ0) = 1) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข ((1 /
2)โ0) = 1 |
106 | 102, 105 | eqtri 2761 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ0) = 1 |
107 | 106 | a1i 11 |
. . . . . . . . . . . . 13
โข (โค
โ ((๐ โ
โ0 โฆ ((1 / 2)โ๐))โ0) = 1) |
108 | 5, 107 | seq1i 13926 |
. . . . . . . . . . . 12
โข (โค
โ (seq0( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐)))โ0) = 1) |
109 | 108 | mptru 1549 |
. . . . . . . . . . 11
โข (seq0( +
, (๐ โ
โ0 โฆ ((1 / 2)โ๐)))โ0) = 1 |
110 | 109 | oveq2i 7369 |
. . . . . . . . . 10
โข (2
โ (seq0( + , (๐
โ โ0 โฆ ((1 / 2)โ๐)))โ0)) = (2 โ
1) |
111 | 110, 90 | eqtri 2761 |
. . . . . . . . 9
โข (2
โ (seq0( + , (๐
โ โ0 โฆ ((1 / 2)โ๐)))โ0)) = 1 |
112 | 96, 98, 111 | 3brtr3g 5139 |
. . . . . . . 8
โข (โค
โ seq1( + , (๐ โ
โ0 โฆ ((1 / 2)โ๐))) โ 1) |
113 | | nnnn0 12425 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
114 | 113, 81 | sylan2 594 |
. . . . . . . 8
โข
((โค โง ๐
โ โ) โ ((๐
โ โ0 โฆ ((1 / 2)โ๐))โ๐) โ โ) |
115 | 71 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (2 ยท ((1 / 2)โ๐)) = (2 ยท ((1 /
2)โ๐))) |
116 | | erelem1.1 |
. . . . . . . . . . 11
โข ๐น = (๐ โ โ โฆ (2 ยท ((1 /
2)โ๐))) |
117 | | ovex 7391 |
. . . . . . . . . . 11
โข (2
ยท ((1 / 2)โ๐))
โ V |
118 | 115, 116,
117 | fvmpt 6949 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐นโ๐) = (2 ยท ((1 / 2)โ๐))) |
119 | 118 | adantl 483 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ) โ (๐นโ๐) = (2 ยท ((1 / 2)โ๐))) |
120 | 113, 75 | sylan2 594 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ) โ ((๐
โ โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
121 | 120 | oveq2d 7374 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ) โ (2 ยท ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐)) = (2 ยท ((1 /
2)โ๐))) |
122 | 119, 121 | eqtr4d 2776 |
. . . . . . . 8
โข
((โค โง ๐
โ โ) โ (๐นโ๐) = (2 ยท ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐))) |
123 | 60, 61, 70, 112, 114, 122 | isermulc2 15548 |
. . . . . . 7
โข (โค
โ seq1( + , ๐น) โ
(2 ยท 1)) |
124 | | 2t1e2 12321 |
. . . . . . 7
โข (2
ยท 1) = 2 |
125 | 123, 124 | breqtrdi 5147 |
. . . . . 6
โข (โค
โ seq1( + , ๐น) โ
2) |
126 | 113, 48 | sylan2 594 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (๐บโ๐) โ โ) |
127 | | remulcl 11141 |
. . . . . . . . 9
โข ((2
โ โ โง ((1 / 2)โ๐) โ โ) โ (2 ยท ((1 /
2)โ๐)) โ
โ) |
128 | 83, 79, 127 | sylancr 588 |
. . . . . . . 8
โข
((โค โง ๐
โ โ0) โ (2 ยท ((1 / 2)โ๐)) โ โ) |
129 | 113, 128 | sylan2 594 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (2 ยท ((1 / 2)โ๐)) โ โ) |
130 | 119, 129 | eqeltrd 2834 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (๐นโ๐) โ โ) |
131 | | faclbnd2 14197 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ((2โ๐) / 2)
โค (!โ๐)) |
132 | 131 | adantl 483 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ ((2โ๐) / 2) โค (!โ๐)) |
133 | | 2nn 12231 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
134 | | nnexpcl 13986 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
135 | 133, 77, 134 | sylancr 588 |
. . . . . . . . . . . . 13
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ โ) |
136 | 135 | nnrpd 12960 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ
โ+) |
137 | 136 | rphalfcld 12974 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((2โ๐) / 2) โ
โ+) |
138 | 46 | nnrpd 12960 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ (!โ๐) โ
โ+) |
139 | 137, 138 | lerecd 12981 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (((2โ๐) / 2) โค (!โ๐) โ (1 / (!โ๐)) โค (1 / ((2โ๐) / 2)))) |
140 | 132, 139 | mpbid 231 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ0) โ (1 / (!โ๐)) โค (1 / ((2โ๐) / 2))) |
141 | | 2cnd 12236 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ 2 โ โ) |
142 | 135 | nncnd 12174 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ โ) |
143 | 135 | nnne0d 12208 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ (2โ๐) โ 0) |
144 | 141, 142,
143 | divrecd 11939 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (2 / (2โ๐)) = (2 ยท (1 / (2โ๐)))) |
145 | | 2ne0 12262 |
. . . . . . . . . . . 12
โข 2 โ
0 |
146 | | recdiv 11866 |
. . . . . . . . . . . 12
โข
((((2โ๐) โ
โ โง (2โ๐)
โ 0) โง (2 โ โ โง 2 โ 0)) โ (1 / ((2โ๐) / 2)) = (2 / (2โ๐))) |
147 | 92, 145, 146 | mpanr12 704 |
. . . . . . . . . . 11
โข
(((2โ๐) โ
โ โง (2โ๐)
โ 0) โ (1 / ((2โ๐) / 2)) = (2 / (2โ๐))) |
148 | 142, 143,
147 | syl2anc 585 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (1 / ((2โ๐) / 2)) = (2 / (2โ๐))) |
149 | 145 | a1i 11 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ 2 โ 0) |
150 | | nn0z 12529 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ๐ โ
โค) |
151 | 150 | adantl 483 |
. . . . . . . . . . . 12
โข
((โค โง ๐
โ โ0) โ ๐ โ โค) |
152 | 141, 149,
151 | exprecd 14065 |
. . . . . . . . . . 11
โข
((โค โง ๐
โ โ0) โ ((1 / 2)โ๐) = (1 / (2โ๐))) |
153 | 152 | oveq2d 7374 |
. . . . . . . . . 10
โข
((โค โง ๐
โ โ0) โ (2 ยท ((1 / 2)โ๐)) = (2 ยท (1 / (2โ๐)))) |
154 | 144, 148,
153 | 3eqtr4rd 2784 |
. . . . . . . . 9
โข
((โค โง ๐
โ โ0) โ (2 ยท ((1 / 2)โ๐)) = (1 / ((2โ๐) / 2))) |
155 | 140, 154 | breqtrrd 5134 |
. . . . . . . 8
โข
((โค โง ๐
โ โ0) โ (1 / (!โ๐)) โค (2 ยท ((1 / 2)โ๐))) |
156 | 113, 155 | sylan2 594 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (1 / (!โ๐)) โค (2 ยท ((1 / 2)โ๐))) |
157 | 113, 44 | sylan2 594 |
. . . . . . 7
โข
((โค โง ๐
โ โ) โ (๐บโ๐) = (1 / (!โ๐))) |
158 | 156, 157,
119 | 3brtr4d 5138 |
. . . . . 6
โข
((โค โง ๐
โ โ) โ (๐บโ๐) โค (๐นโ๐)) |
159 | 60, 61, 69, 125, 126, 130, 158 | iserle 15550 |
. . . . 5
โข (โค
โ (e โ 1) โค 2) |
160 | 159 | mptru 1549 |
. . . 4
โข (e
โ 1) โค 2 |
161 | | ere 15976 |
. . . . 5
โข e โ
โ |
162 | 161, 51, 83 | lesubaddi 11718 |
. . . 4
โข ((e
โ 1) โค 2 โ e โค (2 + 1)) |
163 | 160, 162 | mpbi 229 |
. . 3
โข e โค (2
+ 1) |
164 | | df-3 12222 |
. . 3
โข 3 = (2 +
1) |
165 | 163, 164 | breqtrri 5133 |
. 2
โข e โค
3 |
166 | 59, 165 | pm3.2i 472 |
1
โข (2 โค e
โง e โค 3) |