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

Theorem mbfi1fseqlem4 23391
Description: Lemma for mbfi1fseq 23394. 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 9971 . . . . 5 ℝ ∈ V
21mptex 6440 . . . 4 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3 mbfi1fseq.4 . . . 4 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
42, 3fnmpti 5979 . . 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 23390 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10 elfznn0 12374 . . . . . . . . 9 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
1110nn0red 11296 . . . . . . . 8 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12 2nn 11129 . . . . . . . . . 10 2 ∈ ℕ
13 nnnn0 11243 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14 nnexpcl 12813 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1512, 13, 14sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
1615adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17 nndivre 11000 . . . . . . . 8 ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
1811, 16, 17syl2anr 495 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
19 eqid 2621 . . . . . . 7 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
2018, 19fmptd 6340 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
21 frn 6010 . . . . . 6 ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
2220, 21syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
239, 22fssd 6014 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛):ℝ⟶ℝ)
24 fzfid 12712 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
25 ffn 6002 . . . . . . . 8 ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
2620, 25syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
27 dffn4 6078 . . . . . . 7 ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
2826, 27sylib 208 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
29 fofi 8196 . . . . . 6 (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
3024, 28, 29syl2anc 692 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
31 frn 6010 . . . . . 6 ((𝐺𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → ran (𝐺𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
329, 31syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
33 ssfi 8124 . . . . 5 ((ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin ∧ ran (𝐺𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝐺𝑛) ∈ Fin)
3430, 32, 33syl2anc 692 . . . 4 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ∈ Fin)
356, 7, 8, 3mbfi1fseqlem2 23389 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝐺𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
3635fveq1d 6150 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
3736ad2antlr 762 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
38 simpr 477 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
39 ovex 6632 . . . . . . . . . . . . . . 15 (𝑛𝐽𝑥) ∈ V
40 vex 3189 . . . . . . . . . . . . . . 15 𝑛 ∈ V
4139, 40ifex 4128 . . . . . . . . . . . . . 14 if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
42 c0ex 9978 . . . . . . . . . . . . . 14 0 ∈ V
4341, 42ifex 4128 . . . . . . . . . . . . 13 if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
44 eqid 2621 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4544fvmpt2 6248 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4638, 43, 45sylancl 693 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4737, 46eqtrd 2655 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4847adantlr 750 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
4948eqeq1d 2623 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
50 eldifsni 4289 . . . . . . . . . . . . 13 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ≠ 0)
5150ad2antlr 762 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
52 neeq1 2852 . . . . . . . . . . . 12 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
5351, 52syl5ibrcom 237 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
54 iffalse 4067 . . . . . . . . . . . 12 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
5554necon1ai 2817 . . . . . . . . . . 11 (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
5653, 55syl6 35 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
5756pm4.71rd 666 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
58 iftrue 4064 . . . . . . . . . . . 12 (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
5958eqeq1d 2623 . . . . . . . . . . 11 (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
60 simpllr 798 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
6160nnred 10979 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
6261adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
63 rge0ssre 12222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
64 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
65 ffvelrn 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ (0[,)+∞))
667, 64, 65syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ (0[,)+∞))
6763, 66sseldi 3581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹𝑦) ∈ ℝ)
68 nnnn0 11243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
69 nnexpcl 12813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
7012, 68, 69sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
7170ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
7271nnred 10979 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
7367, 72remulcld 10014 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹𝑦) · (2↑𝑚)) ∈ ℝ)
74 reflcl 12537 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹𝑦) · (2↑𝑚))) ∈ ℝ)
7675, 71nndivred 11013 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
7776ralrimivva 2965 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
788fmpt2 7182 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
7977, 78sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽:(ℕ × ℝ)⟶ℝ)
80 fovrn 6757 . . . . . . . . . . . . . . . . . . . 20 ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
8179, 80syl3an1 1356 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
82813expa 1262 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
8382adantlr 750 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
8483adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
85 lemin 11966 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8662, 84, 62, 85syl3anc 1323 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
8784, 62ifcld 4103 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
8887, 62letri3d 10123 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
89 simpr 477 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
9089eqeq2d 2631 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
91 min2 11964 . . . . . . . . . . . . . . . . . 18 (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
9284, 62, 91syl2anc 692 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
9392biantrurd 529 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
9488, 90, 933bitr4d 300 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
9562leidd 10538 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛𝑛)
9695biantrud 528 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛𝑛)))
9786, 94, 963bitr4d 300 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑛 ≤ (𝑛𝐽𝑥)))
98 breq1 4616 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝐹𝑥)))
997adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
10099ffvelrnda 6315 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
101 elrege0 12220 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
102100, 101sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
103102simpld 475 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
104103adantlr 750 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
10560, 15syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
106105nnred 10979 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
107104, 106remulcld 10014 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) · (2↑𝑛)) ∈ ℝ)
108 reflcl 12537 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
109107, 108syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ)
110105nngt0d 11008 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
111 lemuldiv 10847 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
11261, 109, 106, 110, 111syl112anc 1327 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
113 lemul1 10819 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
11461, 104, 106, 110, 113syl112anc 1327 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
115 nnmulcl 10987 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
11615, 115mpdan 701 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 · (2↑𝑛)) ∈ ℕ)
11760, 116syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
118117nnzd 11425 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
119 flge 12546 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
120107, 118, 119syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
121114, 120bitrd 268 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹𝑥) · (2↑𝑛)))))
122 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
123 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑦 = 𝑥)
124123fveq2d 6152 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (𝐹𝑦) = (𝐹𝑥))
125 simpl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑛𝑦 = 𝑥) → 𝑚 = 𝑛)
126125oveq2d 6620 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑛𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
127124, 126oveq12d 6622 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 = 𝑛𝑦 = 𝑥) → ((𝐹𝑦) · (2↑𝑚)) = ((𝐹𝑥) · (2↑𝑛)))
128127fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑛𝑦 = 𝑥) → (⌊‘((𝐹𝑦) · (2↑𝑚))) = (⌊‘((𝐹𝑥) · (2↑𝑛))))
129128, 126oveq12d 6622 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑛𝑦 = 𝑥) → ((⌊‘((𝐹𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
130 ovex 6632 . . . . . . . . . . . . . . . . . . 19 ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
131129, 8, 130ovmpt2a 6744 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
13260, 122, 131syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)))
133132breq2d 4625 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛))))
134112, 121, 1333bitr4d 300 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
13598, 134sylan9bbr 736 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
136122adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
137 iftrue 4064 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
138137adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
139136, 138eleqtrrd 2701 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
140139biantrurd 529 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
14197, 135, 1403bitr2d 296 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
14232ssdifssd 3726 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
143142sselda 3583 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
14419rnmpt 5331 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
145144abeq2i 2732 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
146 elfzelz 12284 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
147146adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
148147zcnd 11427 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
14915ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
150149nncnd 10980 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
151149nnne0d 11009 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
152148, 150, 151divcan1d 10746 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
153152, 147eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
154 oveq1 6611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
155154eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
156153, 155syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
157156rexlimdva 3024 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
158145, 157syl5bi 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
159158imp 445 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
160143, 159syldan 487 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
161160adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
162 flbi 12557 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
163107, 161, 162syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
164163adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
165 neeq1 2852 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛𝑘𝑛))
166165biimparc 504 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
167 iffalse 4067 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
168167necon1ai 2817 . . . . . . . . . . . . . . . . . . . . . . 23 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
169166, 168syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
170169iftrued 4066 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
171 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
172170, 171eqtr3d 2657 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
173172, 169eqbrtrrd 4637 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘𝑛)
174173, 172jca 554 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
175174ex 450 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
176 breq1 4616 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛𝑘𝑛))
177176biimparc 504 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
178177iftrued 4066 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
179 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
180178, 179eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
181175, 180impbid1 215 . . . . . . . . . . . . . . . 16 (𝑘𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
182181adantl 482 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
183 eldifi 3710 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (ran (𝐺𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺𝑛))
184 nnre 10971 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
185184ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
18682, 185, 91syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
18713ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
188187nn0ge0d 11298 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
189 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . 24 (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
190 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
191189, 190ifboth 4096 . . . . . . . . . . . . . . . . . . . . . . 23 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
192186, 188, 191syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
19347, 192eqbrtrd 4635 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) ≤ 𝑛)
194193ralrimiva 2960 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛)
195 ffn 6002 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑛):ℝ⟶ℝ → (𝐺𝑛) Fn ℝ)
19623, 195syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) Fn ℝ)
197 breq1 4616 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = ((𝐺𝑛)‘𝑥) → (𝑘𝑛 ↔ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
198197ralrn 6318 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
199196, 198syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺𝑛)‘𝑥) ≤ 𝑛))
200194, 199mpbird 247 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺𝑛)𝑘𝑛)
201200r19.21bi 2927 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺𝑛)) → 𝑘𝑛)
202183, 201sylan2 491 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘𝑛)
203202ad2antrr 761 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → 𝑘𝑛)
204203biantrurd 529 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
205132eqeq1d 2623 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
206109recnd 10012 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) · (2↑𝑛))) ∈ ℂ)
20732, 22sstrd 3593 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → ran (𝐺𝑛) ⊆ ℝ)
208207ssdifssd 3726 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (ran (𝐺𝑛) ∖ {0}) ⊆ ℝ)
209208sselda 3583 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
210209adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
211210recnd 10012 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
212105nncnd 10980 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
213105nnne0d 11009 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
214206, 211, 212, 213divmul3d 10779 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
215205, 214bitrd 268 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
216215adantr 481 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
217182, 204, 2163bitr2d 296 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
218 ifnefalse 4070 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
219218eleq2d 2684 . . . . . . . . . . . . . . . . 17 (𝑘𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
220105nnrecred 11010 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
221210, 220readdcld 10013 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
222221rexrd 10033 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
223 elioomnf 12210 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
224222, 223syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
22599ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
226 ffn 6002 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:ℝ⟶(0[,)+∞) → 𝐹 Fn ℝ)
227225, 226syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
228 elpreima 6293 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
229227, 228syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
230122biantrurd 529 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
231229, 230bitr4d 271 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
232104biantrurd 529 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))))))
233224, 231, 2323bitr4d 300 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹𝑥) < (𝑘 + (1 / (2↑𝑛)))))
234 ltmul1 10817 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
235104, 221, 106, 110, 234syl112anc 1327 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
236220recnd 10012 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
237211, 236, 212adddird 10009 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))))
238212, 213recid2d 10741 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
239238oveq2d 6620 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
240237, 239eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
241240breq2d 4625 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
242233, 235, 2413bitrd 294 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
243219, 242sylan9bbr 736 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
244 lemul1 10819 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℝ ∧ (𝐹𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
245210, 104, 106, 110, 244syl112anc 1327 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
246245adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (𝑘 ≤ (𝐹𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))))
247243, 246anbi12d 746 . . . . . . . . . . . . . . 15 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ (((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)))))
248 ancom 466 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛))) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
249247, 248syl6bb 276 . . . . . . . . . . . . . 14 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹𝑥) · (2↑𝑛)) ∧ ((𝐹𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
250164, 217, 2493bitr4d 300 . . . . . . . . . . . . 13 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
251141, 250pm2.61dane 2877 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
252 eldif 3565 . . . . . . . . . . . . 13 (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))))
253210rexrd 10033 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
254 elioomnf 12210 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
255253, 254syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
256 elpreima 6293 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℝ → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
257227, 256syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
258122biantrurd 529 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝐹𝑥) ∈ (-∞(,)𝑘))))
259257, 258bitr4d 271 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) ∈ (-∞(,)𝑘)))
260104biantrurd 529 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < 𝑘 ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < 𝑘)))
261255, 259, 2603bitr4d 300 . . . . . . . . . . . . . . . 16 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ (𝐹𝑥) < 𝑘))
262261notbid 308 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹𝑥) < 𝑘))
263210, 104lenltd 10127 . . . . . . . . . . . . . . 15 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹𝑥) ↔ ¬ (𝐹𝑥) < 𝑘))
264262, 263bitr4d 271 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹𝑥)))
265264anbi2d 739 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
266252, 265syl5bb 272 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹𝑥))))
267251, 266bitr4d 271 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
26859, 267sylan9bbr 736 . . . . . . . . . 10 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
269268pm5.32da 672 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
27049, 57, 2693bitrd 294 . . . . . . . 8 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
271270pm5.32da 672 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
27223adantr 481 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛):ℝ⟶ℝ)
273272, 195syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
274 fniniseg 6294 . . . . . . . 8 ((𝐺𝑛) Fn ℝ → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
275273, 274syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
276 elin 3774 . . . . . . . 8 (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
277184ad2antlr 762 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
278277renegcld 10401 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
279 iccmbl 23241 . . . . . . . . . . . . 13 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
280278, 277, 279syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
281 mblss 23206 . . . . . . . . . . . 12 ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
282280, 281syl 17 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
283282sseld 3582 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
284283adantrd 484 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
285284pm4.71rd 666 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
286276, 285syl5bb 272 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))))
287271, 275, 2863bitr4d 300 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ 𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))))))
288287eqrdv 2619 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))))
289 rembl 23215 . . . . . . . . 9 ℝ ∈ dom vol
290 fss 6013 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
2917, 63, 290sylancl 693 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
292 mbfima 23305 . . . . . . . . . 10 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
2936, 291, 292syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
294 ifcl 4102 . . . . . . . . 9 ((ℝ ∈ dom vol ∧ (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
295289, 293, 294sylancr 694 . . . . . . . 8 (𝜑 → if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
296 mbfima 23305 . . . . . . . . 9 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
2976, 291, 296syl2anc 692 . . . . . . . 8 (𝜑 → (𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
298 difmbl 23218 . . . . . . . 8 ((if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
299295, 297, 298syl2anc 692 . . . . . . 7 (𝜑 → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
300299ad2antrr 761 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
301 inmbl 23217 . . . . . 6 (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
302280, 300, 301syl2anc 692 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
303288, 302eqeltrd 2698 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ∈ dom vol)
304 mblvol 23205 . . . . . 6 (((𝐺𝑛) “ {𝑘}) ∈ dom vol → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
305303, 304syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) = (vol*‘((𝐺𝑛) “ {𝑘})))
306196adantr 481 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝐺𝑛) Fn ℝ)
307306, 274syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘)))
30882, 185ifcld 4103 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
309 0re 9984 . . . . . . . . . . . . . . 15 0 ∈ ℝ
310 ifcl 4102 . . . . . . . . . . . . . . 15 ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
311308, 309, 310sylancl 693 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
31244fvmpt2 6248 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
31338, 311, 312syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
31437, 313eqtrd 2655 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
315314adantlr 750 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
316315eqeq1d 2623 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
317316, 56sylbid 230 . . . . . . . . 9 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺𝑛)‘𝑥) = 𝑘𝑥 ∈ (-𝑛[,]𝑛)))
318317expimpd 628 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
319307, 318sylbid 230 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (𝑥 ∈ ((𝐺𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
320319ssrdv 3589 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → ((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
321 iccssre 12197 . . . . . . 7 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
322278, 277, 321syl2anc 692 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
323 mblvol 23205 . . . . . . . 8 ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
324280, 323syl 17 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
325 iccvolcl 23242 . . . . . . . 8 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
326278, 277, 325syl2anc 692 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
327324, 326eqeltrrd 2699 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
328 ovolsscl 23161 . . . . . 6 ((((𝐺𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
329320, 322, 327, 328syl3anc 1323 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol*‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
330305, 329eqeltrd 2698 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺𝑛) ∖ {0})) → (vol‘((𝐺𝑛) “ {𝑘})) ∈ ℝ)
33123, 34, 303, 330i1fd 23354 . . 3 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ dom ∫1)
332331ralrimiva 2960 . 2 (𝜑 → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1)
333 ffnfv 6343 . 2 (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ dom ∫1))
3345, 332, 333sylanbrc 697 1 (𝜑𝐺:ℕ⟶dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  cdif 3552  cin 3554  wss 3555  ifcif 4058  {csn 4148   class class class wbr 4613  cmpt 4673   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cima 5077   Fn wfn 5842  wf 5843  ontowfo 5845  cfv 5847  (class class class)co 6604  cmpt2 6606  Fincfn 7899  cr 9879  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  +∞cpnf 10015  -∞cmnf 10016  *cxr 10017   < clt 10018  cle 10019  -cneg 10211   / cdiv 10628  cn 10964  2c2 11014  0cn0 11236  cz 11321  (,)cioo 12117  [,)cico 12119  [,]cicc 12120  ...cfz 12268  cfl 12531  cexp 12800  vol*covol 23138  volcvol 23139  MblFncmbf 23289  1citg1 23290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-rlim 14154  df-sum 14351  df-rest 16004  df-topgen 16025  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-top 20621  df-bases 20622  df-topon 20623  df-cmp 21100  df-ovol 23140  df-vol 23141  df-mbf 23294  df-itg1 23295
This theorem is referenced by:  mbfi1fseqlem5  23392  mbfi1fseqlem6  23393
  Copyright terms: Public domain W3C validator