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

Theorem mbfi1fseqlem6 25207
Description: Lemma for mbfi1fseq 25208. Verify that 𝐺 converges pointwise to 𝐹, and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
mbfi1fseq.1 (𝜑𝐹 ∈ MblFn)
mbfi1fseq.2 (𝜑𝐹:ℝ⟶(0[,)+∞))
mbfi1fseq.3 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)))
mbfi1fseq.4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
Assertion
Ref Expression
mbfi1fseqlem6 (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝑔𝑛) ∧ (𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) ⇝ (𝐹𝑥)))
Distinct variable groups:   𝑔,𝑚,𝑛,𝑥,𝑦,𝐹   𝑔,𝐺,𝑛,𝑥   𝑚,𝐽   𝜑,𝑚,𝑛,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑔)   𝐺(𝑦,𝑚)   𝐽(𝑥,𝑦,𝑔,𝑛)

Proof of Theorem mbfi1fseqlem6
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfi1fseq.1 . . 3 (𝜑𝐹 ∈ MblFn)
2 mbfi1fseq.2 . . 3 (𝜑𝐹:ℝ⟶(0[,)+∞))
3 mbfi1fseq.3 . . 3 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)))
4 mbfi1fseq.4 . . 3 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
51, 2, 3, 4mbfi1fseqlem4 25205 . 2 (𝜑𝐺:ℕ⟶dom ∫1)
61, 2, 3, 4mbfi1fseqlem5 25206 . . 3 ((𝜑𝑛 ∈ ℕ) → (0𝑝r ≤ (𝐺𝑛) ∧ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))
76ralrimiva 3147 . 2 (𝜑 → ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝐺𝑛) ∧ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))
8 simpr 486 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
98recnd 11229 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
109abscld 15370 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (abs‘𝑥) ∈ ℝ)
112ffvelcdmda 7074 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
12 elrege0 13418 . . . . . . . 8 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
1311, 12sylib 217 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
1413simpld 496 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
1510, 14readdcld 11230 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹𝑥)) ∈ ℝ)
16 arch 12456 . . . . 5 (((abs‘𝑥) + (𝐹𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)
1715, 16syl 17 . . . 4 ((𝜑𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)
18 eqid 2733 . . . . 5 (ℤ𝑘) = (ℤ𝑘)
19 nnz 12566 . . . . . 6 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
2019ad2antrl 727 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) → 𝑘 ∈ ℤ)
21 nnuz 12852 . . . . . . . 8 ℕ = (ℤ‘1)
22 1zzd 12580 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 1 ∈ ℤ)
23 halfcn 12414 . . . . . . . . . 10 (1 / 2) ∈ ℂ
2423a1i 11 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (1 / 2) ∈ ℂ)
25 halfre 12413 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
26 halfge0 12416 . . . . . . . . . . . 12 0 ≤ (1 / 2)
27 absid 15230 . . . . . . . . . . . 12 (((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 / 2))
2825, 26, 27mp2an 691 . . . . . . . . . . 11 (abs‘(1 / 2)) = (1 / 2)
29 halflt1 12417 . . . . . . . . . . 11 (1 / 2) < 1
3028, 29eqbrtri 5165 . . . . . . . . . 10 (abs‘(1 / 2)) < 1
3130a1i 11 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (abs‘(1 / 2)) < 1)
3224, 31expcnv 15797 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) ⇝ 0)
3314recnd 11229 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
34 nnex 12205 . . . . . . . . . 10 ℕ ∈ V
3534mptex 7212 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛))) ∈ V
3635a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛))) ∈ V)
37 nnnn0 12466 . . . . . . . . . . 11 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
3837adantl 483 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
39 oveq2 7404 . . . . . . . . . . 11 (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗))
40 eqid 2733 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
41 ovex 7429 . . . . . . . . . . 11 ((1 / 2)↑𝑗) ∈ V
4239, 40, 41fvmpt 6987 . . . . . . . . . 10 (𝑗 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
4338, 42syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗))
44 expcl 14032 . . . . . . . . . 10 (((1 / 2) ∈ ℂ ∧ 𝑗 ∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℂ)
4523, 38, 44sylancr 588 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈ ℂ)
4643, 45eqeltrd 2834 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗) ∈ ℂ)
4739oveq2d 7412 . . . . . . . . . . 11 (𝑛 = 𝑗 → ((𝐹𝑥) − ((1 / 2)↑𝑛)) = ((𝐹𝑥) − ((1 / 2)↑𝑗)))
48 eqid 2733 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))
49 ovex 7429 . . . . . . . . . . 11 ((𝐹𝑥) − ((1 / 2)↑𝑗)) ∈ V
5047, 48, 49fvmpt 6987 . . . . . . . . . 10 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹𝑥) − ((1 / 2)↑𝑗)))
5150adantl 483 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹𝑥) − ((1 / 2)↑𝑗)))
5243oveq2d 7412 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗)) = ((𝐹𝑥) − ((1 / 2)↑𝑗)))
5351, 52eqtr4d 2776 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗)))
5421, 22, 32, 33, 36, 46, 53climsubc2 15570 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹𝑥) − 0))
5533subid1d 11547 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → ((𝐹𝑥) − 0) = (𝐹𝑥))
5654, 55breqtrd 5170 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹𝑥))
5756adantr 482 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹𝑥))
5834mptex 7212 . . . . . 6 (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ∈ V
5958a1i 11 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ∈ V)
60 simprl 770 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) → 𝑘 ∈ ℕ)
61 eluznn 12889 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑗 ∈ ℕ)
6260, 61sylan 581 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑗 ∈ ℕ)
6362, 50syl 17 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹𝑥) − ((1 / 2)↑𝑗)))
6414ad2antrr 725 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐹𝑥) ∈ ℝ)
6562, 37syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑗 ∈ ℕ0)
66 reexpcl 14031 . . . . . . . 8 (((1 / 2) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℝ)
6725, 65, 66sylancr 588 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((1 / 2)↑𝑗) ∈ ℝ)
6864, 67resubcld 11629 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ)
6963, 68eqeltrd 2834 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ)
70 fveq2 6881 . . . . . . . . 9 (𝑛 = 𝑗 → (𝐺𝑛) = (𝐺𝑗))
7170fveq1d 6883 . . . . . . . 8 (𝑛 = 𝑗 → ((𝐺𝑛)‘𝑥) = ((𝐺𝑗)‘𝑥))
72 eqid 2733 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))
73 fvex 6894 . . . . . . . 8 ((𝐺𝑗)‘𝑥) ∈ V
7471, 72, 73fvmpt 6987 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗) = ((𝐺𝑗)‘𝑥))
7562, 74syl 17 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗) = ((𝐺𝑗)‘𝑥))
765ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝐺:ℕ⟶dom ∫1)
7776, 62ffvelcdmd 7075 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐺𝑗) ∈ dom ∫1)
78 i1ff 25162 . . . . . . . 8 ((𝐺𝑗) ∈ dom ∫1 → (𝐺𝑗):ℝ⟶ℝ)
7977, 78syl 17 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐺𝑗):ℝ⟶ℝ)
808ad2antrr 725 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑥 ∈ ℝ)
8179, 80ffvelcdmd 7075 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐺𝑗)‘𝑥) ∈ ℝ)
8275, 81eqeltrd 2834 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗) ∈ ℝ)
8333ad2antrr 725 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐹𝑥) ∈ ℂ)
84 2nn 12272 . . . . . . . . . . . . . 14 2 ∈ ℕ
85 nnexpcl 14027 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2↑𝑗) ∈ ℕ)
8684, 65, 85sylancr 588 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (2↑𝑗) ∈ ℕ)
8786nnred 12214 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (2↑𝑗) ∈ ℝ)
8887recnd 11229 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (2↑𝑗) ∈ ℂ)
8986nnne0d 12249 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (2↑𝑗) ≠ 0)
9083, 88, 89divcan4d 11983 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (((𝐹𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹𝑥))
9190eqcomd 2739 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐹𝑥) = (((𝐹𝑥) · (2↑𝑗)) / (2↑𝑗)))
92 2cnd 12277 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 2 ∈ ℂ)
93 2ne0 12303 . . . . . . . . . . 11 2 ≠ 0
9493a1i 11 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 2 ≠ 0)
95 eluzelz 12819 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑘) → 𝑗 ∈ ℤ)
9695adantl 483 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑗 ∈ ℤ)
9792, 94, 96exprecd 14106 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
9891, 97oveq12d 7414 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
9964, 87remulcld 11231 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) · (2↑𝑗)) ∈ ℝ)
10099recnd 11229 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) · (2↑𝑗)) ∈ ℂ)
101 1cnd 11196 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 1 ∈ ℂ)
102100, 101, 88, 89divsubdird 12016 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((((𝐹𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗))))
10398, 102eqtr4d 2776 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)))
104 fllep1 13753 . . . . . . . . . 10 (((𝐹𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) + 1))
10599, 104syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) + 1))
106 1red 11202 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 1 ∈ ℝ)
107 reflcl 13748 . . . . . . . . . . 11 (((𝐹𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹𝑥) · (2↑𝑗))) ∈ ℝ)
10899, 107syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (⌊‘((𝐹𝑥) · (2↑𝑗))) ∈ ℝ)
10999, 106, 108lesubaddd 11798 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((((𝐹𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹𝑥) · (2↑𝑗))) ↔ ((𝐹𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) + 1)))
110105, 109mpbird 257 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (((𝐹𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹𝑥) · (2↑𝑗))))
111 peano2rem 11514 . . . . . . . . . 10 (((𝐹𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
11299, 111syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (((𝐹𝑥) · (2↑𝑗)) − 1) ∈ ℝ)
11386nngt0d 12248 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 0 < (2↑𝑗))
114 lediv1 12066 . . . . . . . . 9 (((((𝐹𝑥) · (2↑𝑗)) − 1) ∈ ℝ ∧ (⌊‘((𝐹𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → ((((𝐹𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹𝑥) · (2↑𝑗))) ↔ ((((𝐹𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗))))
115112, 108, 87, 113, 114syl112anc 1375 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((((𝐹𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹𝑥) · (2↑𝑗))) ↔ ((((𝐹𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗))))
116110, 115mpbid 231 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((((𝐹𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
117103, 116eqbrtrd 5166 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
1181, 2, 3, 4mbfi1fseqlem2 25203 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝐺𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
11962, 118syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐺𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)))
120119fveq1d 6883 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐺𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥))
121 ovex 7429 . . . . . . . . . . 11 (𝑗𝐽𝑥) ∈ V
122 vex 3479 . . . . . . . . . . 11 𝑗 ∈ V
123121, 122ifex 4574 . . . . . . . . . 10 if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V
124 c0ex 11195 . . . . . . . . . 10 0 ∈ V
125123, 124ifex 4574 . . . . . . . . 9 if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V
126 eqid 2733 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
127126fvmpt2 6998 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
12880, 125, 127sylancl 587 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
12975, 120, 1283eqtrd 2777 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))
13010ad2antrr 725 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (abs‘𝑥) ∈ ℝ)
13115ad2antrr 725 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((abs‘𝑥) + (𝐹𝑥)) ∈ ℝ)
13262nnred 12214 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑗 ∈ ℝ)
13311ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐹𝑥) ∈ (0[,)+∞))
134133, 12sylib 217 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
135134simprd 497 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 0 ≤ (𝐹𝑥))
136130, 64addge01d 11789 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (0 ≤ (𝐹𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹𝑥))))
137135, 136mpbid 231 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹𝑥)))
13860adantr 482 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑘 ∈ ℕ)
139138nnred 12214 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑘 ∈ ℝ)
140 simplrr 777 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)
141131, 139, 140ltled 11349 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((abs‘𝑥) + (𝐹𝑥)) ≤ 𝑘)
142 eluzle 12822 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑘) → 𝑘𝑗)
143142adantl 483 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑘𝑗)
144131, 139, 132, 141, 143letrd 11358 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((abs‘𝑥) + (𝐹𝑥)) ≤ 𝑗)
145130, 131, 132, 137, 144letrd 11358 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (abs‘𝑥) ≤ 𝑗)
14680, 132absled 15364 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((abs‘𝑥) ≤ 𝑗 ↔ (-𝑗𝑥𝑥𝑗)))
147145, 146mpbid 231 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (-𝑗𝑥𝑥𝑗))
148147simpld 496 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → -𝑗𝑥)
149147simprd 497 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑥𝑗)
150132renegcld 11628 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → -𝑗 ∈ ℝ)
151 elicc2 13376 . . . . . . . . . 10 ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗𝑥𝑥𝑗)))
152150, 132, 151syl2anc 585 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗𝑥𝑥𝑗)))
15380, 148, 149, 152mpbir3and 1343 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗))
154153iftrued 4532 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗))
155 simpr 486 . . . . . . . . . . . . . . . 16 ((𝑚 = 𝑗𝑦 = 𝑥) → 𝑦 = 𝑥)
156155fveq2d 6885 . . . . . . . . . . . . . . 15 ((𝑚 = 𝑗𝑦 = 𝑥) → (𝐹𝑦) = (𝐹𝑥))
157 simpl 484 . . . . . . . . . . . . . . . 16 ((𝑚 = 𝑗𝑦 = 𝑥) → 𝑚 = 𝑗)
158157oveq2d 7412 . . . . . . . . . . . . . . 15 ((𝑚 = 𝑗𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗))
159156, 158oveq12d 7414 . . . . . . . . . . . . . 14 ((𝑚 = 𝑗𝑦 = 𝑥) → ((𝐹𝑦) · (2↑𝑚)) = ((𝐹𝑥) · (2↑𝑗)))
160159fveq2d 6885 . . . . . . . . . . . . 13 ((𝑚 = 𝑗𝑦 = 𝑥) → (⌊‘((𝐹𝑦) · (2↑𝑚))) = (⌊‘((𝐹𝑥) · (2↑𝑗))))
161160, 158oveq12d 7414 . . . . . . . . . . . 12 ((𝑚 = 𝑗𝑦 = 𝑥) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
162 ovex 7429 . . . . . . . . . . . 12 ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V
163161, 3, 162ovmpoa 7550 . . . . . . . . . . 11 ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
16462, 80, 163syl2anc 585 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
165108, 86nndivred 12253 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ)
166 flle 13751 . . . . . . . . . . . . 13 (((𝐹𝑥) · (2↑𝑗)) ∈ ℝ → (⌊‘((𝐹𝑥) · (2↑𝑗))) ≤ ((𝐹𝑥) · (2↑𝑗)))
16799, 166syl 17 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (⌊‘((𝐹𝑥) · (2↑𝑗))) ≤ ((𝐹𝑥) · (2↑𝑗)))
168 ledivmul2 12080 . . . . . . . . . . . . 13 (((⌊‘((𝐹𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 < (2↑𝑗))) → (((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹𝑥) ↔ (⌊‘((𝐹𝑥) · (2↑𝑗))) ≤ ((𝐹𝑥) · (2↑𝑗))))
169108, 64, 87, 113, 168syl112anc 1375 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹𝑥) ↔ (⌊‘((𝐹𝑥) · (2↑𝑗))) ≤ ((𝐹𝑥) · (2↑𝑗))))
170167, 169mpbird 257 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹𝑥))
1719ad2antrr 725 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 𝑥 ∈ ℂ)
172171absge0d 15378 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → 0 ≤ (abs‘𝑥))
17364, 130addge02d 11790 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (0 ≤ (abs‘𝑥) ↔ (𝐹𝑥) ≤ ((abs‘𝑥) + (𝐹𝑥))))
174172, 173mpbid 231 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐹𝑥) ≤ ((abs‘𝑥) + (𝐹𝑥)))
17564, 131, 132, 174, 144letrd 11358 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝐹𝑥) ≤ 𝑗)
176165, 64, 132, 170, 175letrd 11358 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗)
177164, 176eqbrtrd 5166 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗)
178177iftrued 4532 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥))
179178, 164eqtrd 2773 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
180129, 154, 1793eqtrd 2777 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹𝑥) · (2↑𝑗))) / (2↑𝑗)))
181117, 63, 1803brtr4d 5176 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗))
182180, 170eqbrtrd 5166 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥))‘𝑗) ≤ (𝐹𝑥))
18318, 20, 57, 59, 69, 82, 181, 182climsqz 15572 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥))
18417, 183rexlimddv 3162 . . 3 ((𝜑𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥))
185184ralrimiva 3147 . 2 (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥))
18634mptex 7212 . . . 4 (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V
1874, 186eqeltri 2830 . . 3 𝐺 ∈ V
188 feq1 6688 . . . 4 (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫1𝐺:ℕ⟶dom ∫1))
189 fveq1 6880 . . . . . . 7 (𝑔 = 𝐺 → (𝑔𝑛) = (𝐺𝑛))
190189breq2d 5156 . . . . . 6 (𝑔 = 𝐺 → (0𝑝r ≤ (𝑔𝑛) ↔ 0𝑝r ≤ (𝐺𝑛)))
191 fveq1 6880 . . . . . . 7 (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1)))
192189, 191breq12d 5157 . . . . . 6 (𝑔 = 𝐺 → ((𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))
193190, 192anbi12d 632 . . . . 5 (𝑔 = 𝐺 → ((0𝑝r ≤ (𝑔𝑛) ∧ (𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ↔ (0𝑝r ≤ (𝐺𝑛) ∧ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))))
194193ralbidv 3178 . . . 4 (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0𝑝r ≤ (𝑔𝑛) ∧ (𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝐺𝑛) ∧ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))))
195189fveq1d 6883 . . . . . . 7 (𝑔 = 𝐺 → ((𝑔𝑛)‘𝑥) = ((𝐺𝑛)‘𝑥))
196195mpteq2dv 5246 . . . . . 6 (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)))
197196breq1d 5154 . . . . 5 (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) ⇝ (𝐹𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥)))
198197ralbidv 3178 . . . 4 (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) ⇝ (𝐹𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥)))
199188, 194, 1983anbi123d 1437 . . 3 (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝑔𝑛) ∧ (𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) ⇝ (𝐹𝑥)) ↔ (𝐺:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝐺𝑛) ∧ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥))))
200187, 199spcev 3595 . 2 ((𝐺:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝐺𝑛) ∧ (𝐺𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺𝑛)‘𝑥)) ⇝ (𝐹𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝑔𝑛) ∧ (𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) ⇝ (𝐹𝑥)))
2015, 7, 185, 200syl3anc 1372 1 (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝r ≤ (𝑔𝑛) ∧ (𝑔𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔𝑛)‘𝑥)) ⇝ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  wne 2941  wral 3062  wrex 3071  Vcvv 3475  ifcif 4524   class class class wbr 5144  cmpt 5227  dom cdm 5672  wf 6531  cfv 6535  (class class class)co 7396  cmpo 7398  r cofr 7656  cc 11095  cr 11096  0cc0 11097  1c1 11098   + caddc 11100   · cmul 11102  +∞cpnf 11232   < clt 11235  cle 11236  cmin 11431  -cneg 11432   / cdiv 11858  cn 12199  2c2 12254  0cn0 12459  cz 12545  cuz 12809  [,)cico 13313  [,]cicc 13314  cfl 13742  cexp 14014  abscabs 15168  cli 15415  MblFncmbf 25100  1citg1 25101  0𝑝c0p 25155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-inf2 9623  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174  ax-pre-sup 11175
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7657  df-ofr 7658  df-om 7843  df-1st 7962  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8691  df-map 8810  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fi 9393  df-sup 9424  df-inf 9425  df-oi 9492  df-dju 9883  df-card 9921  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859  df-nn 12200  df-2 12262  df-3 12263  df-n0 12460  df-z 12546  df-uz 12810  df-q 12920  df-rp 12962  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-ioo 13315  df-ico 13317  df-icc 13318  df-fz 13472  df-fzo 13615  df-fl 13744  df-seq 13954  df-exp 14015  df-hash 14278  df-cj 15033  df-re 15034  df-im 15035  df-sqrt 15169  df-abs 15170  df-clim 15419  df-rlim 15420  df-sum 15620  df-rest 17355  df-topgen 17376  df-psmet 20910  df-xmet 20911  df-met 20912  df-bl 20913  df-mopn 20914  df-top 22365  df-topon 22382  df-bases 22418  df-cmp 22860  df-ovol 24950  df-vol 24951  df-mbf 25105  df-itg1 25106  df-0p 25156
This theorem is referenced by:  mbfi1fseq  25208
  Copyright terms: Public domain W3C validator