Step | Hyp | Ref
| Expression |
1 | | peano2nn 12172 |
. . 3
โข (๐ด โ โ โ (๐ด + 1) โ
โ) |
2 | | eqid 2737 |
. . . 4
โข (๐ โ
(โคโฅโ(๐ด + 1)) โฆ ((2โ-(!โ(๐ด + 1))) ยท ((1 /
2)โ(๐ โ (๐ด + 1))))) = (๐ โ (โคโฅโ(๐ด + 1)) โฆ
((2โ-(!โ(๐ด +
1))) ยท ((1 / 2)โ(๐ โ (๐ด + 1))))) |
3 | | aaliou3lem.c |
. . . 4
โข ๐น = (๐ โ โ โฆ
(2โ-(!โ๐))) |
4 | 2, 3 | aaliou3lem3 25720 |
. . 3
โข ((๐ด + 1) โ โ โ
(seq(๐ด + 1)( + , ๐น) โ dom โ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) |
5 | | 3simpc 1151 |
. . 3
โข
((seq(๐ด + 1)( + ,
๐น) โ dom โ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1))))) โ (ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) |
6 | 1, 4, 5 | 3syl 18 |
. 2
โข (๐ด โ โ โ
(ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) |
7 | | nncn 12168 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
8 | | ax-1cn 11116 |
. . . . . . . . . . . 12
โข 1 โ
โ |
9 | | pncan 11414 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด + 1)
โ 1) = ๐ด) |
10 | 7, 8, 9 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((๐ด + 1) โ 1) = ๐ด) |
11 | 10 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(1...((๐ด + 1) โ 1)) =
(1...๐ด)) |
12 | 11 | sumeq1d 15593 |
. . . . . . . . 9
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...((๐ด + 1) โ
1))(๐นโ๐) = ฮฃ๐ โ (1...๐ด)(๐นโ๐)) |
13 | 12 | oveq1d 7377 |
. . . . . . . 8
โข (๐ด โ โ โ
(ฮฃ๐ โ
(1...((๐ด + 1) โ
1))(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐)) = (ฮฃ๐ โ (1...๐ด)(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐))) |
14 | | nnuz 12813 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
15 | | eqid 2737 |
. . . . . . . . 9
โข
(โคโฅโ(๐ด + 1)) =
(โคโฅโ(๐ด + 1)) |
16 | | eqidd 2738 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐นโ๐) = (๐นโ๐)) |
17 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
18 | 17 | negeqd 11402 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ -(!โ๐) = -(!โ๐)) |
19 | 18 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (2โ-(!โ๐)) = (2โ-(!โ๐))) |
20 | | ovex 7395 |
. . . . . . . . . . . 12
โข
(2โ-(!โ๐)) โ V |
21 | 19, 3, 20 | fvmpt 6953 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐นโ๐) = (2โ-(!โ๐))) |
22 | | 2rp 12927 |
. . . . . . . . . . . . 13
โข 2 โ
โ+ |
23 | | nnnn0 12427 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ0) |
24 | | faccl 14190 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(!โ๐) โ
โ) |
26 | 25 | nnzd 12533 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(!โ๐) โ
โค) |
27 | 26 | znegcld 12616 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
-(!โ๐) โ
โค) |
28 | | rpexpcl 13993 |
. . . . . . . . . . . . 13
โข ((2
โ โ+ โง -(!โ๐) โ โค) โ
(2โ-(!โ๐))
โ โ+) |
29 | 22, 27, 28 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(2โ-(!โ๐))
โ โ+) |
30 | 29 | rpcnd 12966 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(2โ-(!โ๐))
โ โ) |
31 | 21, 30 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐นโ๐) โ โ) |
32 | 31 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
33 | | 1nn 12171 |
. . . . . . . . . 10
โข 1 โ
โ |
34 | | eqid 2737 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ1) โฆ ((2โ-(!โ1)) ยท ((1 /
2)โ(๐ โ 1)))) =
(๐ โ
(โคโฅโ1) โฆ ((2โ-(!โ1)) ยท ((1 /
2)โ(๐ โ
1)))) |
35 | 34, 3 | aaliou3lem3 25720 |
. . . . . . . . . . 11
โข (1 โ
โ โ (seq1( + , ๐น) โ dom โ โง ฮฃ๐ โ
(โคโฅโ1)(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ1)(๐นโ๐) โค (2 ยท
(2โ-(!โ1))))) |
36 | 35 | simp1d 1143 |
. . . . . . . . . 10
โข (1 โ
โ โ seq1( + , ๐น)
โ dom โ ) |
37 | 33, 36 | mp1i 13 |
. . . . . . . . 9
โข (๐ด โ โ โ seq1( + ,
๐น) โ dom โ
) |
38 | 14, 15, 1, 16, 32, 37 | isumsplit 15732 |
. . . . . . . 8
โข (๐ด โ โ โ
ฮฃ๐ โ โ
(๐นโ๐) = (ฮฃ๐ โ (1...((๐ด + 1) โ 1))(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐))) |
39 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ = ๐ด โ (1...๐) = (1...๐ด)) |
40 | 39 | sumeq1d 15593 |
. . . . . . . . . 10
โข (๐ = ๐ด โ ฮฃ๐ โ (1...๐)(๐นโ๐) = ฮฃ๐ โ (1...๐ด)(๐นโ๐)) |
41 | | aaliou3lem.e |
. . . . . . . . . 10
โข ๐ป = (๐ โ โ โฆ ฮฃ๐ โ (1...๐)(๐นโ๐)) |
42 | | sumex 15579 |
. . . . . . . . . 10
โข
ฮฃ๐ โ
(1...๐ด)(๐นโ๐) โ V |
43 | 40, 41, 42 | fvmpt 6953 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ปโ๐ด) = ฮฃ๐ โ (1...๐ด)(๐นโ๐)) |
44 | 43 | oveq1d 7377 |
. . . . . . . 8
โข (๐ด โ โ โ ((๐ปโ๐ด) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐)) = (ฮฃ๐ โ (1...๐ด)(๐นโ๐) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐))) |
45 | 13, 38, 44 | 3eqtr4rd 2788 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ปโ๐ด) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐)) = ฮฃ๐ โ โ (๐นโ๐)) |
46 | | aaliou3lem.d |
. . . . . . 7
โข ๐ฟ = ฮฃ๐ โ โ (๐นโ๐) |
47 | 45, 46 | eqtr4di 2795 |
. . . . . 6
โข (๐ด โ โ โ ((๐ปโ๐ด) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐)) = ๐ฟ) |
48 | 3, 46, 41 | aaliou3lem4 25722 |
. . . . . . . . 9
โข ๐ฟ โ โ |
49 | 48 | recni 11176 |
. . . . . . . 8
โข ๐ฟ โ โ |
50 | 49 | a1i 11 |
. . . . . . 7
โข (๐ด โ โ โ ๐ฟ โ
โ) |
51 | 3, 46, 41 | aaliou3lem5 25723 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ปโ๐ด) โ โ) |
52 | 51 | recnd 11190 |
. . . . . . 7
โข (๐ด โ โ โ (๐ปโ๐ด) โ โ) |
53 | 4 | simp2d 1144 |
. . . . . . . . 9
โข ((๐ด + 1) โ โ โ
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ
โ+) |
54 | 1, 53 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ
โ+) |
55 | 54 | rpcnd 12966 |
. . . . . . 7
โข (๐ด โ โ โ
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ) |
56 | 50, 52, 55 | subaddd 11537 |
. . . . . 6
โข (๐ด โ โ โ ((๐ฟ โ (๐ปโ๐ด)) = ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐) โ ((๐ปโ๐ด) + ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐)) = ๐ฟ)) |
57 | 47, 56 | mpbird 257 |
. . . . 5
โข (๐ด โ โ โ (๐ฟ โ (๐ปโ๐ด)) = ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐)) |
58 | 57 | eqcomd 2743 |
. . . 4
โข (๐ด โ โ โ
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) = (๐ฟ โ (๐ปโ๐ด))) |
59 | | eleq1 2826 |
. . . . 5
โข
(ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) = (๐ฟ โ (๐ปโ๐ด)) โ (ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โ (๐ฟ โ (๐ปโ๐ด)) โ
โ+)) |
60 | | breq1 5113 |
. . . . 5
โข
(ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) = (๐ฟ โ (๐ปโ๐ด)) โ (ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1)))) โ (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) |
61 | 59, 60 | anbi12d 632 |
. . . 4
โข
(ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) = (๐ฟ โ (๐ปโ๐ด)) โ ((ฮฃ๐ โ (โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1))))) โ ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1))))))) |
62 | 58, 61 | syl 17 |
. . 3
โข (๐ด โ โ โ
((ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1))))) โ ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1))))))) |
63 | 51 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (๐ปโ๐ด) โ โ) |
64 | | simprl 770 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (๐ฟ โ (๐ปโ๐ด)) โ
โ+) |
65 | | difrp 12960 |
. . . . . . . 8
โข (((๐ปโ๐ด) โ โ โง ๐ฟ โ โ) โ ((๐ปโ๐ด) < ๐ฟ โ (๐ฟ โ (๐ปโ๐ด)) โ
โ+)) |
66 | 63, 48, 65 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ปโ๐ด) < ๐ฟ โ (๐ฟ โ (๐ปโ๐ด)) โ
โ+)) |
67 | 64, 66 | mpbird 257 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (๐ปโ๐ด) < ๐ฟ) |
68 | 63, 67 | ltned 11298 |
. . . . 5
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (๐ปโ๐ด) โ ๐ฟ) |
69 | | nnnn0 12427 |
. . . . . . . . . . . . . . 15
โข ((๐ด + 1) โ โ โ
(๐ด + 1) โ
โ0) |
70 | | faccl 14190 |
. . . . . . . . . . . . . . 15
โข ((๐ด + 1) โ โ0
โ (!โ(๐ด + 1))
โ โ) |
71 | 1, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ
(!โ(๐ด + 1)) โ
โ) |
72 | 71 | nnzd 12533 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ
(!โ(๐ด + 1)) โ
โค) |
73 | 72 | znegcld 12616 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
-(!โ(๐ด + 1)) โ
โค) |
74 | | rpexpcl 13993 |
. . . . . . . . . . . 12
โข ((2
โ โ+ โง -(!โ(๐ด + 1)) โ โค) โ
(2โ-(!โ(๐ด + 1)))
โ โ+) |
75 | 22, 73, 74 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(2โ-(!โ(๐ด + 1)))
โ โ+) |
76 | | rpmulcl 12945 |
. . . . . . . . . . 11
โข ((2
โ โ+ โง (2โ-(!โ(๐ด + 1))) โ โ+) โ
(2 ยท (2โ-(!โ(๐ด + 1)))) โ
โ+) |
77 | 22, 75, 76 | sylancr 588 |
. . . . . . . . . 10
โข (๐ด โ โ โ (2
ยท (2โ-(!โ(๐ด + 1)))) โ
โ+) |
78 | 77 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (2 ยท
(2โ-(!โ(๐ด +
1)))) โ โ+) |
79 | 78 | rpred 12964 |
. . . . . . . 8
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (2 ยท
(2โ-(!โ(๐ด +
1)))) โ โ) |
80 | 63, 79 | resubcld 11590 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ปโ๐ด) โ (2 ยท
(2โ-(!โ(๐ด +
1))))) โ โ) |
81 | 48 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ๐ฟ โ
โ) |
82 | 63, 78 | ltsubrpd 12996 |
. . . . . . . 8
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ปโ๐ด) โ (2 ยท
(2โ-(!โ(๐ด +
1))))) < (๐ปโ๐ด)) |
83 | 80, 63, 81, 82, 67 | lttrd 11323 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ปโ๐ด) โ (2 ยท
(2โ-(!โ(๐ด +
1))))) < ๐ฟ) |
84 | 80, 81, 83 | ltled 11310 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ปโ๐ด) โ (2 ยท
(2โ-(!โ(๐ด +
1))))) โค ๐ฟ) |
85 | | simprr 772 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1))))) |
86 | 81, 63, 79 | lesubadd2d 11761 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))) โ ๐ฟ โค ((๐ปโ๐ด) + (2 ยท (2โ-(!โ(๐ด + 1))))))) |
87 | 85, 86 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ๐ฟ โค ((๐ปโ๐ด) + (2 ยท (2โ-(!โ(๐ด + 1)))))) |
88 | 81, 63, 79 | absdifled 15326 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ
((absโ(๐ฟ โ
(๐ปโ๐ด))) โค (2 ยท
(2โ-(!โ(๐ด +
1)))) โ (((๐ปโ๐ด) โ (2 ยท
(2โ-(!โ(๐ด +
1))))) โค ๐ฟ โง ๐ฟ โค ((๐ปโ๐ด) + (2 ยท (2โ-(!โ(๐ด + 1)))))))) |
89 | 84, 87, 88 | mpbir2and 712 |
. . . . 5
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ
(absโ(๐ฟ โ
(๐ปโ๐ด))) โค (2 ยท
(2โ-(!โ(๐ด +
1))))) |
90 | 68, 89 | jca 513 |
. . . 4
โข ((๐ด โ โ โง ((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1)))))) โ ((๐ปโ๐ด) โ ๐ฟ โง (absโ(๐ฟ โ (๐ปโ๐ด))) โค (2 ยท
(2โ-(!โ(๐ด +
1)))))) |
91 | 90 | ex 414 |
. . 3
โข (๐ด โ โ โ (((๐ฟ โ (๐ปโ๐ด)) โ โ+ โง (๐ฟ โ (๐ปโ๐ด)) โค (2 ยท (2โ-(!โ(๐ด + 1))))) โ ((๐ปโ๐ด) โ ๐ฟ โง (absโ(๐ฟ โ (๐ปโ๐ด))) โค (2 ยท
(2โ-(!โ(๐ด +
1))))))) |
92 | 62, 91 | sylbid 239 |
. 2
โข (๐ด โ โ โ
((ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โ โ+ โง
ฮฃ๐ โ
(โคโฅโ(๐ด + 1))(๐นโ๐) โค (2 ยท (2โ-(!โ(๐ด + 1))))) โ ((๐ปโ๐ด) โ ๐ฟ โง (absโ(๐ฟ โ (๐ปโ๐ด))) โค (2 ยท
(2โ-(!โ(๐ด +
1))))))) |
93 | 6, 92 | mpd 15 |
1
โข (๐ด โ โ โ ((๐ปโ๐ด) โ ๐ฟ โง (absโ(๐ฟ โ (๐ปโ๐ด))) โค (2 ยท
(2โ-(!โ(๐ด +
1)))))) |