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 27426

Description: Lemma for dchrisum 27430. 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 3124	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
3		nfcsb1v 3869	. . . . 5 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴
4	3	nfel1 2911	. . . 4 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ
5		csbeq1a 3859	. . . . 5 ⊢ (𝑛 = 𝐼 → 𝐴 = ⦋𝐼 / 𝑛⦌𝐴)
6	5	eleq1d 2816	. . . 4 ⊢ (𝑛 = 𝐼 → (𝐴 ∈ ℝ ↔ ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
7	4, 6	rspc 3560	. . 3 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
8	2, 7	syl5com 31	. 2 ⊢ (𝜑 → (𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
9		eqid 2731	. . . 4 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) = (ℤ_≥‘((⌊‘𝐼) + 1))
10		dchrisum.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11	10	nnred 12140	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12		elicopnf 13345	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
14	13	simprbda 498	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ)
15	14	flcld 13702	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℤ)
16	15	peano2zd 12580	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℤ)
17		nnuz 12775	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
18		1zzd 12503	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
19		dchrisum.6	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
20		nnrp 12902	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℝ⁺)
21	20	ssriv 3933	. . . . . . 7 ⊢ ℕ ⊆ ℝ⁺
22		eqid 2731	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ⁺ ↦ 𝐴) = (𝑛 ∈ ℝ⁺ ↦ 𝐴)
23	22, 1	dmmptd 6626	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℝ⁺ ↦ 𝐴) = ℝ⁺)
24	21, 23	sseqtrrid 3973	. . . . . 6 ⊢ (𝜑 → ℕ ⊆ dom (𝑛 ∈ ℝ⁺ ↦ 𝐴))
25	17, 18, 19, 24	rlimclim1 15452	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
26	25	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
27		0red 11115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
28	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
29	10	nngt0d 12174	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
30	29	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
31	13	simplbda 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝐼)
32	27, 28, 14, 30, 31	ltletrd 11273	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝐼)
33	14, 32	elrpd 12931	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ⁺)
34	2	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
35	33, 34, 7	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
36	35	recnd 11140	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ)
37		ssid 3952	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ⊆ (ℤ_≥‘((⌊‘𝐼) + 1))
38		fvex 6835	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ∈ V
39	37, 38	climconst2 15455	. . . . 5 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ ∧ ((⌊‘𝐼) + 1) ∈ ℤ) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
40	36, 16, 39	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
41	33	rpge0d 12938	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ 𝐼)
42		flge0nn0 13724	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 0 ≤ 𝐼) → (⌊‘𝐼) ∈ ℕ₀)
43	14, 41, 42	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℕ₀)
44		nn0p1nn 12420	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℕ₀ → ((⌊‘𝐼) + 1) ∈ ℕ)
45	43, 44	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℕ)
46		eluznn 12816	. . . . . . . 8 ⊢ ((((⌊‘𝐼) + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
47	45, 46	sylan 580	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
48	47	nnrpd 12932	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ⁺)
49	2	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
50		nfcsb1v 3869	. . . . . . . . 9 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴
51	50	nfel1 2911	. . . . . . . 8 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ
52		csbeq1a 3859	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
53	52	eleq1d 2816	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
54	51, 53	rspc 3560	. . . . . . 7 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
55	48, 49, 54	sylc 65	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
56	22	fvmpts 6932	. . . . . 6 ⊢ ((𝑖 ∈ ℝ⁺ ∧ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
57	48, 55, 56	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
58	57, 55	eqeltrd 2831	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ∈ ℝ)
59		fvconst2g 7136	. . . . . 6 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
60	35, 59	sylan 580	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
61	35	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
62	60, 61	eqeltrd 2831	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) ∈ ℝ)
63	33	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ⁺)
64		dchrisum.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
65	64	3expia 1121	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺)) → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
66	65	ralrimivva 3175	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
67	66	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
68		nfcv 2894	. . . . . . . . 9 ⊢ Ⅎ𝑛ℝ⁺
69		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)
70		nfcv 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝐵
71		nfcv 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 ≤
72	70, 71, 3	nfbr 5136	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴
73	69, 72	nfim 1897	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
74	68, 73	nfralw 3279	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
75		breq2 5093	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝐼))
76		breq1 5092	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑛 ≤ 𝑥 ↔ 𝐼 ≤ 𝑥))
77	75, 76	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)))
78	5	breq2d 5101	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
79	77, 78	imbi12d 344	. . . . . . . . 9 ⊢ (𝑛 = 𝐼 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
80	79	ralbidv 3155	. . . . . . . 8 ⊢ (𝑛 = 𝐼 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
81	74, 80	rspc 3560	. . . . . . 7 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
82	63, 67, 81	sylc 65	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
83	31	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑀 ≤ 𝐼)
84	14	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ)
85		reflcl 13700	. . . . . . . . 9 ⊢ (𝐼 ∈ ℝ → (⌊‘𝐼) ∈ ℝ)
86		peano2re 11286	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℝ → ((⌊‘𝐼) + 1) ∈ ℝ)
87	84, 85, 86	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ∈ ℝ)
88	47	nnred 12140	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ)
89		fllep1 13705	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → 𝐼 ≤ ((⌊‘𝐼) + 1))
90	14, 89	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ≤ ((⌊‘𝐼) + 1))
91	90	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ ((⌊‘𝐼) + 1))
92		eluzle 12745	. . . . . . . . 9 ⊢ (𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1)) → ((⌊‘𝐼) + 1) ≤ 𝑖)
93	92	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ≤ 𝑖)
94	84, 87, 88, 91, 93	letrd 11270	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ 𝑖)
95	83, 94	jca 511	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖))
96		breq2 5093	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → (𝐼 ≤ 𝑥 ↔ 𝐼 ≤ 𝑖))
97	96	anbi2d 630	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖)))
98		eqvisset 3456	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → 𝑖 ∈ V)
99		equtr2 2028	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝑥 = 𝑛)
100		dchrisum.2	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
101	100	equcoms 2021	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → 𝐴 = 𝐵)
102	99, 101	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵)
103	98, 102	csbied 3881	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ⦋𝑖 / 𝑛⦌𝐴 = 𝐵)
104	103	eqcomd 2737	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑛⦌𝐴)
105	104	breq1d 5099	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴 ↔ ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴))
106	97, 105	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
107	106	rspcv 3568	. . . . . 6 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
108	48, 82, 95, 107	syl3c 66	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)
109	108, 57, 60	3brtr4d 5121	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ≤ (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖))
110	9, 16, 26, 40, 58, 62, 109	climle 15547	. . 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 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 Vcvv 3436 ⦋csb 3845 {csn 4573 class class class wbr 5089 ↦ cmpt 5170 × cxp 5612 dom cdm 5614 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 +∞cpnf 11143 < clt 11146 ≤ cle 11147 ℕcn 12125 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 ℝ⁺crp 12890 [,)cico 13247 ⌊cfl 13694 ⇝ cli 15391 ⇝_𝑟 crli 15392 Basecbs 17120 0_gc0g 17343 ℤRHomczrh 21436 ℤ/nℤczn 21439 DChrcdchr 27170

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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

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 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-pm 8753 df-en 8870 df-dom 8871 df-sdom 8872 df-sup 9326 df-inf 9327 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-ico 13251 df-fl 13696 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-rlim 15396

This theorem is referenced by: dchrisumlem2 27428 dchrisumlem3 27429

W3C validator