MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlema Structured version   Visualization version   GIF version

Theorem dchrisumlema 26852
Description: Lemma for dchrisum 26856. 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 = (0gβ€˜πΊ)
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.
StepHypRef Expression
1 dchrisum.4 . . . 4 ((πœ‘ ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
21ralrimiva 3144 . . 3 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
3 nfcsb1v 3885 . . . . 5 Ⅎ𝑛⦋𝐼 / π‘›β¦Œπ΄
43nfel1 2924 . . . 4 Ⅎ𝑛⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ
5 csbeq1a 3874 . . . . 5 (𝑛 = 𝐼 β†’ 𝐴 = ⦋𝐼 / π‘›β¦Œπ΄)
65eleq1d 2823 . . . 4 (𝑛 = 𝐼 β†’ (𝐴 ∈ ℝ ↔ ⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ))
74, 6rspc 3572 . . 3 (𝐼 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ))
82, 7syl5com 31 . 2 (πœ‘ β†’ (𝐼 ∈ ℝ+ β†’ ⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ))
9 eqid 2737 . . . 4 (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) = (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))
10 dchrisum.3 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ∈ β„•)
1110nnred 12175 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ ℝ)
12 elicopnf 13369 . . . . . . . 8 (𝑀 ∈ ℝ β†’ (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≀ 𝐼)))
1311, 12syl 17 . . . . . . 7 (πœ‘ β†’ (𝐼 ∈ (𝑀[,)+∞) ↔ (𝐼 ∈ ℝ ∧ 𝑀 ≀ 𝐼)))
1413simprbda 500 . . . . . 6 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 𝐼 ∈ ℝ)
1514flcld 13710 . . . . 5 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ (βŒŠβ€˜πΌ) ∈ β„€)
1615peano2zd 12617 . . . 4 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ ((βŒŠβ€˜πΌ) + 1) ∈ β„€)
17 nnuz 12813 . . . . . 6 β„• = (β„€β‰₯β€˜1)
18 1zzd 12541 . . . . . 6 (πœ‘ β†’ 1 ∈ β„€)
19 dchrisum.6 . . . . . 6 (πœ‘ β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
20 nnrp 12933 . . . . . . . 8 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
2120ssriv 3953 . . . . . . 7 β„• βŠ† ℝ+
22 eqid 2737 . . . . . . . 8 (𝑛 ∈ ℝ+ ↦ 𝐴) = (𝑛 ∈ ℝ+ ↦ 𝐴)
2322, 1dmmptd 6651 . . . . . . 7 (πœ‘ β†’ dom (𝑛 ∈ ℝ+ ↦ 𝐴) = ℝ+)
2421, 23sseqtrrid 4002 . . . . . 6 (πœ‘ β†’ β„• βŠ† dom (𝑛 ∈ ℝ+ ↦ 𝐴))
2517, 18, 19, 24rlimclim1 15434 . . . . 5 (πœ‘ β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝ 0)
2625adantr 482 . . . 4 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝ 0)
27 0red 11165 . . . . . . . . 9 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 0 ∈ ℝ)
2811adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ ℝ)
2910nngt0d 12209 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝑀)
3029adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 0 < 𝑀)
3113simplbda 501 . . . . . . . . 9 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 𝑀 ≀ 𝐼)
3227, 28, 14, 30, 31ltletrd 11322 . . . . . . . 8 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 0 < 𝐼)
3314, 32elrpd 12961 . . . . . . 7 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 𝐼 ∈ ℝ+)
342adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
3533, 34, 7sylc 65 . . . . . 6 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ ⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ)
3635recnd 11190 . . . . 5 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ ⦋𝐼 / π‘›β¦Œπ΄ ∈ β„‚)
37 ssid 3971 . . . . . 6 (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) βŠ† (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))
38 fvex 6860 . . . . . 6 (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) ∈ V
3937, 38climconst2 15437 . . . . 5 ((⦋𝐼 / π‘›β¦Œπ΄ ∈ β„‚ ∧ ((βŒŠβ€˜πΌ) + 1) ∈ β„€) β†’ ((β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) Γ— {⦋𝐼 / π‘›β¦Œπ΄}) ⇝ ⦋𝐼 / π‘›β¦Œπ΄)
4036, 16, 39syl2anc 585 . . . 4 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ ((β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) Γ— {⦋𝐼 / π‘›β¦Œπ΄}) ⇝ ⦋𝐼 / π‘›β¦Œπ΄)
4133rpge0d 12968 . . . . . . . . . 10 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 0 ≀ 𝐼)
42 flge0nn0 13732 . . . . . . . . . 10 ((𝐼 ∈ ℝ ∧ 0 ≀ 𝐼) β†’ (βŒŠβ€˜πΌ) ∈ β„•0)
4314, 41, 42syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ (βŒŠβ€˜πΌ) ∈ β„•0)
44 nn0p1nn 12459 . . . . . . . . 9 ((βŒŠβ€˜πΌ) ∈ β„•0 β†’ ((βŒŠβ€˜πΌ) + 1) ∈ β„•)
4543, 44syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ ((βŒŠβ€˜πΌ) + 1) ∈ β„•)
46 eluznn 12850 . . . . . . . 8 ((((βŒŠβ€˜πΌ) + 1) ∈ β„• ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝑖 ∈ β„•)
4745, 46sylan 581 . . . . . . 7 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝑖 ∈ β„•)
4847nnrpd 12962 . . . . . 6 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝑖 ∈ ℝ+)
492ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
50 nfcsb1v 3885 . . . . . . . . 9 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄
5150nfel1 2924 . . . . . . . 8 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ
52 csbeq1a 3874 . . . . . . . . 9 (𝑛 = 𝑖 β†’ 𝐴 = ⦋𝑖 / π‘›β¦Œπ΄)
5352eleq1d 2823 . . . . . . . 8 (𝑛 = 𝑖 β†’ (𝐴 ∈ ℝ ↔ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
5451, 53rspc 3572 . . . . . . 7 (𝑖 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
5548, 49, 54sylc 65 . . . . . 6 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
5622fvmpts 6956 . . . . . 6 ((𝑖 ∈ ℝ+ ∧ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ) β†’ ((𝑛 ∈ ℝ+ ↦ 𝐴)β€˜π‘–) = ⦋𝑖 / π‘›β¦Œπ΄)
5748, 55, 56syl2anc 585 . . . . 5 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ((𝑛 ∈ ℝ+ ↦ 𝐴)β€˜π‘–) = ⦋𝑖 / π‘›β¦Œπ΄)
5857, 55eqeltrd 2838 . . . 4 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ((𝑛 ∈ ℝ+ ↦ 𝐴)β€˜π‘–) ∈ ℝ)
59 fvconst2g 7156 . . . . . 6 ((⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ (((β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) Γ— {⦋𝐼 / π‘›β¦Œπ΄})β€˜π‘–) = ⦋𝐼 / π‘›β¦Œπ΄)
6035, 59sylan 581 . . . . 5 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ (((β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) Γ— {⦋𝐼 / π‘›β¦Œπ΄})β€˜π‘–) = ⦋𝐼 / π‘›β¦Œπ΄)
6135adantr 482 . . . . 5 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ)
6260, 61eqeltrd 2838 . . . 4 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ (((β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) Γ— {⦋𝐼 / π‘›β¦Œπ΄})β€˜π‘–) ∈ ℝ)
6333adantr 482 . . . . . . 7 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝐼 ∈ ℝ+)
64 dchrisum.5 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
65643expia 1122 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+)) β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
6665ralrimivva 3198 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
6766ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
68 nfcv 2908 . . . . . . . . 9 Ⅎ𝑛ℝ+
69 nfv 1918 . . . . . . . . . 10 Ⅎ𝑛(𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯)
70 nfcv 2908 . . . . . . . . . . 11 Ⅎ𝑛𝐡
71 nfcv 2908 . . . . . . . . . . 11 Ⅎ𝑛 ≀
7270, 71, 3nfbr 5157 . . . . . . . . . 10 Ⅎ𝑛 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄
7369, 72nfim 1900 . . . . . . . . 9 Ⅎ𝑛((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄)
7468, 73nfralw 3297 . . . . . . . 8 β„²π‘›βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄)
75 breq2 5114 . . . . . . . . . . 11 (𝑛 = 𝐼 β†’ (𝑀 ≀ 𝑛 ↔ 𝑀 ≀ 𝐼))
76 breq1 5113 . . . . . . . . . . 11 (𝑛 = 𝐼 β†’ (𝑛 ≀ π‘₯ ↔ 𝐼 ≀ π‘₯))
7775, 76anbi12d 632 . . . . . . . . . 10 (𝑛 = 𝐼 β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) ↔ (𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯)))
785breq2d 5122 . . . . . . . . . 10 (𝑛 = 𝐼 β†’ (𝐡 ≀ 𝐴 ↔ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄))
7977, 78imbi12d 345 . . . . . . . . 9 (𝑛 = 𝐼 β†’ (((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄)))
8079ralbidv 3175 . . . . . . . 8 (𝑛 = 𝐼 β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄)))
8174, 80rspc 3572 . . . . . . 7 (𝐼 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄)))
8263, 67, 81sylc 65 . . . . . 6 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄))
8331adantr 482 . . . . . . 7 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝑀 ≀ 𝐼)
8414adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝐼 ∈ ℝ)
85 reflcl 13708 . . . . . . . . 9 (𝐼 ∈ ℝ β†’ (βŒŠβ€˜πΌ) ∈ ℝ)
86 peano2re 11335 . . . . . . . . 9 ((βŒŠβ€˜πΌ) ∈ ℝ β†’ ((βŒŠβ€˜πΌ) + 1) ∈ ℝ)
8784, 85, 863syl 18 . . . . . . . 8 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ((βŒŠβ€˜πΌ) + 1) ∈ ℝ)
8847nnred 12175 . . . . . . . 8 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝑖 ∈ ℝ)
89 fllep1 13713 . . . . . . . . . 10 (𝐼 ∈ ℝ β†’ 𝐼 ≀ ((βŒŠβ€˜πΌ) + 1))
9014, 89syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 𝐼 ≀ ((βŒŠβ€˜πΌ) + 1))
9190adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝐼 ≀ ((βŒŠβ€˜πΌ) + 1))
92 eluzle 12783 . . . . . . . . 9 (𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) β†’ ((βŒŠβ€˜πΌ) + 1) ≀ 𝑖)
9392adantl 483 . . . . . . . 8 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ((βŒŠβ€˜πΌ) + 1) ≀ 𝑖)
9484, 87, 88, 91, 93letrd 11319 . . . . . . 7 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ 𝐼 ≀ 𝑖)
9583, 94jca 513 . . . . . 6 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ (𝑀 ≀ 𝐼 ∧ 𝐼 ≀ 𝑖))
96 breq2 5114 . . . . . . . . 9 (π‘₯ = 𝑖 β†’ (𝐼 ≀ π‘₯ ↔ 𝐼 ≀ 𝑖))
9796anbi2d 630 . . . . . . . 8 (π‘₯ = 𝑖 β†’ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) ↔ (𝑀 ≀ 𝐼 ∧ 𝐼 ≀ 𝑖)))
98 eqvisset 3465 . . . . . . . . . . 11 (π‘₯ = 𝑖 β†’ 𝑖 ∈ V)
99 equtr2 2031 . . . . . . . . . . . 12 ((π‘₯ = 𝑖 ∧ 𝑛 = 𝑖) β†’ π‘₯ = 𝑛)
100 dchrisum.2 . . . . . . . . . . . . 13 (𝑛 = π‘₯ β†’ 𝐴 = 𝐡)
101100equcoms 2024 . . . . . . . . . . . 12 (π‘₯ = 𝑛 β†’ 𝐴 = 𝐡)
10299, 101syl 17 . . . . . . . . . . 11 ((π‘₯ = 𝑖 ∧ 𝑛 = 𝑖) β†’ 𝐴 = 𝐡)
10398, 102csbied 3898 . . . . . . . . . 10 (π‘₯ = 𝑖 β†’ ⦋𝑖 / π‘›β¦Œπ΄ = 𝐡)
104103eqcomd 2743 . . . . . . . . 9 (π‘₯ = 𝑖 β†’ 𝐡 = ⦋𝑖 / π‘›β¦Œπ΄)
105104breq1d 5120 . . . . . . . 8 (π‘₯ = 𝑖 β†’ (𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄ ↔ ⦋𝑖 / π‘›β¦Œπ΄ ≀ ⦋𝐼 / π‘›β¦Œπ΄))
10697, 105imbi12d 345 . . . . . . 7 (π‘₯ = 𝑖 β†’ (((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄) ↔ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ 𝑖) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ≀ ⦋𝐼 / π‘›β¦Œπ΄)))
107106rspcv 3580 . . . . . 6 (𝑖 ∈ ℝ+ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝐼 / π‘›β¦Œπ΄) β†’ ((𝑀 ≀ 𝐼 ∧ 𝐼 ≀ 𝑖) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ≀ ⦋𝐼 / π‘›β¦Œπ΄)))
10848, 82, 95, 107syl3c 66 . . . . 5 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ≀ ⦋𝐼 / π‘›β¦Œπ΄)
109108, 57, 603brtr4d 5142 . . . 4 (((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1))) β†’ ((𝑛 ∈ ℝ+ ↦ 𝐴)β€˜π‘–) ≀ (((β„€β‰₯β€˜((βŒŠβ€˜πΌ) + 1)) Γ— {⦋𝐼 / π‘›β¦Œπ΄})β€˜π‘–))
1109, 16, 26, 40, 58, 62, 109climle 15529 . . 3 ((πœ‘ ∧ 𝐼 ∈ (𝑀[,)+∞)) β†’ 0 ≀ ⦋𝐼 / π‘›β¦Œπ΄)
111110ex 414 . 2 (πœ‘ β†’ (𝐼 ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋𝐼 / π‘›β¦Œπ΄))
1128, 111jca 513 1 (πœ‘ β†’ ((𝐼 ∈ ℝ+ β†’ ⦋𝐼 / π‘›β¦Œπ΄ ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋𝐼 / π‘›β¦Œπ΄)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  Vcvv 3448  β¦‹csb 3860  {csn 4591   class class class wbr 5110   ↦ cmpt 5193   Γ— cxp 5636  dom cdm 5638  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193   < clt 11196   ≀ cle 11197  β„•cn 12160  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  [,)cico 13273  βŒŠcfl 13702   ⇝ cli 15373   β‡π‘Ÿ crli 15374  Basecbs 17090  0gc0g 17328  β„€RHomczrh 20916  β„€/nβ„€czn 20919  DChrcdchr 26596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-sup 9385  df-inf 9386  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fl 13704  df-seq 13914  df-exp 13975  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-rlim 15378
This theorem is referenced by:  dchrisumlem2  26854  dchrisumlem3  26855
  Copyright terms: Public domain W3C validator