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 27451

Description: Lemma for dchrisum 27455. 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 3129	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
3		nfcsb1v 3861	. . . . 5 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴
4	3	nfel1 2915	. . . 4 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ
5		csbeq1a 3851	. . . . 5 ⊢ (𝑛 = 𝐼 → 𝐴 = ⦋𝐼 / 𝑛⦌𝐴)
6	5	eleq1d 2821	. . . 4 ⊢ (𝑛 = 𝐼 → (𝐴 ∈ ℝ ↔ ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
7	4, 6	rspc 3552	. . 3 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
8	2, 7	syl5com 31	. 2 ⊢ (𝜑 → (𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
9		eqid 2736	. . . 4 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) = (ℤ_≥‘((⌊‘𝐼) + 1))
10		dchrisum.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11	10	nnred 12189	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12		elicopnf 13398	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
14	13	simprbda 498	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ)
15	14	flcld 13757	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℤ)
16	15	peano2zd 12636	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℤ)
17		nnuz 12827	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
18		1zzd 12558	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
19		dchrisum.6	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
20		nnrp 12954	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℝ⁺)
21	20	ssriv 3925	. . . . . . 7 ⊢ ℕ ⊆ ℝ⁺
22		eqid 2736	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ⁺ ↦ 𝐴) = (𝑛 ∈ ℝ⁺ ↦ 𝐴)
23	22, 1	dmmptd 6643	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℝ⁺ ↦ 𝐴) = ℝ⁺)
24	21, 23	sseqtrrid 3965	. . . . . 6 ⊢ (𝜑 → ℕ ⊆ dom (𝑛 ∈ ℝ⁺ ↦ 𝐴))
25	17, 18, 19, 24	rlimclim1 15507	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
26	25	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
27		0red 11147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
28	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
29	10	nngt0d 12226	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
30	29	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
31	13	simplbda 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝐼)
32	27, 28, 14, 30, 31	ltletrd 11306	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝐼)
33	14, 32	elrpd 12983	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ⁺)
34	2	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
35	33, 34, 7	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
36	35	recnd 11173	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ)
37		ssid 3944	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ⊆ (ℤ_≥‘((⌊‘𝐼) + 1))
38		fvex 6853	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ∈ V
39	37, 38	climconst2 15510	. . . . 5 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ ∧ ((⌊‘𝐼) + 1) ∈ ℤ) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
40	36, 16, 39	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
41	33	rpge0d 12990	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ 𝐼)
42		flge0nn0 13779	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 0 ≤ 𝐼) → (⌊‘𝐼) ∈ ℕ₀)
43	14, 41, 42	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℕ₀)
44		nn0p1nn 12476	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℕ₀ → ((⌊‘𝐼) + 1) ∈ ℕ)
45	43, 44	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℕ)
46		eluznn 12868	. . . . . . . 8 ⊢ ((((⌊‘𝐼) + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
47	45, 46	sylan 581	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
48	47	nnrpd 12984	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ⁺)
49	2	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
50		nfcsb1v 3861	. . . . . . . . 9 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴
51	50	nfel1 2915	. . . . . . . 8 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ
52		csbeq1a 3851	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
53	52	eleq1d 2821	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
54	51, 53	rspc 3552	. . . . . . 7 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
55	48, 49, 54	sylc 65	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
56	22	fvmpts 6951	. . . . . 6 ⊢ ((𝑖 ∈ ℝ⁺ ∧ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
57	48, 55, 56	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
58	57, 55	eqeltrd 2836	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ∈ ℝ)
59		fvconst2g 7157	. . . . . 6 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
60	35, 59	sylan 581	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
61	35	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
62	60, 61	eqeltrd 2836	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) ∈ ℝ)
63	33	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ⁺)
64		dchrisum.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
65	64	3expia 1122	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺)) → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
66	65	ralrimivva 3180	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
67	66	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
68		nfcv 2898	. . . . . . . . 9 ⊢ Ⅎ𝑛ℝ⁺
69		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)
70		nfcv 2898	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝐵
71		nfcv 2898	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 ≤
72	70, 71, 3	nfbr 5132	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴
73	69, 72	nfim 1898	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
74	68, 73	nfralw 3284	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
75		breq2 5089	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝐼))
76		breq1 5088	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑛 ≤ 𝑥 ↔ 𝐼 ≤ 𝑥))
77	75, 76	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)))
78	5	breq2d 5097	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
79	77, 78	imbi12d 344	. . . . . . . . 9 ⊢ (𝑛 = 𝐼 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
80	79	ralbidv 3160	. . . . . . . 8 ⊢ (𝑛 = 𝐼 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
81	74, 80	rspc 3552	. . . . . . 7 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
82	63, 67, 81	sylc 65	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
83	31	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑀 ≤ 𝐼)
84	14	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ)
85		reflcl 13755	. . . . . . . . 9 ⊢ (𝐼 ∈ ℝ → (⌊‘𝐼) ∈ ℝ)
86		peano2re 11319	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℝ → ((⌊‘𝐼) + 1) ∈ ℝ)
87	84, 85, 86	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ∈ ℝ)
88	47	nnred 12189	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ)
89		fllep1 13760	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → 𝐼 ≤ ((⌊‘𝐼) + 1))
90	14, 89	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ≤ ((⌊‘𝐼) + 1))
91	90	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ ((⌊‘𝐼) + 1))
92		eluzle 12801	. . . . . . . . 9 ⊢ (𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1)) → ((⌊‘𝐼) + 1) ≤ 𝑖)
93	92	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ≤ 𝑖)
94	84, 87, 88, 91, 93	letrd 11303	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ 𝑖)
95	83, 94	jca 511	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖))
96		breq2 5089	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → (𝐼 ≤ 𝑥 ↔ 𝐼 ≤ 𝑖))
97	96	anbi2d 631	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖)))
98		eqvisset 3449	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → 𝑖 ∈ V)
99		equtr2 2029	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝑥 = 𝑛)
100		dchrisum.2	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
101	100	equcoms 2022	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → 𝐴 = 𝐵)
102	99, 101	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵)
103	98, 102	csbied 3873	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ⦋𝑖 / 𝑛⦌𝐴 = 𝐵)
104	103	eqcomd 2742	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑛⦌𝐴)
105	104	breq1d 5095	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴 ↔ ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴))
106	97, 105	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
107	106	rspcv 3560	. . . . . 6 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
108	48, 82, 95, 107	syl3c 66	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)
109	108, 57, 60	3brtr4d 5117	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ≤ (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖))
110	9, 16, 26, 40, 58, 62, 109	climle 15602	. . 3 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)
111	110	ex 412	. 2 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴))
112	8, 111	jca 511	1 ⊢ (𝜑 → ((𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∀wral 3051 Vcvv 3429 ⦋csb 3837 {csn 4567 class class class wbr 5085 ↦ cmpt 5166 × cxp 5629 dom cdm 5631 ‘cfv 6498 (class class class)co 7367 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 +∞cpnf 11176 < clt 11179 ≤ cle 11180 ℕcn 12174 ℕ₀cn0 12437 ℤcz 12524 ℤ_≥cuz 12788 ℝ⁺crp 12942 [,)cico 13300 ⌊cfl 13749 ⇝ cli 15446 ⇝_𝑟 crli 15447 Basecbs 17179 0_gc0g 17402 ℤRHomczrh 21479 ℤ/nℤczn 21482 DChrcdchr 27195

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-pm 8776 df-en 8894 df-dom 8895 df-sdom 8896 df-sup 9355 df-inf 9356 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-rp 12943 df-ico 13304 df-fl 13751 df-seq 13964 df-exp 14024 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-rlim 15451

This theorem is referenced by: dchrisumlem2 27453 dchrisumlem3 27454

W3C validator