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 27815

Description: Lemma for dchrisum 27819. 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 3155	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
3		nfcsb1v 3871	. . . . 5 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴
4	3	nfel1 2939	. . . 4 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ
5		csbeq1a 3861	. . . . 5 ⊢ (𝑛 = 𝐼 → 𝐴 = ⦋𝐼 / 𝑛⦌𝐴)
6	5	eleq1d 2846	. . . 4 ⊢ (𝑛 = 𝐼 → (𝐴 ∈ ℝ ↔ ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
7	4, 6	rspc 3565	. . 3 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
8	2, 7	syl5com 32	. 2 ⊢ (𝜑 → (𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
9		eqid 2761	. . . 4 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) = (ℤ_≥‘((⌊‘𝐼) + 1))
10		dchrisum.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11	10	nnred 12350	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12		elicopnf 13576	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
13	11, 12	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
14	13	simprbda 504	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ)
15	14	flcld 13938	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℤ)
16	15	peano2zd 12806	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℤ)
17		nnuz 13004	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
18		1zzd 12727	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
19		dchrisum.6	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
20		nnrp 13132	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℝ⁺)
21	20	ssriv 3935	. . . . . . 7 ⊢ ℕ ⊆ ℝ⁺
22		eqid 2761	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ⁺ ↦ 𝐴) = (𝑛 ∈ ℝ⁺ ↦ 𝐴)
23	22, 1	dmmptd 6684	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℝ⁺ ↦ 𝐴) = ℝ⁺)
24	21, 23	sseqtrrid 3974	. . . . . 6 ⊢ (𝜑 → ℕ ⊆ dom (𝑛 ∈ ℝ⁺ ↦ 𝐴))
25	17, 18, 19, 24	rlimclim1 15712	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
26	25	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
27		0red 11311	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
28	11	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
29	10	nngt0d 12387	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
30	29	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
31	13	simplbda 505	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝐼)
32	27, 28, 14, 30, 31	ltletrd 11470	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝐼)
33	14, 32	elrpd 13161	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ⁺)
34	2	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
35	33, 34, 7	sylc 66	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
36	35	recnd 11337	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ)
37		ssid 3953	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ⊆ (ℤ_≥‘((⌊‘𝐼) + 1))
38		fvex 6898	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ∈ V
39	37, 38	climconst2 15715	. . . . 5 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ ∧ ((⌊‘𝐼) + 1) ∈ ℤ) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
40	36, 16, 39	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
41	33	rpge0d 13168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ 𝐼)
42		flge0nn0 13960	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 0 ≤ 𝐼) → (⌊‘𝐼) ∈ ℕ₀)
43	14, 41, 42	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℕ₀)
44		nn0p1nn 12645	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℕ₀ → ((⌊‘𝐼) + 1) ∈ ℕ)
45	43, 44	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℕ)
46		eluznn 13045	. . . . . . . 8 ⊢ ((((⌊‘𝐼) + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
47	45, 46	sylan 592	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
48	47	nnrpd 13162	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ⁺)
49	2	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
50		nfcsb1v 3871	. . . . . . . . 9 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴
51	50	nfel1 2939	. . . . . . . 8 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ
52		csbeq1a 3861	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
53	52	eleq1d 2846	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
54	51, 53	rspc 3565	. . . . . . 7 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
55	48, 49, 54	sylc 66	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
56	22	fvmpts 6997	. . . . . 6 ⊢ ((𝑖 ∈ ℝ⁺ ∧ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
57	48, 55, 56	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
58	57, 55	eqeltrd 2861	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ∈ ℝ)
59		fvconst2g 7208	. . . . . 6 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
60	35, 59	sylan 592	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
61	35	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
62	60, 61	eqeltrd 2861	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) ∈ ℝ)
63	33	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ⁺)
64		dchrisum.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
65	64	3expia 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺)) → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
66	65	ralrimivva 3206	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
67	66	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
68		nfcv 2923	. . . . . . . . 9 ⊢ Ⅎ𝑛ℝ⁺
69		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)
70		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝐵
71		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 ≤
72	70, 71, 3	nfbr 5152	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴
73	69, 72	nfim 1929	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
74	68, 73	nfralw 3310	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
75		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝐼))
76		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐼 → (𝑛 ≤ 𝑥 ↔ 𝐼 ≤ 𝑥))
77	75, 76	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)))
78	5	breq2d 5115	. . . . . . . . . 10 ⊢ (𝑛 = 𝐼 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
79	77, 78	imbi12d 347	. . . . . . . . 9 ⊢ (𝑛 = 𝐼 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
80	79	ralbidv 3186	. . . . . . . 8 ⊢ (𝑛 = 𝐼 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
81	74, 80	rspc 3565	. . . . . . 7 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
82	63, 67, 81	sylc 66	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
83	31	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑀 ≤ 𝐼)
84	14	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ)
85		reflcl 13936	. . . . . . . . 9 ⊢ (𝐼 ∈ ℝ → (⌊‘𝐼) ∈ ℝ)
86		peano2re 11483	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℝ → ((⌊‘𝐼) + 1) ∈ ℝ)
87	84, 85, 86	3syl 19	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ∈ ℝ)
88	47	nnred 12350	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ)
89		fllep1 13941	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → 𝐼 ≤ ((⌊‘𝐼) + 1))
90	14, 89	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ≤ ((⌊‘𝐼) + 1))
91	90	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ ((⌊‘𝐼) + 1))
92		eluzle 12978	. . . . . . . . 9 ⊢ (𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1)) → ((⌊‘𝐼) + 1) ≤ 𝑖)
93	92	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ≤ 𝑖)
94	84, 87, 88, 91, 93	letrd 11467	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ 𝑖)
95	83, 94	jca 521	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖))
96		breq2 5107	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → (𝐼 ≤ 𝑥 ↔ 𝐼 ≤ 𝑖))
97	96	anbi2d 642	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖)))
98		eqvisset 3471	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → 𝑖 ∈ V)
99		equtr2 2060	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝑥 = 𝑛)
100		dchrisum.2	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
101	100	equcoms 2053	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → 𝐴 = 𝐵)
102	99, 101	syl 18	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑖 ∧ 𝑛 = 𝑖) → 𝐴 = 𝐵)
103	98, 102	csbied 3883	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ⦋𝑖 / 𝑛⦌𝐴 = 𝐵)
104	103	eqcomd 2767	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑛⦌𝐴)
105	104	breq1d 5113	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴 ↔ ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴))
106	97, 105	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
107	106	rspcv 3573	. . . . . 6 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
108	48, 82, 95, 107	syl3c 67	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)
109	108, 57, 60	3brtr4d 5137	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ≤ (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖))
110	9, 16, 26, 40, 58, 62, 109	climle 15807	. . 3 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)
111	110	ex 418	. 2 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴))
112	8, 111	jca 521	1 ⊢ (𝜑 → ((𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 Vcvv 3451 ⦋csb 3847 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 × cxp 5649 dom cdm 5651 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 +∞cpnf 11340 < clt 11343 ≤ cle 11344 ℕcn 12335 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ℝ⁺crp 13120 [,)cico 13478 ⌊cfl 13930 ⇝ cli 15651 ⇝_𝑟 crli 15652 Basecbs 17387 0_gc0g 17610 ℤRHomczrh 21805 ℤ/nℤczn 21808 DChrcdchr 27559

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-er 8717 df-pm 8850 df-en 8974 df-dom 8975 df-sdom 8976 df-sup 9434 df-inf 9435 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-ico 13482 df-fl 13932 df-seq 14145 df-exp 14205 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-rlim 15656

This theorem is used by: dchrisumlem2 27817 dchrisumlem3 27818

W3C validator