Proof of Theorem limsupequzmptlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | limsupequzmptlem.j | . 2
⊢
Ⅎ𝑗𝜑 | 
| 2 |  | nfmpt1 5250 | . 2
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴 ↦ 𝐶) | 
| 3 |  | nfmpt1 5250 | . 2
⊢
Ⅎ𝑗(𝑗 ∈ 𝐵 ↦ 𝐶) | 
| 4 |  | limsupequzmptlem.m | . 2
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 5 |  | limsupequzmptlem.a | . . . . . . 7
⊢ 𝐴 =
(ℤ≥‘𝑀) | 
| 6 | 5 | eqcomi 2746 | . . . . . 6
⊢
(ℤ≥‘𝑀) = 𝐴 | 
| 7 | 6 | eleq2i 2833 | . . . . 5
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↔ 𝑗 ∈ 𝐴) | 
| 8 | 7 | biimpi 216 | . . . 4
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ 𝐴) | 
| 9 |  | limsupequzmptlem.c | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑉) | 
| 10 | 8, 9 | sylan2 593 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐶 ∈ 𝑉) | 
| 11 | 5 | mpteq1i 5238 | . . 3
⊢ (𝑗 ∈ 𝐴 ↦ 𝐶) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐶) | 
| 12 | 1, 10, 11 | fnmptd 6709 | . 2
⊢ (𝜑 → (𝑗 ∈ 𝐴 ↦ 𝐶) Fn (ℤ≥‘𝑀)) | 
| 13 |  | limsupequzmptlem.n | . 2
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 14 |  | limsupequzmptlem.b | . . . . . . 7
⊢ 𝐵 =
(ℤ≥‘𝑁) | 
| 15 | 14 | eleq2i 2833 | . . . . . 6
⊢ (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ (ℤ≥‘𝑁)) | 
| 16 | 15 | bicomi 224 | . . . . 5
⊢ (𝑗 ∈
(ℤ≥‘𝑁) ↔ 𝑗 ∈ 𝐵) | 
| 17 | 16 | biimpi 216 | . . . 4
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑗 ∈ 𝐵) | 
| 18 |  | limsupequzmptlem.d | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐵) → 𝐶 ∈ 𝑊) | 
| 19 | 17, 18 | sylan2 593 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ 𝑊) | 
| 20 | 14 | mpteq1i 5238 | . . 3
⊢ (𝑗 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ (ℤ≥‘𝑁) ↦ 𝐶) | 
| 21 | 1, 19, 20 | fnmptd 6709 | . 2
⊢ (𝜑 → (𝑗 ∈ 𝐵 ↦ 𝐶) Fn (ℤ≥‘𝑁)) | 
| 22 |  | limsupequzmptlem.k | . . 3
⊢ 𝐾 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) | 
| 23 | 13, 4 | ifcld 4572 | . . 3
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ) | 
| 24 | 22, 23 | eqeltrid 2845 | . 2
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 25 |  | eqid 2737 | . . . . . . . . 9
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) | 
| 26 | 4 | zred 12722 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 27 | 13 | zred 12722 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 28 |  | max1 13227 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) | 
| 29 | 26, 27, 28 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) | 
| 30 | 29, 22 | breqtrrdi 5185 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝐾) | 
| 31 | 25, 4, 24, 30 | eluzd 45420 | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) | 
| 32 | 31 | uzssd 45419 | . . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆
(ℤ≥‘𝑀)) | 
| 33 | 6 | a1i 11 | . . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝑀) = 𝐴) | 
| 34 | 32, 33 | sseqtrd 4020 | . . . . . 6
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆ 𝐴) | 
| 35 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(ℤ≥‘𝐾) ⊆ 𝐴) | 
| 36 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ (ℤ≥‘𝐾)) | 
| 37 | 35, 36 | sseldd 3984 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ 𝐴) | 
| 38 | 37, 9 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐶 ∈ 𝑉) | 
| 39 |  | eqid 2737 | . . . . 5
⊢ (𝑗 ∈ 𝐴 ↦ 𝐶) = (𝑗 ∈ 𝐴 ↦ 𝐶) | 
| 40 | 39 | fvmpt2 7027 | . . . 4
⊢ ((𝑗 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑗 ∈ 𝐴 ↦ 𝐶)‘𝑗) = 𝐶) | 
| 41 | 37, 38, 40 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝑗 ∈ 𝐴 ↦ 𝐶)‘𝑗) = 𝐶) | 
| 42 |  | eqid 2737 | . . . . . . . . 9
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) | 
| 43 |  | max2 13229 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) | 
| 44 | 26, 27, 43 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) | 
| 45 | 44, 22 | breqtrrdi 5185 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ≤ 𝐾) | 
| 46 | 42, 13, 24, 45 | eluzd 45420 | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁)) | 
| 47 | 46 | uzssd 45419 | . . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆
(ℤ≥‘𝑁)) | 
| 48 | 14 | eqcomi 2746 | . . . . . . . 8
⊢
(ℤ≥‘𝑁) = 𝐵 | 
| 49 | 48 | a1i 11 | . . . . . . 7
⊢ (𝜑 →
(ℤ≥‘𝑁) = 𝐵) | 
| 50 | 47, 49 | sseqtrd 4020 | . . . . . 6
⊢ (𝜑 →
(ℤ≥‘𝐾) ⊆ 𝐵) | 
| 51 | 50 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(ℤ≥‘𝐾) ⊆ 𝐵) | 
| 52 | 51, 36 | sseldd 3984 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ 𝐵) | 
| 53 |  | eqid 2737 | . . . . 5
⊢ (𝑗 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ 𝐵 ↦ 𝐶) | 
| 54 | 53 | fvmpt2 7027 | . . . 4
⊢ ((𝑗 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → ((𝑗 ∈ 𝐵 ↦ 𝐶)‘𝑗) = 𝐶) | 
| 55 | 52, 38, 54 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝑗 ∈ 𝐵 ↦ 𝐶)‘𝑗) = 𝐶) | 
| 56 | 41, 55 | eqtr4d 2780 | . 2
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝑗 ∈ 𝐴 ↦ 𝐶)‘𝑗) = ((𝑗 ∈ 𝐵 ↦ 𝐶)‘𝑗)) | 
| 57 | 1, 2, 3, 4, 12, 13, 21, 24, 56 | limsupequz 45738 | 1
⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim sup‘(𝑗 ∈ 𝐵 ↦ 𝐶))) |