Proof of Theorem limsup10exlem
| Step | Hyp | Ref
| Expression |
| 1 | | c0ex 11255 |
. . . . . . 7
⊢ 0 ∈
V |
| 2 | 1 | prid1 4762 |
. . . . . 6
⊢ 0 ∈
{0, 1} |
| 3 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 4 | 3 | elexi 3503 |
. . . . . . 7
⊢ 1 ∈
V |
| 5 | 4 | prid2 4763 |
. . . . . 6
⊢ 1 ∈
{0, 1} |
| 6 | 2, 5 | ifcli 4573 |
. . . . 5
⊢ if(2
∥ 𝑛, 0, 1) ∈ {0,
1} |
| 7 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∩ (𝐾[,)+∞))) → if(2 ∥ 𝑛, 0, 1) ∈ {0,
1}) |
| 8 | 7 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ (ℕ ∩ (𝐾[,)+∞))if(2 ∥ 𝑛, 0, 1) ∈ {0, 1}) |
| 9 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑛𝜑 |
| 10 | 1, 4 | ifex 4576 |
. . . . 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 45269 |
. . 3
⊢ (𝜑 → ((𝐹 “ (𝐾[,)+∞)) ⊆ {0, 1} ↔
∀𝑛 ∈ (ℕ
∩ (𝐾[,)+∞))if(2
∥ 𝑛, 0, 1) ∈ {0,
1})) |
| 14 | 8, 13 | mpbird 257 |
. 2
⊢ (𝜑 → (𝐹 “ (𝐾[,)+∞)) ⊆ {0,
1}) |
| 15 | | limsup10exlem.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 16 | 15 | ceilcld 13883 |
. . . . . . . . 9
⊢ (𝜑 → (⌈‘𝐾) ∈
ℤ) |
| 17 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
| 18 | 16, 17 | ifcld 4572 |
. . . . . . . 8
⊢ (𝜑 → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈
ℤ) |
| 19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈ ℤ) |
| 20 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) → 𝑛 = (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) |
| 21 | | 2teven 16392 |
. . . . . . 7
⊢ ((if(1
≤ 𝐾,
(⌈‘𝐾), 1)
∈ ℤ ∧ 𝑛 = (2
· if(1 ≤ 𝐾,
(⌈‘𝐾), 1)))
→ 2 ∥ 𝑛) |
| 22 | 19, 20, 21 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) → 2 ∥ 𝑛) |
| 23 | 22 | iftrued 4533 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 = (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) → if(2 ∥ 𝑛, 0, 1) = 0) |
| 24 | | 2nn 12339 |
. . . . . . 7
⊢ 2 ∈
ℕ |
| 25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℕ) |
| 26 | | eqid 2737 |
. . . . . . . 8
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
| 27 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 1 ∈ ℝ) |
| 28 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝐾 ∈ ℝ) |
| 29 | 16 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌈‘𝐾) ∈
ℝ) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → (⌈‘𝐾) ∈ ℝ) |
| 31 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 1 ≤ 𝐾) |
| 32 | 15 | ceilged 13886 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≤ (⌈‘𝐾)) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝐾 ≤ (⌈‘𝐾)) |
| 34 | 27, 28, 30, 31, 33 | letrd 11418 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 1 ≤ (⌈‘𝐾)) |
| 35 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (1 ≤
𝐾 → if(1 ≤ 𝐾, (⌈‘𝐾), 1) = (⌈‘𝐾)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → if(1 ≤ 𝐾, (⌈‘𝐾), 1) = (⌈‘𝐾)) |
| 37 | 34, 36 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 1 ≤ if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 38 | 3 | leidi 11797 |
. . . . . . . . . . 11
⊢ 1 ≤
1 |
| 39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 1 ≤
1) |
| 40 | | iffalse 4534 |
. . . . . . . . . . 11
⊢ (¬ 1
≤ 𝐾 → if(1 ≤
𝐾, (⌈‘𝐾), 1) = 1) |
| 41 | 40 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → if(1 ≤ 𝐾, (⌈‘𝐾), 1) = 1) |
| 42 | 39, 41 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 1 ≤ if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 43 | 37, 42 | pm2.61dan 813 |
. . . . . . . 8
⊢ (𝜑 → 1 ≤ if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 44 | 26, 17, 18, 43 | eluzd 45420 |
. . . . . . 7
⊢ (𝜑 → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈
(ℤ≥‘1)) |
| 45 | | nnuz 12921 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
| 46 | 44, 45 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝜑 → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈
ℕ) |
| 47 | 25, 46 | nnmulcld 12319 |
. . . . 5
⊢ (𝜑 → (2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) ∈
ℕ) |
| 48 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
V) |
| 49 | 12, 23, 47, 48 | fvmptd2 7024 |
. . . 4
⊢ (𝜑 → (𝐹‘(2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) = 0) |
| 50 | 10, 12 | fnmpti 6711 |
. . . . . 6
⊢ 𝐹 Fn ℕ |
| 51 | 50 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn ℕ) |
| 52 | 15 | rexrd 11311 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℝ*) |
| 53 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 54 | 53 | a1i 11 |
. . . . . 6
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 55 | 47 | nnxrd 45285 |
. . . . . 6
⊢ (𝜑 → (2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) ∈
ℝ*) |
| 56 | 47 | nnred 12281 |
. . . . . . 7
⊢ (𝜑 → (2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) ∈
ℝ) |
| 57 | 46 | nnred 12281 |
. . . . . . . 8
⊢ (𝜑 → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈
ℝ) |
| 58 | 33, 36 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝐾 ≤ if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 59 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 𝐾 ∈ ℝ) |
| 60 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 1 ∈
ℝ) |
| 61 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → ¬ 1 ≤ 𝐾) |
| 62 | 59, 60, 61 | nleltd 45463 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 𝐾 < 1) |
| 63 | 59, 60, 62 | ltled 11409 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 𝐾 ≤ 1) |
| 64 | 41 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 1 = if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 65 | 63, 64 | breqtrd 5169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 1 ≤ 𝐾) → 𝐾 ≤ if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 66 | 58, 65 | pm2.61dan 813 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ≤ if(1 ≤ 𝐾, (⌈‘𝐾), 1)) |
| 67 | 46 | nnrpd 13075 |
. . . . . . . . 9
⊢ (𝜑 → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈
ℝ+) |
| 68 | | 2timesgt 45300 |
. . . . . . . . 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 11419 |
. . . . . . 7
⊢ (𝜑 → 𝐾 < (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) |
| 71 | 15, 56, 70 | ltled 11409 |
. . . . . 6
⊢ (𝜑 → 𝐾 ≤ (2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) |
| 72 | 56 | ltpnfd 13163 |
. . . . . 6
⊢ (𝜑 → (2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) <
+∞) |
| 73 | 52, 54, 55, 71, 72 | elicod 13437 |
. . . . 5
⊢ (𝜑 → (2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) ∈ (𝐾[,)+∞)) |
| 74 | 51, 47, 73 | fnfvimad 7254 |
. . . 4
⊢ (𝜑 → (𝐹‘(2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1))) ∈ (𝐹 “ (𝐾[,)+∞))) |
| 75 | 49, 74 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐹 “ (𝐾[,)+∞))) |
| 76 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) → if(1 ≤ 𝐾, (⌈‘𝐾), 1) ∈
ℤ) |
| 77 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) → 𝑛 = ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) |
| 78 | | 2tp1odd 16389 |
. . . . . . 7
⊢ ((if(1
≤ 𝐾,
(⌈‘𝐾), 1)
∈ ℤ ∧ 𝑛 =
((2 · if(1 ≤ 𝐾,
(⌈‘𝐾), 1)) +
1)) → ¬ 2 ∥ 𝑛) |
| 79 | 76, 77, 78 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) → ¬ 2 ∥ 𝑛) |
| 80 | 79 | iffalsed 4536 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 = ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) → if(2 ∥ 𝑛, 0, 1) = 1) |
| 81 | 47 | peano2nnd 12283 |
. . . . 5
⊢ (𝜑 → ((2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) + 1) ∈
ℕ) |
| 82 | | 1xr 11320 |
. . . . . 6
⊢ 1 ∈
ℝ* |
| 83 | 82 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ*) |
| 84 | 12, 80, 81, 83 | fvmptd2 7024 |
. . . 4
⊢ (𝜑 → (𝐹‘((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) =
1) |
| 85 | 81 | nnxrd 45285 |
. . . . . 6
⊢ (𝜑 → ((2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) + 1) ∈
ℝ*) |
| 86 | 81 | nnred 12281 |
. . . . . . 7
⊢ (𝜑 → ((2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) + 1) ∈
ℝ) |
| 87 | 56 | ltp1d 12198 |
. . . . . . . 8
⊢ (𝜑 → (2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) < ((2 · if(1
≤ 𝐾,
(⌈‘𝐾), 1)) +
1)) |
| 88 | 15, 56, 86, 70, 87 | lttrd 11422 |
. . . . . . 7
⊢ (𝜑 → 𝐾 < ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) |
| 89 | 15, 86, 88 | ltled 11409 |
. . . . . 6
⊢ (𝜑 → 𝐾 ≤ ((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) |
| 90 | 86 | ltpnfd 13163 |
. . . . . 6
⊢ (𝜑 → ((2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) + 1) <
+∞) |
| 91 | 52, 54, 85, 89, 90 | elicod 13437 |
. . . . 5
⊢ (𝜑 → ((2 · if(1 ≤
𝐾, (⌈‘𝐾), 1)) + 1) ∈ (𝐾[,)+∞)) |
| 92 | 51, 81, 91 | fnfvimad 7254 |
. . . 4
⊢ (𝜑 → (𝐹‘((2 · if(1 ≤ 𝐾, (⌈‘𝐾), 1)) + 1)) ∈ (𝐹 “ (𝐾[,)+∞))) |
| 93 | 84, 92 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → 1 ∈ (𝐹 “ (𝐾[,)+∞))) |
| 94 | 75, 93 | prssd 4822 |
. 2
⊢ (𝜑 → {0, 1} ⊆ (𝐹 “ (𝐾[,)+∞))) |
| 95 | 14, 94 | eqssd 4001 |
1
⊢ (𝜑 → (𝐹 “ (𝐾[,)+∞)) = {0, 1}) |