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

Theorem mbfi1fseqlem4 25731
Description: Lemma for mbfi1fseq 25734. This lemma is not as interesting as it is long - it is simply checking that 𝐺 is in fact a sequence of simple functions, by verifying that its range is in (0...𝑛2↑𝑛) / (2↑𝑛) (which is to say, the numbers from 0 to 𝑛 in increments of 1 / (2↑𝑛)), and also that the preimage of each point 𝑘 is measurable, because it is equal to (-𝑛[,]𝑛) ∩ (𝐹 “ (𝑘[,)𝑘 + 1 / (2↑𝑛))) for 𝑘 < 𝑛 and (-𝑛[,]𝑛) ∩ (𝐹 “ (𝑘[,)+∞)) for 𝑘 = 𝑛. (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
mbfi1fseqlem4 (𝜑𝐺:ℕ⟶dom ∫1)
Distinct variable groups:   𝑥,𝑚,𝑦,𝐹   𝑥,𝐺   𝑚,𝐽   𝜑,𝑚,𝑥,𝑦
Allowed substitution hints:   𝐺(𝑦,𝑚)   𝐽(𝑥,𝑦)

Proof of Theorem mbfi1fseqlem4
Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 11245 . . . . 5 ℝ ∈ V
21mptex 7239 . . . 4 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3 mbfi1fseq.4 . . . 4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
42, 3fnmpti 6703 . . 3 𝐺 Fn ℕ
54a1i 11 . 2 (𝜑𝐺 Fn ℕ)
6 mbfi1fseq.1 . . . . . 6 (𝜑𝐹 ∈ MblFn)
7 mbfi1fseq.2 . . . . . 6 (𝜑𝐹:ℝ⟶(0[,)+∞))
8 mbfi1fseq.3 . . . . . 6 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)))
96, 7, 8, 3mbfi1fseqlem3 25730 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10 elfznn0 13643 . . . . . . . . 9 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
1110nn0red 12580 . . . . . . . 8 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12 2nn 12332 . . . . . . . . . 10 2 ∈ ℕ
13 nnnn0 12526 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14 nnexpcl 14089 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1512, 13, 14sylancr 585 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
1615adantl 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17 nndivre 12300 . . . . . . . 8 ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1811, 16, 17syl2anr 595 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1918fmpttd 7128 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
2019frnd 6735 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
219, 20fssd 6744 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ℝ)
22 fzfid 13988 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
2319ffnd 6728 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24 dffn4 6820 . . . . . . 7 ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
2523, 24sylib 217 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
26 fofi 9378 . . . . . 6 (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
2722, 25, 26syl2anc 582 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
289frnd 6735 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
2927, 28ssfid 9304 . . . 4 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ∈ Fin)
306, 7, 8, 3mbfi1fseqlem2 25729 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝐺𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
3130fveq1d 6902 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
3231ad2antlr 725 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33 simpr 483 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34 ovex 7456 . . . . . . . . . . . . . . 15 (𝑛𝐽𝑥) ∈ V
35 vex 3465 . . . . . . . . . . . . . . 15 𝑛 ∈ V
3634, 35ifex 4582 . . . . . . . . . . . . . 14 if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37 c0ex 11254 . . . . . . . . . . . . . 14 0 ∈ V
3836, 37ifex 4582 . . . . . . . . . . . . 13 if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39 eqid 2725 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4039fvmpt2 7019 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4133, 38, 40sylancl 584 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4232, 41eqtrd 2765 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4342adantlr 713 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4443eqeq1d 2727 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45 eldifsni 4798 . . . . . . . . . . . . 13 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ≠ 0)
4645ad2antlr 725 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47 neeq1 2992 . . . . . . . . . . . 12 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
4846, 47syl5ibrcom 246 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
49 iffalse 4541 . . . . . . . . . . . 12 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
5049necon1ai 2957 . . . . . . . . . . 11 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
5148, 50syl6 35 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
5251pm4.71rd 561 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
53 iftrue 4538 . . . . . . . . . . . 12 (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
5453eqeq1d 2727 . . . . . . . . . . 11 (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
5655nnred 12274 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
5756adantr 479 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58 rge0ssre 13482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
59 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60 ffvelcdm 7094 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ (0[,)+∞))
617, 59, 60syl2an 594 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ (0[,)+∞))
6258, 61sselid 3976 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ ℝ)
63 nnnn0 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64 nnexpcl 14089 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
6512, 63, 64sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
6665ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
6766nnred 12274 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
6862, 67remulcld 11290 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹𝑦) · (2↑𝑚)) ∈ ℝ)
69 reflcl 13811 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7170, 66nndivred 12313 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
7271ralrimivva 3190 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
738fmpo 8081 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
7472, 73sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽:(ℕ × ℝ)⟶ℝ)
75 fovcdm 7595 . . . . . . . . . . . . . . . . . . . 20 ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7674, 75syl3an1 1160 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77763expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7877adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7978adantr 479 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80 lemin 13220 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8157, 79, 57, 80syl3anc 1368 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8279, 57ifcld 4578 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
8382, 57letri3d 11402 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84 simpr 483 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
8584eqeq2d 2736 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86 min2 13218 . . . . . . . . . . . . . . . . . 18 (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
8779, 57, 86syl2anc 582 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
8887biantrurd 531 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
8983, 85, 883bitr4d 310 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
9057leidd 11826 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛𝑛)
9190biantrud 530 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
9281, 89, 913bitr4d 310 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ (𝑛𝐽𝑥)))
93 breq1 5155 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝐹𝑥)))
947adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
9594ffvelcdmda 7097 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
96 elrege0 13480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
9795, 96sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
9897simpld 493 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
9998adantlr 713 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
10055, 15syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101100nnred 12274 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
10299, 101remulcld 11290 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) · (2↑𝑛)) ∈ ℝ)
103 reflcl 13811 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
105100nngt0d 12308 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106 lemuldiv 12141 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
10756, 104, 101, 105, 106syl112anc 1371 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
108 lemul1 12113 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
10956, 99, 101, 105, 108syl112anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
110 nnmulcl 12283 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
11155, 15, 110syl2anc2 583 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112111nnzd 12632 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113 flge 13820 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
114102, 112, 113syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
115109, 114bitrd 278 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
116 simpr 483 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
117 simpr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑦 = 𝑥)
118117fveq2d 6904 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (𝐹𝑦) = (𝐹𝑥))
119 simpl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑚 = 𝑛)
120119oveq2d 7439 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121118, 120oveq12d 7441 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 = 𝑛𝑦 = 𝑥) → ((𝐹𝑦) · (2↑𝑚)) = ((𝐹𝑥) · (2↑𝑛)))
122121fveq2d 6904 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑛𝑦 = 𝑥) → (⌊‘((𝐹𝑦) · (2↑𝑚))) = (⌊‘((𝐹𝑥) · (2↑𝑛))))
123122, 120oveq12d 7441 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑛𝑦 = 𝑥) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
124 ovex 7456 . . . . . . . . . . . . . . . . . . 19 ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125123, 8, 124ovmpoa 7580 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
12655, 116, 125syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
127126breq2d 5164 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
128107, 115, 1273bitr4d 310 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
12993, 128sylan9bbr 509 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
130116adantr 479 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
131 iftrue 4538 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132131adantl 480 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133130, 132eleqtrrd 2828 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
134133biantrurd 531 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
13592, 129, 1343bitr2d 306 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
13628ssdifssd 4141 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137136sselda 3978 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139138rnmpt 5960 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140139eqabri 2869 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141 elfzelz 13550 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142141adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143142zcnd 12714 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
14415ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145144nncnd 12275 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146144nnne0d 12309 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147143, 145, 146divcan1d 12038 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148147, 142eqeltrd 2825 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149 oveq1 7430 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150149eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151148, 150syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152151rexlimdva 3144 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
153140, 152biimtrid 241 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
154153imp 405 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
155137, 154syldan 589 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156155adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157 flbi 13831 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158102, 156, 157syl2anc 582 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
159158adantr 479 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
160 neeq1 2992 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛𝑘𝑛))
161160biimparc 478 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162 iffalse 4541 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163162necon1ai 2957 . . . . . . . . . . . . . . . . . . . . . . 23 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165164iftrued 4540 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167165, 166eqtr3d 2767 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168167, 164eqbrtrrd 5176 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘𝑛)
169168, 167jca 510 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170169ex 411 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171 breq1 5155 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛𝑘𝑛))
172171biimparc 478 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173172iftrued 4540 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174 simpr 483 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175173, 174eqtrd 2765 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176170, 175impbid1 224 . . . . . . . . . . . . . . . 16 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177176adantl 480 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178 eldifi 4125 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺𝑛))
179 nnre 12266 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180179ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
18177, 180, 86syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
18213ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183182nn0ge0d 12582 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184 breq1 5155 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185 breq1 5155 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186184, 185ifboth 4571 . . . . . . . . . . . . . . . . . . . . . . 23 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187181, 183, 186syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
18842, 187eqbrtrd 5174 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) ≤ 𝑛)
189188ralrimiva 3135 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛)
1909ffnd 6728 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) Fn ℝ)
191 breq1 5155 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = ((𝐺𝑛)‘𝑥) → (𝑘𝑛 ↔ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
192191ralrn 7101 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
193190, 192syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
194189, 193mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛)
195194r19.21bi 3238 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺𝑛)) → 𝑘𝑛)
196178, 195sylan2 591 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘𝑛)
197196ad2antrr 724 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → 𝑘𝑛)
198197biantrurd 531 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199126eqeq1d 2727 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200104recnd 11288 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℂ)
20128, 20sstrd 3989 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ℝ)
202201ssdifssd 4141 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ℝ)
203202sselda 3978 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204203adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205204recnd 11288 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206100nncnd 12275 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207100nnne0d 12309 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208200, 205, 206, 207divmul3d 12071 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
209199, 208bitrd 278 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
210209adantr 479 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
211177, 198, 2103bitr2d 306 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
212 ifnefalse 4544 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213212eleq2d 2811 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214100nnrecred 12310 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215204, 214readdcld 11289 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216215rexrd 11310 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217 elioomnf 13470 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218216, 217syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
21994ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220219ffnd 6728 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221 elpreima 7070 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223116, 222mpbirand 705 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
22499biantrurd 531 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225218, 223, 2243bitr4d 310 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛)))))
226 ltmul1 12111 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
22799, 215, 101, 105, 226syl112anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
228214recnd 11288 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229206, 207recid2d 12033 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230229oveq2d 7439 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231205, 206, 228, 230joinlmuladdmuld 11287 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232231breq2d 5164 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
233225, 227, 2323bitrd 304 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
234213, 233sylan9bbr 509 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
235 lemul1 12113 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
236204, 99, 101, 105, 235syl112anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
237236adantr 479 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
238234, 237anbi12d 630 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)))))
239238biancomd 462 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
240159, 211, 2393bitr4d 310 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
241135, 240pm2.61dane 3018 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
242 eldif 3956 . . . . . . . . . . . . 13 (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))))
243204rexrd 11310 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244 elioomnf 13470 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
245243, 244syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
246 elpreima 7070 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
247220, 246syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
248116, 247mpbirand 705 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) ∈ (-∞(,)𝑘)))
24999biantrurd 531 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < 𝑘 ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
250245, 248, 2493bitr4d 310 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) < 𝑘))
251250notbid 317 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹𝑥) < 𝑘))
252204, 99lenltd 11406 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ ¬ (𝐹𝑥) < 𝑘))
253251, 252bitr4d 281 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹𝑥)))
254253anbi2d 628 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
255242, 254bitrid 282 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
256241, 255bitr4d 281 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
25754, 256sylan9bbr 509 . . . . . . . . . 10 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
258257pm5.32da 577 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
25944, 52, 2583bitrd 304 . . . . . . . 8 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
260259pm5.32da 577 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
26121adantr 479 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛):ℝ⟶ℝ)
262261ffnd 6728 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
263 fniniseg 7072 . . . . . . . 8 ((𝐺𝑛) Fn ℝ → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
264262, 263syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
265 elin 3962 . . . . . . . 8 (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
266179ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267266renegcld 11687 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268 iccmbl 25578 . . . . . . . . . . . . 13 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
269267, 266, 268syl2anc 582 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
270 mblss 25543 . . . . . . . . . . . 12 ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
271269, 270syl 17 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
272271sseld 3977 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
273272adantrd 490 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
274273pm4.71rd 561 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
275265, 274bitrid 282 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
276260, 264, 2753bitr4d 310 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ 𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
277276eqrdv 2723 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
278 rembl 25552 . . . . . . . . 9 ℝ ∈ dom vol
279 fss 6743 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
2807, 58, 279sylancl 584 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
281 mbfima 25642 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
2826, 280, 281syl2anc 582 . . . . . . . . 9 (𝜑 → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283 ifcl 4577 . . . . . . . . 9 ((ℝ ∈ dom vol ∧ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284278, 282, 283sylancr 585 . . . . . . . 8 (𝜑 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285 mbfima 25642 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
2866, 280, 285syl2anc 582 . . . . . . . 8 (𝜑 → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287 difmbl 25555 . . . . . . . 8 ((if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288284, 286, 287syl2anc 582 . . . . . . 7 (𝜑 → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289288ad2antrr 724 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290 inmbl 25554 . . . . . 6 (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291269, 289, 290syl2anc 582 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292277, 291eqeltrd 2825 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ∈ dom vol)
293 mblvol 25542 . . . . . 6 (((𝐺𝑛) “ {𝑘}) ∈ dom vol → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
294292, 293syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
295190adantr 479 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
296295, 263syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
29777, 180ifcld 4578 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298 0re 11262 . . . . . . . . . . . . . . 15 0 ∈ ℝ
299 ifcl 4577 . . . . . . . . . . . . . . 15 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300297, 298, 299sylancl 584 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
30139fvmpt2 7019 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
30233, 300, 301syl2anc 582 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
30332, 302eqtrd 2765 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304303adantlr 713 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305304eqeq1d 2727 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
306305, 51sylbid 239 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
307306expimpd 452 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
308296, 307sylbid 239 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
309308ssrdv 3984 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
310 iccssre 13455 . . . . . . 7 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
311267, 266, 310syl2anc 582 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
312 mblvol 25542 . . . . . . . 8 ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
313269, 312syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
314 iccvolcl 25579 . . . . . . . 8 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
315267, 266, 314syl2anc 582 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
316313, 315eqeltrrd 2826 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
317 ovolsscl 25498 . . . . . 6 ((((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
318309, 311, 316, 317syl3anc 1368 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
319294, 318eqeltrd 2825 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
32021, 29, 292, 319i1fd 25693 . . 3 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ dom ∫1)
321320ralrimiva 3135 . 2 (𝜑 → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1)
322 ffnfv 7132 . 2 (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1))
3235, 321, 322sylanbrc 581 1 (𝜑𝐺:ℕ⟶dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  Vcvv 3461  cdif 3943  cin 3945  wss 3946  ifcif 4532  {csn 4632   class class class wbr 5152  cmpt 5235   × cxp 5679  ccnv 5680  dom cdm 5681  ran crn 5682  cima 5684   Fn wfn 6548  wf 6549  ontowfo 6551  cfv 6553  (class class class)co 7423  cmpo 7425  Fincfn 8973  cr 11153  0cc0 11154  1c1 11155   + caddc 11157   · cmul 11159  +∞cpnf 11291  -∞cmnf 11292  *cxr 11293   < clt 11294  cle 11295  -cneg 11491   / cdiv 11917  cn 12259  2c2 12314  0cn0 12519  cz 12605  (,)cioo 13373  [,)cico 13375  [,]cicc 13376  ...cfz 13533  cfl 13805  cexp 14076  vol*covol 25474  volcvol 25475  MblFncmbf 25626  1citg1 25627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-inf2 9680  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-se 5637  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-of 7689  df-om 7876  df-1st 8002  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-er 8733  df-map 8856  df-pm 8857  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fi 9450  df-sup 9481  df-inf 9482  df-oi 9549  df-dju 9940  df-card 9978  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-n0 12520  df-z 12606  df-uz 12870  df-q 12980  df-rp 13024  df-xneg 13141  df-xadd 13142  df-xmul 13143  df-ioo 13377  df-ico 13379  df-icc 13380  df-fz 13534  df-fzo 13677  df-fl 13807  df-seq 14017  df-exp 14077  df-hash 14343  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485  df-rlim 15486  df-sum 15686  df-rest 17432  df-topgen 17453  df-psmet 21327  df-xmet 21328  df-met 21329  df-bl 21330  df-mopn 21331  df-top 22879  df-topon 22896  df-bases 22932  df-cmp 23374  df-ovol 25476  df-vol 25477  df-mbf 25631  df-itg1 25632
This theorem is referenced by:  mbfi1fseqlem5  25732  mbfi1fseqlem6  25733
  Copyright terms: Public domain W3C validator