Theorem dchrisumlema

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrisum.2	⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
	dchrisum.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	dchrisum.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
	dchrisum.5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
	dchrisum.6	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
	dchrisum.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
Assertion	dchrisumlema	⊢ ( 𝜑 → ( ( 𝐼 ∈ ℝ+ → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( 𝐼 ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrisum.2	⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
10		dchrisum.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11		dchrisum.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
12		dchrisum.5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
13		dchrisum.6	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
14		dchrisum.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
15	11	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
16		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝐼 / 𝑛 ⦌ 𝐴
17	16	nfel1	⊢ Ⅎ 𝑛 ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ
18		csbeq1a	⊢ ( 𝑛 = 𝐼 → 𝐴 = ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
19	18	eleq1d	⊢ ( 𝑛 = 𝐼 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
20	17 19	rspc	⊢ ( 𝐼 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
21	15 20	syl5com	⊢ ( 𝜑 → ( 𝐼 ∈ ℝ+ → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
22		eqid	⊢ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) = ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) )
23	10	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
24		elicopnf	⊢ ( 𝑀 ∈ ℝ → ( 𝐼 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼 ) ) )
25	23 24	syl	⊢ ( 𝜑 → ( 𝐼 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝐼 ∈ ℝ ∧ 𝑀 ≤ 𝐼 ) ) )
26	25	simprbda	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 𝐼 ∈ ℝ )
27	26	flcld	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ( ⌊ ‘ 𝐼 ) ∈ ℤ )
28	27	peano2zd	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℤ )
29		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
30		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
31		nnrp	⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ+ )
32	31	ssriv	⊢ ℕ ⊆ ℝ+
33		eqid	⊢ ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) = ( 𝑛 ∈ ℝ+ ↦ 𝐴 )
34	33 11	dmmptd	⊢ ( 𝜑 → dom ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) = ℝ+ )
35	32 34	sseqtrrid	⊢ ( 𝜑 → ℕ ⊆ dom ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) )
36	29 30 13 35	rlimclim1	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝ 0 )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝ 0 )
38		0red	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 0 ∈ ℝ )
39	23	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℝ )
40	10	nngt0d	⊢ ( 𝜑 → 0 < 𝑀 )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 0 < 𝑀 )
42	25	simplbda	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝐼 )
43	38 39 26 41 42	ltletrd	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 0 < 𝐼 )
44	26 43	elrpd	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 𝐼 ∈ ℝ+ )
45	15	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
46	44 45 20	sylc	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ )
47	46	recnd	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℂ )
48		ssid	⊢ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ⊆ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) )
49		fvex	⊢ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ∈ V
50	48 49	climconst2	⊢ ( ( ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℂ ∧ ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℤ ) → ( ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) × { ⦋ 𝐼 / 𝑛 ⦌ 𝐴 } ) ⇝ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
51	47 28 50	syl2anc	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ( ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) × { ⦋ 𝐼 / 𝑛 ⦌ 𝐴 } ) ⇝ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
52	44	rpge0d	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 0 ≤ 𝐼 )
53		flge0nn0	⊢ ( ( 𝐼 ∈ ℝ ∧ 0 ≤ 𝐼 ) → ( ⌊ ‘ 𝐼 ) ∈ ℕ0 )
54	26 52 53	syl2anc	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ( ⌊ ‘ 𝐼 ) ∈ ℕ0 )
55		nn0p1nn	⊢ ( ( ⌊ ‘ 𝐼 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℕ )
56	54 55	syl	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℕ )
57		eluznn	⊢ ( ( ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝑖 ∈ ℕ )
58	56 57	sylan	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝑖 ∈ ℕ )
59	58	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝑖 ∈ ℝ+ )
60	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
61		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴
62	61	nfel1	⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ
63		csbeq1a	⊢ ( 𝑛 = 𝑖 → 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
64	63	eleq1d	⊢ ( 𝑛 = 𝑖 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
65	62 64	rspc	⊢ ( 𝑖 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
66	59 60 65	sylc	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
67	33	fvmpts	⊢ ( ( 𝑖 ∈ ℝ+ ∧ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) → ( ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ‘ 𝑖 ) = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
68	59 66 67	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ‘ 𝑖 ) = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
69	68 66	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
70		fvconst2g	⊢ ( ( ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) × { ⦋ 𝐼 / 𝑛 ⦌ 𝐴 } ) ‘ 𝑖 ) = ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
71	46 70	sylan	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) × { ⦋ 𝐼 / 𝑛 ⦌ 𝐴 } ) ‘ 𝑖 ) = ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
72	46	adantr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ )
73	71 72	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) × { ⦋ 𝐼 / 𝑛 ⦌ 𝐴 } ) ‘ 𝑖 ) ∈ ℝ )
74	44	adantr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝐼 ∈ ℝ+ )
75	12	3expia	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ) → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) )
76	75	ralrimivva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) )
77	76	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) )
78		nfcv	⊢ Ⅎ 𝑛 ℝ+
79		nfv	⊢ Ⅎ 𝑛 ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 )
80		nfcv	⊢ Ⅎ 𝑛 𝐵
81		nfcv	⊢ Ⅎ 𝑛 ≤
82	80 81 16	nfbr	⊢ Ⅎ 𝑛 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴
83	79 82	nfim	⊢ Ⅎ 𝑛 ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
84	78 83	nfralw	⊢ Ⅎ 𝑛 ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
85		breq2	⊢ ( 𝑛 = 𝐼 → ( 𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝐼 ) )
86		breq1	⊢ ( 𝑛 = 𝐼 → ( 𝑛 ≤ 𝑥 ↔ 𝐼 ≤ 𝑥 ) )
87	85 86	anbi12d	⊢ ( 𝑛 = 𝐼 → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ↔ ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) ) )
88	18	breq2d	⊢ ( 𝑛 = 𝐼 → ( 𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) )
89	87 88	imbi12d	⊢ ( 𝑛 = 𝐼 → ( ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) ↔ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )
90	89	ralbidv	⊢ ( 𝑛 = 𝐼 → ( ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )
91	84 90	rspc	⊢ ( 𝐼 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )
92	74 77 91	sylc	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) )
93	42	adantr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝑀 ≤ 𝐼 )
94	26	adantr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝐼 ∈ ℝ )
95		reflcl	⊢ ( 𝐼 ∈ ℝ → ( ⌊ ‘ 𝐼 ) ∈ ℝ )
96		peano2re	⊢ ( ( ⌊ ‘ 𝐼 ) ∈ ℝ → ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℝ )
97	94 95 96	3syl	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝐼 ) + 1 ) ∈ ℝ )
98	58	nnred	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝑖 ∈ ℝ )
99		fllep1	⊢ ( 𝐼 ∈ ℝ → 𝐼 ≤ ( ( ⌊ ‘ 𝐼 ) + 1 ) )
100	26 99	syl	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 𝐼 ≤ ( ( ⌊ ‘ 𝐼 ) + 1 ) )
101	100	adantr	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝐼 ≤ ( ( ⌊ ‘ 𝐼 ) + 1 ) )
102		eluzle	⊢ ( 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) → ( ( ⌊ ‘ 𝐼 ) + 1 ) ≤ 𝑖 )
103	102	adantl	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝐼 ) + 1 ) ≤ 𝑖 )
104	94 97 98 101 103	letrd	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → 𝐼 ≤ 𝑖 )
105	93 104	jca	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖 ) )
106		breq2	⊢ ( 𝑥 = 𝑖 → ( 𝐼 ≤ 𝑥 ↔ 𝐼 ≤ 𝑖 ) )
107	106	anbi2d	⊢ ( 𝑥 = 𝑖 → ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) ↔ ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖 ) ) )
108		eqvisset	⊢ ( 𝑥 = 𝑖 → 𝑖 ∈ V )
109		equtr2	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑛 = 𝑖 ) → 𝑥 = 𝑛 )
110	9	equcoms	⊢ ( 𝑥 = 𝑛 → 𝐴 = 𝐵 )
111	109 110	syl	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑛 = 𝑖 ) → 𝐴 = 𝐵 )
112	108 111	csbied	⊢ ( 𝑥 = 𝑖 → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 = 𝐵 )
113	112	eqcomd	⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
114	113	breq1d	⊢ ( 𝑥 = 𝑖 → ( 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ↔ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) )
115	107 114	imbi12d	⊢ ( 𝑥 = 𝑖 → ( ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ↔ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖 ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )
116	115	rspcv	⊢ ( 𝑖 ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) → ( ( 𝑀 ≤ 𝐼 ∧ 𝐼 ≤ 𝑖 ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )
117	59 92 105 116	syl3c	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
118	117 68 71	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) ) → ( ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ‘ 𝑖 ) ≤ ( ( ( ℤ≥ ‘ ( ( ⌊ ‘ 𝐼 ) + 1 ) ) × { ⦋ 𝐼 / 𝑛 ⦌ 𝐴 } ) ‘ 𝑖 ) )
119	22 28 37 51 69 73 118	climle	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 [,) +∞ ) ) → 0 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 )
120	119	ex	⊢ ( 𝜑 → ( 𝐼 ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) )
121	21 120	jca	⊢ ( 𝜑 → ( ( 𝐼 ∈ ℝ+ → ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( 𝐼 ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )