Metamath Proof Explorer

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 ≤ ⦋ 𝐼 / 𝑛 ⦌ 𝐴 ) ) )