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

Theorem mbfi1fseqlem4 24966
Description: Lemma for mbfi1fseq 24969. 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 11042 . . . . 5 ℝ ∈ V
21mptex 7139 . . . 4 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3 mbfi1fseq.4 . . . 4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
42, 3fnmpti 6614 . . 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 24965 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10 elfznn0 13429 . . . . . . . . 9 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
1110nn0red 12374 . . . . . . . 8 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12 2nn 12126 . . . . . . . . . 10 2 ∈ ℕ
13 nnnn0 12320 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14 nnexpcl 13875 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1512, 13, 14sylancr 587 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
1615adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17 nndivre 12094 . . . . . . . 8 ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1811, 16, 17syl2anr 597 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1918fmpttd 7029 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
2019frnd 6646 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
219, 20fssd 6656 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ℝ)
22 fzfid 13773 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
2319ffnd 6639 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24 dffn4 6732 . . . . . . 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 9182 . . . . . 6 (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
2722, 25, 26syl2anc 584 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
289frnd 6646 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
2927, 28ssfid 9111 . . . 4 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ∈ Fin)
306, 7, 8, 3mbfi1fseqlem2 24964 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝐺𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
3130fveq1d 6814 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
3231ad2antlr 724 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34 ovex 7350 . . . . . . . . . . . . . . 15 (𝑛𝐽𝑥) ∈ V
35 vex 3445 . . . . . . . . . . . . . . 15 𝑛 ∈ V
3634, 35ifex 4521 . . . . . . . . . . . . . 14 if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37 c0ex 11049 . . . . . . . . . . . . . 14 0 ∈ V
3836, 37ifex 4521 . . . . . . . . . . . . 13 if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39 eqid 2737 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4039fvmpt2 6926 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4133, 38, 40sylancl 586 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4232, 41eqtrd 2777 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4342adantlr 712 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4443eqeq1d 2739 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45 eldifsni 4735 . . . . . . . . . . . . 13 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ≠ 0)
4645ad2antlr 724 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47 neeq1 3004 . . . . . . . . . . . 12 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
4846, 47syl5ibrcom 246 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
49 iffalse 4480 . . . . . . . . . . . 12 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
5049necon1ai 2969 . . . . . . . . . . 11 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
5148, 50syl6 35 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
5251pm4.71rd 563 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
53 iftrue 4477 . . . . . . . . . . . 12 (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
5453eqeq1d 2739 . . . . . . . . . . 11 (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55 simpllr 773 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
5655nnred 12068 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
5756adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58 rge0ssre 13268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
59 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60 ffvelcdm 6999 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ (0[,)+∞))
617, 59, 60syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ (0[,)+∞))
6258, 61sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ ℝ)
63 nnnn0 12320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64 nnexpcl 13875 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
6512, 63, 64sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
6665ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
6766nnred 12068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
6862, 67remulcld 11085 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹𝑦) · (2↑𝑚)) ∈ ℝ)
69 reflcl 13596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7170, 66nndivred 12107 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
7271ralrimivva 3194 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
738fmpo 7955 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
7472, 73sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽:(ℕ × ℝ)⟶ℝ)
75 fovcdm 7484 . . . . . . . . . . . . . . . . . . . 20 ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7674, 75syl3an1 1162 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77763expa 1117 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7877adantlr 712 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
7978adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80 lemin 13006 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8157, 79, 57, 80syl3anc 1370 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8279, 57ifcld 4517 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
8382, 57letri3d 11197 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
8584eqeq2d 2748 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86 min2 13004 . . . . . . . . . . . . . . . . . 18 (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
8779, 57, 86syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
8887biantrurd 533 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
8983, 85, 883bitr4d 310 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
9057leidd 11621 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛𝑛)
9190biantrud 532 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
9281, 89, 913bitr4d 310 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ (𝑛𝐽𝑥)))
93 breq1 5090 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝐹𝑥)))
947adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
9594ffvelcdmda 7001 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
96 elrege0 13266 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
9795, 96sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
9897simpld 495 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
9998adantlr 712 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
10055, 15syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101100nnred 12068 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
10299, 101remulcld 11085 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) · (2↑𝑛)) ∈ ℝ)
103 reflcl 13596 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
105100nngt0d 12102 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106 lemuldiv 11935 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
10756, 104, 101, 105, 106syl112anc 1373 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
108 lemul1 11907 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
10956, 99, 101, 105, 108syl112anc 1373 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
110 nnmulcl 12077 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
11155, 15, 110syl2anc2 585 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112111nnzd 12505 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113 flge 13605 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
114102, 112, 113syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
115109, 114bitrd 278 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
116 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
117 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑦 = 𝑥)
118117fveq2d 6816 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (𝐹𝑦) = (𝐹𝑥))
119 simpl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑚 = 𝑛)
120119oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121118, 120oveq12d 7335 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 = 𝑛𝑦 = 𝑥) → ((𝐹𝑦) · (2↑𝑚)) = ((𝐹𝑥) · (2↑𝑛)))
122121fveq2d 6816 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑛𝑦 = 𝑥) → (⌊‘((𝐹𝑦) · (2↑𝑚))) = (⌊‘((𝐹𝑥) · (2↑𝑛))))
123122, 120oveq12d 7335 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑛𝑦 = 𝑥) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
124 ovex 7350 . . . . . . . . . . . . . . . . . . 19 ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125123, 8, 124ovmpoa 7470 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
12655, 116, 125syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
127126breq2d 5099 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
128107, 115, 1273bitr4d 310 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
12993, 128sylan9bbr 511 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
130116adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
131 iftrue 4477 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132131adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133130, 132eleqtrrd 2841 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
134133biantrurd 533 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
13592, 129, 1343bitr2d 306 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
13628ssdifssd 4088 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137136sselda 3931 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139138rnmpt 5884 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140139abeq2i 2874 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141 elfzelz 13336 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142141adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143142zcnd 12507 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
14415ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145144nncnd 12069 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146144nnne0d 12103 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147143, 145, 146divcan1d 11832 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148147, 142eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149 oveq1 7324 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150149eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151148, 150syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152151rexlimdva 3149 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
153140, 152biimtrid 241 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
154153imp 407 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
155137, 154syldan 591 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156155adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157 flbi 13616 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158102, 156, 157syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
159158adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
160 neeq1 3004 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛𝑘𝑛))
161160biimparc 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162 iffalse 4480 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163162necon1ai 2969 . . . . . . . . . . . . . . . . . . . . . . 23 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165164iftrued 4479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167165, 166eqtr3d 2779 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168167, 164eqbrtrrd 5111 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘𝑛)
169168, 167jca 512 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170169ex 413 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171 breq1 5090 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛𝑘𝑛))
172171biimparc 480 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173172iftrued 4479 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175173, 174eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176170, 175impbid1 224 . . . . . . . . . . . . . . . 16 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177176adantl 482 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178 eldifi 4072 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺𝑛))
179 nnre 12060 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180179ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
18177, 180, 86syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
18213ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183182nn0ge0d 12376 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184 breq1 5090 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185 breq1 5090 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186184, 185ifboth 4510 . . . . . . . . . . . . . . . . . . . . . . 23 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187181, 183, 186syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
18842, 187eqbrtrd 5109 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) ≤ 𝑛)
189188ralrimiva 3140 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛)
1909ffnd 6639 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) Fn ℝ)
191 breq1 5090 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = ((𝐺𝑛)‘𝑥) → (𝑘𝑛 ↔ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
192191ralrn 7004 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
193190, 192syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
194189, 193mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛)
195194r19.21bi 3231 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺𝑛)) → 𝑘𝑛)
196178, 195sylan2 593 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘𝑛)
197196ad2antrr 723 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → 𝑘𝑛)
198197biantrurd 533 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199126eqeq1d 2739 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200104recnd 11083 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℂ)
20128, 20sstrd 3941 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ℝ)
202201ssdifssd 4088 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ℝ)
203202sselda 3931 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204203adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205204recnd 11083 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206100nncnd 12069 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207100nnne0d 12103 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208200, 205, 206, 207divmul3d 11865 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
209199, 208bitrd 278 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
210209adantr 481 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
211177, 198, 2103bitr2d 306 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
212 ifnefalse 4483 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213212eleq2d 2823 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214100nnrecred 12104 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215204, 214readdcld 11084 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216215rexrd 11105 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217 elioomnf 13256 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218216, 217syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
21994ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220219ffnd 6639 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221 elpreima 6975 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223116, 222mpbirand 704 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
22499biantrurd 533 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225218, 223, 2243bitr4d 310 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛)))))
226 ltmul1 11905 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
22799, 215, 101, 105, 226syl112anc 1373 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
228214recnd 11083 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229206, 207recid2d 11827 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230229oveq2d 7333 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231205, 206, 228, 230joinlmuladdmuld 11082 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232231breq2d 5099 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
233225, 227, 2323bitrd 304 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
234213, 233sylan9bbr 511 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
235 lemul1 11907 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
236204, 99, 101, 105, 235syl112anc 1373 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
237236adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
238234, 237anbi12d 631 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)))))
239238biancomd 464 . . . . . . . . . . . . . 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 3030 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
242 eldif 3907 . . . . . . . . . . . . 13 (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))))
243204rexrd 11105 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244 elioomnf 13256 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
245243, 244syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
246 elpreima 6975 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
247220, 246syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
248116, 247mpbirand 704 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) ∈ (-∞(,)𝑘)))
24999biantrurd 533 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < 𝑘 ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
250245, 248, 2493bitr4d 310 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) < 𝑘))
251250notbid 317 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹𝑥) < 𝑘))
252204, 99lenltd 11201 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ ¬ (𝐹𝑥) < 𝑘))
253251, 252bitr4d 281 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹𝑥)))
254253anbi2d 629 . . . . . . . . . . . . 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 511 . . . . . . . . . 10 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
258257pm5.32da 579 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
25944, 52, 2583bitrd 304 . . . . . . . 8 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
260259pm5.32da 579 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
26121adantr 481 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛):ℝ⟶ℝ)
262261ffnd 6639 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
263 fniniseg 6977 . . . . . . . 8 ((𝐺𝑛) Fn ℝ → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
264262, 263syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
265 elin 3913 . . . . . . . 8 (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
266179ad2antlr 724 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267266renegcld 11482 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268 iccmbl 24813 . . . . . . . . . . . . 13 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
269267, 266, 268syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
270 mblss 24778 . . . . . . . . . . . 12 ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
271269, 270syl 17 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
272271sseld 3930 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
273272adantrd 492 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
274273pm4.71rd 563 . . . . . . . 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 2735 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
278 rembl 24787 . . . . . . . . 9 ℝ ∈ dom vol
279 fss 6655 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
2807, 58, 279sylancl 586 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
281 mbfima 24877 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
2826, 280, 281syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283 ifcl 4516 . . . . . . . . 9 ((ℝ ∈ dom vol ∧ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284278, 282, 283sylancr 587 . . . . . . . 8 (𝜑 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285 mbfima 24877 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
2866, 280, 285syl2anc 584 . . . . . . . 8 (𝜑 → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287 difmbl 24790 . . . . . . . 8 ((if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288284, 286, 287syl2anc 584 . . . . . . 7 (𝜑 → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289288ad2antrr 723 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290 inmbl 24789 . . . . . 6 (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291269, 289, 290syl2anc 584 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292277, 291eqeltrd 2838 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ∈ dom vol)
293 mblvol 24777 . . . . . 6 (((𝐺𝑛) “ {𝑘}) ∈ dom vol → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
294292, 293syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
295190adantr 481 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
296295, 263syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
29777, 180ifcld 4517 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298 0re 11057 . . . . . . . . . . . . . . 15 0 ∈ ℝ
299 ifcl 4516 . . . . . . . . . . . . . . 15 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300297, 298, 299sylancl 586 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
30139fvmpt2 6926 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
30233, 300, 301syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
30332, 302eqtrd 2777 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304303adantlr 712 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305304eqeq1d 2739 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
306305, 51sylbid 239 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
307306expimpd 454 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
308296, 307sylbid 239 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
309308ssrdv 3937 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
310 iccssre 13241 . . . . . . 7 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
311267, 266, 310syl2anc 584 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
312 mblvol 24777 . . . . . . . 8 ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
313269, 312syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
314 iccvolcl 24814 . . . . . . . 8 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
315267, 266, 314syl2anc 584 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
316313, 315eqeltrrd 2839 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
317 ovolsscl 24733 . . . . . 6 ((((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
318309, 311, 316, 317syl3anc 1370 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
319294, 318eqeltrd 2838 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
32021, 29, 292, 319i1fd 24928 . . 3 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ dom ∫1)
321320ralrimiva 3140 . 2 (𝜑 → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1)
322 ffnfv 7032 . 2 (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1))
3235, 321, 322sylanbrc 583 1 (𝜑𝐺:ℕ⟶dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wne 2941  wral 3062  wrex 3071  Vcvv 3441  cdif 3894  cin 3896  wss 3897  ifcif 4471  {csn 4571   class class class wbr 5087  cmpt 5170   × cxp 5606  ccnv 5607  dom cdm 5608  ran crn 5609  cima 5611   Fn wfn 6461  wf 6462  ontowfo 6464  cfv 6466  (class class class)co 7317  cmpo 7319  Fincfn 8783  cr 10950  0cc0 10951  1c1 10952   + caddc 10954   · cmul 10956  +∞cpnf 11086  -∞cmnf 11087  *cxr 11088   < clt 11089  cle 11090  -cneg 11286   / cdiv 11712  cn 12053  2c2 12108  0cn0 12313  cz 12399  (,)cioo 13159  [,)cico 13161  [,]cicc 13162  ...cfz 13319  cfl 13590  cexp 13862  vol*covol 24709  volcvol 24710  MblFncmbf 24861  1citg1 24862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-inf2 9477  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-pre-sup 11029
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-of 7575  df-om 7760  df-1st 7878  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-2o 8347  df-er 8548  df-map 8667  df-pm 8668  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fi 9247  df-sup 9278  df-inf 9279  df-oi 9346  df-dju 9737  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-2 12116  df-3 12117  df-n0 12314  df-z 12400  df-uz 12663  df-q 12769  df-rp 12811  df-xneg 12928  df-xadd 12929  df-xmul 12930  df-ioo 13163  df-ico 13165  df-icc 13166  df-fz 13320  df-fzo 13463  df-fl 13592  df-seq 13802  df-exp 13863  df-hash 14125  df-cj 14889  df-re 14890  df-im 14891  df-sqrt 15025  df-abs 15026  df-clim 15276  df-rlim 15277  df-sum 15477  df-rest 17210  df-topgen 17231  df-psmet 20672  df-xmet 20673  df-met 20674  df-bl 20675  df-mopn 20676  df-top 22126  df-topon 22143  df-bases 22179  df-cmp 22621  df-ovol 24711  df-vol 24712  df-mbf 24866  df-itg1 24867
This theorem is referenced by:  mbfi1fseqlem5  24967  mbfi1fseqlem6  24968
  Copyright terms: Public domain W3C validator