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

Theorem dvfsumlem2 25979
Description: Lemma for dvfsumrlim 25984. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11218. (Revised by GG, 16-Mar-2025.)
Hypotheses
Ref Expression
dvfsum.s 𝑆 = (𝑇(,)+∞)
dvfsum.z 𝑍 = (β„€β‰₯β€˜π‘€)
dvfsum.m (πœ‘ β†’ 𝑀 ∈ β„€)
dvfsum.d (πœ‘ β†’ 𝐷 ∈ ℝ)
dvfsum.md (πœ‘ β†’ 𝑀 ≀ (𝐷 + 1))
dvfsum.t (πœ‘ β†’ 𝑇 ∈ ℝ)
dvfsum.a ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ ℝ)
dvfsum.b1 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐡 ∈ 𝑉)
dvfsum.b2 ((πœ‘ ∧ π‘₯ ∈ 𝑍) β†’ 𝐡 ∈ ℝ)
dvfsum.b3 (πœ‘ β†’ (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = (π‘₯ ∈ 𝑆 ↦ 𝐡))
dvfsum.c (π‘₯ = π‘˜ β†’ 𝐡 = 𝐢)
dvfsum.u (πœ‘ β†’ π‘ˆ ∈ ℝ*)
dvfsum.l ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡)
dvfsum.h 𝐻 = (π‘₯ ∈ 𝑆 ↦ (((π‘₯ βˆ’ (βŒŠβ€˜π‘₯)) Β· 𝐡) + (Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘₯))𝐢 βˆ’ 𝐴)))
dvfsumlem1.1 (πœ‘ β†’ 𝑋 ∈ 𝑆)
dvfsumlem1.2 (πœ‘ β†’ π‘Œ ∈ 𝑆)
dvfsumlem1.3 (πœ‘ β†’ 𝐷 ≀ 𝑋)
dvfsumlem1.4 (πœ‘ β†’ 𝑋 ≀ π‘Œ)
dvfsumlem1.5 (πœ‘ β†’ π‘Œ ≀ π‘ˆ)
dvfsumlem1.6 (πœ‘ β†’ π‘Œ ≀ ((βŒŠβ€˜π‘‹) + 1))
Assertion
Ref Expression
dvfsumlem2 (πœ‘ β†’ ((π»β€˜π‘Œ) ≀ (π»β€˜π‘‹) ∧ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡)))
Distinct variable groups:   𝐡,π‘˜   π‘₯,𝐢   π‘₯,π‘˜,𝐷   πœ‘,π‘˜,π‘₯   𝑆,π‘˜,π‘₯   π‘˜,𝑀,π‘₯   π‘₯,𝑇   π‘˜,π‘Œ,π‘₯   π‘₯,𝑍   π‘ˆ,π‘˜,π‘₯   π‘˜,𝑋,π‘₯
Allowed substitution hints:   𝐴(π‘₯,π‘˜)   𝐡(π‘₯)   𝐢(π‘˜)   𝑇(π‘˜)   𝐻(π‘₯,π‘˜)   𝑉(π‘₯,π‘˜)   𝑍(π‘˜)

Proof of Theorem dvfsumlem2
Dummy variables 𝑦 𝑧 π‘š 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . . . . 9 𝑆 = (𝑇(,)+∞)
2 ioossre 13417 . . . . . . . . 9 (𝑇(,)+∞) βŠ† ℝ
31, 2eqsstri 4007 . . . . . . . 8 𝑆 βŠ† ℝ
4 dvfsumlem1.2 . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ 𝑆)
53, 4sselid 3970 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ ℝ)
6 dvfsumlem1.1 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ 𝑆)
76, 1eleqtrdi 2835 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ (𝑇(,)+∞))
8 dvfsum.t . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ ℝ)
98rexrd 11294 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ ℝ*)
10 elioopnf 13452 . . . . . . . . . . 11 (𝑇 ∈ ℝ* β†’ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
119, 10syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
127, 11mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
1312simpld 493 . . . . . . . 8 (πœ‘ β†’ 𝑋 ∈ ℝ)
14 reflcl 13793 . . . . . . . 8 (𝑋 ∈ ℝ β†’ (βŒŠβ€˜π‘‹) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 (πœ‘ β†’ (βŒŠβ€˜π‘‹) ∈ ℝ)
165, 15resubcld 11672 . . . . . 6 (πœ‘ β†’ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ)
17 csbeq1 3887 . . . . . . . 8 (𝑦 = π‘Œ β†’ ⦋𝑦 / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
1817eleq1d 2810 . . . . . . 7 (𝑦 = π‘Œ β†’ (⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
193a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 βŠ† ℝ)
20 dvfsum.a . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ ℝ)
21 dvfsum.b1 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐡 ∈ 𝑉)
22 dvfsum.b3 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = (π‘₯ ∈ 𝑆 ↦ 𝐡))
2319, 20, 21, 22dvmptrecl 25976 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐡 ∈ ℝ)
2423fmpttd 7120 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
25 nfcv 2892 . . . . . . . . . 10 Ⅎ𝑦𝐡
26 nfcsb1v 3909 . . . . . . . . . 10 β„²π‘₯⦋𝑦 / π‘₯⦌𝐡
27 csbeq1a 3898 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ 𝐡 = ⦋𝑦 / π‘₯⦌𝐡)
2825, 26, 27cbvmpt 5254 . . . . . . . . 9 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐡)
2928fmpt 7115 . . . . . . . 8 (βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
3024, 29sylibr 233 . . . . . . 7 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ)
3118, 30, 4rspcdva 3602 . . . . . 6 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
3216, 31remulcld 11274 . . . . 5 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
33 csbeq1 3887 . . . . . . 7 (𝑦 = π‘Œ β†’ ⦋𝑦 / π‘₯⦌𝐴 = β¦‹π‘Œ / π‘₯⦌𝐴)
3433eleq1d 2810 . . . . . 6 (𝑦 = π‘Œ β†’ (⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐴 ∈ ℝ))
3520fmpttd 7120 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„)
36 nfcv 2892 . . . . . . . . 9 Ⅎ𝑦𝐴
37 nfcsb1v 3909 . . . . . . . . 9 β„²π‘₯⦋𝑦 / π‘₯⦌𝐴
38 csbeq1a 3898 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ 𝐴 = ⦋𝑦 / π‘₯⦌𝐴)
3936, 37, 38cbvmpt 5254 . . . . . . . 8 (π‘₯ ∈ 𝑆 ↦ 𝐴) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴)
4039fmpt 7115 . . . . . . 7 (βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„)
4135, 40sylibr 233 . . . . . 6 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
4234, 41, 4rspcdva 3602 . . . . 5 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐴 ∈ ℝ)
4332, 42resubcld 11672 . . . 4 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ ℝ)
4413, 15resubcld 11672 . . . . . 6 (πœ‘ β†’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ)
45 csbeq1 3887 . . . . . . . 8 (𝑦 = 𝑋 β†’ ⦋𝑦 / π‘₯⦌𝐡 = ⦋𝑋 / π‘₯⦌𝐡)
4645eleq1d 2810 . . . . . . 7 (𝑦 = 𝑋 β†’ (⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ ↔ ⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ))
4746, 30, 6rspcdva 3602 . . . . . 6 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ)
4844, 47remulcld 11274 . . . . 5 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
49 csbeq1 3887 . . . . . . 7 (𝑦 = 𝑋 β†’ ⦋𝑦 / π‘₯⦌𝐴 = ⦋𝑋 / π‘₯⦌𝐴)
5049eleq1d 2810 . . . . . 6 (𝑦 = 𝑋 β†’ (⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ ⦋𝑋 / π‘₯⦌𝐴 ∈ ℝ))
5150, 41, 6rspcdva 3602 . . . . 5 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ∈ ℝ)
5248, 51resubcld 11672 . . . 4 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ ℝ)
53 fzfid 13970 . . . . 5 (πœ‘ β†’ (𝑀...(βŒŠβ€˜π‘‹)) ∈ Fin)
54 dvfsum.b2 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑍) β†’ 𝐡 ∈ ℝ)
5554ralrimiva 3136 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑍 𝐡 ∈ ℝ)
56 elfzuz 13529 . . . . . . 7 (π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹)) β†’ π‘˜ ∈ (β„€β‰₯β€˜π‘€))
57 dvfsum.z . . . . . . 7 𝑍 = (β„€β‰₯β€˜π‘€)
5856, 57eleqtrrdi 2836 . . . . . 6 (π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹)) β†’ π‘˜ ∈ 𝑍)
59 dvfsum.c . . . . . . . 8 (π‘₯ = π‘˜ β†’ 𝐡 = 𝐢)
6059eleq1d 2810 . . . . . . 7 (π‘₯ = π‘˜ β†’ (𝐡 ∈ ℝ ↔ 𝐢 ∈ ℝ))
6160rspccva 3600 . . . . . 6 ((βˆ€π‘₯ ∈ 𝑍 𝐡 ∈ ℝ ∧ π‘˜ ∈ 𝑍) β†’ 𝐢 ∈ ℝ)
6255, 58, 61syl2an 594 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))) β†’ 𝐢 ∈ ℝ)
6353, 62fsumrecl 15712 . . . 4 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢 ∈ ℝ)
6444, 31remulcld 11274 . . . . . 6 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
6564, 51resubcld 11672 . . . . 5 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ ℝ)
665, 13resubcld 11672 . . . . . . . . 9 (πœ‘ β†’ (π‘Œ βˆ’ 𝑋) ∈ ℝ)
6731, 66remulcld 11274 . . . . . . . 8 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ∈ ℝ)
6831recnd 11272 . . . . . . . . . 10 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
695recnd 11272 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ β„‚)
7013recnd 11272 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ β„‚)
7168, 69, 70subdid 11700 . . . . . . . . 9 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) = ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑋)))
72 eqid 2725 . . . . . . . . . . . . 13 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
7372mpomulcn 24803 . . . . . . . . . . . . 13 (𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣)) ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
74 csbeq1 3887 . . . . . . . . . . . . . . . 16 (𝑧 = π‘Œ β†’ ⦋𝑧 / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
7574eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑧 = π‘Œ β†’ (⦋𝑧 / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
76 nfcv 2892 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧𝐡
77 nfcsb1v 3909 . . . . . . . . . . . . . . . . . 18 β„²π‘₯⦋𝑧 / π‘₯⦌𝐡
78 csbeq1a 3898 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑧 β†’ 𝐡 = ⦋𝑧 / π‘₯⦌𝐡)
7976, 77, 78cbvmpt 5254 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (𝑧 ∈ 𝑆 ↦ ⦋𝑧 / π‘₯⦌𝐡)
8079fmpt 7115 . . . . . . . . . . . . . . . 16 (βˆ€π‘§ ∈ 𝑆 ⦋𝑧 / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
8124, 80sylibr 233 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘§ ∈ 𝑆 ⦋𝑧 / π‘₯⦌𝐡 ∈ ℝ)
8275, 81, 4rspcdva 3602 . . . . . . . . . . . . . 14 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
83 pnfxr 11298 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
8483a1i 11 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ +∞ ∈ ℝ*)
8512simprd 494 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑇 < 𝑋)
865ltpnfd 13133 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Œ < +∞)
87 iccssioo 13425 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋 ∧ π‘Œ < +∞)) β†’ (𝑋[,]π‘Œ) βŠ† (𝑇(,)+∞))
889, 84, 85, 86, 87syl22anc 837 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† (𝑇(,)+∞))
8988, 2sstrdi 3985 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† ℝ)
90 ax-resscn 11195 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
9189, 90sstrdi 3985 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† β„‚)
9290a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ ℝ βŠ† β„‚)
93 cncfmptc 24850 . . . . . . . . . . . . . 14 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ (𝑋[,]π‘Œ) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
9482, 91, 92, 93syl3anc 1368 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
95 cncfmptid 24851 . . . . . . . . . . . . . 14 (((𝑋[,]π‘Œ) βŠ† ℝ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ 𝑦) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
9689, 90, 95sylancl 584 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ 𝑦) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
97 remulcl 11223 . . . . . . . . . . . . . 14 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ)
98 simpl 481 . . . . . . . . . . . . . . . . . . 19 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
9998recnd 11272 . . . . . . . . . . . . . . . . . 18 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
100 simpr 483 . . . . . . . . . . . . . . . . . . 19 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
101100recnd 11272 . . . . . . . . . . . . . . . . . 18 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
10299, 101jca 510 . . . . . . . . . . . . . . . . 17 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
103 ovmpot 7579 . . . . . . . . . . . . . . . . . 18 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))
104103eqcomd 2731 . . . . . . . . . . . . . . . . 17 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
106105eleq1d 2810 . . . . . . . . . . . . . . 15 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ ↔ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
107106biimpd 228 . . . . . . . . . . . . . 14 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
10897, 107mpd 15 . . . . . . . . . . . . 13 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ)
10972, 73, 94, 96, 90, 108cncfmpt2ss 24854 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
110 df-mpt 5227 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))}
111110eleq1i 2816 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
112111biimpi 215 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
113109, 112syl 17 . . . . . . . . . . 11 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
114 idd 24 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
115114a1dd 50 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
116115impd 409 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
117 csbeq1 3887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘š = π‘Œ β†’ β¦‹π‘š / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
118117eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘š = π‘Œ β†’ (β¦‹π‘š / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
119 nfcv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘šπ΅
120 nfcsb1v 3909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘₯β¦‹π‘š / π‘₯⦌𝐡
121 csbeq1a 3898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = π‘š β†’ 𝐡 = β¦‹π‘š / π‘₯⦌𝐡)
122119, 120, 121cbvmpt 5254 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (π‘š ∈ 𝑆 ↦ β¦‹π‘š / π‘₯⦌𝐡)
123122fmpt 7115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘š ∈ 𝑆 β¦‹π‘š / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
12424, 123sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘š ∈ 𝑆 β¦‹π‘š / π‘₯⦌𝐡 ∈ ℝ)
125118, 124, 4rspcdva 3602 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
126125recnd 11272 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
127126adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
128 elicc2 13421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑋 ∈ ℝ ∧ π‘Œ ∈ ℝ) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ)))
12913, 5, 128syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ)))
130129biimpa 475 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑦 ∈ ℝ ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ))
131130simp1d 1139 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ ℝ)
132131recnd 11272 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ β„‚)
133127, 132jca 510 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
134133, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))
135134eqeq2d 2736 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ↔ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
136135biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
137136ex 411 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))))
138137impd 409 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
139116, 138jcad 511 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))))
140114a1dd 50 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
141140impd 409 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
142 csbeq1 3887 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ = π‘Œ β†’ β¦‹π‘˜ / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
143142eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ = π‘Œ β†’ (β¦‹π‘˜ / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
144 nfcv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘˜π΅
145 nfcsb1v 3909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘₯β¦‹π‘˜ / π‘₯⦌𝐡
146 csbeq1a 3898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = π‘˜ β†’ 𝐡 = β¦‹π‘˜ / π‘₯⦌𝐡)
147144, 145, 146cbvmpt 5254 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (π‘˜ ∈ 𝑆 ↦ β¦‹π‘˜ / π‘₯⦌𝐡)
148147fmpt 7115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘˜ ∈ 𝑆 β¦‹π‘˜ / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
14924, 148sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝑆 β¦‹π‘˜ / π‘₯⦌𝐡 ∈ ℝ)
150143, 149, 4rspcdva 3602 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
151150recnd 11272 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
152151adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
153152, 132jca 510 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
154153, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
155154eqeq2d 2736 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ↔ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
156155biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
157156ex 411 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
158157impd 409 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
159141, 158jcad 511 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
160139, 159impbid 211 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))))
161160opabbidv 5209 . . . . . . . . . . . . . 14 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))})
162 df-mpt 5227 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))}
163162eqcomi 2734 . . . . . . . . . . . . . . . 16 {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))
164163eqeq2i 2738 . . . . . . . . . . . . . . 15 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))} ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
165164biimpi 215 . . . . . . . . . . . . . 14 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))} β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
166161, 165syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
167166eleq1d 2810 . . . . . . . . . . . 12 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
168167biimpd 228 . . . . . . . . . . 11 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
169113, 168mpd 15 . . . . . . . . . 10 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
170 reelprrecn 11230 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, β„‚}
171170a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ ℝ ∈ {ℝ, β„‚})
172 ioossicc 13442 . . . . . . . . . . . . . . 15 (𝑋(,)π‘Œ) βŠ† (𝑋[,]π‘Œ)
173172, 89sstrid 3984 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋(,)π‘Œ) βŠ† ℝ)
174173sselda 3972 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ 𝑦 ∈ ℝ)
175174recnd 11272 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ 𝑦 ∈ β„‚)
176 1cnd 11239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ 1 ∈ β„‚)
177 simpr 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
178177recnd 11272 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
179 1cnd 11239 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 1 ∈ β„‚)
180171dvmptid 25907 . . . . . . . . . . . . 13 (πœ‘ β†’ (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
18172tgioo2 24737 . . . . . . . . . . . . 13 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
182 iooretop 24700 . . . . . . . . . . . . . 14 (𝑋(,)π‘Œ) ∈ (topGenβ€˜ran (,))
183182a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑋(,)π‘Œ) ∈ (topGenβ€˜ran (,)))
184171, 178, 179, 180, 173, 181, 72, 183dvmptres 25913 . . . . . . . . . . . 12 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ 1))
185171, 175, 176, 184, 68dvmptcmul 25914 . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 1)))
18668mulridd 11261 . . . . . . . . . . . 12 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 1) = β¦‹π‘Œ / π‘₯⦌𝐡)
187186mpteq2dv 5245 . . . . . . . . . . 11 (πœ‘ β†’ (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 1)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡))
188185, 187eqtrd 2765 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡))
18988, 1sseqtrrdi 4024 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† 𝑆)
190189resmptd 6039 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) β†Ύ (𝑋[,]π‘Œ)) = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐴))
19120recnd 11272 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ β„‚)
192191fmpttd 7120 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„‚)
19322dmeqd 5902 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = dom (π‘₯ ∈ 𝑆 ↦ 𝐡))
19421ralrimiva 3136 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑆 𝐡 ∈ 𝑉)
195 dmmptg 6241 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘₯ ∈ 𝑆 𝐡 ∈ 𝑉 β†’ dom (π‘₯ ∈ 𝑆 ↦ 𝐡) = 𝑆)
196194, 195syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom (π‘₯ ∈ 𝑆 ↦ 𝐡) = 𝑆)
197193, 196eqtrd 2765 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = 𝑆)
198 dvcn 25869 . . . . . . . . . . . . . . . 16 (((ℝ βŠ† β„‚ ∧ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„‚ ∧ 𝑆 βŠ† ℝ) ∧ dom (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = 𝑆) β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cnβ†’β„‚))
19992, 192, 19, 197, 198syl31anc 1370 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cnβ†’β„‚))
200 cncfcdm 24836 . . . . . . . . . . . . . . 15 ((ℝ βŠ† β„‚ ∧ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cnβ†’β„‚)) β†’ ((π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„))
20190, 199, 200sylancr 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„))
20235, 201mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ))
20339, 202eqeltrrid 2830 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ (𝑆–cn→ℝ))
204 rescncf 24835 . . . . . . . . . . . 12 ((𝑋[,]π‘Œ) βŠ† 𝑆 β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ (𝑆–cn→ℝ) β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) β†Ύ (𝑋[,]π‘Œ)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
205189, 203, 204sylc 65 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) β†Ύ (𝑋[,]π‘Œ)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
206190, 205eqeltrrd 2826 . . . . . . . . . 10 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
20741r19.21bi 3239 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ 𝑆) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
208207recnd 11272 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ 𝑆) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ β„‚)
20930r19.21bi 3239 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ 𝑆) β†’ ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ)
21039oveq2i 7427 . . . . . . . . . . . 12 (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴))
21122, 210, 283eqtr3g 2788 . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴)) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐡))
212172, 189sstrid 3984 . . . . . . . . . . 11 (πœ‘ β†’ (𝑋(,)π‘Œ) βŠ† 𝑆)
213171, 208, 209, 211, 212, 181, 72, 183dvmptres 25913 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐴)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐡))
214172sseli 3968 . . . . . . . . . . 11 (𝑦 ∈ (𝑋(,)π‘Œ) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))
215 simpl 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ πœ‘)
216189sselda 3972 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ 𝑆)
2174adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘Œ ∈ 𝑆)
218 dvfsum.d . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ ℝ)
219218adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝐷 ∈ ℝ)
22013adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑋 ∈ ℝ)
221 dvfsumlem1.3 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ≀ 𝑋)
222221adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝐷 ≀ 𝑋)
223130simp2d 1140 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑋 ≀ 𝑦)
224219, 220, 131, 222, 223letrd 11401 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝐷 ≀ 𝑦)
225130simp3d 1141 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ≀ π‘Œ)
226 dvfsumlem1.5 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ≀ π‘ˆ)
227226adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘Œ ≀ π‘ˆ)
228 simp2r 1197 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ π‘Œ ∈ 𝑆)
229 eleq1 2813 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘Œ β†’ (π‘˜ ∈ 𝑆 ↔ π‘Œ ∈ 𝑆))
230229anbi2d 628 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘Œ β†’ ((𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆)))
231 breq2 5147 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘Œ β†’ (𝑦 ≀ π‘˜ ↔ 𝑦 ≀ π‘Œ))
232 breq1 5146 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘Œ β†’ (π‘˜ ≀ π‘ˆ ↔ π‘Œ ≀ π‘ˆ))
233231, 2323anbi23d 1435 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘Œ β†’ ((𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)))
234230, 2333anbi23d 1435 . . . . . . . . . . . . . . 15 (π‘˜ = π‘Œ β†’ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ))))
235 vex 3467 . . . . . . . . . . . . . . . . . 18 π‘˜ ∈ V
236235, 59csbie 3920 . . . . . . . . . . . . . . . . 17 β¦‹π‘˜ / π‘₯⦌𝐡 = 𝐢
237236, 142eqtr3id 2779 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘Œ β†’ 𝐢 = β¦‹π‘Œ / π‘₯⦌𝐡)
238237breq1d 5153 . . . . . . . . . . . . . . 15 (π‘˜ = π‘Œ β†’ (𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡 ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡))
239234, 238imbi12d 343 . . . . . . . . . . . . . 14 (π‘˜ = π‘Œ β†’ (((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡) ↔ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)))
240 nfv 1909 . . . . . . . . . . . . . . . 16 β„²π‘₯(πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))
241 nfcv 2892 . . . . . . . . . . . . . . . . 17 β„²π‘₯𝐢
242 nfcv 2892 . . . . . . . . . . . . . . . . 17 β„²π‘₯ ≀
243241, 242, 26nfbr 5190 . . . . . . . . . . . . . . . 16 β„²π‘₯ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡
244240, 243nfim 1891 . . . . . . . . . . . . . . 15 β„²π‘₯((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡)
245 eleq1 2813 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (π‘₯ ∈ 𝑆 ↔ 𝑦 ∈ 𝑆))
246245anbi1d 629 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ ((π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆)))
247 breq2 5147 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (𝐷 ≀ π‘₯ ↔ 𝐷 ≀ 𝑦))
248 breq1 5146 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (π‘₯ ≀ π‘˜ ↔ 𝑦 ≀ π‘˜))
249247, 2483anbi12d 1433 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ ((𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)))
250246, 2493anbi23d 1435 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))))
25127breq2d 5155 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ (𝐢 ≀ 𝐡 ↔ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡))
252250, 251imbi12d 343 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ (((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡) ↔ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡)))
253 dvfsum.l . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡)
254244, 252, 253chvarfv 2228 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡)
255239, 254vtoclg 3532 . . . . . . . . . . . . 13 (π‘Œ ∈ 𝑆 β†’ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡))
256228, 255mpcom 38 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
257215, 216, 217, 224, 225, 227, 256syl123anc 1384 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
258214, 257sylan2 591 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
25913rexrd 11294 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ℝ*)
2605rexrd 11294 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ ℝ*)
261 dvfsumlem1.4 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ≀ π‘Œ)
262 lbicc2 13473 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ π‘Œ ∈ ℝ* ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ∈ (𝑋[,]π‘Œ))
263259, 260, 261, 262syl3anc 1368 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ (𝑋[,]π‘Œ))
264 ubicc2 13474 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ π‘Œ ∈ ℝ* ∧ 𝑋 ≀ π‘Œ) β†’ π‘Œ ∈ (𝑋[,]π‘Œ))
265259, 260, 261, 264syl3anc 1368 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ (𝑋[,]π‘Œ))
266 oveq2 7424 . . . . . . . . . 10 (𝑦 = 𝑋 β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑋))
267 oveq2 7424 . . . . . . . . . 10 (𝑦 = π‘Œ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· π‘Œ))
26813, 5, 169, 188, 206, 213, 258, 263, 265, 261, 266, 49, 267, 33dvle 25958 . . . . . . . . 9 (πœ‘ β†’ ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑋)) ≀ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
26971, 268eqbrtrd 5165 . . . . . . . 8 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ≀ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
27067, 42, 51, 269lesubd 11848 . . . . . . 7 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ≀ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
27164recnd 11272 . . . . . . . . 9 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ β„‚)
27232recnd 11272 . . . . . . . . 9 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ β„‚)
27342recnd 11272 . . . . . . . . 9 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐴 ∈ β„‚)
274271, 272, 273subsubd 11629 . . . . . . . 8 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴))
275272, 271negsubdi2d 11617 . . . . . . . . . . 11 (πœ‘ β†’ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)))
27615recnd 11272 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜π‘‹) ∈ β„‚)
27769, 70, 276nnncan2d 11636 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))) = (π‘Œ βˆ’ 𝑋))
278277oveq1d 7431 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = ((π‘Œ βˆ’ 𝑋) Β· β¦‹π‘Œ / π‘₯⦌𝐡))
27916recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ∈ β„‚)
28044recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ∈ β„‚)
281279, 280, 68subdird 11701 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)))
28266recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ βˆ’ 𝑋) ∈ β„‚)
283282, 68mulcomd 11265 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘Œ βˆ’ 𝑋) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
284278, 281, 2833eqtr3d 2773 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
285284negeqd 11484 . . . . . . . . . . 11 (πœ‘ β†’ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = -(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
286275, 285eqtr3d 2767 . . . . . . . . . 10 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = -(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
287286oveq1d 7431 . . . . . . . . 9 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴) = (-(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) + β¦‹π‘Œ / π‘₯⦌𝐴))
28867recnd 11272 . . . . . . . . . 10 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ∈ β„‚)
289288, 273negsubdid 11616 . . . . . . . . 9 (πœ‘ β†’ -((β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) = (-(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) + β¦‹π‘Œ / π‘₯⦌𝐴))
290287, 289eqtr4d 2768 . . . . . . . 8 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴) = -((β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
291288, 273negsubdi2d 11617 . . . . . . . 8 (πœ‘ β†’ -((β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
292274, 290, 2913eqtrd 2769 . . . . . . 7 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
293270, 292breqtrrd 5171 . . . . . 6 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)))
29451, 64, 43, 293lesubd 11848 . . . . 5 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
295 flle 13796 . . . . . . . . 9 (𝑋 ∈ ℝ β†’ (βŒŠβ€˜π‘‹) ≀ 𝑋)
29613, 295syl 17 . . . . . . . 8 (πœ‘ β†’ (βŒŠβ€˜π‘‹) ≀ 𝑋)
29713, 15subge0d 11834 . . . . . . . 8 (πœ‘ β†’ (0 ≀ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ↔ (βŒŠβ€˜π‘‹) ≀ 𝑋))
298296, 297mpbird 256 . . . . . . 7 (πœ‘ β†’ 0 ≀ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)))
29945breq2d 5155 . . . . . . . 8 (𝑦 = 𝑋 β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡 ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡))
300257ralrimiva 3136 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘¦ ∈ (𝑋[,]π‘Œ)β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
301299, 300, 263rspcdva 3602 . . . . . . 7 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
30231, 47, 44, 298, 301lemul2ad 12184 . . . . . 6 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡))
30364, 48, 51, 302lesub1dd 11860 . . . . 5 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
30443, 65, 52, 294, 303letrd 11401 . . . 4 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
30543, 52, 63, 304leadd1dd 11858 . . 3 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) ≀ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
306 dvfsum.m . . . 4 (πœ‘ β†’ 𝑀 ∈ β„€)
307 dvfsum.md . . . 4 (πœ‘ β†’ 𝑀 ≀ (𝐷 + 1))
308 dvfsum.u . . . 4 (πœ‘ β†’ π‘ˆ ∈ ℝ*)
309 dvfsum.h . . . 4 𝐻 = (π‘₯ ∈ 𝑆 ↦ (((π‘₯ βˆ’ (βŒŠβ€˜π‘₯)) Β· 𝐡) + (Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘₯))𝐢 βˆ’ 𝐴)))
310 dvfsumlem1.6 . . . 4 (πœ‘ β†’ π‘Œ ≀ ((βŒŠβ€˜π‘‹) + 1))
3111, 57, 306, 218, 307, 8, 20, 21, 54, 22, 59, 308, 253, 309, 6, 4, 221, 261, 226, 310dvfsumlem1 25978 . . 3 (πœ‘ β†’ (π»β€˜π‘Œ) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
31213leidd 11810 . . . 4 (πœ‘ β†’ 𝑋 ≀ 𝑋)
313259, 260, 308, 261, 226xrletrd 13173 . . . 4 (πœ‘ β†’ 𝑋 ≀ π‘ˆ)
314 fllep1 13798 . . . . 5 (𝑋 ∈ ℝ β†’ 𝑋 ≀ ((βŒŠβ€˜π‘‹) + 1))
31513, 314syl 17 . . . 4 (πœ‘ β†’ 𝑋 ≀ ((βŒŠβ€˜π‘‹) + 1))
3161, 57, 306, 218, 307, 8, 20, 21, 54, 22, 59, 308, 253, 309, 6, 6, 221, 312, 313, 315dvfsumlem1 25978 . . 3 (πœ‘ β†’ (π»β€˜π‘‹) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
317305, 311, 3163brtr4d 5175 . 2 (πœ‘ β†’ (π»β€˜π‘Œ) ≀ (π»β€˜π‘‹))
31852, 47resubcld 11672 . . . . 5 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
31943, 31resubcld 11672 . . . . 5 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
320 peano2rem 11557 . . . . . . . . . . 11 ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
32144, 320syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
322321, 47remulcld 11274 . . . . . . . . 9 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
323322, 51resubcld 11672 . . . . . . . 8 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ ℝ)
324 peano2rem 11557 . . . . . . . . . . 11 ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
32516, 324syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
326325, 47remulcld 11274 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
327326, 42resubcld 11672 . . . . . . . 8 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ ℝ)
328325, 31remulcld 11274 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
329328, 42resubcld 11672 . . . . . . . 8 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ ℝ)
330322recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ β„‚)
331326recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ β„‚)
332330, 331subcld 11601 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) ∈ β„‚)
333332, 273addcomd 11446 . . . . . . . . . . . 12 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴) = (β¦‹π‘Œ / π‘₯⦌𝐴 + ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))))
334330, 331, 273subsubd 11629 . . . . . . . . . . . 12 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴))
335273, 331, 330subsub2d 11630 . . . . . . . . . . . 12 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))) = (β¦‹π‘Œ / π‘₯⦌𝐴 + ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))))
336333, 334, 3353eqtr4d 2775 . . . . . . . . . . 11 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))))
337 1cnd 11239 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 1 ∈ β„‚)
338279, 280, 337nnncan2d 11636 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) = ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))))
339338, 277eqtrd 2765 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) = (π‘Œ βˆ’ 𝑋))
340339oveq1d 7431 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) Β· ⦋𝑋 / π‘₯⦌𝐡) = ((π‘Œ βˆ’ 𝑋) Β· ⦋𝑋 / π‘₯⦌𝐡))
341325recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ β„‚)
342321recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ β„‚)
34347recnd 11272 . . . . . . . . . . . . . 14 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚)
344341, 342, 343subdird 11701 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) Β· ⦋𝑋 / π‘₯⦌𝐡) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)))
345282, 343mulcomd 11265 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘Œ βˆ’ 𝑋) Β· ⦋𝑋 / π‘₯⦌𝐡) = (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
346340, 344, 3453eqtr3d 2773 . . . . . . . . . . . 12 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) = (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
347346oveq2d 7432 . . . . . . . . . . 11 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
348336, 347eqtrd 2765 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
34947, 66remulcld 11274 . . . . . . . . . . 11 (πœ‘ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ∈ ℝ)
350 cncfmptc 24850 . . . . . . . . . . . . . . . . 17 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ (𝑋[,]π‘Œ) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
35147, 91, 92, 350syl3anc 1368 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
352 remulcl 11223 . . . . . . . . . . . . . . . . 17 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ)
353 simpl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ)
354353recnd 11272 . . . . . . . . . . . . . . . . . . . . 21 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚)
355 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
356355recnd 11272 . . . . . . . . . . . . . . . . . . . . 21 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
357354, 356jca 510 . . . . . . . . . . . . . . . . . . . 20 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
358 ovmpot 7579 . . . . . . . . . . . . . . . . . . . . 21 ((⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))
359358eqcomd 2731 . . . . . . . . . . . . . . . . . . . 20 ((⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
360357, 359syl 17 . . . . . . . . . . . . . . . . . . 19 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
361360eleq1d 2810 . . . . . . . . . . . . . . . . . 18 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ ↔ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
362361biimpd 228 . . . . . . . . . . . . . . . . 17 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
363352, 362mpd 15 . . . . . . . . . . . . . . . 16 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ)
36472, 73, 351, 96, 90, 363cncfmpt2ss 24854 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
365 df-mpt 5227 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))}
366365eleq1i 2816 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
367366biimpi 215 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
368364, 367syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
369114a1dd 50 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
370369impd 409 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
371343adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚)
372371, 132jca 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
373372, 358syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))
374373eqeq2d 2736 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ↔ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
375374biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
376375ex 411 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))))
377376impd 409 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
378370, 377jcad 511 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))))
379114a1dd 50 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
380379impd 409 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
381372, 359syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
382381eqeq2d 2736 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ↔ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
383382biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
384383ex 411 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
385384impd 409 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
386380, 385jcad 511 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
387378, 386impbid 211 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))))
388387opabbidv 5209 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))})
389 df-mpt 5227 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))}
390389eqcomi 2734 . . . . . . . . . . . . . . . . . . 19 {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))
391390eqeq2i 2738 . . . . . . . . . . . . . . . . . 18 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))} ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
392391biimpi 215 . . . . . . . . . . . . . . . . 17 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))} β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
393388, 392syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
394393eleq1d 2810 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
395394biimpd 228 . . . . . . . . . . . . . 14 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
396368, 395mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
397171, 175, 176, 184, 343dvmptcmul 25914 . . . . . . . . . . . . . 14 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 1)))
398343mulridd 11261 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 1) = ⦋𝑋 / π‘₯⦌𝐡)
399398mpteq2dv 5245 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 1)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡))
400397, 399eqtrd 2765 . . . . . . . . . . . . 13 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡))
4016adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑋 ∈ 𝑆)
402131rexrd 11294 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ ℝ*)
403260adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘Œ ∈ ℝ*)
404308adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘ˆ ∈ ℝ*)
405402, 403, 404, 225, 227xrletrd 13173 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ≀ π‘ˆ)
406 vex 3467 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
407 eleq1 2813 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ (π‘˜ ∈ 𝑆 ↔ 𝑦 ∈ 𝑆))
408407anbi2d 628 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ ((𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)))
409 breq2 5147 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ (𝑋 ≀ π‘˜ ↔ 𝑋 ≀ 𝑦))
410 breq1 5146 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ (π‘˜ ≀ π‘ˆ ↔ 𝑦 ≀ π‘ˆ))
411409, 4103anbi23d 1435 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ ((𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ)))
412408, 4113anbi23d 1435 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑦 β†’ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ))))
413 csbeq1 3887 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ β¦‹π‘˜ / π‘₯⦌𝐡 = ⦋𝑦 / π‘₯⦌𝐡)
414236, 413eqtr3id 2779 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ 𝐢 = ⦋𝑦 / π‘₯⦌𝐡)
415414breq1d 5153 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑦 β†’ (𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡 ↔ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡))
416412, 415imbi12d 343 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ (((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡) ↔ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)))
417 simp2l 1196 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝑋 ∈ 𝑆)
418 nfv 1909 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯(πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))
419 nfcsb1v 3909 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯⦋𝑋 / π‘₯⦌𝐡
420241, 242, 419nfbr 5190 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡
421418, 420nfim 1891 . . . . . . . . . . . . . . . . . 18 β„²π‘₯((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡)
422 eleq1 2813 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑋 β†’ (π‘₯ ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
423422anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑋 β†’ ((π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆)))
424 breq2 5147 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑋 β†’ (𝐷 ≀ π‘₯ ↔ 𝐷 ≀ 𝑋))
425 breq1 5146 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑋 β†’ (π‘₯ ≀ π‘˜ ↔ 𝑋 ≀ π‘˜))
426424, 4253anbi12d 1433 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑋 β†’ ((𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)))
427423, 4263anbi23d 1435 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑋 β†’ ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))))
428 csbeq1a 3898 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑋 β†’ 𝐡 = ⦋𝑋 / π‘₯⦌𝐡)
429428breq2d 5155 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑋 β†’ (𝐢 ≀ 𝐡 ↔ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡))
430427, 429imbi12d 343 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑋 β†’ (((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡) ↔ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡)))
431421, 430, 253vtoclg1f 3548 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ 𝑆 β†’ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡))
432417, 431mpcom 38 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡)
433406, 416, 432vtocl 3535 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
434215, 401, 216, 222, 223, 405, 433syl123anc 1384 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
435214, 434sylan2 591 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
436 oveq2 7424 . . . . . . . . . . . . 13 (𝑦 = 𝑋 β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑋))
437 oveq2 7424 . . . . . . . . . . . . 13 (𝑦 = π‘Œ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· π‘Œ))
43813, 5, 206, 213, 396, 400, 435, 263, 265, 261, 49, 436, 33, 437dvle 25958 . . . . . . . . . . . 12 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((⦋𝑋 / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑋)))
439343, 69, 70subdid 11700 . . . . . . . . . . . 12 (πœ‘ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) = ((⦋𝑋 / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑋)))
440438, 439breqtrrd 5171 . . . . . . . . . . 11 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
44142, 51, 349, 440subled 11847 . . . . . . . . . 10 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))) ≀ ⦋𝑋 / π‘₯⦌𝐴)
442348, 441eqbrtrd 5165 . . . . . . . . 9 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) ≀ ⦋𝑋 / π‘₯⦌𝐴)
443322, 327, 51, 442subled 11847 . . . . . . . 8 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
444325renegcld 11671 . . . . . . . . . . . 12 (πœ‘ β†’ -((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
445 1red 11245 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 1 ∈ ℝ)
4465, 15, 445lesubadd2d 11843 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ≀ 1 ↔ π‘Œ ≀ ((βŒŠβ€˜π‘‹) + 1)))
447310, 446mpbird 256 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ≀ 1)
44816, 445suble0d 11835 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ≀ 0 ↔ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ≀ 1))
449447, 448mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ≀ 0)
450325le0neg1d 11815 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ≀ 0 ↔ 0 ≀ -((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)))
451449, 450mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ 0 ≀ -((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1))
45231, 47, 444, 451, 301lemul2ad 12184 . . . . . . . . . . 11 (πœ‘ β†’ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))
453341, 68mulneg1d 11697 . . . . . . . . . . 11 (πœ‘ β†’ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡))
454341, 343mulneg1d 11697 . . . . . . . . . . 11 (πœ‘ β†’ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) = -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))
455452, 453, 4543brtr3d 5174 . . . . . . . . . 10 (πœ‘ β†’ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))
456326, 328lenegd 11823 . . . . . . . . . 10 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ≀ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ↔ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)))
457455, 456mpbird 256 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ≀ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡))
458326, 328, 42, 457lesub1dd 11860 . . . . . . . 8 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
459323, 327, 329, 443, 458letrd 11401 . . . . . . 7 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
460280, 337, 343subdird 11701 . . . . . . . . 9 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (1 Β· ⦋𝑋 / π‘₯⦌𝐡)))
461343mullidd 11262 . . . . . . . . . 10 (πœ‘ β†’ (1 Β· ⦋𝑋 / π‘₯⦌𝐡) = ⦋𝑋 / π‘₯⦌𝐡)
462461oveq2d 7432 . . . . . . . . 9 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (1 Β· ⦋𝑋 / π‘₯⦌𝐡)) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡))
463460, 462eqtrd 2765 . . . . . . . 8 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡))
464463oveq1d 7431 . . . . . . 7 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
465279, 337, 68subdird 11701 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (1 Β· β¦‹π‘Œ / π‘₯⦌𝐡)))
46668mullidd 11262 . . . . . . . . . 10 (πœ‘ β†’ (1 Β· β¦‹π‘Œ / π‘₯⦌𝐡) = β¦‹π‘Œ / π‘₯⦌𝐡)
467466oveq2d 7432 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (1 Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
468465, 467eqtrd 2765 . . . . . . . 8 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
469468oveq1d 7431 . . . . . . 7 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
470459, 464, 4693brtr3d 5174 . . . . . 6 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
47148recnd 11272 . . . . . . 7 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ β„‚)
47251recnd 11272 . . . . . . 7 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ∈ β„‚)
473471, 472, 343sub32d 11633 . . . . . 6 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
474272, 273, 68sub32d 11633 . . . . . 6 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
475470, 473, 4743brtr4d 5175 . . . . 5 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
476318, 319, 63, 475leadd1dd 11858 . . . 4 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) ≀ (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
47752recnd 11272 . . . . 5 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ β„‚)
47863recnd 11272 . . . . 5 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢 ∈ β„‚)
479477, 478, 343addsubd 11622 . . . 4 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) = (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
48043recnd 11272 . . . . 5 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ β„‚)
481480, 478, 68addsubd 11622 . . . 4 (πœ‘ β†’ (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) = (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
482476, 479, 4813brtr4d 5175 . . 3 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
483316oveq1d 7431 . . 3 (πœ‘ β†’ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) = (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ ⦋𝑋 / π‘₯⦌𝐡))
484311oveq1d 7431 . . 3 (πœ‘ β†’ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) = (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
485482, 483, 4843brtr4d 5175 . 2 (πœ‘ β†’ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
486317, 485jca 510 1 (πœ‘ β†’ ((π»β€˜π‘Œ) ≀ (π»β€˜π‘‹) ∧ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  β¦‹csb 3884   βŠ† wss 3939  {cpr 4626   class class class wbr 5143  {copab 5205   ↦ cmpt 5226  dom cdm 5672  ran crn 5673   β†Ύ cres 5674  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7416   ∈ cmpo 7418  β„‚cc 11136  β„cr 11137  0cc0 11138  1c1 11139   + caddc 11141   Β· cmul 11143  +∞cpnf 11275  β„*cxr 11277   < clt 11278   ≀ cle 11279   βˆ’ cmin 11474  -cneg 11475  β„€cz 12588  β„€β‰₯cuz 12852  (,)cioo 13356  [,]cicc 13359  ...cfz 13516  βŒŠcfl 13787  Ξ£csu 15664  TopOpenctopn 17402  topGenctg 17418  β„‚fldccnfld 21283  β€“cnβ†’ccncf 24814   D cdv 25810
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 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-inf2 9664  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216  ax-addf 11217
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 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7991  df-2nd 7992  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-er 8723  df-map 8845  df-pm 8846  df-ixp 8915  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-fsupp 9386  df-fi 9434  df-sup 9465  df-inf 9466  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312  df-n0 12503  df-z 12589  df-dec 12708  df-uz 12853  df-q 12963  df-rp 13007  df-xneg 13124  df-xadd 13125  df-xmul 13126  df-ioo 13360  df-ico 13362  df-icc 13363  df-fz 13517  df-fzo 13660  df-fl 13789  df-seq 13999  df-exp 14059  df-hash 14322  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-clim 15464  df-sum 15665  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-mulr 17246  df-starv 17247  df-sca 17248  df-vsca 17249  df-ip 17250  df-tset 17251  df-ple 17252  df-ds 17254  df-unif 17255  df-hom 17256  df-cco 17257  df-rest 17403  df-topn 17404  df-0g 17422  df-gsum 17423  df-topgen 17424  df-pt 17425  df-prds 17428  df-xrs 17483  df-qtop 17488  df-imas 17489  df-xps 17491  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18740  df-mulg 19028  df-cntz 19272  df-cmn 19741  df-psmet 21275  df-xmet 21276  df-met 21277  df-bl 21278  df-mopn 21279  df-fbas 21280  df-fg 21281  df-cnfld 21284  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22867  df-cld 22941  df-ntr 22942  df-cls 22943  df-nei 23020  df-lp 23058  df-perf 23059  df-cn 23149  df-cnp 23150  df-haus 23237  df-cmp 23309  df-tx 23484  df-hmeo 23677  df-fil 23768  df-fm 23860  df-flim 23861  df-flf 23862  df-xms 24244  df-ms 24245  df-tms 24246  df-cncf 24816  df-limc 25813  df-dv 25814
This theorem is referenced by:  dvfsumlem3  25981
  Copyright terms: Public domain W3C validator