Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfi1fseqlem3 Structured version   Visualization version   GIF version

Theorem mbfi1fseqlem3 24328
 Description: Lemma for mbfi1fseq 24332. (Contributed by Mario Carneiro, 16-Aug-2014.)
Hypotheses
Ref Expression
mbfi1fseq.1 (𝜑𝐹 ∈ MblFn)
mbfi1fseq.2 (𝜑𝐹:ℝ⟶(0[,)+∞))
mbfi1fseq.3 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)))
mbfi1fseq.4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
Assertion
Ref Expression
mbfi1fseqlem3 ((𝜑𝐴 ∈ ℕ) → (𝐺𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
Distinct variable groups:   𝑥,𝑚,𝑦,𝐹   𝑥,𝐺   𝑚,𝐽   𝜑,𝑚,𝑥,𝑦   𝐴,𝑚,𝑥,𝑦
Allowed substitution hints:   𝐺(𝑦,𝑚)   𝐽(𝑥,𝑦)

Proof of Theorem mbfi1fseqlem3
StepHypRef Expression
1 mbfi1fseq.1 . . . 4 (𝜑𝐹 ∈ MblFn)
2 mbfi1fseq.2 . . . 4 (𝜑𝐹:ℝ⟶(0[,)+∞))
3 mbfi1fseq.3 . . . 4 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)))
4 mbfi1fseq.4 . . . 4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
51, 2, 3, 4mbfi1fseqlem2 24327 . . 3 (𝐴 ∈ ℕ → (𝐺𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
65adantl 485 . 2 ((𝜑𝐴 ∈ ℕ) → (𝐺𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
7 rge0ssre 12836 . . . . . . . . . . . . . . . . . 18 (0[,)+∞) ⊆ ℝ
8 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
9 ffvelrn 6826 . . . . . . . . . . . . . . . . . . 19 ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ (0[,)+∞))
102, 8, 9syl2an 598 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ (0[,)+∞))
117, 10sseldi 3913 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ ℝ)
12 2nn 11700 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℕ
13 nnnn0 11894 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
14 nnexpcl 13440 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
1512, 13, 14sylancr 590 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
1615ad2antrl 727 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
1716nnred 11642 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
1811, 17remulcld 10662 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹𝑦) · (2↑𝑚)) ∈ ℝ)
19 reflcl 13163 . . . . . . . . . . . . . . . 16 (((𝐹𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
2018, 19syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
2120, 16nndivred 11681 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
2221ralrimivva 3156 . . . . . . . . . . . . 13 (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
233fmpo 7750 . . . . . . . . . . . . 13 (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
2422, 23sylib 221 . . . . . . . . . . . 12 (𝜑𝐽:(ℕ × ℝ)⟶ℝ)
25 fovrn 7299 . . . . . . . . . . . 12 ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
2624, 25syl3an1 1160 . . . . . . . . . . 11 ((𝜑𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
27263expa 1115 . . . . . . . . . 10 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
28 nnre 11634 . . . . . . . . . . 11 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2928ad2antlr 726 . . . . . . . . . 10 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
30 nnnn0 11894 . . . . . . . . . . . . 13 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
31 nnexpcl 13440 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ0) → (2↑𝐴) ∈ ℕ)
3212, 30, 31sylancr 590 . . . . . . . . . . . 12 (𝐴 ∈ ℕ → (2↑𝐴) ∈ ℕ)
3332ad2antlr 726 . . . . . . . . . . 11 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ)
34 nnre 11634 . . . . . . . . . . . 12 ((2↑𝐴) ∈ ℕ → (2↑𝐴) ∈ ℝ)
35 nngt0 11658 . . . . . . . . . . . 12 ((2↑𝐴) ∈ ℕ → 0 < (2↑𝐴))
3634, 35jca 515 . . . . . . . . . . 11 ((2↑𝐴) ∈ ℕ → ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴)))
3733, 36syl 17 . . . . . . . . . 10 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴)))
38 lemul1 11483 . . . . . . . . . 10 (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) → ((𝐴𝐽𝑥) ≤ 𝐴 ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴))))
3927, 29, 37, 38syl3anc 1368 . . . . . . . . 9 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴𝐽𝑥) ≤ 𝐴 ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴))))
4039biimpa 480 . . . . . . . 8 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴)))
41 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝐴𝑦 = 𝑥) → 𝑦 = 𝑥)
4241fveq2d 6649 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝐴𝑦 = 𝑥) → (𝐹𝑦) = (𝐹𝑥))
43 simpl 486 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝐴𝑦 = 𝑥) → 𝑚 = 𝐴)
4443oveq2d 7151 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝐴𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴))
4542, 44oveq12d 7153 . . . . . . . . . . . . . . . . 17 ((𝑚 = 𝐴𝑦 = 𝑥) → ((𝐹𝑦) · (2↑𝑚)) = ((𝐹𝑥) · (2↑𝐴)))
4645fveq2d 6649 . . . . . . . . . . . . . . . 16 ((𝑚 = 𝐴𝑦 = 𝑥) → (⌊‘((𝐹𝑦) · (2↑𝑚))) = (⌊‘((𝐹𝑥) · (2↑𝐴))))
4746, 44oveq12d 7153 . . . . . . . . . . . . . . 15 ((𝑚 = 𝐴𝑦 = 𝑥) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹𝑥) · (2↑𝐴))) / (2↑𝐴)))
48 ovex 7168 . . . . . . . . . . . . . . 15 ((⌊‘((𝐹𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V
4947, 3, 48ovmpoa 7285 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝐴))) / (2↑𝐴)))
5049ad4ant23 752 . . . . . . . . . . . . 13 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝐴))) / (2↑𝐴)))
5150oveq1d 7150 . . . . . . . . . . . 12 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) = (((⌊‘((𝐹𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)))
522adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐴 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
5352ffvelrnda 6828 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
54 elrege0 12834 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
5553, 54sylib 221 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
5655simpld 498 . . . . . . . . . . . . . . . . 17 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
5733nnred 11642 . . . . . . . . . . . . . . . . 17 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℝ)
5856, 57remulcld 10662 . . . . . . . . . . . . . . . 16 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) · (2↑𝐴)) ∈ ℝ)
5933nnnn0d 11945 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ0)
6059nn0ge0d 11948 . . . . . . . . . . . . . . . . 17 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴))
61 mulge0 11149 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹𝑥) · (2↑𝐴)))
6255, 57, 60, 61syl12anc 835 . . . . . . . . . . . . . . . 16 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹𝑥) · (2↑𝐴)))
63 flge0nn0 13187 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑥) · (2↑𝐴))) → (⌊‘((𝐹𝑥) · (2↑𝐴))) ∈ ℕ0)
6458, 62, 63syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝐴))) ∈ ℕ0)
6564adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (⌊‘((𝐹𝑥) · (2↑𝐴))) ∈ ℕ0)
6665nn0cnd 11947 . . . . . . . . . . . . 13 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (⌊‘((𝐹𝑥) · (2↑𝐴))) ∈ ℂ)
6733adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (2↑𝐴) ∈ ℕ)
6867nncnd 11643 . . . . . . . . . . . . 13 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (2↑𝐴) ∈ ℂ)
6967nnne0d 11677 . . . . . . . . . . . . 13 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (2↑𝐴) ≠ 0)
7066, 68, 69divcan1d 11408 . . . . . . . . . . . 12 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (((⌊‘((𝐹𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹𝑥) · (2↑𝐴))))
7151, 70eqtrd 2833 . . . . . . . . . . 11 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) = (⌊‘((𝐹𝑥) · (2↑𝐴))))
7271, 65eqeltrd 2890 . . . . . . . . . 10 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ∈ ℕ0)
73 nn0uz 12270 . . . . . . . . . 10 0 = (ℤ‘0)
7472, 73eleqtrdi 2900 . . . . . . . . 9 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (ℤ‘0))
75 nnmulcl 11651 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ (2↑𝐴) ∈ ℕ) → (𝐴 · (2↑𝐴)) ∈ ℕ)
7632, 75mpdan 686 . . . . . . . . . . . 12 (𝐴 ∈ ℕ → (𝐴 · (2↑𝐴)) ∈ ℕ)
7776ad2antlr 726 . . . . . . . . . . 11 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈ ℕ)
7877adantr 484 . . . . . . . . . 10 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴 · (2↑𝐴)) ∈ ℕ)
7978nnzd 12076 . . . . . . . . 9 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴 · (2↑𝐴)) ∈ ℤ)
80 elfz5 12896 . . . . . . . . 9 ((((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (ℤ‘0) ∧ (𝐴 · (2↑𝐴)) ∈ ℤ) → (((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴))))
8174, 79, 80syl2anc 587 . . . . . . . 8 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) ↔ ((𝐴𝐽𝑥) · (2↑𝐴)) ≤ (𝐴 · (2↑𝐴))))
8240, 81mpbird 260 . . . . . . 7 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))))
83 oveq1 7142 . . . . . . . 8 (𝑚 = ((𝐴𝐽𝑥) · (2↑𝐴)) → (𝑚 / (2↑𝐴)) = (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)))
84 eqid 2798 . . . . . . . 8 (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) = (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))
85 ovex 7168 . . . . . . . 8 (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)) ∈ V
8683, 84, 85fvmpt 6745 . . . . . . 7 (((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) = (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)))
8782, 86syl 17 . . . . . 6 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) = (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)))
8827adantr 484 . . . . . . . 8 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) ∈ ℝ)
8988recnd 10660 . . . . . . 7 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) ∈ ℂ)
9089, 68, 69divcan4d 11413 . . . . . 6 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (((𝐴𝐽𝑥) · (2↑𝐴)) / (2↑𝐴)) = (𝐴𝐽𝑥))
9187, 90eqtrd 2833 . . . . 5 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) = (𝐴𝐽𝑥))
92 elfznn0 12997 . . . . . . . . . . . 12 (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) → 𝑚 ∈ ℕ0)
9392nn0red 11946 . . . . . . . . . . 11 (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) → 𝑚 ∈ ℝ)
9432adantl 485 . . . . . . . . . . 11 ((𝜑𝐴 ∈ ℕ) → (2↑𝐴) ∈ ℕ)
95 nndivre 11668 . . . . . . . . . . 11 ((𝑚 ∈ ℝ ∧ (2↑𝐴) ∈ ℕ) → (𝑚 / (2↑𝐴)) ∈ ℝ)
9693, 94, 95syl2anr 599 . . . . . . . . . 10 (((𝜑𝐴 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐴 · (2↑𝐴)))) → (𝑚 / (2↑𝐴)) ∈ ℝ)
9796fmpttd 6856 . . . . . . . . 9 ((𝜑𝐴 ∈ ℕ) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))):(0...(𝐴 · (2↑𝐴)))⟶ℝ)
9897ffnd 6488 . . . . . . . 8 ((𝜑𝐴 ∈ ℕ) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))))
9998adantr 484 . . . . . . 7 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))))
10099adantr 484 . . . . . 6 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))))
101 fnfvelrn 6825 . . . . . 6 (((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))) ∧ ((𝐴𝐽𝑥) · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
102100, 82, 101syl2anc 587 . . . . 5 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘((𝐴𝐽𝑥) · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
10391, 102eqeltrrd 2891 . . . 4 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐴𝐽𝑥) ≤ 𝐴) → (𝐴𝐽𝑥) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
10477nnnn0d 11945 . . . . . . . . . 10 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈ ℕ0)
105104, 73eleqtrdi 2900 . . . . . . . . 9 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈ (ℤ‘0))
106 eluzfz2 12912 . . . . . . . . 9 ((𝐴 · (2↑𝐴)) ∈ (ℤ‘0) → (𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))))
107105, 106syl 17 . . . . . . . 8 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))))
108 oveq1 7142 . . . . . . . . 9 (𝑚 = (𝐴 · (2↑𝐴)) → (𝑚 / (2↑𝐴)) = ((𝐴 · (2↑𝐴)) / (2↑𝐴)))
109 ovex 7168 . . . . . . . . 9 ((𝐴 · (2↑𝐴)) / (2↑𝐴)) ∈ V
110108, 84, 109fvmpt 6745 . . . . . . . 8 ((𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) = ((𝐴 · (2↑𝐴)) / (2↑𝐴)))
111107, 110syl 17 . . . . . . 7 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) = ((𝐴 · (2↑𝐴)) / (2↑𝐴)))
11229recnd 10660 . . . . . . . 8 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ)
11333nncnd 11643 . . . . . . . 8 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℂ)
11433nnne0d 11677 . . . . . . . 8 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0)
115112, 113, 114divcan4d 11413 . . . . . . 7 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 · (2↑𝐴)) / (2↑𝐴)) = 𝐴)
116111, 115eqtrd 2833 . . . . . 6 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) = 𝐴)
117 fnfvelrn 6825 . . . . . . 7 (((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))) ∧ (𝐴 · (2↑𝐴)) ∈ (0...(𝐴 · (2↑𝐴)))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
11899, 107, 117syl2anc 587 . . . . . 6 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘(𝐴 · (2↑𝐴))) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
119116, 118eqeltrrd 2891 . . . . 5 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
120119adantr 484 . . . 4 ((((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐴𝐽𝑥) ≤ 𝐴) → 𝐴 ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
121103, 120ifclda 4459 . . 3 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
122 eluzfz1 12911 . . . . . . 7 ((𝐴 · (2↑𝐴)) ∈ (ℤ‘0) → 0 ∈ (0...(𝐴 · (2↑𝐴))))
123105, 122syl 17 . . . . . 6 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ (0...(𝐴 · (2↑𝐴))))
124 oveq1 7142 . . . . . . 7 (𝑚 = 0 → (𝑚 / (2↑𝐴)) = (0 / (2↑𝐴)))
125 ovex 7168 . . . . . . 7 (0 / (2↑𝐴)) ∈ V
126124, 84, 125fvmpt 6745 . . . . . 6 (0 ∈ (0...(𝐴 · (2↑𝐴))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) = (0 / (2↑𝐴)))
127123, 126syl 17 . . . . 5 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) = (0 / (2↑𝐴)))
128 nncn 11635 . . . . . . 7 ((2↑𝐴) ∈ ℕ → (2↑𝐴) ∈ ℂ)
129 nnne0 11661 . . . . . . 7 ((2↑𝐴) ∈ ℕ → (2↑𝐴) ≠ 0)
130128, 129div0d 11406 . . . . . 6 ((2↑𝐴) ∈ ℕ → (0 / (2↑𝐴)) = 0)
13133, 130syl 17 . . . . 5 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 / (2↑𝐴)) = 0)
132127, 131eqtrd 2833 . . . 4 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) = 0)
133 fnfvelrn 6825 . . . . 5 (((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))) Fn (0...(𝐴 · (2↑𝐴))) ∧ 0 ∈ (0...(𝐴 · (2↑𝐴)))) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
13499, 123, 133syl2anc 587 . . . 4 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴)))‘0) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
135132, 134eqeltrrd 2891 . . 3 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
136121, 135ifcld 4470 . 2 (((𝜑𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
1376, 136fmpt3d 6857 1 ((𝜑𝐴 ∈ ℕ) → (𝐺𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ifcif 4425   class class class wbr 5030   ↦ cmpt 5110   × cxp 5517  ran crn 5520   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137  ℝcr 10527  0cc0 10528   · cmul 10533  +∞cpnf 10663   < clt 10666   ≤ cle 10667  -cneg 10862   / cdiv 11288  ℕcn 11627  2c2 11682  ℕ0cn0 11887  ℤcz 11971  ℤ≥cuz 12233  [,)cico 12730  [,]cicc 12731  ...cfz 12887  ⌊cfl 13157  ↑cexp 13427  MblFncmbf 24225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-er 8274  df-en 8495  df-dom 8496  df-sdom 8497  df-sup 8892  df-inf 8893  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-n0 11888  df-z 11972  df-uz 12234  df-ico 12734  df-fz 12888  df-fl 13159  df-seq 13367  df-exp 13428 This theorem is referenced by:  mbfi1fseqlem4  24329
 Copyright terms: Public domain W3C validator