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

Theorem mbfi1fseqlem4 24326
Description: Lemma for mbfi1fseq 24329. 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 10621 . . . . 5 ℝ ∈ V
21mptex 6967 . . . 4 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3 mbfi1fseq.4 . . . 4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
42, 3fnmpti 6467 . . 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 24325 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10 elfznn0 12999 . . . . . . . . 9 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
1110nn0red 11948 . . . . . . . 8 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12 2nn 11702 . . . . . . . . . 10 2 ∈ ℕ
13 nnnn0 11896 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14 nnexpcl 13442 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1512, 13, 14sylancr 590 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
1615adantl 485 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17 nndivre 11670 . . . . . . . 8 ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1811, 16, 17syl2anr 599 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1918fmpttd 6860 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
2019frnd 6498 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
219, 20fssd 6506 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ℝ)
22 fzfid 13340 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
2319ffnd 6492 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24 dffn4 6575 . . . . . . 7 ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
2523, 24sylib 221 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
26 fofi 8798 . . . . . 6 (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
2722, 25, 26syl2anc 587 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
289frnd 6498 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
2927, 28ssfid 8729 . . . 4 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ∈ Fin)
306, 7, 8, 3mbfi1fseqlem2 24324 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝐺𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
3130fveq1d 6651 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
3231ad2antlr 726 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34 ovex 7172 . . . . . . . . . . . . . . 15 (𝑛𝐽𝑥) ∈ V
35 vex 3447 . . . . . . . . . . . . . . 15 𝑛 ∈ V
3634, 35ifex 4476 . . . . . . . . . . . . . 14 if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37 c0ex 10628 . . . . . . . . . . . . . 14 0 ∈ V
3836, 37ifex 4476 . . . . . . . . . . . . 13 if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39 eqid 2801 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4039fvmpt2 6760 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4133, 38, 40sylancl 589 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4232, 41eqtrd 2836 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4342adantlr 714 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4443eqeq1d 2803 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45 eldifsni 4686 . . . . . . . . . . . . 13 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ≠ 0)
4645ad2antlr 726 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47 neeq1 3052 . . . . . . . . . . . 12 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
4846, 47syl5ibrcom 250 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
49 iffalse 4437 . . . . . . . . . . . 12 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
5049necon1ai 3017 . . . . . . . . . . 11 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
5148, 50syl6 35 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
5251pm4.71rd 566 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
53 iftrue 4434 . . . . . . . . . . . 12 (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
5453eqeq1d 2803 . . . . . . . . . . 11 (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
5655nnred 11644 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
5756adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58 rge0ssre 12838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
59 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60 ffvelrn 6830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ (0[,)+∞))
617, 59, 60syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ (0[,)+∞))
6258, 61sseldi 3916 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ ℝ)
63 nnnn0 11896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64 nnexpcl 13442 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
6512, 63, 64sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
6665ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
6766nnred 11644 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
6862, 67remulcld 10664 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹𝑦) · (2↑𝑚)) ∈ ℝ)
69 reflcl 13165 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7170, 66nndivred 11683 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
7271ralrimivva 3159 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
738fmpo 7752 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
7472, 73sylib 221 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽:(ℕ × ℝ)⟶ℝ)
75 fovrn 7302 . . . . . . . . . . . . . . . . . . . 20 ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7674, 75syl3an1 1160 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77763expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7877adantlr 714 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7978adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80 lemin 12577 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8157, 79, 57, 80syl3anc 1368 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8279, 57ifcld 4473 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
8382, 57letri3d 10775 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84 simpr 488 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
8584eqeq2d 2812 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86 min2 12575 . . . . . . . . . . . . . . . . . 18 (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
8779, 57, 86syl2anc 587 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
8887biantrurd 536 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
8983, 85, 883bitr4d 314 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
9057leidd 11199 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛𝑛)
9190biantrud 535 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
9281, 89, 913bitr4d 314 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ (𝑛𝐽𝑥)))
93 breq1 5036 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝐹𝑥)))
947adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
9594ffvelrnda 6832 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
96 elrege0 12836 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
9795, 96sylib 221 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
9897simpld 498 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
9998adantlr 714 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
10055, 15syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101100nnred 11644 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
10299, 101remulcld 10664 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) · (2↑𝑛)) ∈ ℝ)
103 reflcl 13165 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
105100nngt0d 11678 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106 lemuldiv 11513 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
10756, 104, 101, 105, 106syl112anc 1371 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
108 lemul1 11485 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
10956, 99, 101, 105, 108syl112anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
110 nnmulcl 11653 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
11155, 15, 110syl2anc2 588 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112111nnzd 12078 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113 flge 13174 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
114102, 112, 113syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
115109, 114bitrd 282 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
116 simpr 488 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
117 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑦 = 𝑥)
118117fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (𝐹𝑦) = (𝐹𝑥))
119 simpl 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑚 = 𝑛)
120119oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121118, 120oveq12d 7157 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 = 𝑛𝑦 = 𝑥) → ((𝐹𝑦) · (2↑𝑚)) = ((𝐹𝑥) · (2↑𝑛)))
122121fveq2d 6653 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑛𝑦 = 𝑥) → (⌊‘((𝐹𝑦) · (2↑𝑚))) = (⌊‘((𝐹𝑥) · (2↑𝑛))))
123122, 120oveq12d 7157 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑛𝑦 = 𝑥) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
124 ovex 7172 . . . . . . . . . . . . . . . . . . 19 ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125123, 8, 124ovmpoa 7288 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
12655, 116, 125syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
127126breq2d 5045 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
128107, 115, 1273bitr4d 314 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
12993, 128sylan9bbr 514 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
130116adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
131 iftrue 4434 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132131adantl 485 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133130, 132eleqtrrd 2896 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
134133biantrurd 536 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
13592, 129, 1343bitr2d 310 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
13628ssdifssd 4073 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137136sselda 3918 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139138rnmpt 5795 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140139abeq2i 2928 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142141adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143142zcnd 12080 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
14415ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145144nncnd 11645 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146144nnne0d 11679 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147143, 145, 146divcan1d 11410 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148147, 142eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149 oveq1 7146 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150149eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151148, 150syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152151rexlimdva 3246 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
153140, 152syl5bi 245 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
154153imp 410 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
155137, 154syldan 594 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156155adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157 flbi 13185 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158102, 156, 157syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
159158adantr 484 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
160 neeq1 3052 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛𝑘𝑛))
161160biimparc 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162 iffalse 4437 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163162necon1ai 3017 . . . . . . . . . . . . . . . . . . . . . . 23 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165164iftrued 4436 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167165, 166eqtr3d 2838 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168167, 164eqbrtrrd 5057 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘𝑛)
169168, 167jca 515 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170169ex 416 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171 breq1 5036 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛𝑘𝑛))
172171biimparc 483 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173172iftrued 4436 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174 simpr 488 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175173, 174eqtrd 2836 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176170, 175impbid1 228 . . . . . . . . . . . . . . . 16 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177176adantl 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178 eldifi 4057 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺𝑛))
179 nnre 11636 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180179ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
18177, 180, 86syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
18213ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183182nn0ge0d 11950 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184 breq1 5036 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185 breq1 5036 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186184, 185ifboth 4466 . . . . . . . . . . . . . . . . . . . . . . 23 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187181, 183, 186syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
18842, 187eqbrtrd 5055 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) ≤ 𝑛)
189188ralrimiva 3152 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛)
1909ffnd 6492 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) Fn ℝ)
191 breq1 5036 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = ((𝐺𝑛)‘𝑥) → (𝑘𝑛 ↔ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
192191ralrn 6835 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
193190, 192syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
194189, 193mpbird 260 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛)
195194r19.21bi 3176 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺𝑛)) → 𝑘𝑛)
196178, 195sylan2 595 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘𝑛)
197196ad2antrr 725 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → 𝑘𝑛)
198197biantrurd 536 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199126eqeq1d 2803 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200104recnd 10662 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℂ)
20128, 20sstrd 3928 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ℝ)
202201ssdifssd 4073 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ℝ)
203202sselda 3918 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204203adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205204recnd 10662 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206100nncnd 11645 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207100nnne0d 11679 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208200, 205, 206, 207divmul3d 11443 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
209199, 208bitrd 282 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
210209adantr 484 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
211177, 198, 2103bitr2d 310 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
212 ifnefalse 4440 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213212eleq2d 2878 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214100nnrecred 11680 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215204, 214readdcld 10663 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216215rexrd 10684 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217 elioomnf 12826 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218216, 217syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
21994ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220219ffnd 6492 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221 elpreima 6809 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223116, 222mpbirand 706 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
22499biantrurd 536 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225218, 223, 2243bitr4d 314 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛)))))
226 ltmul1 11483 . . . . . . . . . . . . . . . . . . 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 10662 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229206, 207recid2d 11405 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230229oveq2d 7155 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231205, 206, 228, 230joinlmuladdmuld 10661 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232231breq2d 5045 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
233225, 227, 2323bitrd 308 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
234213, 233sylan9bbr 514 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
235 lemul1 11485 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
236204, 99, 101, 105, 235syl112anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
237236adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
238234, 237anbi12d 633 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)))))
239238biancomd 467 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
240159, 211, 2393bitr4d 314 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
241135, 240pm2.61dane 3077 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
242 eldif 3894 . . . . . . . . . . . . 13 (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))))
243204rexrd 10684 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244 elioomnf 12826 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
245243, 244syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
246 elpreima 6809 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
247220, 246syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
248116, 247mpbirand 706 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) ∈ (-∞(,)𝑘)))
24999biantrurd 536 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < 𝑘 ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
250245, 248, 2493bitr4d 314 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) < 𝑘))
251250notbid 321 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹𝑥) < 𝑘))
252204, 99lenltd 10779 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ ¬ (𝐹𝑥) < 𝑘))
253251, 252bitr4d 285 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹𝑥)))
254253anbi2d 631 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
255242, 254syl5bb 286 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
256241, 255bitr4d 285 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
25754, 256sylan9bbr 514 . . . . . . . . . 10 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
258257pm5.32da 582 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
25944, 52, 2583bitrd 308 . . . . . . . 8 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
260259pm5.32da 582 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
26121adantr 484 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛):ℝ⟶ℝ)
262261ffnd 6492 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
263 fniniseg 6811 . . . . . . . 8 ((𝐺𝑛) Fn ℝ → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
264262, 263syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
265 elin 3900 . . . . . . . 8 (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
266179ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267266renegcld 11060 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268 iccmbl 24174 . . . . . . . . . . . . 13 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
269267, 266, 268syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
270 mblss 24139 . . . . . . . . . . . 12 ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
271269, 270syl 17 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
272271sseld 3917 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
273272adantrd 495 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
274273pm4.71rd 566 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
275265, 274syl5bb 286 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
276260, 264, 2753bitr4d 314 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ 𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
277276eqrdv 2799 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
278 rembl 24148 . . . . . . . . 9 ℝ ∈ dom vol
279 fss 6505 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
2807, 58, 279sylancl 589 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
281 mbfima 24238 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
2826, 280, 281syl2anc 587 . . . . . . . . 9 (𝜑 → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283 ifcl 4472 . . . . . . . . 9 ((ℝ ∈ dom vol ∧ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284278, 282, 283sylancr 590 . . . . . . . 8 (𝜑 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285 mbfima 24238 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
2866, 280, 285syl2anc 587 . . . . . . . 8 (𝜑 → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287 difmbl 24151 . . . . . . . 8 ((if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288284, 286, 287syl2anc 587 . . . . . . 7 (𝜑 → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289288ad2antrr 725 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290 inmbl 24150 . . . . . 6 (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291269, 289, 290syl2anc 587 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292277, 291eqeltrd 2893 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ∈ dom vol)
293 mblvol 24138 . . . . . 6 (((𝐺𝑛) “ {𝑘}) ∈ dom vol → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
294292, 293syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
295190adantr 484 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
296295, 263syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
29777, 180ifcld 4473 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298 0re 10636 . . . . . . . . . . . . . . 15 0 ∈ ℝ
299 ifcl 4472 . . . . . . . . . . . . . . 15 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300297, 298, 299sylancl 589 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
30139fvmpt2 6760 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
30233, 300, 301syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
30332, 302eqtrd 2836 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304303adantlr 714 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305304eqeq1d 2803 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
306305, 51sylbid 243 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
307306expimpd 457 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
308296, 307sylbid 243 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
309308ssrdv 3924 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
310 iccssre 12811 . . . . . . 7 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
311267, 266, 310syl2anc 587 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
312 mblvol 24138 . . . . . . . 8 ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
313269, 312syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
314 iccvolcl 24175 . . . . . . . 8 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
315267, 266, 314syl2anc 587 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
316313, 315eqeltrrd 2894 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
317 ovolsscl 24094 . . . . . 6 ((((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
318309, 311, 316, 317syl3anc 1368 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
319294, 318eqeltrd 2893 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
32021, 29, 292, 319i1fd 24289 . . 3 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ dom ∫1)
321320ralrimiva 3152 . 2 (𝜑 → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1)
322 ffnfv 6863 . 2 (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1))
3235, 321, 322sylanbrc 586 1 (𝜑𝐺:ℕ⟶dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  wne 2990  wral 3109  wrex 3110  Vcvv 3444  cdif 3881  cin 3883  wss 3884  ifcif 4428  {csn 4528   class class class wbr 5033  cmpt 5113   × cxp 5521  ccnv 5522  dom cdm 5523  ran crn 5524  cima 5526   Fn wfn 6323  wf 6324  ontowfo 6326  cfv 6328  (class class class)co 7139  cmpo 7141  Fincfn 8496  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  +∞cpnf 10665  -∞cmnf 10666  *cxr 10667   < clt 10668  cle 10669  -cneg 10864   / cdiv 11290  cn 11629  2c2 11684  0cn0 11889  cz 11973  (,)cioo 12730  [,)cico 12732  [,]cicc 12733  ...cfz 12889  cfl 13159  cexp 13429  vol*covol 24070  volcvol 24071  MblFncmbf 24222  1citg1 24223
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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-rlim 14842  df-sum 15039  df-rest 16692  df-topgen 16713  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21503  df-topon 21520  df-bases 21555  df-cmp 21996  df-ovol 24072  df-vol 24073  df-mbf 24227  df-itg1 24228
This theorem is referenced by:  mbfi1fseqlem5  24327  mbfi1fseqlem6  24328
  Copyright terms: Public domain W3C validator