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 27727

Description: Lemma for dchrisum 27731. 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 3154	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
3		nfcsb1v 3871	. . . . 5 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴
4	3	nfel1 2938	. . . 4 ⊢ Ⅎ𝑛⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ
5		csbeq1a 3861	. . . . 5 ⊢ (𝑛 = 𝐼 → 𝐴 = ⦋𝐼 / 𝑛⦌𝐴)
6	5	eleq1d 2845	. . . 4 ⊢ (𝑛 = 𝐼 → (𝐴 ∈ ℝ ↔ ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
7	4, 6	rspc 3564	. . 3 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
8	2, 7	syl5com 32	. 2 ⊢ (𝜑 → (𝐼 ∈ ℝ⁺ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ))
9		eqid 2760	. . . 4 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) = (ℤ_≥‘((⌊‘𝐼) + 1))
10		dchrisum.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11	10	nnred 12275	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℝ)
12		elicopnf 13501	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
13	11, 12	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼)))
14	13	simprbda 504	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ)
15	14	flcld 13862	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℤ)
16	15	peano2zd 12731	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℤ)
17		nnuz 12929	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
18		1zzd 12652	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
19		dchrisum.6	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
20		nnrp 13057	. . . . . . . 8 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℝ⁺)
21	20	ssriv 3935	. . . . . . 7 ⊢ ℕ ⊆ ℝ⁺
22		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ⁺ ↦ 𝐴) = (𝑛 ∈ ℝ⁺ ↦ 𝐴)
23	22, 1	dmmptd 6678	. . . . . . 7 ⊢ (𝜑 → dom (𝑛 ∈ ℝ⁺ ↦ 𝐴) = ℝ⁺)
24	21, 23	sseqtrrid 3974	. . . . . 6 ⊢ (𝜑 → ℕ ⊆ dom (𝑛 ∈ ℝ⁺ ↦ 𝐴))
25	17, 18, 19, 24	rlimclim1 15635	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
26	25	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝ 0)
27		0red 11238	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
28	11	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
29	10	nngt0d 12312	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
30	29	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
31	13	simplbda 505	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝐼)
32	27, 28, 14, 30, 31	ltletrd 11397	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 < 𝐼)
33	14, 32	elrpd 13086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ∈ ℝ⁺)
34	2	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
35	33, 34, 7	sylc 66	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
36	35	recnd 11264	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ)
37		ssid 3953	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ⊆ (ℤ_≥‘((⌊‘𝐼) + 1))
38		fvex 6892	. . . . . 6 ⊢ (ℤ_≥‘((⌊‘𝐼) + 1)) ∈ V
39	37, 38	climconst2 15638	. . . . 5 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℂ ∧ ((⌊‘𝐼) + 1) ∈ ℤ) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
40	36, 16, 39	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴}) ⇝ ⦋𝐼 / 𝑛⦌𝐴)
41	33	rpge0d 13093	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 0 ≤ 𝐼)
42		flge0nn0 13884	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 0 ≤ 𝐼) → (⌊‘𝐼) ∈ ℕ₀)
43	14, 41, 42	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → (⌊‘𝐼) ∈ ℕ₀)
44		nn0p1nn 12570	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℕ₀ → ((⌊‘𝐼) + 1) ∈ ℕ)
45	43, 44	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → ((⌊‘𝐼) + 1) ∈ ℕ)
46		eluznn 12970	. . . . . . . 8 ⊢ ((((⌊‘𝐼) + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
47	45, 46	sylan 592	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℕ)
48	47	nnrpd 13087	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ⁺)
49	2	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
50		nfcsb1v 3871	. . . . . . . . 9 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴
51	50	nfel1 2938	. . . . . . . 8 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ
52		csbeq1a 3861	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
53	52	eleq1d 2845	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
54	51, 53	rspc 3564	. . . . . . 7 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
55	48, 49, 54	sylc 66	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
56	22	fvmpts 6991	. . . . . 6 ⊢ ((𝑖 ∈ ℝ⁺ ∧ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
57	48, 55, 56	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) = ⦋𝑖 / 𝑛⦌𝐴)
58	57, 55	eqeltrd 2860	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((𝑛 ∈ ℝ⁺ ↦ 𝐴)‘𝑖) ∈ ℝ)
59		fvconst2g 7202	. . . . . 6 ⊢ ((⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
60	35, 59	sylan 592	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) = ⦋𝐼 / 𝑛⦌𝐴)
61	35	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ)
62	60, 61	eqeltrd 2860	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (((ℤ_≥‘((⌊‘𝐼) + 1)) × {⦋𝐼 / 𝑛⦌𝐴})‘𝑖) ∈ ℝ)
63	33	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ⁺)
64		dchrisum.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
65	64	3expia 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺)) → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
66	65	ralrimivva 3205	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
67	66	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
68		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑛ℝ⁺
69		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥)
70		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝐵
71		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 ≤
72	70, 71, 3	nfbr 5152	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴
73	69, 72	nfim 1929	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)
74	68, 73	nfralw 3309	. . . . . . . 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 3185	. . . . . . . 8 ⊢ (𝑛 = 𝐼 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
81	74, 80	rspc 3564	. . . . . . 7 ⊢ (𝐼 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
82	63, 67, 81	sylc 66	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴))
83	31	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑀 ≤ 𝐼)
84	14	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ∈ ℝ)
85		reflcl 13860	. . . . . . . . 9 ⊢ (𝐼 ∈ ℝ → (⌊‘𝐼) ∈ ℝ)
86		peano2re 11410	. . . . . . . . 9 ⊢ ((⌊‘𝐼) ∈ ℝ → ((⌊‘𝐼) + 1) ∈ ℝ)
87	84, 85, 86	3syl 19	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ∈ ℝ)
88	47	nnred 12275	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝑖 ∈ ℝ)
89		fllep1 13865	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → 𝐼 ≤ ((⌊‘𝐼) + 1))
90	14, 89	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) → 𝐼 ≤ ((⌊‘𝐼) + 1))
91	90	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ ((⌊‘𝐼) + 1))
92		eluzle 12903	. . . . . . . . 9 ⊢ (𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1)) → ((⌊‘𝐼) + 1) ≤ 𝑖)
93	92	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → ((⌊‘𝐼) + 1) ≤ 𝑖)
94	84, 87, 88, 91, 93	letrd 11394	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → 𝐼 ≤ 𝑖)
95	83, 94	jca 521	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ_≥‘((⌊‘𝐼) + 1))) → (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖))
96		breq2 5107	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → (𝐼 ≤ 𝑥 ↔ 𝐼 ≤ 𝑖))
97	96	anbi2d 642	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) ↔ (𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖)))
98		eqvisset 3470	. . . . . . . . . . 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 2766	. . . . . . . . 9 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑛⦌𝐴)
105	104	breq1d 5113	. . . . . . . 8 ⊢ (𝑥 = 𝑖 → (𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴 ↔ ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴))
106	97, 105	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥) → 𝐵 ≤ ⦋𝐼 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖) → ⦋𝑖 / 𝑛⦌𝐴 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
107	106	rspcv 3572	. . . . . 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 15730	. . 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 2955 ∀wral 3076 Vcvv 3450 ⦋csb 3847 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 × cxp 5653 dom cdm 5655 ‘cfv 6533 (class class class)co 7414 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 +∞cpnf 11267 < clt 11270 ≤ cle 11271 ℕcn 12260 ℕ₀cn0 12531 ℤcz 12618 ℤ_≥cuz 12890 ℝ⁺crp 13045 [,)cico 13403 ⌊cfl 13854 ⇝ cli 15574 ⇝_𝑟 crli 15575 Basecbs 17304 0_gc0g 17527 ℤRHomczrh 21715 ℤ/nℤczn 21718 DChrcdchr 27471

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 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 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 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-er 8699 df-pm 8832 df-en 8956 df-dom 8957 df-sdom 8958 df-sup 9415 df-inf 9416 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-rp 13046 df-ico 13407 df-fl 13856 df-seq 14069 df-exp 14129 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-clim 15578 df-rlim 15579

This theorem is used by: dchrisumlem2 27729 dchrisumlem3 27730

W3C validator