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

Theorem dvfsumleOLD 25975
Description: Obsolete version of dvfsumle 25974 as of 17-Apr-2025. (Contributed by Mario Carneiro, 14-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
dvfsumleOLD.m (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))
dvfsumleOLD.a (πœ‘ β†’ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
dvfsumleOLD.v ((πœ‘ ∧ π‘₯ ∈ (𝑀(,)𝑁)) β†’ 𝐡 ∈ 𝑉)
dvfsumleOLD.b (πœ‘ β†’ (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡))
dvfsumleOLD.c (π‘₯ = 𝑀 β†’ 𝐴 = 𝐢)
dvfsumleOLD.d (π‘₯ = 𝑁 β†’ 𝐴 = 𝐷)
dvfsumleOLD.x ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑋 ∈ ℝ)
dvfsumleOLD.l ((πœ‘ ∧ (π‘˜ ∈ (𝑀..^𝑁) ∧ π‘₯ ∈ (π‘˜(,)(π‘˜ + 1)))) β†’ 𝑋 ≀ 𝐡)
Assertion
Ref Expression
dvfsumleOLD (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀..^𝑁)𝑋 ≀ (𝐷 βˆ’ 𝐢))
Distinct variable groups:   𝐴,π‘˜   π‘₯,π‘˜,𝑀   π‘˜,𝑁,π‘₯   πœ‘,π‘˜,π‘₯   π‘₯,𝑋   π‘₯,𝐢   π‘₯,𝐷   π‘₯,𝑉
Allowed substitution hints:   𝐴(π‘₯)   𝐡(π‘₯,π‘˜)   𝐢(π‘˜)   𝐷(π‘˜)   𝑉(π‘˜)   𝑋(π‘˜)

Proof of Theorem dvfsumleOLD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fzofi 13979 . . . 4 (𝑀..^𝑁) ∈ Fin
21a1i 11 . . 3 (πœ‘ β†’ (𝑀..^𝑁) ∈ Fin)
3 dvfsumleOLD.x . . 3 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑋 ∈ ℝ)
4 dvfsumleOLD.m . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))
5 eluzel2 12865 . . . . . . . . . . 11 (𝑁 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ∈ β„€)
64, 5syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ β„€)
7 eluzelz 12870 . . . . . . . . . . 11 (𝑁 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑁 ∈ β„€)
84, 7syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„€)
9 fzval2 13527 . . . . . . . . . 10 ((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ β„€))
106, 8, 9syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ β„€))
11 inss1 4231 . . . . . . . . 9 ((𝑀[,]𝑁) ∩ β„€) βŠ† (𝑀[,]𝑁)
1210, 11eqsstrdi 4036 . . . . . . . 8 (πœ‘ β†’ (𝑀...𝑁) βŠ† (𝑀[,]𝑁))
1312sselda 3982 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ (𝑀...𝑁)) β†’ 𝑦 ∈ (𝑀[,]𝑁))
14 dvfsumleOLD.a . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
15 cncff 24833 . . . . . . . . . 10 ((π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) β†’ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)βŸΆβ„)
1614, 15syl 17 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)βŸΆβ„)
17 eqid 2728 . . . . . . . . . 10 (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) = (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴)
1817fmpt 7125 . . . . . . . . 9 (βˆ€π‘₯ ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)βŸΆβ„)
1916, 18sylibr 233 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ)
20 nfcsb1v 3919 . . . . . . . . . 10 β„²π‘₯⦋𝑦 / π‘₯⦌𝐴
2120nfel1 2916 . . . . . . . . 9 β„²π‘₯⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ
22 csbeq1a 3908 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ 𝐴 = ⦋𝑦 / π‘₯⦌𝐴)
2322eleq1d 2814 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (𝐴 ∈ ℝ ↔ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ))
2421, 23rspc 3599 . . . . . . . 8 (𝑦 ∈ (𝑀[,]𝑁) β†’ (βˆ€π‘₯ ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ))
2519, 24mpan9 505 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ (𝑀[,]𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
2613, 25syldan 589 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (𝑀...𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
2726ralrimiva 3143 . . . . 5 (πœ‘ β†’ βˆ€π‘¦ ∈ (𝑀...𝑁)⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
28 fzofzp1 13769 . . . . 5 (π‘˜ ∈ (𝑀..^𝑁) β†’ (π‘˜ + 1) ∈ (𝑀...𝑁))
29 csbeq1 3897 . . . . . . 7 (𝑦 = (π‘˜ + 1) β†’ ⦋𝑦 / π‘₯⦌𝐴 = ⦋(π‘˜ + 1) / π‘₯⦌𝐴)
3029eleq1d 2814 . . . . . 6 (𝑦 = (π‘˜ + 1) β†’ (⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ ⦋(π‘˜ + 1) / π‘₯⦌𝐴 ∈ ℝ))
3130rspccva 3610 . . . . 5 ((βˆ€π‘¦ ∈ (𝑀...𝑁)⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ∧ (π‘˜ + 1) ∈ (𝑀...𝑁)) β†’ ⦋(π‘˜ + 1) / π‘₯⦌𝐴 ∈ ℝ)
3227, 28, 31syl2an 594 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ⦋(π‘˜ + 1) / π‘₯⦌𝐴 ∈ ℝ)
33 elfzofz 13688 . . . . 5 (π‘˜ ∈ (𝑀..^𝑁) β†’ π‘˜ ∈ (𝑀...𝑁))
34 csbeq1 3897 . . . . . . 7 (𝑦 = π‘˜ β†’ ⦋𝑦 / π‘₯⦌𝐴 = β¦‹π‘˜ / π‘₯⦌𝐴)
3534eleq1d 2814 . . . . . 6 (𝑦 = π‘˜ β†’ (⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ β¦‹π‘˜ / π‘₯⦌𝐴 ∈ ℝ))
3635rspccva 3610 . . . . 5 ((βˆ€π‘¦ ∈ (𝑀...𝑁)⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ∧ π‘˜ ∈ (𝑀...𝑁)) β†’ β¦‹π‘˜ / π‘₯⦌𝐴 ∈ ℝ)
3727, 33, 36syl2an 594 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ β¦‹π‘˜ / π‘₯⦌𝐴 ∈ ℝ)
3832, 37resubcld 11680 . . 3 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (⦋(π‘˜ + 1) / π‘₯⦌𝐴 βˆ’ β¦‹π‘˜ / π‘₯⦌𝐴) ∈ ℝ)
39 elfzoelz 13672 . . . . . . . . . 10 (π‘˜ ∈ (𝑀..^𝑁) β†’ π‘˜ ∈ β„€)
4039adantl 480 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ π‘˜ ∈ β„€)
4140zred 12704 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ π‘˜ ∈ ℝ)
4241recnd 11280 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ π‘˜ ∈ β„‚)
43 ax-1cn 11204 . . . . . . 7 1 ∈ β„‚
44 pncan2 11505 . . . . . . 7 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ π‘˜) = 1)
4542, 43, 44sylancl 584 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ((π‘˜ + 1) βˆ’ π‘˜) = 1)
4645oveq2d 7442 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑋 Β· ((π‘˜ + 1) βˆ’ π‘˜)) = (𝑋 Β· 1))
473recnd 11280 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑋 ∈ β„‚)
48 peano2re 11425 . . . . . . . 8 (π‘˜ ∈ ℝ β†’ (π‘˜ + 1) ∈ ℝ)
4941, 48syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜ + 1) ∈ ℝ)
5049recnd 11280 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜ + 1) ∈ β„‚)
5147, 50, 42subdid 11708 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑋 Β· ((π‘˜ + 1) βˆ’ π‘˜)) = ((𝑋 Β· (π‘˜ + 1)) βˆ’ (𝑋 Β· π‘˜)))
5247mulridd 11269 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑋 Β· 1) = 𝑋)
5346, 51, 523eqtr3d 2776 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ((𝑋 Β· (π‘˜ + 1)) βˆ’ (𝑋 Β· π‘˜)) = 𝑋)
54 eqid 2728 . . . . . 6 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
5554mulcn 24803 . . . . . 6 Β· ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
566zred 12704 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ ℝ)
5756adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑀 ∈ ℝ)
588zred 12704 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ ℝ)
5958adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑁 ∈ ℝ)
60 elfzole1 13680 . . . . . . . . . . 11 (π‘˜ ∈ (𝑀..^𝑁) β†’ 𝑀 ≀ π‘˜)
6160adantl 480 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑀 ≀ π‘˜)
6228adantl 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜ + 1) ∈ (𝑀...𝑁))
63 elfzle2 13545 . . . . . . . . . . 11 ((π‘˜ + 1) ∈ (𝑀...𝑁) β†’ (π‘˜ + 1) ≀ 𝑁)
6462, 63syl 17 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜ + 1) ≀ 𝑁)
65 iccss 13432 . . . . . . . . . 10 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≀ π‘˜ ∧ (π‘˜ + 1) ≀ 𝑁)) β†’ (π‘˜[,](π‘˜ + 1)) βŠ† (𝑀[,]𝑁))
6657, 59, 61, 64, 65syl22anc 837 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜[,](π‘˜ + 1)) βŠ† (𝑀[,]𝑁))
67 iccssre 13446 . . . . . . . . . . 11 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ (𝑀[,]𝑁) βŠ† ℝ)
6856, 58, 67syl2anc 582 . . . . . . . . . 10 (πœ‘ β†’ (𝑀[,]𝑁) βŠ† ℝ)
6968adantr 479 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑀[,]𝑁) βŠ† ℝ)
7066, 69sstrd 3992 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜[,](π‘˜ + 1)) βŠ† ℝ)
71 ax-resscn 11203 . . . . . . . 8 ℝ βŠ† β„‚
7270, 71sstrdi 3994 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜[,](π‘˜ + 1)) βŠ† β„‚)
7371a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ℝ βŠ† β„‚)
74 cncfmptc 24852 . . . . . . 7 ((𝑋 ∈ ℝ ∧ (π‘˜[,](π‘˜ + 1)) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝑋) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
753, 72, 73, 74syl3anc 1368 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝑋) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
76 cncfmptid 24853 . . . . . . 7 (((π‘˜[,](π‘˜ + 1)) βŠ† ℝ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝑦) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
7770, 71, 76sylancl 584 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝑦) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
78 remulcl 11231 . . . . . 6 ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (𝑋 Β· 𝑦) ∈ ℝ)
7954, 55, 75, 77, 71, 78cncfmpt2ss 24856 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ (𝑋 Β· 𝑦)) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
80 reelprrecn 11238 . . . . . . . 8 ℝ ∈ {ℝ, β„‚}
8180a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ℝ ∈ {ℝ, β„‚})
8257rexrd 11302 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑀 ∈ ℝ*)
83 iooss1 13399 . . . . . . . . . . 11 ((𝑀 ∈ ℝ* ∧ 𝑀 ≀ π‘˜) β†’ (π‘˜(,)(π‘˜ + 1)) βŠ† (𝑀(,)(π‘˜ + 1)))
8482, 61, 83syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜(,)(π‘˜ + 1)) βŠ† (𝑀(,)(π‘˜ + 1)))
8559rexrd 11302 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑁 ∈ ℝ*)
86 iooss2 13400 . . . . . . . . . . 11 ((𝑁 ∈ ℝ* ∧ (π‘˜ + 1) ≀ 𝑁) β†’ (𝑀(,)(π‘˜ + 1)) βŠ† (𝑀(,)𝑁))
8785, 64, 86syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑀(,)(π‘˜ + 1)) βŠ† (𝑀(,)𝑁))
8884, 87sstrd 3992 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜(,)(π‘˜ + 1)) βŠ† (𝑀(,)𝑁))
89 ioossicc 13450 . . . . . . . . . 10 (𝑀(,)𝑁) βŠ† (𝑀[,]𝑁)
9069, 71sstrdi 3994 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑀[,]𝑁) βŠ† β„‚)
9189, 90sstrid 3993 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑀(,)𝑁) βŠ† β„‚)
9288, 91sstrd 3992 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜(,)(π‘˜ + 1)) βŠ† β„‚)
9392sselda 3982 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (π‘˜(,)(π‘˜ + 1))) β†’ 𝑦 ∈ β„‚)
94 1cnd 11247 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (π‘˜(,)(π‘˜ + 1))) β†’ 1 ∈ β„‚)
9573sselda 3982 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
96 1cnd 11247 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) β†’ 1 ∈ β„‚)
9781dvmptid 25909 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
98 ioossre 13425 . . . . . . . . 9 (π‘˜(,)(π‘˜ + 1)) βŠ† ℝ
9998a1i 11 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜(,)(π‘˜ + 1)) βŠ† ℝ)
10054tgioo2 24739 . . . . . . . 8 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
101 iooretop 24702 . . . . . . . . 9 (π‘˜(,)(π‘˜ + 1)) ∈ (topGenβ€˜ran (,))
102101a1i 11 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜(,)(π‘˜ + 1)) ∈ (topGenβ€˜ran (,)))
10381, 95, 96, 97, 99, 100, 54, 102dvmptres 25915 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ 𝑦)) = (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ 1))
10481, 93, 94, 103, 47dvmptcmul 25916 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ (𝑋 Β· 𝑦))) = (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ (𝑋 Β· 1)))
10552mpteq2dv 5254 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ (𝑋 Β· 1)) = (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ 𝑋))
106104, 105eqtrd 2768 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ (𝑋 Β· 𝑦))) = (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ 𝑋))
107 nfcv 2899 . . . . . . 7 Ⅎ𝑦𝐴
108107, 20, 22cbvmpt 5263 . . . . . 6 (π‘₯ ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝐴) = (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ ⦋𝑦 / π‘₯⦌𝐴)
10966resmptd 6049 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ((π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) β†Ύ (π‘˜[,](π‘˜ + 1))) = (π‘₯ ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝐴))
11014adantr 479 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
111 rescncf 24837 . . . . . . . 8 ((π‘˜[,](π‘˜ + 1)) βŠ† (𝑀[,]𝑁) β†’ ((π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) β†’ ((π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) β†Ύ (π‘˜[,](π‘˜ + 1))) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ)))
11266, 110, 111sylc 65 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ((π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴) β†Ύ (π‘˜[,](π‘˜ + 1))) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
113109, 112eqeltrrd 2830 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘₯ ∈ (π‘˜[,](π‘˜ + 1)) ↦ 𝐴) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
114108, 113eqeltrrid 2834 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (𝑦 ∈ (π‘˜[,](π‘˜ + 1)) ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ ((π‘˜[,](π‘˜ + 1))–cn→ℝ))
11516adantr 479 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘₯ ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)βŸΆβ„)
116115, 18sylibr 233 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ βˆ€π‘₯ ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ)
11789sseli 3978 . . . . . . . 8 (𝑦 ∈ (𝑀(,)𝑁) β†’ 𝑦 ∈ (𝑀[,]𝑁))
11824impcom 406 . . . . . . . 8 ((βˆ€π‘₯ ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ ∧ 𝑦 ∈ (𝑀[,]𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
119116, 117, 118syl2an 594 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
120119recnd 11280 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ β„‚)
12189sseli 3978 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑀(,)𝑁) β†’ π‘₯ ∈ (𝑀[,]𝑁))
12216fvmptelcdm 7128 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (𝑀[,]𝑁)) β†’ 𝐴 ∈ ℝ)
123122adantlr 713 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ π‘₯ ∈ (𝑀[,]𝑁)) β†’ 𝐴 ∈ ℝ)
124121, 123sylan2 591 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ π‘₯ ∈ (𝑀(,)𝑁)) β†’ 𝐴 ∈ ℝ)
125124fmpttd 7130 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)βŸΆβ„)
126 ioossre 13425 . . . . . . . . . 10 (𝑀(,)𝑁) βŠ† ℝ
127 dvfre 25903 . . . . . . . . . 10 (((π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)βŸΆβ„ ∧ (𝑀(,)𝑁) βŠ† ℝ) β†’ (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴))βŸΆβ„)
128125, 126, 127sylancl 584 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴))βŸΆβ„)
129 dvfsumleOLD.b . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡))
130129adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡))
131130dmeqd 5912 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ dom (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡))
132 dvfsumleOLD.v . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝑀(,)𝑁)) β†’ 𝐡 ∈ 𝑉)
133132adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ π‘₯ ∈ (𝑀(,)𝑁)) β†’ 𝐡 ∈ 𝑉)
134133ralrimiva 3143 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ βˆ€π‘₯ ∈ (𝑀(,)𝑁)𝐡 ∈ 𝑉)
135 dmmptg 6251 . . . . . . . . . . . 12 (βˆ€π‘₯ ∈ (𝑀(,)𝑁)𝐡 ∈ 𝑉 β†’ dom (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡) = (𝑀(,)𝑁))
136134, 135syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ dom (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡) = (𝑀(,)𝑁))
137131, 136eqtrd 2768 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ dom (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁))
138130, 137feq12d 6715 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ((ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴))βŸΆβ„ ↔ (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡):(𝑀(,)𝑁)βŸΆβ„))
139128, 138mpbid 231 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡):(𝑀(,)𝑁)βŸΆβ„)
140 eqid 2728 . . . . . . . . 9 (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡) = (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡)
141140fmpt 7125 . . . . . . . 8 (βˆ€π‘₯ ∈ (𝑀(,)𝑁)𝐡 ∈ ℝ ↔ (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡):(𝑀(,)𝑁)βŸΆβ„)
142139, 141sylibr 233 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ βˆ€π‘₯ ∈ (𝑀(,)𝑁)𝐡 ∈ ℝ)
143 nfcsb1v 3919 . . . . . . . . 9 β„²π‘₯⦋𝑦 / π‘₯⦌𝐡
144143nfel1 2916 . . . . . . . 8 β„²π‘₯⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ
145 csbeq1a 3908 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ 𝐡 = ⦋𝑦 / π‘₯⦌𝐡)
146145eleq1d 2814 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (𝐡 ∈ ℝ ↔ ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ))
147144, 146rspc 3599 . . . . . . 7 (𝑦 ∈ (𝑀(,)𝑁) β†’ (βˆ€π‘₯ ∈ (𝑀(,)𝑁)𝐡 ∈ ℝ β†’ ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ))
148142, 147mpan9 505 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ)
149107, 20, 22cbvmpt 5263 . . . . . . . 8 (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / π‘₯⦌𝐴)
150149oveq2i 7437 . . . . . . 7 (ℝ D (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / π‘₯⦌𝐴))
151 nfcv 2899 . . . . . . . 8 Ⅎ𝑦𝐡
152151, 143, 145cbvmpt 5263 . . . . . . 7 (π‘₯ ∈ (𝑀(,)𝑁) ↦ 𝐡) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / π‘₯⦌𝐡)
153130, 150, 1523eqtr3g 2791 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / π‘₯⦌𝐴)) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / π‘₯⦌𝐡))
15481, 120, 148, 153, 88, 100, 54, 102dvmptres 25915 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (ℝ D (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ ⦋𝑦 / π‘₯⦌𝐴)) = (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) ↦ ⦋𝑦 / π‘₯⦌𝐡))
155 dvfsumleOLD.l . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ (𝑀..^𝑁) ∧ π‘₯ ∈ (π‘˜(,)(π‘˜ + 1)))) β†’ 𝑋 ≀ 𝐡)
156155anassrs 466 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ π‘₯ ∈ (π‘˜(,)(π‘˜ + 1))) β†’ 𝑋 ≀ 𝐡)
157156ralrimiva 3143 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ βˆ€π‘₯ ∈ (π‘˜(,)(π‘˜ + 1))𝑋 ≀ 𝐡)
158 nfcv 2899 . . . . . . . 8 β„²π‘₯𝑋
159 nfcv 2899 . . . . . . . 8 β„²π‘₯ ≀
160158, 159, 143nfbr 5199 . . . . . . 7 β„²π‘₯ 𝑋 ≀ ⦋𝑦 / π‘₯⦌𝐡
161145breq2d 5164 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑋 ≀ 𝐡 ↔ 𝑋 ≀ ⦋𝑦 / π‘₯⦌𝐡))
162160, 161rspc 3599 . . . . . 6 (𝑦 ∈ (π‘˜(,)(π‘˜ + 1)) β†’ (βˆ€π‘₯ ∈ (π‘˜(,)(π‘˜ + 1))𝑋 ≀ 𝐡 β†’ 𝑋 ≀ ⦋𝑦 / π‘₯⦌𝐡))
163157, 162mpan9 505 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (π‘˜(,)(π‘˜ + 1))) β†’ 𝑋 ≀ ⦋𝑦 / π‘₯⦌𝐡)
16441rexrd 11302 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ π‘˜ ∈ ℝ*)
16549rexrd 11302 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜ + 1) ∈ ℝ*)
16641lep1d 12183 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ π‘˜ ≀ (π‘˜ + 1))
167 lbicc2 13481 . . . . . 6 ((π‘˜ ∈ ℝ* ∧ (π‘˜ + 1) ∈ ℝ* ∧ π‘˜ ≀ (π‘˜ + 1)) β†’ π‘˜ ∈ (π‘˜[,](π‘˜ + 1)))
168164, 165, 166, 167syl3anc 1368 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ π‘˜ ∈ (π‘˜[,](π‘˜ + 1)))
169 ubicc2 13482 . . . . . 6 ((π‘˜ ∈ ℝ* ∧ (π‘˜ + 1) ∈ ℝ* ∧ π‘˜ ≀ (π‘˜ + 1)) β†’ (π‘˜ + 1) ∈ (π‘˜[,](π‘˜ + 1)))
170164, 165, 166, 169syl3anc 1368 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ (π‘˜ + 1) ∈ (π‘˜[,](π‘˜ + 1)))
171 oveq2 7434 . . . . 5 (𝑦 = π‘˜ β†’ (𝑋 Β· 𝑦) = (𝑋 Β· π‘˜))
172 oveq2 7434 . . . . 5 (𝑦 = (π‘˜ + 1) β†’ (𝑋 Β· 𝑦) = (𝑋 Β· (π‘˜ + 1)))
17341, 49, 79, 106, 114, 154, 163, 168, 170, 166, 171, 34, 172, 29dvle 25960 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ ((𝑋 Β· (π‘˜ + 1)) βˆ’ (𝑋 Β· π‘˜)) ≀ (⦋(π‘˜ + 1) / π‘₯⦌𝐴 βˆ’ β¦‹π‘˜ / π‘₯⦌𝐴))
17453, 173eqbrtrrd 5176 . . 3 ((πœ‘ ∧ π‘˜ ∈ (𝑀..^𝑁)) β†’ 𝑋 ≀ (⦋(π‘˜ + 1) / π‘₯⦌𝐴 βˆ’ β¦‹π‘˜ / π‘₯⦌𝐴))
1752, 3, 38, 174fsumle 15785 . 2 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀..^𝑁)𝑋 ≀ Ξ£π‘˜ ∈ (𝑀..^𝑁)(⦋(π‘˜ + 1) / π‘₯⦌𝐴 βˆ’ β¦‹π‘˜ / π‘₯⦌𝐴))
176 vex 3477 . . . . 5 𝑦 ∈ V
177176a1i 11 . . . 4 (𝑦 = 𝑀 β†’ 𝑦 ∈ V)
178 eqeq2 2740 . . . . . 6 (𝑦 = 𝑀 β†’ (π‘₯ = 𝑦 ↔ π‘₯ = 𝑀))
179178biimpa 475 . . . . 5 ((𝑦 = 𝑀 ∧ π‘₯ = 𝑦) β†’ π‘₯ = 𝑀)
180 dvfsumleOLD.c . . . . 5 (π‘₯ = 𝑀 β†’ 𝐴 = 𝐢)
181179, 180syl 17 . . . 4 ((𝑦 = 𝑀 ∧ π‘₯ = 𝑦) β†’ 𝐴 = 𝐢)
182177, 181csbied 3932 . . 3 (𝑦 = 𝑀 β†’ ⦋𝑦 / π‘₯⦌𝐴 = 𝐢)
183176a1i 11 . . . 4 (𝑦 = 𝑁 β†’ 𝑦 ∈ V)
184 eqeq2 2740 . . . . . 6 (𝑦 = 𝑁 β†’ (π‘₯ = 𝑦 ↔ π‘₯ = 𝑁))
185184biimpa 475 . . . . 5 ((𝑦 = 𝑁 ∧ π‘₯ = 𝑦) β†’ π‘₯ = 𝑁)
186 dvfsumleOLD.d . . . . 5 (π‘₯ = 𝑁 β†’ 𝐴 = 𝐷)
187185, 186syl 17 . . . 4 ((𝑦 = 𝑁 ∧ π‘₯ = 𝑦) β†’ 𝐴 = 𝐷)
188183, 187csbied 3932 . . 3 (𝑦 = 𝑁 β†’ ⦋𝑦 / π‘₯⦌𝐴 = 𝐷)
18926recnd 11280 . . 3 ((πœ‘ ∧ 𝑦 ∈ (𝑀...𝑁)) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ β„‚)
19034, 29, 182, 188, 4, 189telfsumo2 15789 . 2 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀..^𝑁)(⦋(π‘˜ + 1) / π‘₯⦌𝐴 βˆ’ β¦‹π‘˜ / π‘₯⦌𝐴) = (𝐷 βˆ’ 𝐢))
191175, 190breqtrd 5178 1 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀..^𝑁)𝑋 ≀ (𝐷 βˆ’ 𝐢))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  βˆ€wral 3058  Vcvv 3473  β¦‹csb 3894   ∩ cin 3948   βŠ† wss 3949  {cpr 4634   class class class wbr 5152   ↦ cmpt 5235  dom cdm 5682  ran crn 5683   β†Ύ cres 5684  βŸΆwf 6549  β€˜cfv 6553  (class class class)co 7426  Fincfn 8970  β„‚cc 11144  β„cr 11145  1c1 11147   + caddc 11149   Β· cmul 11151  β„*cxr 11285   ≀ cle 11287   βˆ’ cmin 11482  β„€cz 12596  β„€β‰₯cuz 12860  (,)cioo 13364  [,]cicc 13367  ...cfz 13524  ..^cfzo 13667  Ξ£csu 15672  TopOpenctopn 17410  topGenctg 17426  β„‚fldccnfld 21286  β€“cnβ†’ccncf 24816   D cdv 25812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225  ax-mulf 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-er 8731  df-map 8853  df-pm 8854  df-ixp 8923  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-fi 9442  df-sup 9473  df-inf 9474  df-oi 9541  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-seq 14007  df-exp 14067  df-hash 14330  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-clim 15472  df-sum 15673  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-mulr 17254  df-starv 17255  df-sca 17256  df-vsca 17257  df-ip 17258  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-hom 17264  df-cco 17265  df-rest 17411  df-topn 17412  df-0g 17430  df-gsum 17431  df-topgen 17432  df-pt 17433  df-prds 17436  df-xrs 17491  df-qtop 17496  df-imas 17497  df-xps 17499  df-mre 17573  df-mrc 17574  df-acs 17576  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-submnd 18748  df-mulg 19031  df-cntz 19275  df-cmn 19744  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-fbas 21283  df-fg 21284  df-cnfld 21287  df-top 22816  df-topon 22833  df-topsp 22855  df-bases 22869  df-cld 22943  df-ntr 22944  df-cls 22945  df-nei 23022  df-lp 23060  df-perf 23061  df-cn 23151  df-cnp 23152  df-haus 23239  df-cmp 23311  df-tx 23486  df-hmeo 23679  df-fil 23770  df-fm 23862  df-flim 23863  df-flf 23864  df-xms 24246  df-ms 24247  df-tms 24248  df-cncf 24818  df-limc 25815  df-dv 25816
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator