dchrisumlema

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrisum.2	$⊢ n = x \to A = B$
	dchrisum.3	$⊢ φ \to M \in ℕ$
	dchrisum.4	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℝ$
	dchrisum.5	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
	dchrisum.6	$⊢ φ \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
	dchrisum.7	$⊢ F = (n \in ℕ ⟼ X (L (n)) A)$
Assertion	dchrisumlema	$⊢ φ \to ((I \in ℝ^{+} \to ⦋ I / n ⦌ A \in ℝ) \land (I \in [M, +∞) \to 0 \leq ⦋ I / n ⦌ A))$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrisum.2	$⊢ n = x \to A = B$
10		dchrisum.3	$⊢ φ \to M \in ℕ$
11		dchrisum.4	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℝ$
12		dchrisum.5	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
13		dchrisum.6	$⊢ φ \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
14		dchrisum.7	$⊢ F = (n \in ℕ ⟼ X (L (n)) A)$
15	11	ralrimiva	$⊢ φ \to \forall n \in ℝ^{+} A \in ℝ$
16		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ I / n ⦌ A$
17	16	nfel1	$⊢ Ⅎ n ⦋ I / n ⦌ A \in ℝ$
18		csbeq1a	$⊢ n = I \to A = ⦋ I / n ⦌ A$
19	18	eleq1d	$⊢ n = I \to (A \in ℝ \leftrightarrow ⦋ I / n ⦌ A \in ℝ)$
20	17 19	rspc	$⊢ I \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ I / n ⦌ A \in ℝ)$
21	15 20	syl5com	$⊢ φ \to (I \in ℝ^{+} \to ⦋ I / n ⦌ A \in ℝ)$
22		eqid	$⊢ ℤ_{\geq (⌊I⌋ + 1)} = ℤ_{\geq (⌊I⌋ + 1)}$
23	10	nnred	$⊢ φ \to M \in ℝ$
24		elicopnf	$⊢ M \in ℝ \to (I \in [M, +∞) \leftrightarrow (I \in ℝ \land M \leq I))$
25	23 24	syl	$⊢ φ \to (I \in [M, +∞) \leftrightarrow (I \in ℝ \land M \leq I))$
26	25	simprbda	$⊢ (φ \land I \in [M, +∞)) \to I \in ℝ$
27	26	flcld	$⊢ (φ \land I \in [M, +∞)) \to ⌊I⌋ \in ℤ$
28	27	peano2zd	$⊢ (φ \land I \in [M, +∞)) \to ⌊I⌋ + 1 \in ℤ$
29		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
30		1zzd	$⊢ φ \to 1 \in ℤ$
31		nnrp	$⊢ i \in ℕ \to i \in ℝ^{+}$
32	31	ssriv	$⊢ ℕ \subseteq ℝ^{+}$
33		eqid	$⊢ (n \in ℝ^{+} ⟼ A) = (n \in ℝ^{+} ⟼ A)$
34	33 11	dmmptd	$⊢ φ \to dom (n \in ℝ^{+} ⟼ A) = ℝ^{+}$
35	32 34	sseqtrrid	$⊢ φ \to ℕ \subseteq dom (n \in ℝ^{+} ⟼ A)$
36	29 30 13 35	rlimclim1	$⊢ φ \to (n \in ℝ^{+} ⟼ A) ⇝ 0$
37	36	adantr	$⊢ (φ \land I \in [M, +∞)) \to (n \in ℝ^{+} ⟼ A) ⇝ 0$
38		0red	$⊢ (φ \land I \in [M, +∞)) \to 0 \in ℝ$
39	23	adantr	$⊢ (φ \land I \in [M, +∞)) \to M \in ℝ$
40	10	nngt0d	$⊢ φ \to 0 < M$
41	40	adantr	$⊢ (φ \land I \in [M, +∞)) \to 0 < M$
42	25	simplbda	$⊢ (φ \land I \in [M, +∞)) \to M \leq I$
43	38 39 26 41 42	ltletrd	$⊢ (φ \land I \in [M, +∞)) \to 0 < I$
44	26 43	elrpd	$⊢ (φ \land I \in [M, +∞)) \to I \in ℝ^{+}$
45	15	adantr	$⊢ (φ \land I \in [M, +∞)) \to \forall n \in ℝ^{+} A \in ℝ$
46	44 45 20	sylc	$⊢ (φ \land I \in [M, +∞)) \to ⦋ I / n ⦌ A \in ℝ$
47	46	recnd	$⊢ (φ \land I \in [M, +∞)) \to ⦋ I / n ⦌ A \in ℂ$
48		ssid	$⊢ ℤ_{\geq (⌊I⌋ + 1)} \subseteq ℤ_{\geq (⌊I⌋ + 1)}$
49		fvex	$⊢ ℤ_{\geq (⌊I⌋ + 1)} \in V$
50	48 49	climconst2	$⊢ (⦋ I / n ⦌ A \in ℂ \land ⌊I⌋ + 1 \in ℤ) \to (ℤ_{\geq (⌊I⌋ + 1)} \times \{⦋ I / n ⦌ A\}) ⇝ ⦋ I / n ⦌ A$
51	47 28 50	syl2anc	$⊢ (φ \land I \in [M, +∞)) \to (ℤ_{\geq (⌊I⌋ + 1)} \times \{⦋ I / n ⦌ A\}) ⇝ ⦋ I / n ⦌ A$
52	44	rpge0d	$⊢ (φ \land I \in [M, +∞)) \to 0 \leq I$
53		flge0nn0	$⊢ (I \in ℝ \land 0 \leq I) \to ⌊I⌋ \in ℕ_{0}$
54	26 52 53	syl2anc	$⊢ (φ \land I \in [M, +∞)) \to ⌊I⌋ \in ℕ_{0}$
55		nn0p1nn	$⊢ ⌊I⌋ \in ℕ_{0} \to ⌊I⌋ + 1 \in ℕ$
56	54 55	syl	$⊢ (φ \land I \in [M, +∞)) \to ⌊I⌋ + 1 \in ℕ$
57		eluznn	$⊢ (⌊I⌋ + 1 \in ℕ \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to i \in ℕ$
58	56 57	sylan	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to i \in ℕ$
59	58	nnrpd	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to i \in ℝ^{+}$
60	15	ad2antrr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to \forall n \in ℝ^{+} A \in ℝ$
61		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ i / n ⦌ A$
62	61	nfel1	$⊢ Ⅎ n ⦋ i / n ⦌ A \in ℝ$
63		csbeq1a	$⊢ n = i \to A = ⦋ i / n ⦌ A$
64	63	eleq1d	$⊢ n = i \to (A \in ℝ \leftrightarrow ⦋ i / n ⦌ A \in ℝ)$
65	62 64	rspc	$⊢ i \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ i / n ⦌ A \in ℝ)$
66	59 60 65	sylc	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to ⦋ i / n ⦌ A \in ℝ$
67	33	fvmpts	$⊢ (i \in ℝ^{+} \land ⦋ i / n ⦌ A \in ℝ) \to (n \in ℝ^{+} ⟼ A) (i) = ⦋ i / n ⦌ A$
68	59 66 67	syl2anc	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (n \in ℝ^{+} ⟼ A) (i) = ⦋ i / n ⦌ A$
69	68 66	eqeltrd	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (n \in ℝ^{+} ⟼ A) (i) \in ℝ$
70		fvconst2g	$⊢ (⦋ I / n ⦌ A \in ℝ \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (ℤ_{\geq (⌊I⌋ + 1)} \times \{⦋ I / n ⦌ A\}) (i) = ⦋ I / n ⦌ A$
71	46 70	sylan	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (ℤ_{\geq (⌊I⌋ + 1)} \times \{⦋ I / n ⦌ A\}) (i) = ⦋ I / n ⦌ A$
72	46	adantr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to ⦋ I / n ⦌ A \in ℝ$
73	71 72	eqeltrd	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (ℤ_{\geq (⌊I⌋ + 1)} \times \{⦋ I / n ⦌ A\}) (i) \in ℝ$
74	44	adantr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to I \in ℝ^{+}$
75	12	3expia	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+})) \to ((M \leq n \land n \leq x) \to B \leq A)$
76	75	ralrimivva	$⊢ φ \to \forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A)$
77	76	ad2antrr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to \forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A)$
78		nfcv	$⊢ \underline{Ⅎ} n ℝ^{+}$
79		nfv	$⊢ Ⅎ n (M \leq I \land I \leq x)$
80		nfcv	$⊢ \underline{Ⅎ} n B$
81		nfcv	$⊢ \underline{Ⅎ} n \leq$
82	80 81 16	nfbr	$⊢ Ⅎ n B \leq ⦋ I / n ⦌ A$
83	79 82	nfim	$⊢ Ⅎ n ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A)$
84	78 83	nfralw	$⊢ Ⅎ n \forall x \in ℝ^{+} ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A)$
85		breq2	$⊢ n = I \to (M \leq n \leftrightarrow M \leq I)$
86		breq1	$⊢ n = I \to (n \leq x \leftrightarrow I \leq x)$
87	85 86	anbi12d	$⊢ n = I \to ((M \leq n \land n \leq x) \leftrightarrow (M \leq I \land I \leq x))$
88	18	breq2d	$⊢ n = I \to (B \leq A \leftrightarrow B \leq ⦋ I / n ⦌ A)$
89	87 88	imbi12d	$⊢ n = I \to (((M \leq n \land n \leq x) \to B \leq A) \leftrightarrow ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A))$
90	89	ralbidv	$⊢ n = I \to (\forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A) \leftrightarrow \forall x \in ℝ^{+} ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A))$
91	84 90	rspc	$⊢ I \in ℝ^{+} \to (\forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A) \to \forall x \in ℝ^{+} ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A))$
92	74 77 91	sylc	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to \forall x \in ℝ^{+} ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A)$
93	42	adantr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to M \leq I$
94	26	adantr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to I \in ℝ$
95		reflcl	$⊢ I \in ℝ \to ⌊I⌋ \in ℝ$
96		peano2re	$⊢ ⌊I⌋ \in ℝ \to ⌊I⌋ + 1 \in ℝ$
97	94 95 96	3syl	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to ⌊I⌋ + 1 \in ℝ$
98	58	nnred	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to i \in ℝ$
99		fllep1	$⊢ I \in ℝ \to I \leq ⌊I⌋ + 1$
100	26 99	syl	$⊢ (φ \land I \in [M, +∞)) \to I \leq ⌊I⌋ + 1$
101	100	adantr	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to I \leq ⌊I⌋ + 1$
102		eluzle	$⊢ i \in ℤ_{\geq (⌊I⌋ + 1)} \to ⌊I⌋ + 1 \leq i$
103	102	adantl	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to ⌊I⌋ + 1 \leq i$
104	94 97 98 101 103	letrd	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to I \leq i$
105	93 104	jca	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (M \leq I \land I \leq i)$
106		breq2	$⊢ x = i \to (I \leq x \leftrightarrow I \leq i)$
107	106	anbi2d	$⊢ x = i \to ((M \leq I \land I \leq x) \leftrightarrow (M \leq I \land I \leq i))$
108		eqvisset	$⊢ x = i \to i \in V$
109		equtr2	$⊢ (x = i \land n = i) \to x = n$
110	9	equcoms	$⊢ x = n \to A = B$
111	109 110	syl	$⊢ (x = i \land n = i) \to A = B$
112	108 111	csbied	$⊢ x = i \to ⦋ i / n ⦌ A = B$
113	112	eqcomd	$⊢ x = i \to B = ⦋ i / n ⦌ A$
114	113	breq1d	$⊢ x = i \to (B \leq ⦋ I / n ⦌ A \leftrightarrow ⦋ i / n ⦌ A \leq ⦋ I / n ⦌ A)$
115	107 114	imbi12d	$⊢ x = i \to (((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A) \leftrightarrow ((M \leq I \land I \leq i) \to ⦋ i / n ⦌ A \leq ⦋ I / n ⦌ A))$
116	115	rspcv	$⊢ i \in ℝ^{+} \to (\forall x \in ℝ^{+} ((M \leq I \land I \leq x) \to B \leq ⦋ I / n ⦌ A) \to ((M \leq I \land I \leq i) \to ⦋ i / n ⦌ A \leq ⦋ I / n ⦌ A))$
117	59 92 105 116	syl3c	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to ⦋ i / n ⦌ A \leq ⦋ I / n ⦌ A$
118	117 68 71	3brtr4d	$⊢ ((φ \land I \in [M, +∞)) \land i \in ℤ_{\geq (⌊I⌋ + 1)}) \to (n \in ℝ^{+} ⟼ A) (i) \leq (ℤ_{\geq (⌊I⌋ + 1)} \times \{⦋ I / n ⦌ A\}) (i)$
119	22 28 37 51 69 73 118	climle	$⊢ (φ \land I \in [M, +∞)) \to 0 \leq ⦋ I / n ⦌ A$
120	119	ex	$⊢ φ \to (I \in [M, +∞) \to 0 \leq ⦋ I / n ⦌ A)$
121	21 120	jca	$⊢ φ \to ((I \in ℝ^{+} \to ⦋ I / n ⦌ A \in ℝ) \land (I \in [M, +∞) \to 0 \leq ⦋ I / n ⦌ A))$

Metamath Proof Explorer

Theorem dchrisumlema

Proof