Theorem mbfi1fseqlem4 25647

Description: Lemma for mbfi1fseq 25650. 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.

Step	Hyp	Ref	Expression
1		reex 11104	. . . . 5 ⊢ ℝ ∈ V
2	1	mptex 7163	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3		mbfi1fseq.4	. . . 4 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
4	2, 3	fnmpti 6629	. . 3 ⊢ 𝐺 Fn ℕ
5	4	a1i 11	. 2 ⊢ (𝜑 → 𝐺 Fn ℕ)
6		mbfi1fseq.1	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
7		mbfi1fseq.2	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
8		mbfi1fseq.3	. . . . . 6 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
9	6, 7, 8, 3	mbfi1fseqlem3 25646	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10		elfznn0 13522	. . . . . . . . 9 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
11	10	nn0red 12450	. . . . . . . 8 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12		2nn 12205	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
13		nnnn0 12395	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14		nnexpcl 13983	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
15	12, 13, 14	sylancr 587	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
16	15	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17		nndivre 12173	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
18	11, 16, 17	syl2anr 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
19	18	fmpttd 7054	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
20	19	frnd 6664	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
21	9, 20	fssd 6673	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ℝ)
22		fzfid 13882	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
23	19	ffnd 6657	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24		dffn4 6746	. . . . . . 7 ⊢ ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
25	23, 24	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
26		fofi 9204	. . . . . 6 ⊢ (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
27	22, 25, 26	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
28	9	frnd 6664	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
29	27, 28	ssfid 9160	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ∈ Fin)
30	6, 7, 8, 3	mbfi1fseqlem2 25645	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
31	30	fveq1d 6830	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
32	31	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34		ovex 7385	. . . . . . . . . . . . . . 15 ⊢ (𝑛𝐽𝑥) ∈ V
35		vex 3441	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
36	34, 35	ifex 4525	. . . . . . . . . . . . . 14 ⊢ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37		c0ex 11113	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
38	36, 37	ifex 4525	. . . . . . . . . . . . 13 ⊢ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39		eqid 2733	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
40	39	fvmpt2 6946	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
41	33, 38, 40	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
42	32, 41	eqtrd 2768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
43	42	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
44	43	eqeq1d 2735	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45		eldifsni 4741	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ≠ 0)
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47		neeq1 2991	. . . . . . . . . . . 12 ⊢ (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
48	46, 47	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
49		iffalse 4483	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
50	49	necon1ai 2956	. . . . . . . . . . 11 ⊢ (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
51	48, 50	syl6 35	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → 𝑥 ∈ (-𝑛[,]𝑛)))
52	51	pm4.71rd 562	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
53		iftrue 4480	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
54	53	eqeq1d 2735	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
56	55	nnred 12147	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
57	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58		rge0ssre 13358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
59		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60		ffvelcdm 7020	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
61	7, 59, 60	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
62	58, 61	sselid 3928	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
63		nnnn0 12395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64		nnexpcl 13983	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
65	12, 63, 64	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
66	65	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
67	66	nnred 12147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
68	62, 67	remulcld 11149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
69		reflcl 13702	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
71	70, 66	nndivred 12186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
72	71	ralrimivva 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
73	8	fmpo 8006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
74	72, 73	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
75		fovcdm 7522	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
76	74, 75	syl3an1 1163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77	76	3expa 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
78	77	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80		lemin 13093	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
81	57, 79, 57, 80	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
82	79, 57	ifcld 4521	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
83	82, 57	letri3d 11262	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
85	84	eqeq2d 2744	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86		min2 13091	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
87	79, 57, 86	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
88	87	biantrurd 532	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
89	83, 85, 88	3bitr4d 311	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
90	57	leidd 11690	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ≤ 𝑛)
91	90	biantrud 531	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
92	81, 89, 91	3bitr4d 311	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
93		breq1 5096	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝐹‘𝑥)))
94	7	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
95	94	ffvelcdmda 7023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
96		elrege0 13356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
97	95, 96	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
98	97	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
99	98	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
100	55, 15	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101	100	nnred 12147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
102	99, 101	remulcld 11149	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ)
103		reflcl 13702	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
105	100	nngt0d 12181	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106		lemuldiv 12009	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
107	56, 104, 101, 105, 106	syl112anc 1376	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
108		lemul1 11980	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
109	56, 99, 101, 105, 108	syl112anc 1376	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
110		nnmulcl 12156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
111	55, 15, 110	syl2anc2 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112	111	nnzd 12501	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113		flge 13711	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
114	102, 112, 113	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
115	109, 114	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
116		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
117		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
118	117	fveq2d 6832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
119		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑛)
120	119	oveq2d 7368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121	118, 120	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑛)))
122	121	fveq2d 6832	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑛))))
123	122, 120	oveq12d 7370	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
124		ovex 7385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125	123, 8, 124	ovmpoa 7507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
126	55, 116, 125	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
127	126	breq2d 5105	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
128	107, 115, 127	3bitr4d 311	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
129	93, 128	sylan9bbr 510	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
130	116	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
131		iftrue 4480	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132	131	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133	130, 132	eleqtrrd 2836	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
134	133	biantrurd 532	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
135	92, 129, 134	3bitr2d 307	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
136	28	ssdifssd 4096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137	136	sselda 3930	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138		eqid 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139	138	rnmpt 5901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140	139	eqabri 2875	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141		elfzelz 13426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142	141	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143	142	zcnd 12584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
144	15	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145	144	nncnd 12148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146	144	nnne0d 12182	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147	143, 145, 146	divcan1d 11905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148	147, 142	eqeltrd 2833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149		oveq1 7359	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150	149	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151	148, 150	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152	151	rexlimdva 3134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
153	140, 152	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
154	153	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
155	137, 154	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157		flbi 13722	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158	102, 156, 157	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
159	158	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
160		neeq1 2991	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 ↔ 𝑘 ≠ 𝑛))
161	160	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162		iffalse 4483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163	162	necon1ai 2956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165	164	iftrued 4482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167	165, 166	eqtr3d 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168	167, 164	eqbrtrrd 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘 ≤ 𝑛)
169	168, 167	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170	169	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171		breq1 5096	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛 ↔ 𝑘 ≤ 𝑛))
172	171	biimparc 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173	172	iftrued 4482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175	173, 174	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176	170, 175	impbid1 225	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177	176	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178		eldifi 4080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺‘𝑛))
179		nnre 12139	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180	179	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
181	77, 180, 86	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
182	13	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183	182	nn0ge0d 12452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184		breq1 5096	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185		breq1 5096	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186	184, 185	ifboth 4514	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187	181, 183, 186	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
188	42, 187	eqbrtrd 5115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
189	188	ralrimiva 3125	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
190	9	ffnd 6657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) Fn ℝ)
191		breq1 5096	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = ((𝐺‘𝑛)‘𝑥) → (𝑘 ≤ 𝑛 ↔ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
192	191	ralrn 7027	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
194	189, 193	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛)
195	194	r19.21bi 3225	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺‘𝑛)) → 𝑘 ≤ 𝑛)
196	178, 195	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ≤ 𝑛)
197	196	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → 𝑘 ≤ 𝑛)
198	197	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199	126	eqeq1d 2735	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200	104	recnd 11147	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℂ)
201	28, 20	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ℝ)
202	201	ssdifssd 4096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ℝ)
203	202	sselda 3930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204	203	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205	204	recnd 11147	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206	100	nncnd 12148	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207	100	nnne0d 12182	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208	200, 205, 206, 207	divmul3d 11938	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
209	199, 208	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
210	209	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
211	177, 198, 210	3bitr2d 307	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
212		ifnefalse 4486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ≠ 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213	212	eleq2d 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214	100	nnrecred 12183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215	204, 214	readdcld 11148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216	215	rexrd 11169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217		elioomnf 13346	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218	216, 217	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
219	94	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220	219	ffnd 6657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221		elpreima 6997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223	116, 222	mpbirand 707	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
224	99	biantrurd 532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225	218, 223, 224	3bitr4d 311	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛)))))
226		ltmul1 11978	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
227	99, 215, 101, 105, 226	syl112anc 1376	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
228	214	recnd 11147	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229	206, 207	recid2d 11900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230	229	oveq2d 7368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231	205, 206, 228, 230	joinlmuladdmuld 11146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232	231	breq2d 5105	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
233	225, 227, 232	3bitrd 305	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
234	213, 233	sylan9bbr 510	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
235		lemul1 11980	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
236	204, 99, 101, 105, 235	syl112anc 1376	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
237	236	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
238	234, 237	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)))))
239	238	biancomd 463	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
240	159, 211, 239	3bitr4d 311	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
241	135, 240	pm2.61dane 3016	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
242		eldif 3908	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))))
243	204	rexrd 11169	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244		elioomnf 13346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
245	243, 244	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
246		elpreima 6997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
247	220, 246	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
248	116, 247	mpbirand 707	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) ∈ (-∞(,)𝑘)))
249	99	biantrurd 532	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < 𝑘 ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
250	245, 248, 249	3bitr4d 311	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) < 𝑘))
251	250	notbid 318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹‘𝑥) < 𝑘))
252	204, 99	lenltd 11266	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < 𝑘))
253	251, 252	bitr4d 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹‘𝑥)))
254	253	anbi2d 630	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
255	242, 254	bitrid 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
256	241, 255	bitr4d 282	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
257	54, 256	sylan9bbr 510	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
258	257	pm5.32da 579	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
259	44, 52, 258	3bitrd 305	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
260	259	pm5.32da 579	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
261	21	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛):ℝ⟶ℝ)
262	261	ffnd 6657	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
263		fniniseg 6999	. . . . . . . 8 ⊢ ((𝐺‘𝑛) Fn ℝ → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
264	262, 263	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
265		elin 3914	. . . . . . . 8 ⊢ (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
266	179	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267	266	renegcld 11551	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268		iccmbl 25495	. . . . . . . . . . . . 13 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
269	267, 266, 268	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
270		mblss 25460	. . . . . . . . . . . 12 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
271	269, 270	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
272	271	sseld 3929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
273	272	adantrd 491	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
274	273	pm4.71rd 562	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
275	265, 274	bitrid 283	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
276	260, 264, 275	3bitr4d 311	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ 𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
277	276	eqrdv 2731	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
278		rembl 25469	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
279		fss 6672	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
280	7, 58, 279	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
281		mbfima 25559	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
282	6, 280, 281	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283		ifcl 4520	. . . . . . . . 9 ⊢ ((ℝ ∈ dom vol ∧ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284	278, 282, 283	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285		mbfima 25559	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
286	6, 280, 285	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287		difmbl 25472	. . . . . . . 8 ⊢ ((if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288	284, 286, 287	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289	288	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290		inmbl 25471	. . . . . 6 ⊢ (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291	269, 289, 290	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292	277, 291	eqeltrd 2833	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol)
293		mblvol 25459	. . . . . 6 ⊢ ((◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
294	292, 293	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
295	190	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
296	295, 263	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
297	77, 180	ifcld 4521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298		0re 11121	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
299		ifcl 4520	. . . . . . . . . . . . . . 15 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300	297, 298, 299	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
301	39	fvmpt2 6946	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
302	33, 300, 301	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
303	32, 302	eqtrd 2768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304	303	adantlr 715	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305	304	eqeq1d 2735	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
306	305, 51	sylbid 240	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 → 𝑥 ∈ (-𝑛[,]𝑛)))
307	306	expimpd 453	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
308	296, 307	sylbid 240	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
309	308	ssrdv 3936	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
310		iccssre 13331	. . . . . . 7 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
311	267, 266, 310	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
312		mblvol 25459	. . . . . . . 8 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
313	269, 312	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
314		iccvolcl 25496	. . . . . . . 8 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
315	267, 266, 314	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
316	313, 315	eqeltrrd 2834	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
317		ovolsscl 25415	. . . . . 6 ⊢ (((◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
318	309, 311, 316, 317	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
319	294, 318	eqeltrd 2833	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
320	21, 29, 292, 319	i1fd 25610	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ dom ∫1)
321	320	ralrimiva 3125	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1)
322		ffnfv 7058	. 2 ⊢ (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1))
323	5, 321, 322	sylanbrc 583	1 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∖ cdif 3895   ∩ cin 3897   ⊆ wss 3898  ifcif 4474  {csn 4575   class class class wbr 5093   ↦ cmpt 5174   × cxp 5617  ^◡ccnv 5618  dom cdm 5619  ran crn 5620   “ cima 5622   Fn wfn 6481  ⟶wf 6482  –onto→wfo 6484  ‘cfv 6486  (class class class)co 7352   ∈ cmpo 7354  Fincfn 8875  ℝcr 11012  0cc0 11013  1c1 11014   + caddc 11016   · cmul 11018  +∞cpnf 11150  -∞cmnf 11151  ℝ^*cxr 11152   < clt 11153   ≤ cle 11154  -cneg 11352   / cdiv 11781  ℕcn 12132  2c2 12187  ℕ₀cn0 12388  ℤcz 12475  (,)cioo 13247  [,)cico 13249  [,]cicc 13250  ...cfz 13409  ⌊cfl 13696  ↑cexp 13970  vol*covol 25391  volcvol 25392  MblFncmbf 25543  ∫₁citg1 25544

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-inf2 9538  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090  ax-pre-sup 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-of 7616  df-om 7803  df-1st 7927  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-1o 8391  df-2o 8392  df-er 8628  df-map 8758  df-pm 8759  df-en 8876  df-dom 8877  df-sdom 8878  df-fin 8879  df-fi 9302  df-sup 9333  df-inf 9334  df-oi 9403  df-dju 9801  df-card 9839  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-div 11782  df-nn 12133  df-2 12195  df-3 12196  df-n0 12389  df-z 12476  df-uz 12739  df-q 12849  df-rp 12893  df-xneg 13013  df-xadd 13014  df-xmul 13015  df-ioo 13251  df-ico 13253  df-icc 13254  df-fz 13410  df-fzo 13557  df-fl 13698  df-seq 13911  df-exp 13971  df-hash 14240  df-cj 15008  df-re 15009  df-im 15010  df-sqrt 15144  df-abs 15145  df-clim 15397  df-rlim 15398  df-sum 15596  df-rest 17328  df-topgen 17349  df-psmet 21285  df-xmet 21286  df-met 21287  df-bl 21288  df-mopn 21289  df-top 22810  df-topon 22827  df-bases 22862  df-cmp 23303  df-ovol 25393  df-vol 25394  df-mbf 25548  df-itg1 25549

This theorem is referenced by:  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649