dchrisumlema - Metamath Proof Explorer

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

Theorem dchrisumlema 26171

Description: Lemma for dchrisum 26175. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)

**Hypotheses**
Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum.g	⊢ 𝐺 = (DChr‘𝑁)
rpvmasum.d	⊢ 𝐷 = (Base‘𝐺)
rpvmasum.1	⊢ 1 = (0_g‘𝐺)
dchrisum.b	⊢ (𝜑 → 𝑋 ∈ 𝐷)
dchrisum.n1	⊢ (𝜑 → 𝑋 ≠ 1 )
dchrisum.2	⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
dchrisum.3	⊢ (𝜑 → 𝑀 ∈ ℕ)
dchrisum.4	⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
dchrisum.5	⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
dchrisum.6	⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
dchrisum.7	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))

**Assertion**
Ref	Expression
dchrisumlema	⊢ (𝜑 → ((𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)))

Distinct variable groups: 𝑥,𝑛, 1 𝑛,𝐹,𝑥 𝑛,𝐼,𝑥 𝑥,𝐴 𝑛,𝑁,𝑥 𝜑,𝑛,𝑥 𝐵,𝑛 𝑛,𝑍,𝑥 𝐷,𝑛,𝑥 𝑛,𝐿,𝑥 𝑛,𝑀,𝑥 𝑛,𝑋,𝑥 Allowed substitution hints: 𝐴(𝑛) 𝐵(𝑥) 𝐺(𝑥,𝑛)

