Step | Hyp | Ref
| Expression |
1 | | c0ex 11156 |
. . . . . . 7
โข 0 โ
V |
2 | 1 | prid1 4728 |
. . . . . 6
โข 0 โ
{0, 1} |
3 | | 1re 11162 |
. . . . . . . 8
โข 1 โ
โ |
4 | 3 | elexi 3467 |
. . . . . . 7
โข 1 โ
V |
5 | 4 | prid2 4729 |
. . . . . 6
โข 1 โ
{0, 1} |
6 | 2, 5 | ifcli 4538 |
. . . . 5
โข if(2
โฅ ๐, 0, 1) โ {0,
1} |
7 | 6 | a1i 11 |
. . . 4
โข ((๐ โง ๐ โ (โ โฉ (๐พ[,)+โ))) โ if(2 โฅ ๐, 0, 1) โ {0,
1}) |
8 | 7 | ralrimiva 3144 |
. . 3
โข (๐ โ โ๐ โ (โ โฉ (๐พ[,)+โ))if(2 โฅ ๐, 0, 1) โ {0, 1}) |
9 | | nfv 1918 |
. . . 4
โข
โฒ๐๐ |
10 | 1, 4 | ifex 4541 |
. . . . 5
โข if(2
โฅ ๐, 0, 1) โ
V |
11 | 10 | a1i 11 |
. . . 4
โข ((๐ โง ๐ โ (โ โฉ (๐พ[,)+โ))) โ if(2 โฅ ๐, 0, 1) โ
V) |
12 | | limsup10exlem.1 |
. . . 4
โข ๐น = (๐ โ โ โฆ if(2 โฅ ๐, 0, 1)) |
13 | 9, 11, 12 | imassmpt 43565 |
. . 3
โข (๐ โ ((๐น โ (๐พ[,)+โ)) โ {0, 1} โ
โ๐ โ (โ
โฉ (๐พ[,)+โ))if(2
โฅ ๐, 0, 1) โ {0,
1})) |
14 | 8, 13 | mpbird 257 |
. 2
โข (๐ โ (๐น โ (๐พ[,)+โ)) โ {0,
1}) |
15 | | limsup10exlem.2 |
. . . . . . . . . 10
โข (๐ โ ๐พ โ โ) |
16 | 15 | ceilcld 13755 |
. . . . . . . . 9
โข (๐ โ (โโ๐พ) โ
โค) |
17 | | 1zzd 12541 |
. . . . . . . . 9
โข (๐ โ 1 โ
โค) |
18 | 16, 17 | ifcld 4537 |
. . . . . . . 8
โข (๐ โ if(1 โค ๐พ, (โโ๐พ), 1) โ
โค) |
19 | 18 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ = (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) โ if(1 โค ๐พ, (โโ๐พ), 1) โ โค) |
20 | | simpr 486 |
. . . . . . 7
โข ((๐ โง ๐ = (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) โ ๐ = (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) |
21 | | 2teven 16244 |
. . . . . . 7
โข ((if(1
โค ๐พ,
(โโ๐พ), 1)
โ โค โง ๐ = (2
ยท if(1 โค ๐พ,
(โโ๐พ), 1)))
โ 2 โฅ ๐) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ = (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) โ 2 โฅ ๐) |
23 | 22 | iftrued 4499 |
. . . . 5
โข ((๐ โง ๐ = (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) โ if(2 โฅ ๐, 0, 1) = 0) |
24 | | 2nn 12233 |
. . . . . . 7
โข 2 โ
โ |
25 | 24 | a1i 11 |
. . . . . 6
โข (๐ โ 2 โ
โ) |
26 | | eqid 2737 |
. . . . . . . 8
โข
(โคโฅโ1) =
(โคโฅโ1) |
27 | 3 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง 1 โค ๐พ) โ 1 โ โ) |
28 | 15 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง 1 โค ๐พ) โ ๐พ โ โ) |
29 | 16 | zred 12614 |
. . . . . . . . . . . 12
โข (๐ โ (โโ๐พ) โ
โ) |
30 | 29 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง 1 โค ๐พ) โ (โโ๐พ) โ โ) |
31 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง 1 โค ๐พ) โ 1 โค ๐พ) |
32 | 15 | ceilged 13758 |
. . . . . . . . . . . 12
โข (๐ โ ๐พ โค (โโ๐พ)) |
33 | 32 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง 1 โค ๐พ) โ ๐พ โค (โโ๐พ)) |
34 | 27, 28, 30, 31, 33 | letrd 11319 |
. . . . . . . . . 10
โข ((๐ โง 1 โค ๐พ) โ 1 โค (โโ๐พ)) |
35 | | iftrue 4497 |
. . . . . . . . . . 11
โข (1 โค
๐พ โ if(1 โค ๐พ, (โโ๐พ), 1) = (โโ๐พ)) |
36 | 35 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง 1 โค ๐พ) โ if(1 โค ๐พ, (โโ๐พ), 1) = (โโ๐พ)) |
37 | 34, 36 | breqtrrd 5138 |
. . . . . . . . 9
โข ((๐ โง 1 โค ๐พ) โ 1 โค if(1 โค ๐พ, (โโ๐พ), 1)) |
38 | 3 | leidi 11696 |
. . . . . . . . . . 11
โข 1 โค
1 |
39 | 38 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ยฌ 1 โค ๐พ) โ 1 โค
1) |
40 | | iffalse 4500 |
. . . . . . . . . . 11
โข (ยฌ 1
โค ๐พ โ if(1 โค
๐พ, (โโ๐พ), 1) = 1) |
41 | 40 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ยฌ 1 โค ๐พ) โ if(1 โค ๐พ, (โโ๐พ), 1) = 1) |
42 | 39, 41 | breqtrrd 5138 |
. . . . . . . . 9
โข ((๐ โง ยฌ 1 โค ๐พ) โ 1 โค if(1 โค ๐พ, (โโ๐พ), 1)) |
43 | 37, 42 | pm2.61dan 812 |
. . . . . . . 8
โข (๐ โ 1 โค if(1 โค ๐พ, (โโ๐พ), 1)) |
44 | 26, 17, 18, 43 | eluzd 43718 |
. . . . . . 7
โข (๐ โ if(1 โค ๐พ, (โโ๐พ), 1) โ
(โคโฅโ1)) |
45 | | nnuz 12813 |
. . . . . . 7
โข โ =
(โคโฅโ1) |
46 | 44, 45 | eleqtrrdi 2849 |
. . . . . 6
โข (๐ โ if(1 โค ๐พ, (โโ๐พ), 1) โ
โ) |
47 | 25, 46 | nnmulcld 12213 |
. . . . 5
โข (๐ โ (2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) โ
โ) |
48 | 1 | a1i 11 |
. . . . 5
โข (๐ โ 0 โ
V) |
49 | 12, 23, 47, 48 | fvmptd2 6961 |
. . . 4
โข (๐ โ (๐นโ(2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) = 0) |
50 | 10, 12 | fnmpti 6649 |
. . . . . 6
โข ๐น Fn โ |
51 | 50 | a1i 11 |
. . . . 5
โข (๐ โ ๐น Fn โ) |
52 | 15 | rexrd 11212 |
. . . . . 6
โข (๐ โ ๐พ โ
โ*) |
53 | | pnfxr 11216 |
. . . . . . 7
โข +โ
โ โ* |
54 | 53 | a1i 11 |
. . . . . 6
โข (๐ โ +โ โ
โ*) |
55 | 47 | nnxrd 43581 |
. . . . . 6
โข (๐ โ (2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) โ
โ*) |
56 | 47 | nnred 12175 |
. . . . . . 7
โข (๐ โ (2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) โ
โ) |
57 | 46 | nnred 12175 |
. . . . . . . 8
โข (๐ โ if(1 โค ๐พ, (โโ๐พ), 1) โ
โ) |
58 | 33, 36 | breqtrrd 5138 |
. . . . . . . . 9
โข ((๐ โง 1 โค ๐พ) โ ๐พ โค if(1 โค ๐พ, (โโ๐พ), 1)) |
59 | 15 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ 1 โค ๐พ) โ ๐พ โ โ) |
60 | 3 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ 1 โค ๐พ) โ 1 โ
โ) |
61 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ 1 โค ๐พ) โ ยฌ 1 โค ๐พ) |
62 | 59, 60, 61 | nleltd 43761 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ 1 โค ๐พ) โ ๐พ < 1) |
63 | 59, 60, 62 | ltled 11310 |
. . . . . . . . . 10
โข ((๐ โง ยฌ 1 โค ๐พ) โ ๐พ โค 1) |
64 | 41 | eqcomd 2743 |
. . . . . . . . . 10
โข ((๐ โง ยฌ 1 โค ๐พ) โ 1 = if(1 โค ๐พ, (โโ๐พ), 1)) |
65 | 63, 64 | breqtrd 5136 |
. . . . . . . . 9
โข ((๐ โง ยฌ 1 โค ๐พ) โ ๐พ โค if(1 โค ๐พ, (โโ๐พ), 1)) |
66 | 58, 65 | pm2.61dan 812 |
. . . . . . . 8
โข (๐ โ ๐พ โค if(1 โค ๐พ, (โโ๐พ), 1)) |
67 | 46 | nnrpd 12962 |
. . . . . . . . 9
โข (๐ โ if(1 โค ๐พ, (โโ๐พ), 1) โ
โ+) |
68 | | 2timesgt 43596 |
. . . . . . . . 9
โข (if(1
โค ๐พ,
(โโ๐พ), 1)
โ โ+ โ if(1 โค ๐พ, (โโ๐พ), 1) < (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
โข (๐ โ if(1 โค ๐พ, (โโ๐พ), 1) < (2 ยท if(1 โค
๐พ, (โโ๐พ), 1))) |
70 | 15, 57, 56, 66, 69 | lelttrd 11320 |
. . . . . . 7
โข (๐ โ ๐พ < (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) |
71 | 15, 56, 70 | ltled 11310 |
. . . . . 6
โข (๐ โ ๐พ โค (2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) |
72 | 56 | ltpnfd 13049 |
. . . . . 6
โข (๐ โ (2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) <
+โ) |
73 | 52, 54, 55, 71, 72 | elicod 13321 |
. . . . 5
โข (๐ โ (2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) โ (๐พ[,)+โ)) |
74 | 51, 47, 73 | fnfvimad 7189 |
. . . 4
โข (๐ โ (๐นโ(2 ยท if(1 โค ๐พ, (โโ๐พ), 1))) โ (๐น โ (๐พ[,)+โ))) |
75 | 49, 74 | eqeltrrd 2839 |
. . 3
โข (๐ โ 0 โ (๐น โ (๐พ[,)+โ))) |
76 | 18 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ = ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) โ if(1 โค ๐พ, (โโ๐พ), 1) โ
โค) |
77 | | simpr 486 |
. . . . . . 7
โข ((๐ โง ๐ = ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) โ ๐ = ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) |
78 | | 2tp1odd 16241 |
. . . . . . 7
โข ((if(1
โค ๐พ,
(โโ๐พ), 1)
โ โค โง ๐ =
((2 ยท if(1 โค ๐พ,
(โโ๐พ), 1)) +
1)) โ ยฌ 2 โฅ ๐) |
79 | 76, 77, 78 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ = ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) โ ยฌ 2 โฅ ๐) |
80 | 79 | iffalsed 4502 |
. . . . 5
โข ((๐ โง ๐ = ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) โ if(2 โฅ ๐, 0, 1) = 1) |
81 | 47 | peano2nnd 12177 |
. . . . 5
โข (๐ โ ((2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) + 1) โ
โ) |
82 | | 1xr 11221 |
. . . . . 6
โข 1 โ
โ* |
83 | 82 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ
โ*) |
84 | 12, 80, 81, 83 | fvmptd2 6961 |
. . . 4
โข (๐ โ (๐นโ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) =
1) |
85 | 81 | nnxrd 43581 |
. . . . . 6
โข (๐ โ ((2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) + 1) โ
โ*) |
86 | 81 | nnred 12175 |
. . . . . . 7
โข (๐ โ ((2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) + 1) โ
โ) |
87 | 56 | ltp1d 12092 |
. . . . . . . 8
โข (๐ โ (2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) < ((2 ยท if(1
โค ๐พ,
(โโ๐พ), 1)) +
1)) |
88 | 15, 56, 86, 70, 87 | lttrd 11323 |
. . . . . . 7
โข (๐ โ ๐พ < ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) |
89 | 15, 86, 88 | ltled 11310 |
. . . . . 6
โข (๐ โ ๐พ โค ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) |
90 | 86 | ltpnfd 13049 |
. . . . . 6
โข (๐ โ ((2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) + 1) <
+โ) |
91 | 52, 54, 85, 89, 90 | elicod 13321 |
. . . . 5
โข (๐ โ ((2 ยท if(1 โค
๐พ, (โโ๐พ), 1)) + 1) โ (๐พ[,)+โ)) |
92 | 51, 81, 91 | fnfvimad 7189 |
. . . 4
โข (๐ โ (๐นโ((2 ยท if(1 โค ๐พ, (โโ๐พ), 1)) + 1)) โ (๐น โ (๐พ[,)+โ))) |
93 | 84, 92 | eqeltrrd 2839 |
. . 3
โข (๐ โ 1 โ (๐น โ (๐พ[,)+โ))) |
94 | 75, 93 | prssd 4787 |
. 2
โข (๐ โ {0, 1} โ (๐น โ (๐พ[,)+โ))) |
95 | 14, 94 | eqssd 3966 |
1
โข (๐ โ (๐น โ (๐พ[,)+โ)) = {0, 1}) |