Proof of Theorem mbfi1fseqlem3
Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12151 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0[,)+∞) ⊆ ℝ |
2 | | mbfi1fseq.2 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
3 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) |
4 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ 𝑦 ∈ ℝ)
→ (𝐹‘𝑦) ∈
(0[,)+∞)) |
5 | 2, 3, 4 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
6 | 1, 5 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ) |
7 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℕ |
8 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) |
9 | | nnexpcl 12735 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℕ ∧ 𝑚
∈ ℕ0) → (2↑𝑚) ∈ ℕ) |
10 | 7, 8, 9 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ →
(2↑𝑚) ∈
ℕ) |
11 | 10 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈
ℕ) |
12 | 11 | nnred 10912 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈
ℝ) |
13 | 6, 12 | remulcld 9949 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ) |
14 | | reflcl 12459 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ →
(⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) →
(⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ) |
16 | 15, 11 | nndivred 10946 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) →
((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ) |
17 | 16 | ralrimivva 2954 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ) |
18 | | mbfi1fseq.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦
((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) |
19 | 18 | fmpt2 7126 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ∀𝑦 ∈
ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ ×
ℝ)⟶ℝ) |
20 | 17, 19 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽:(ℕ ×
ℝ)⟶ℝ) |
21 | | fovrn 6702 |
. . . . . . . . . . . . 13
⊢ ((𝐽:(ℕ ×
ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ) |
22 | 20, 21 | syl3an1 1351 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ) |
23 | 22 | 3expa 1257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ) |
24 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
25 | 24 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
26 | | nnnn0 11176 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
27 | | nnexpcl 12735 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ0) → (2↑𝐴) ∈ ℕ) |
28 | 7, 26, 27 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ →
(2↑𝐴) ∈
ℕ) |
29 | 28 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℕ) |
30 | | nnre 10904 |
. . . . . . . . . . . . 13
⊢
((2↑𝐴) ∈
ℕ → (2↑𝐴)
∈ ℝ) |
31 | | nngt0 10926 |
. . . . . . . . . . . . 13
⊢
((2↑𝐴) ∈
ℕ → 0 < (2↑𝐴)) |
32 | 30, 31 | jca 553 |
. . . . . . . . . . . 12
⊢
((2↑𝐴) ∈
ℕ → ((2↑𝐴)
∈ ℝ ∧ 0 < (2↑𝐴))) |
33 | 29, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((2↑𝐴) ∈ ℝ ∧ 0 <
(2↑𝐴))) |
34 | | lemul1 10754 |
. . . . . . . . . . 11
⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ((2↑𝐴) ∈ ℝ ∧ 0 <
(2↑𝐴))) → ((𝐴𝐽𝑥) ≤ 𝐴 ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴)))) |
35 | 23, 25, 33, 34 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴𝐽𝑥) ≤ 𝐴 ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴)))) |
36 | 35 | biimpa 500 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴))) |
37 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℕ) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → 𝐴 ∈ ℕ) |
39 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → 𝑥 ∈ ℝ) |
40 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
41 | 40 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
42 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑚 = 𝐴) |
43 | 42 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴)) |
44 | 41, 43 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝐴))) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) |
46 | 45, 43 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
47 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V |
48 | 46, 18, 47 | ovmpt2a 6689 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
49 | 38, 39, 48 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
50 | 49 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴))) |
51 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞)) |
52 | 51 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
53 | | elrege0 12149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
54 | 52, 53 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
55 | 54 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
56 | 29 | nnred 10912 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℝ) |
57 | 55, 56 | remulcld 9949 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ) |
58 | 29 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℕ0) |
59 | 58 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴)) |
60 | | mulge0 10425 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) |
61 | 54, 56, 59, 60 | syl12anc 1316 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) |
62 | | flge0nn0 12483 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈
ℕ0) |
63 | 57, 61, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈
ℕ0) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈
ℕ0) |
65 | 64 | nn0cnd 11230 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℂ) |
66 | 29 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (2↑𝐴) ∈ ℕ) |
67 | 66 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (2↑𝐴) ∈ ℂ) |
68 | 66 | nnne0d 10942 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (2↑𝐴) ≠ 0) |
69 | 65, 67, 68 | divcan1d 10681 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) |
70 | 50, 69 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) |
71 | 70, 64 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ∈
ℕ0) |
72 | | nn0uz 11598 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
73 | 71, 72 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ∈
(ℤ≥‘0)) |
74 | | nnmulcl 10920 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧
(2↑𝐴) ∈ ℕ)
→ (𝐴 ·
(2↑𝐴)) ∈
ℕ) |
75 | 28, 74 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → (𝐴 · (2↑𝐴)) ∈
ℕ) |
76 | 75 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈ ℕ) |
77 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴 · (2↑𝐴)) ∈ ℕ) |
78 | 77 | nnzd 11357 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴 · (2↑𝐴)) ∈ ℤ) |
79 | | elfz5 12205 |
. . . . . . . . . 10
⊢ ((((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (ℤ≥‘0)
∧ (𝐴 ·
(2↑𝐴)) ∈ ℤ)
→ (((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴)))) |
80 | 73, 78, 79 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴)))) |
81 | 36, 80 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) |
82 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑚 = ((𝐴𝐽𝑥) · (2↑𝐴)) → (𝑚 / (2↑𝐴)) = (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴))) |
83 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) = (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) |
84 | | ovex 6577 |
. . . . . . . . 9
⊢ (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)) ∈ V |
85 | 82, 83, 84 | fvmpt 6191 |
. . . . . . . 8
⊢ (((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) = (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴))) |
86 | 81, 85 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) = (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴))) |
87 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) ∈ ℝ) |
88 | 87 | recnd 9947 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) ∈ ℂ) |
89 | 88, 67, 68 | divcan4d 10686 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)) = (𝐴𝐽𝑥)) |
90 | 86, 89 | eqtrd 2644 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) = (𝐴𝐽𝑥)) |
91 | | elfznn0 12302 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) → 𝑚 ∈ ℕ0) |
92 | 91 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) → 𝑚 ∈ ℝ) |
93 | 28 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (2↑𝐴) ∈
ℕ) |
94 | | nndivre 10933 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℝ ∧
(2↑𝐴) ∈ ℕ)
→ (𝑚 / (2↑𝐴)) ∈
ℝ) |
95 | 92, 93, 94 | syl2anr 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐴 · (2↑𝐴)))) → (𝑚 / (2↑𝐴)) ∈ ℝ) |
96 | 95, 83 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))):(0...(𝐴 · (2↑𝐴)))⟶ℝ) |
97 | | ffn 5958 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))):(0...(𝐴 · (2↑𝐴)))⟶ℝ → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴)))) |
98 | 96, 97 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴)))) |
99 | 98 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴)))) |
100 | 99 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴)))) |
101 | | fnfvelrn 6264 |
. . . . . . 7
⊢ (((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))) ∧ ((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
102 | 100, 81, 101 | syl2anc 691 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
103 | 90, 102 | eqeltrrd 2689 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
104 | 76 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈
ℕ0) |
105 | 104, 72 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈
(ℤ≥‘0)) |
106 | | eluzfz2 12220 |
. . . . . . . . . 10
⊢ ((𝐴 · (2↑𝐴)) ∈
(ℤ≥‘0) → (𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) |
107 | 105, 106 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) |
108 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑚 = (𝐴 · (2↑𝐴)) → (𝑚 / (2↑𝐴)) = ((𝐴 · (2↑𝐴)) / (2↑𝐴))) |
109 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝐴 · (2↑𝐴)) / (2↑𝐴)) ∈ V |
110 | 108, 83, 109 | fvmpt 6191 |
. . . . . . . . 9
⊢ ((𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) = ((𝐴 · (2↑𝐴)) / (2↑𝐴))) |
111 | 107, 110 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) = ((𝐴 · (2↑𝐴)) / (2↑𝐴))) |
112 | 25 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ) |
113 | 29 | nncnd 10913 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℂ) |
114 | 29 | nnne0d 10942 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0) |
115 | 112, 113,
114 | divcan4d 10686 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 · (2↑𝐴)) / (2↑𝐴)) = 𝐴) |
116 | 111, 115 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) = 𝐴) |
117 | | fnfvelrn 6264 |
. . . . . . . 8
⊢ (((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))) ∧ (𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
118 | 99, 107, 117 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
119 | 116, 118 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
120 | 119 | adantr 480 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐴𝐽𝑥) ≤ 𝐴) → 𝐴 ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
121 | 103, 120 | ifclda 4070 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
122 | | eluzfz1 12219 |
. . . . . . . 8
⊢ ((𝐴 · (2↑𝐴)) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝐴 · (2↑𝐴)))) |
123 | 105, 122 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ (0...(𝐴 · (2↑𝐴)))) |
124 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑚 = 0 → (𝑚 / (2↑𝐴)) = (0 / (2↑𝐴))) |
125 | | ovex 6577 |
. . . . . . . 8
⊢ (0 /
(2↑𝐴)) ∈
V |
126 | 124, 83, 125 | fvmpt 6191 |
. . . . . . 7
⊢ (0 ∈
(0...(𝐴 ·
(2↑𝐴))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) = (0 / (2↑𝐴))) |
127 | 123, 126 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) = (0 / (2↑𝐴))) |
128 | | nncn 10905 |
. . . . . . . 8
⊢
((2↑𝐴) ∈
ℕ → (2↑𝐴)
∈ ℂ) |
129 | | nnne0 10930 |
. . . . . . . 8
⊢
((2↑𝐴) ∈
ℕ → (2↑𝐴)
≠ 0) |
130 | 128, 129 | div0d 10679 |
. . . . . . 7
⊢
((2↑𝐴) ∈
ℕ → (0 / (2↑𝐴)) = 0) |
131 | 29, 130 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 / (2↑𝐴)) = 0) |
132 | 127, 131 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) = 0) |
133 | | fnfvelrn 6264 |
. . . . . 6
⊢ (((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))) ∧ 0 ∈ (0...(𝐴 · (2↑𝐴)))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
134 | 99, 123, 133 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
135 | 132, 134 | eqeltrrd 2689 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
136 | 121, 135 | ifcld 4081 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
137 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
138 | 136, 137 | fmptd 6292 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |
139 | | mbfi1fseq.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
140 | | mbfi1fseq.4 |
. . . . 5
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) |
141 | 139, 2, 18, 140 | mbfi1fseqlem2 23289 |
. . . 4
⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) |
142 | 141 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) |
143 | 142 | feq1d 5943 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ((𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) ↔ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))) |
144 | 138, 143 | mpbird 246 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))) |