Proof of Theorem dchrisumlema Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dchrisum.4	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
2	1	ralrimiva 3113	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
3		nfcsb1v 3829	. . . . 5 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴
4	3	nfel1 2935	. . . 4 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ
5		csbeq1a 3819	. . . . 5 ⊢ (𝑛 = 𝐼 → 𝐴 = ⦋𝐼 / 𝑛⦌𝐴)
6	5	eleq1d 2836	. . . 4 ⊢ (𝑛 = 𝐼 → (𝐴 ∈ ℝ ↔ ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
7	4, 6	rspc 3529	. . 3 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
8	2, 7	syl5com 31	. 2 ⊢ (𝜑 → (𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
9		eqid 2758	. . . 4 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) = (ℤ_≥‘((⌊‘𝐼) + 1))
10		dchrisum.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11	10	nnred 11689	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12		elicopnf 12877	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
14	13	simprbda 502	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ)
15	14	flcld 13217	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℤ)
16	15	peano2zd 12129	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℤ)
17		nnuz 12321	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
18		1zzd 12052	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
19		dchrisum.6	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
20		nnrp 12441	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℝ⁺)
21	20	ssriv 3896	. . . . . . 7 ⊢ ℕ ⊆ ℝ⁺
22		eqid 2758	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ⁺ ↦ 𝐴) = (𝑛 ∈ ℝ⁺ ↦ 𝐴)
23	22, 1	dmmptd 6476	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℝ⁺ ↦ 𝐴) = ℝ⁺)
24	21, 23	sseqtrrid 3945	. . . . . 6 ⊢ (𝜑 → ℕ ⊆ dom (𝑛 ∈ ℝ⁺ ↦ 𝐴))
25	17, 18, 19, 24	rlimclim1 14950	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
26	25	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
27		0red 10682	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
28	11	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
29	10	nngt0d 11723	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
30	29	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
31	13	simplbda 503	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝐼)
32	27, 28, 14, 30, 31	ltletrd 10838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝐼)
33	14, 32	elrpd 12469	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ⁺)
34	2	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
35	33, 34, 7	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
36	35	recnd 10707	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ)
37		ssid 3914	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ⊆ (ℤ_≥‘((⌊‘𝐼) + 1))
38		fvex 6671	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ∈ V
39	37, 38	climconst2 14953	. . . . 5 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ ∧ ((⌊‘𝐼) + 1) ∈ ℤ) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
40	36, 16, 39	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
41	33	rpge0d 12476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ 𝐼)
42		flge0nn0 13239	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 0 ≤ 𝐼) → (⌊‘𝐼) ∈ ℕ₀)
43	14, 41, 42	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℕ₀)
44		nn0p1nn 11973	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℕ₀ → ((⌊‘𝐼) + 1) ∈ ℕ)
45	43, 44	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℕ)
46		eluznn 12358	. . . . . . . 8 ⊢ ((((⌊‘𝐼) + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
47	45, 46	sylan 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
48	47	nnrpd 12470	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ⁺)
49	2	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
50		nfcsb1v 3829	. . . . . . . . 9 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴
51	50	nfel1 2935	. . . . . . . 8 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ
52		csbeq1a 3819	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
53	52	eleq1d 2836	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
54	51, 53	rspc 3529	. . . . . . 7 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
55	48, 49, 54	sylc 65	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
56	22	fvmpts 6762	. . . . . 6 ⊢ ((𝑖 ∈ ℝ⁺ ∧ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
57	48, 55, 56	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
58	57, 55	eqeltrd 2852	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ∈ ℝ)
59		fvconst2g 6955	. . . . . 6 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
60	35, 59	sylan 583	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
61	35	adantr 484	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
62	60, 61	eqeltrd 2852	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) ∈ ℝ)
63	33	adantr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ⁺)
64		dchrisum.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
65	64	3expia 1118	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺)) → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
66	65	ralrimivva 3120	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
67	66	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
68		nfcv 2919	. . . . . . . . 9 ⊢ Ⅎ𝑛ℝ⁺
69		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)
70		nfcv 2919	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝐵
71		nfcv 2919	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 ≤
72	70, 71, 3	nfbr 5079	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴
73	69, 72	nfim 1897	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
74	68, 73	nfralw 3153	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
75		breq2 5036	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝐼))
76		breq1 5035	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑛 ≤ 𝑥 ↔ 𝐼 ≤ 𝑥))
77	75, 76	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)))
78	5	breq2d 5044	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
79	77, 78	imbi12d 348	. . . . . . . . 9 ⊢ (𝑛 = 𝐼 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
80	79	ralbidv 3126	. . . . . . . 8 ⊢ (𝑛 = 𝐼 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
81	74, 80	rspc 3529	. . . . . . 7 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
82	63, 67, 81	sylc 65	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
83	31	adantr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑀 ≤ 𝐼)
84	14	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ)
85		reflcl 13215	. . . . . . . . 9 ⊢ (𝐼 ∈ ℝ → (⌊‘𝐼) ∈ ℝ)
86		peano2re 10851	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℝ → ((⌊‘𝐼) + 1) ∈ ℝ)
87	84, 85, 86	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ∈ ℝ)
88	47	nnred 11689	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ)
89		fllep1 13220	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → 𝐼 ≤ ((⌊‘𝐼) + 1))
90	14, 89	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ≤ ((⌊‘𝐼) + 1))
91	90	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ ((⌊‘𝐼) + 1))
92		eluzle 12295	. . . . . . . . 9 ⊢ (𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1)) → ((⌊‘𝐼) + 1) ≤ 𝑖)
93	92	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ≤ 𝑖)
94	84, 87, 88, 91, 93	letrd 10835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ 𝑖)
95	83, 94	jca 515	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖))
96		breq2 5036	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → (𝐼 ≤ 𝑥 ↔ 𝐼 ≤ 𝑖))
97	96	anbi2d 631	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖)))
98		eqvisset 3427	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → 𝑖 ∈ V)
99		equtr2 2034	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝑥 = 𝑛)
100		dchrisum.2	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
101	100	equcoms 2027	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → 𝐴 = 𝐵)
102	99, 101	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵)
103	98, 102	csbied 3841	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ⦋𝑖 / 𝑛⦌𝐴 = 𝐵)
104	103	eqcomd 2764	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑛⦌𝐴)
105	104	breq1d 5042	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴 ↔ ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴))
106	97, 105	imbi12d 348	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
107	106	rspcv 3536	. . . . . 6 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
108	48, 82, 95, 107	syl3c 66	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)
109	108, 57, 60	3brtr4d 5064	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ≤ (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖))
110	9, 16, 26, 40, 58, 62, 109	climle 15044	. . 3 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)
111	110	ex 416	. 2 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴))
112	8, 111	jca 515	1 ⊢ (𝜑 → ((𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ∀wral 3070 Vcvv 3409 ⦋csb 3805 {csn 4522 class class class wbr 5032 ↦ cmpt 5112 × cxp 5522 dom cdm 5524 ‘cfv 6335 (class class class)co 7150 ℂcc 10573 ℝcr 10574 0cc0 10575 1c1 10576 + caddc 10578 · cmul 10580 +∞cpnf 10710 < clt 10713 ≤ cle 10714 ℕcn 11674 ℕ₀cn0 11934 ℤcz 12020 ℤ_≥cuz 12282 ℝ⁺crp 12430 [,)cico 12781 ⌊cfl 13209 ⇝ cli 14889 ⇝_𝑟 crli 14890 Basecbs 16541 0_gc0g 16771 ℤRHomczrh 20269 ℤ/nℤczn 20272 DChrcdchr 25915

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-iun 4885 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-2nd 7694 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-er 8299 df-pm 8419 df-en 8528 df-dom 8529 df-sdom 8530 df-sup 8939 df-inf 8940 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-div 11336 df-nn 11675 df-2 11737 df-3 11738 df-n0 11935 df-z 12021 df-uz 12283 df-rp 12431 df-ico 12785 df-fl 13211 df-seq 13419 df-exp 13480 df-cj 14506 df-re 14507 df-im 14508 df-sqrt 14642 df-abs 14643 df-clim 14893 df-rlim 14894

This theorem is referenced by: dchrisumlem2 26173 dchrisumlem3 26174

W3C validator