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

Theorem dvfsumlem2 25916
Description: Lemma for dvfsumrlim 25921. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11192. (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 13391 . . . . . . . . 9 (𝑇(,)+∞) βŠ† ℝ
31, 2eqsstri 4011 . . . . . . . 8 𝑆 βŠ† ℝ
4 dvfsumlem1.2 . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ 𝑆)
53, 4sselid 3975 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ ℝ)
6 dvfsumlem1.1 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ 𝑆)
76, 1eleqtrdi 2837 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ (𝑇(,)+∞))
8 dvfsum.t . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ ℝ)
98rexrd 11268 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ ℝ*)
10 elioopnf 13426 . . . . . . . . . . 11 (𝑇 ∈ ℝ* β†’ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
119, 10syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
127, 11mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
1312simpld 494 . . . . . . . 8 (πœ‘ β†’ 𝑋 ∈ ℝ)
14 reflcl 13767 . . . . . . . 8 (𝑋 ∈ ℝ β†’ (βŒŠβ€˜π‘‹) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 (πœ‘ β†’ (βŒŠβ€˜π‘‹) ∈ ℝ)
165, 15resubcld 11646 . . . . . 6 (πœ‘ β†’ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ)
17 csbeq1 3891 . . . . . . . 8 (𝑦 = π‘Œ β†’ ⦋𝑦 / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
1817eleq1d 2812 . . . . . . 7 (𝑦 = π‘Œ β†’ (⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
193a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 βŠ† ℝ)
20 dvfsum.a . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ ℝ)
21 dvfsum.b1 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐡 ∈ 𝑉)
22 dvfsum.b3 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = (π‘₯ ∈ 𝑆 ↦ 𝐡))
2319, 20, 21, 22dvmptrecl 25913 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐡 ∈ ℝ)
2423fmpttd 7110 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
25 nfcv 2897 . . . . . . . . . 10 Ⅎ𝑦𝐡
26 nfcsb1v 3913 . . . . . . . . . 10 β„²π‘₯⦋𝑦 / π‘₯⦌𝐡
27 csbeq1a 3902 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ 𝐡 = ⦋𝑦 / π‘₯⦌𝐡)
2825, 26, 27cbvmpt 5252 . . . . . . . . 9 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐡)
2928fmpt 7105 . . . . . . . 8 (βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
3024, 29sylibr 233 . . . . . . 7 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ)
3118, 30, 4rspcdva 3607 . . . . . 6 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
3216, 31remulcld 11248 . . . . 5 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
33 csbeq1 3891 . . . . . . 7 (𝑦 = π‘Œ β†’ ⦋𝑦 / π‘₯⦌𝐴 = β¦‹π‘Œ / π‘₯⦌𝐴)
3433eleq1d 2812 . . . . . 6 (𝑦 = π‘Œ β†’ (⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐴 ∈ ℝ))
3520fmpttd 7110 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„)
36 nfcv 2897 . . . . . . . . 9 Ⅎ𝑦𝐴
37 nfcsb1v 3913 . . . . . . . . 9 β„²π‘₯⦋𝑦 / π‘₯⦌𝐴
38 csbeq1a 3902 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ 𝐴 = ⦋𝑦 / π‘₯⦌𝐴)
3936, 37, 38cbvmpt 5252 . . . . . . . 8 (π‘₯ ∈ 𝑆 ↦ 𝐴) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴)
4039fmpt 7105 . . . . . . 7 (βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„)
4135, 40sylibr 233 . . . . . 6 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝑆 ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
4234, 41, 4rspcdva 3607 . . . . 5 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐴 ∈ ℝ)
4332, 42resubcld 11646 . . . 4 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ ℝ)
4413, 15resubcld 11646 . . . . . 6 (πœ‘ β†’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ)
45 csbeq1 3891 . . . . . . . 8 (𝑦 = 𝑋 β†’ ⦋𝑦 / π‘₯⦌𝐡 = ⦋𝑋 / π‘₯⦌𝐡)
4645eleq1d 2812 . . . . . . 7 (𝑦 = 𝑋 β†’ (⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ ↔ ⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ))
4746, 30, 6rspcdva 3607 . . . . . 6 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ)
4844, 47remulcld 11248 . . . . 5 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
49 csbeq1 3891 . . . . . . 7 (𝑦 = 𝑋 β†’ ⦋𝑦 / π‘₯⦌𝐴 = ⦋𝑋 / π‘₯⦌𝐴)
5049eleq1d 2812 . . . . . 6 (𝑦 = 𝑋 β†’ (⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ ↔ ⦋𝑋 / π‘₯⦌𝐴 ∈ ℝ))
5150, 41, 6rspcdva 3607 . . . . 5 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ∈ ℝ)
5248, 51resubcld 11646 . . . 4 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ ℝ)
53 fzfid 13944 . . . . 5 (πœ‘ β†’ (𝑀...(βŒŠβ€˜π‘‹)) ∈ Fin)
54 dvfsum.b2 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑍) β†’ 𝐡 ∈ ℝ)
5554ralrimiva 3140 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑍 𝐡 ∈ ℝ)
56 elfzuz 13503 . . . . . . 7 (π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹)) β†’ π‘˜ ∈ (β„€β‰₯β€˜π‘€))
57 dvfsum.z . . . . . . 7 𝑍 = (β„€β‰₯β€˜π‘€)
5856, 57eleqtrrdi 2838 . . . . . 6 (π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹)) β†’ π‘˜ ∈ 𝑍)
59 dvfsum.c . . . . . . . 8 (π‘₯ = π‘˜ β†’ 𝐡 = 𝐢)
6059eleq1d 2812 . . . . . . 7 (π‘₯ = π‘˜ β†’ (𝐡 ∈ ℝ ↔ 𝐢 ∈ ℝ))
6160rspccva 3605 . . . . . 6 ((βˆ€π‘₯ ∈ 𝑍 𝐡 ∈ ℝ ∧ π‘˜ ∈ 𝑍) β†’ 𝐢 ∈ ℝ)
6255, 58, 61syl2an 595 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))) β†’ 𝐢 ∈ ℝ)
6353, 62fsumrecl 15686 . . . 4 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢 ∈ ℝ)
6444, 31remulcld 11248 . . . . . 6 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
6564, 51resubcld 11646 . . . . 5 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ ℝ)
665, 13resubcld 11646 . . . . . . . . 9 (πœ‘ β†’ (π‘Œ βˆ’ 𝑋) ∈ ℝ)
6731, 66remulcld 11248 . . . . . . . 8 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ∈ ℝ)
6831recnd 11246 . . . . . . . . . 10 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
695recnd 11246 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ β„‚)
7013recnd 11246 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ β„‚)
7168, 69, 70subdid 11674 . . . . . . . . 9 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) = ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑋)))
72 eqid 2726 . . . . . . . . . . . . 13 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
7372mpomulcn 24740 . . . . . . . . . . . . 13 (𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣)) ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
74 csbeq1 3891 . . . . . . . . . . . . . . . 16 (𝑧 = π‘Œ β†’ ⦋𝑧 / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
7574eleq1d 2812 . . . . . . . . . . . . . . 15 (𝑧 = π‘Œ β†’ (⦋𝑧 / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
76 nfcv 2897 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧𝐡
77 nfcsb1v 3913 . . . . . . . . . . . . . . . . . 18 β„²π‘₯⦋𝑧 / π‘₯⦌𝐡
78 csbeq1a 3902 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑧 β†’ 𝐡 = ⦋𝑧 / π‘₯⦌𝐡)
7976, 77, 78cbvmpt 5252 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (𝑧 ∈ 𝑆 ↦ ⦋𝑧 / π‘₯⦌𝐡)
8079fmpt 7105 . . . . . . . . . . . . . . . 16 (βˆ€π‘§ ∈ 𝑆 ⦋𝑧 / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
8124, 80sylibr 233 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘§ ∈ 𝑆 ⦋𝑧 / π‘₯⦌𝐡 ∈ ℝ)
8275, 81, 4rspcdva 3607 . . . . . . . . . . . . . 14 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
83 pnfxr 11272 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
8483a1i 11 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ +∞ ∈ ℝ*)
8512simprd 495 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑇 < 𝑋)
865ltpnfd 13107 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Œ < +∞)
87 iccssioo 13399 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋 ∧ π‘Œ < +∞)) β†’ (𝑋[,]π‘Œ) βŠ† (𝑇(,)+∞))
889, 84, 85, 86, 87syl22anc 836 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† (𝑇(,)+∞))
8988, 2sstrdi 3989 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† ℝ)
90 ax-resscn 11169 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
9189, 90sstrdi 3989 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† β„‚)
9290a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ ℝ βŠ† β„‚)
93 cncfmptc 24787 . . . . . . . . . . . . . 14 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ (𝑋[,]π‘Œ) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
9482, 91, 92, 93syl3anc 1368 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
95 cncfmptid 24788 . . . . . . . . . . . . . 14 (((𝑋[,]π‘Œ) βŠ† ℝ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ 𝑦) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
9689, 90, 95sylancl 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ 𝑦) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
97 remulcl 11197 . . . . . . . . . . . . . 14 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ)
98 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
9998recnd 11246 . . . . . . . . . . . . . . . . . 18 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
100 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
101100recnd 11246 . . . . . . . . . . . . . . . . . 18 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
10299, 101jca 511 . . . . . . . . . . . . . . . . 17 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
103 ovmpot 7565 . . . . . . . . . . . . . . . . . 18 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))
104103eqcomd 2732 . . . . . . . . . . . . . . . . 17 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
106105eleq1d 2812 . . . . . . . . . . . . . . 15 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ ↔ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
107106biimpd 228 . . . . . . . . . . . . . 14 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
10897, 107mpd 15 . . . . . . . . . . . . 13 ((β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ)
10972, 73, 94, 96, 90, 108cncfmpt2ss 24791 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
110 df-mpt 5225 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))}
111110eleq1i 2818 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
112111biimpi 215 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
113109, 112syl 17 . . . . . . . . . . 11 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
114 idd 24 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
115114a1dd 50 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
116115impd 410 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
117 csbeq1 3891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘š = π‘Œ β†’ β¦‹π‘š / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
118117eleq1d 2812 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘š = π‘Œ β†’ (β¦‹π‘š / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
119 nfcv 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘šπ΅
120 nfcsb1v 3913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘₯β¦‹π‘š / π‘₯⦌𝐡
121 csbeq1a 3902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = π‘š β†’ 𝐡 = β¦‹π‘š / π‘₯⦌𝐡)
122119, 120, 121cbvmpt 5252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (π‘š ∈ 𝑆 ↦ β¦‹π‘š / π‘₯⦌𝐡)
123122fmpt 7105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘š ∈ 𝑆 β¦‹π‘š / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
12424, 123sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘š ∈ 𝑆 β¦‹π‘š / π‘₯⦌𝐡 ∈ ℝ)
125118, 124, 4rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
126125recnd 11246 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
127126adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
128 elicc2 13395 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑋 ∈ ℝ ∧ π‘Œ ∈ ℝ) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ)))
12913, 5, 128syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ)))
130129biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑦 ∈ ℝ ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ))
131130simp1d 1139 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ ℝ)
132131recnd 11246 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ β„‚)
133127, 132jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
134133, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))
135134eqeq2d 2737 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ↔ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
136135biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
137136ex 412 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))))
138137impd 410 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
139116, 138jcad 512 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))))
140114a1dd 50 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
141140impd 410 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
142 csbeq1 3891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ = π‘Œ β†’ β¦‹π‘˜ / π‘₯⦌𝐡 = β¦‹π‘Œ / π‘₯⦌𝐡)
143142eleq1d 2812 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ = π‘Œ β†’ (β¦‹π‘˜ / π‘₯⦌𝐡 ∈ ℝ ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ))
144 nfcv 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘˜π΅
145 nfcsb1v 3913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘₯β¦‹π‘˜ / π‘₯⦌𝐡
146 csbeq1a 3902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = π‘˜ β†’ 𝐡 = β¦‹π‘˜ / π‘₯⦌𝐡)
147144, 145, 146cbvmpt 5252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ 𝑆 ↦ 𝐡) = (π‘˜ ∈ 𝑆 ↦ β¦‹π‘˜ / π‘₯⦌𝐡)
148147fmpt 7105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘˜ ∈ 𝑆 β¦‹π‘˜ / π‘₯⦌𝐡 ∈ ℝ ↔ (π‘₯ ∈ 𝑆 ↦ 𝐡):π‘†βŸΆβ„)
14924, 148sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝑆 β¦‹π‘˜ / π‘₯⦌𝐡 ∈ ℝ)
150143, 149, 4rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ ℝ)
151150recnd 11246 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
152151adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚)
153152, 132jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
154153, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
155154eqeq2d 2737 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) ↔ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
156155biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
157156ex 412 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
158157impd 410 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
159141, 158jcad 512 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
160139, 159impbid 211 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))))
161160opabbidv 5207 . . . . . . . . . . . . . 14 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))})
162 df-mpt 5225 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))}
163162eqcomi 2735 . . . . . . . . . . . . . . . 16 {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))
164163eqeq2i 2739 . . . . . . . . . . . . . . 15 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))} ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
165164biimpi 215 . . . . . . . . . . . . . 14 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))} β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
166161, 165syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)))
167166eleq1d 2812 . . . . . . . . . . . 12 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
168167biimpd 228 . . . . . . . . . . 11 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (β¦‹π‘Œ / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
169113, 168mpd 15 . . . . . . . . . 10 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
170 reelprrecn 11204 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, β„‚}
171170a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ ℝ ∈ {ℝ, β„‚})
172 ioossicc 13416 . . . . . . . . . . . . . . 15 (𝑋(,)π‘Œ) βŠ† (𝑋[,]π‘Œ)
173172, 89sstrid 3988 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋(,)π‘Œ) βŠ† ℝ)
174173sselda 3977 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ 𝑦 ∈ ℝ)
175174recnd 11246 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ 𝑦 ∈ β„‚)
176 1cnd 11213 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ 1 ∈ β„‚)
177 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
178177recnd 11246 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
179 1cnd 11213 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 1 ∈ β„‚)
180171dvmptid 25844 . . . . . . . . . . . . 13 (πœ‘ β†’ (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
18172tgioo2 24674 . . . . . . . . . . . . 13 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
182 iooretop 24637 . . . . . . . . . . . . . 14 (𝑋(,)π‘Œ) ∈ (topGenβ€˜ran (,))
183182a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑋(,)π‘Œ) ∈ (topGenβ€˜ran (,)))
184171, 178, 179, 180, 173, 181, 72, 183dvmptres 25850 . . . . . . . . . . . 12 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ 1))
185171, 175, 176, 184, 68dvmptcmul 25851 . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 1)))
18668mulridd 11235 . . . . . . . . . . . 12 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 1) = β¦‹π‘Œ / π‘₯⦌𝐡)
187186mpteq2dv 5243 . . . . . . . . . . 11 (πœ‘ β†’ (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 1)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡))
188185, 187eqtrd 2766 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ β¦‹π‘Œ / π‘₯⦌𝐡))
18988, 1sseqtrrdi 4028 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋[,]π‘Œ) βŠ† 𝑆)
190189resmptd 6034 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) β†Ύ (𝑋[,]π‘Œ)) = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐴))
19120recnd 11246 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ β„‚)
192191fmpttd 7110 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„‚)
19322dmeqd 5899 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = dom (π‘₯ ∈ 𝑆 ↦ 𝐡))
19421ralrimiva 3140 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑆 𝐡 ∈ 𝑉)
195 dmmptg 6235 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘₯ ∈ 𝑆 𝐡 ∈ 𝑉 β†’ dom (π‘₯ ∈ 𝑆 ↦ 𝐡) = 𝑆)
196194, 195syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom (π‘₯ ∈ 𝑆 ↦ 𝐡) = 𝑆)
197193, 196eqtrd 2766 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ dom (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = 𝑆)
198 dvcn 25806 . . . . . . . . . . . . . . . 16 (((ℝ βŠ† β„‚ ∧ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„‚ ∧ 𝑆 βŠ† ℝ) ∧ dom (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = 𝑆) β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cnβ†’β„‚))
19992, 192, 19, 197, 198syl31anc 1370 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cnβ†’β„‚))
200 cncfcdm 24773 . . . . . . . . . . . . . . 15 ((ℝ βŠ† β„‚ ∧ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cnβ†’β„‚)) β†’ ((π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„))
20190, 199, 200sylancr 586 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (π‘₯ ∈ 𝑆 ↦ 𝐴):π‘†βŸΆβ„))
20235, 201mpbird 257 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ))
20339, 202eqeltrrid 2832 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ (𝑆–cn→ℝ))
204 rescncf 24772 . . . . . . . . . . . 12 ((𝑋[,]π‘Œ) βŠ† 𝑆 β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ (𝑆–cn→ℝ) β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) β†Ύ (𝑋[,]π‘Œ)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
205189, 203, 204sylc 65 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴) β†Ύ (𝑋[,]π‘Œ)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
206190, 205eqeltrrd 2828 . . . . . . . . . 10 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐴) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
20741r19.21bi 3242 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ 𝑆) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ ℝ)
208207recnd 11246 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ 𝑆) β†’ ⦋𝑦 / π‘₯⦌𝐴 ∈ β„‚)
20930r19.21bi 3242 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ 𝑆) β†’ ⦋𝑦 / π‘₯⦌𝐡 ∈ ℝ)
21039oveq2i 7416 . . . . . . . . . . . 12 (ℝ D (π‘₯ ∈ 𝑆 ↦ 𝐴)) = (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴))
21122, 210, 283eqtr3g 2789 . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐴)) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / π‘₯⦌𝐡))
212172, 189sstrid 3988 . . . . . . . . . . 11 (πœ‘ β†’ (𝑋(,)π‘Œ) βŠ† 𝑆)
213171, 208, 209, 211, 212, 181, 72, 183dvmptres 25850 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐴)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑦 / π‘₯⦌𝐡))
214172sseli 3973 . . . . . . . . . . 11 (𝑦 ∈ (𝑋(,)π‘Œ) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))
215 simpl 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ πœ‘)
216189sselda 3977 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ 𝑆)
2174adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘Œ ∈ 𝑆)
218 dvfsum.d . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ ℝ)
219218adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝐷 ∈ ℝ)
22013adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑋 ∈ ℝ)
221 dvfsumlem1.3 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ≀ 𝑋)
222221adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝐷 ≀ 𝑋)
223130simp2d 1140 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑋 ≀ 𝑦)
224219, 220, 131, 222, 223letrd 11375 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝐷 ≀ 𝑦)
225130simp3d 1141 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ≀ π‘Œ)
226 dvfsumlem1.5 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ≀ π‘ˆ)
227226adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘Œ ≀ π‘ˆ)
228 simp2r 1197 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ π‘Œ ∈ 𝑆)
229 eleq1 2815 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘Œ β†’ (π‘˜ ∈ 𝑆 ↔ π‘Œ ∈ 𝑆))
230229anbi2d 628 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘Œ β†’ ((𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆)))
231 breq2 5145 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘Œ β†’ (𝑦 ≀ π‘˜ ↔ 𝑦 ≀ π‘Œ))
232 breq1 5144 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘Œ β†’ (π‘˜ ≀ π‘ˆ ↔ π‘Œ ≀ π‘ˆ))
233231, 2323anbi23d 1435 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘Œ β†’ ((𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)))
234230, 2333anbi23d 1435 . . . . . . . . . . . . . . 15 (π‘˜ = π‘Œ β†’ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ))))
235 vex 3472 . . . . . . . . . . . . . . . . . 18 π‘˜ ∈ V
236235, 59csbie 3924 . . . . . . . . . . . . . . . . 17 β¦‹π‘˜ / π‘₯⦌𝐡 = 𝐢
237236, 142eqtr3id 2780 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘Œ β†’ 𝐢 = β¦‹π‘Œ / π‘₯⦌𝐡)
238237breq1d 5151 . . . . . . . . . . . . . . 15 (π‘˜ = π‘Œ β†’ (𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡 ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡))
239234, 238imbi12d 344 . . . . . . . . . . . . . 14 (π‘˜ = π‘Œ β†’ (((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡) ↔ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)))
240 nfv 1909 . . . . . . . . . . . . . . . 16 β„²π‘₯(πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))
241 nfcv 2897 . . . . . . . . . . . . . . . . 17 β„²π‘₯𝐢
242 nfcv 2897 . . . . . . . . . . . . . . . . 17 β„²π‘₯ ≀
243241, 242, 26nfbr 5188 . . . . . . . . . . . . . . . 16 β„²π‘₯ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡
244240, 243nfim 1891 . . . . . . . . . . . . . . 15 β„²π‘₯((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡)
245 eleq1 2815 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (π‘₯ ∈ 𝑆 ↔ 𝑦 ∈ 𝑆))
246245anbi1d 629 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ ((π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆)))
247 breq2 5145 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (𝐷 ≀ π‘₯ ↔ 𝐷 ≀ 𝑦))
248 breq1 5144 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (π‘₯ ≀ π‘˜ ↔ 𝑦 ≀ π‘˜))
249247, 2483anbi12d 1433 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ ((𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)))
250246, 2493anbi23d 1435 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))))
25127breq2d 5153 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ (𝐢 ≀ 𝐡 ↔ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡))
252250, 251imbi12d 344 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ (((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡) ↔ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡)))
253 dvfsum.l . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡)
254244, 252, 253chvarfv 2225 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑦 / π‘₯⦌𝐡)
255239, 254vtoclg 3537 . . . . . . . . . . . . 13 (π‘Œ ∈ 𝑆 β†’ ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡))
256228, 255mpcom 38 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝐷 ≀ 𝑦 ∧ 𝑦 ≀ π‘Œ ∧ π‘Œ ≀ π‘ˆ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
257215, 216, 217, 224, 225, 227, 256syl123anc 1384 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
258214, 257sylan2 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
25913rexrd 11268 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ℝ*)
2605rexrd 11268 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ ℝ*)
261 dvfsumlem1.4 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ≀ π‘Œ)
262 lbicc2 13447 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ π‘Œ ∈ ℝ* ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ∈ (𝑋[,]π‘Œ))
263259, 260, 261, 262syl3anc 1368 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ (𝑋[,]π‘Œ))
264 ubicc2 13448 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ π‘Œ ∈ ℝ* ∧ 𝑋 ≀ π‘Œ) β†’ π‘Œ ∈ (𝑋[,]π‘Œ))
265259, 260, 261, 264syl3anc 1368 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ (𝑋[,]π‘Œ))
266 oveq2 7413 . . . . . . . . . 10 (𝑦 = 𝑋 β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑋))
267 oveq2 7413 . . . . . . . . . 10 (𝑦 = π‘Œ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑦) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· π‘Œ))
26813, 5, 169, 188, 206, 213, 258, 263, 265, 261, 266, 49, 267, 33dvle 25895 . . . . . . . . 9 (πœ‘ β†’ ((β¦‹π‘Œ / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· 𝑋)) ≀ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
26971, 268eqbrtrd 5163 . . . . . . . 8 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ≀ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
27067, 42, 51, 269lesubd 11822 . . . . . . 7 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ≀ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
27164recnd 11246 . . . . . . . . 9 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ β„‚)
27232recnd 11246 . . . . . . . . 9 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ β„‚)
27342recnd 11246 . . . . . . . . 9 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐴 ∈ β„‚)
274271, 272, 273subsubd 11603 . . . . . . . 8 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴))
275272, 271negsubdi2d 11591 . . . . . . . . . . 11 (πœ‘ β†’ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)))
27615recnd 11246 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜π‘‹) ∈ β„‚)
27769, 70, 276nnncan2d 11610 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))) = (π‘Œ βˆ’ 𝑋))
278277oveq1d 7420 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = ((π‘Œ βˆ’ 𝑋) Β· β¦‹π‘Œ / π‘₯⦌𝐡))
27916recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ∈ β„‚)
28044recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ∈ β„‚)
281279, 280, 68subdird 11675 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)))
28266recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ βˆ’ 𝑋) ∈ β„‚)
283282, 68mulcomd 11239 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘Œ βˆ’ 𝑋) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
284278, 281, 2833eqtr3d 2774 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
285284negeqd 11458 . . . . . . . . . . 11 (πœ‘ β†’ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = -(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
286275, 285eqtr3d 2768 . . . . . . . . . 10 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = -(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
287286oveq1d 7420 . . . . . . . . 9 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴) = (-(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) + β¦‹π‘Œ / π‘₯⦌𝐴))
28867recnd 11246 . . . . . . . . . 10 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ∈ β„‚)
289288, 273negsubdid 11590 . . . . . . . . 9 (πœ‘ β†’ -((β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) = (-(β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) + β¦‹π‘Œ / π‘₯⦌𝐴))
290287, 289eqtr4d 2769 . . . . . . . 8 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴) = -((β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
291288, 273negsubdi2d 11591 . . . . . . . 8 (πœ‘ β†’ -((β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
292274, 290, 2913eqtrd 2770 . . . . . . 7 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (β¦‹π‘Œ / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
293270, 292breqtrrd 5169 . . . . . 6 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)))
29451, 64, 43, 293lesubd 11822 . . . . 5 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
295 flle 13770 . . . . . . . . 9 (𝑋 ∈ ℝ β†’ (βŒŠβ€˜π‘‹) ≀ 𝑋)
29613, 295syl 17 . . . . . . . 8 (πœ‘ β†’ (βŒŠβ€˜π‘‹) ≀ 𝑋)
29713, 15subge0d 11808 . . . . . . . 8 (πœ‘ β†’ (0 ≀ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ↔ (βŒŠβ€˜π‘‹) ≀ 𝑋))
298296, 297mpbird 257 . . . . . . 7 (πœ‘ β†’ 0 ≀ (𝑋 βˆ’ (βŒŠβ€˜π‘‹)))
29945breq2d 5153 . . . . . . . 8 (𝑦 = 𝑋 β†’ (β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡 ↔ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡))
300257ralrimiva 3140 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘¦ ∈ (𝑋[,]π‘Œ)β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑦 / π‘₯⦌𝐡)
301299, 300, 263rspcdva 3607 . . . . . . 7 (πœ‘ β†’ β¦‹π‘Œ / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
30231, 47, 44, 298, 301lemul2ad 12158 . . . . . 6 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡))
30364, 48, 51, 302lesub1dd 11834 . . . . 5 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
30443, 65, 52, 294, 303letrd 11375 . . . 4 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ≀ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
30543, 52, 63, 304leadd1dd 11832 . . 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 25915 . . 3 (πœ‘ β†’ (π»β€˜π‘Œ) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
31213leidd 11784 . . . 4 (πœ‘ β†’ 𝑋 ≀ 𝑋)
313259, 260, 308, 261, 226xrletrd 13147 . . . 4 (πœ‘ β†’ 𝑋 ≀ π‘ˆ)
314 fllep1 13772 . . . . 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 25915 . . 3 (πœ‘ β†’ (π»β€˜π‘‹) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
317305, 311, 3163brtr4d 5173 . 2 (πœ‘ β†’ (π»β€˜π‘Œ) ≀ (π»β€˜π‘‹))
31852, 47resubcld 11646 . . . . 5 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
31943, 31resubcld 11646 . . . . 5 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
320 peano2rem 11531 . . . . . . . . . . 11 ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
32144, 320syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
322321, 47remulcld 11248 . . . . . . . . 9 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
323322, 51resubcld 11646 . . . . . . . 8 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ ℝ)
324 peano2rem 11531 . . . . . . . . . . 11 ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ∈ ℝ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
32516, 324syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
326325, 47remulcld 11248 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ ℝ)
327326, 42resubcld 11646 . . . . . . . 8 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ ℝ)
328325, 31remulcld 11248 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ∈ ℝ)
329328, 42resubcld 11646 . . . . . . . 8 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ ℝ)
330322recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ β„‚)
331326recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ β„‚)
332330, 331subcld 11575 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) ∈ β„‚)
333332, 273addcomd 11420 . . . . . . . . . . . 12 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴) = (β¦‹π‘Œ / π‘₯⦌𝐴 + ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))))
334330, 331, 273subsubd 11603 . . . . . . . . . . . 12 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) + β¦‹π‘Œ / π‘₯⦌𝐴))
335273, 331, 330subsub2d 11604 . . . . . . . . . . . 12 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))) = (β¦‹π‘Œ / π‘₯⦌𝐴 + ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))))
336333, 334, 3353eqtr4d 2776 . . . . . . . . . . 11 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))))
337 1cnd 11213 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 1 ∈ β„‚)
338279, 280, 337nnncan2d 11610 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) = ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ (𝑋 βˆ’ (βŒŠβ€˜π‘‹))))
339338, 277eqtrd 2766 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) = (π‘Œ βˆ’ 𝑋))
340339oveq1d 7420 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) Β· ⦋𝑋 / π‘₯⦌𝐡) = ((π‘Œ βˆ’ 𝑋) Β· ⦋𝑋 / π‘₯⦌𝐡))
341325recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ β„‚)
342321recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ β„‚)
34347recnd 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚)
344341, 342, 343subdird 11675 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) βˆ’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)) Β· ⦋𝑋 / π‘₯⦌𝐡) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)))
345282, 343mulcomd 11239 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘Œ βˆ’ 𝑋) Β· ⦋𝑋 / π‘₯⦌𝐡) = (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
346340, 344, 3453eqtr3d 2774 . . . . . . . . . . . 12 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)) = (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
347346oveq2d 7421 . . . . . . . . . . 11 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
348336, 347eqtrd 2766 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) = (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))))
34947, 66remulcld 11248 . . . . . . . . . . 11 (πœ‘ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) ∈ ℝ)
350 cncfmptc 24787 . . . . . . . . . . . . . . . . 17 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ (𝑋[,]π‘Œ) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
35147, 91, 92, 350syl3anc 1368 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
352 remulcl 11197 . . . . . . . . . . . . . . . . 17 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ)
353 simpl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ)
354353recnd 11246 . . . . . . . . . . . . . . . . . . . . 21 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚)
355 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
356355recnd 11246 . . . . . . . . . . . . . . . . . . . . 21 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
357354, 356jca 511 . . . . . . . . . . . . . . . . . . . 20 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
358 ovmpot 7565 . . . . . . . . . . . . . . . . . . . . 21 ((⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))
359358eqcomd 2732 . . . . . . . . . . . . . . . . . . . 20 ((⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
360357, 359syl 17 . . . . . . . . . . . . . . . . . . 19 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
361360eleq1d 2812 . . . . . . . . . . . . . . . . . 18 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ ↔ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
362361biimpd 228 . . . . . . . . . . . . . . . . 17 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ ((⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ∈ ℝ β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ))
363352, 362mpd 15 . . . . . . . . . . . . . . . 16 ((⦋𝑋 / π‘₯⦌𝐡 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ∈ ℝ)
36472, 73, 351, 96, 90, 363cncfmpt2ss 24791 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
365 df-mpt 5225 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))}
366365eleq1i 2818 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
367366biimpi 215 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
368364, 367syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
369114a1dd 50 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
370369impd 410 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
371343adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ ⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚)
372371, 132jca 511 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (⦋𝑋 / π‘₯⦌𝐡 ∈ β„‚ ∧ 𝑦 ∈ β„‚))
373372, 358syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))
374373eqeq2d 2737 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) ↔ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
375374biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
376375ex 412 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))))
377376impd 410 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
378370, 377jcad 512 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))))
379114a1dd 50 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑦 ∈ (𝑋[,]π‘Œ))))
380379impd 410 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑦 ∈ (𝑋[,]π‘Œ)))
381372, 359syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))
382381eqeq2d 2737 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) ↔ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
383382biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
384383ex 412 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) β†’ (𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
385384impd 410 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) β†’ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)))
386380, 385jcad 512 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))))
387378, 386impbid 211 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))))
388387opabbidv 5207 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))})
389 df-mpt 5225 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))}
390389eqcomi 2735 . . . . . . . . . . . . . . . . . . 19 {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))
391390eqeq2i 2739 . . . . . . . . . . . . . . . . . 18 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))} ↔ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
392391biimpi 215 . . . . . . . . . . . . . . . . 17 ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))} β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
393388, 392syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ {βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)))
394393eleq1d 2812 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
395394biimpd 228 . . . . . . . . . . . . . 14 (πœ‘ β†’ ({βŸ¨π‘¦, π‘€βŸ© ∣ (𝑦 ∈ (𝑋[,]π‘Œ) ∧ 𝑀 = (⦋𝑋 / π‘₯⦌𝐡(𝑒 ∈ β„‚, 𝑣 ∈ β„‚ ↦ (𝑒 Β· 𝑣))𝑦))} ∈ ((𝑋[,]π‘Œ)–cn→ℝ) β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ)))
396368, 395mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ (𝑋[,]π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦)) ∈ ((𝑋[,]π‘Œ)–cn→ℝ))
397171, 175, 176, 184, 343dvmptcmul 25851 . . . . . . . . . . . . . 14 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 1)))
398343mulridd 11235 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 1) = ⦋𝑋 / π‘₯⦌𝐡)
399398mpteq2dv 5243 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 1)) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡))
400397, 399eqtrd 2766 . . . . . . . . . . . . 13 (πœ‘ β†’ (ℝ D (𝑦 ∈ (𝑋(,)π‘Œ) ↦ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦))) = (𝑦 ∈ (𝑋(,)π‘Œ) ↦ ⦋𝑋 / π‘₯⦌𝐡))
4016adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑋 ∈ 𝑆)
402131rexrd 11268 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ∈ ℝ*)
403260adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘Œ ∈ ℝ*)
404308adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ π‘ˆ ∈ ℝ*)
405402, 403, 404, 225, 227xrletrd 13147 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ 𝑦 ≀ π‘ˆ)
406 vex 3472 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
407 eleq1 2815 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ (π‘˜ ∈ 𝑆 ↔ 𝑦 ∈ 𝑆))
408407anbi2d 628 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ ((𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)))
409 breq2 5145 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ (𝑋 ≀ π‘˜ ↔ 𝑋 ≀ 𝑦))
410 breq1 5144 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ (π‘˜ ≀ π‘ˆ ↔ 𝑦 ≀ π‘ˆ))
411409, 4103anbi23d 1435 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ ((𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ)))
412408, 4113anbi23d 1435 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑦 β†’ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ))))
413 csbeq1 3891 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑦 β†’ β¦‹π‘˜ / π‘₯⦌𝐡 = ⦋𝑦 / π‘₯⦌𝐡)
414236, 413eqtr3id 2780 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ 𝐢 = ⦋𝑦 / π‘₯⦌𝐡)
415414breq1d 5151 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑦 β†’ (𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡 ↔ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡))
416412, 415imbi12d 344 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ (((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡) ↔ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)))
417 simp2l 1196 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝑋 ∈ 𝑆)
418 nfv 1909 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯(πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))
419 nfcsb1v 3913 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯⦋𝑋 / π‘₯⦌𝐡
420241, 242, 419nfbr 5188 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡
421418, 420nfim 1891 . . . . . . . . . . . . . . . . . 18 β„²π‘₯((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡)
422 eleq1 2815 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑋 β†’ (π‘₯ ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
423422anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑋 β†’ ((π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆)))
424 breq2 5145 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑋 β†’ (𝐷 ≀ π‘₯ ↔ 𝐷 ≀ 𝑋))
425 breq1 5144 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑋 β†’ (π‘₯ ≀ π‘˜ ↔ 𝑋 ≀ π‘˜))
426424, 4253anbi12d 1433 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑋 β†’ ((𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ) ↔ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)))
427423, 4263anbi23d 1435 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑋 β†’ ((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) ↔ (πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ))))
428 csbeq1a 3902 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑋 β†’ 𝐡 = ⦋𝑋 / π‘₯⦌𝐡)
429428breq2d 5153 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑋 β†’ (𝐢 ≀ 𝐡 ↔ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡))
430427, 429imbi12d 344 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑋 β†’ (((πœ‘ ∧ (π‘₯ ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ π‘₯ ∧ π‘₯ ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ 𝐡) ↔ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡)))
431421, 430, 253vtoclg1f 3553 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ 𝑆 β†’ ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡))
432417, 431mpcom 38 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ π‘˜ ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ π‘˜ ∧ π‘˜ ≀ π‘ˆ)) β†’ 𝐢 ≀ ⦋𝑋 / π‘₯⦌𝐡)
433406, 416, 432vtocl 3540 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≀ 𝑋 ∧ 𝑋 ≀ 𝑦 ∧ 𝑦 ≀ π‘ˆ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
434215, 401, 216, 222, 223, 405, 433syl123anc 1384 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ (𝑋[,]π‘Œ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
435214, 434sylan2 592 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝑋(,)π‘Œ)) β†’ ⦋𝑦 / π‘₯⦌𝐡 ≀ ⦋𝑋 / π‘₯⦌𝐡)
436 oveq2 7413 . . . . . . . . . . . . 13 (𝑦 = 𝑋 β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑋))
437 oveq2 7413 . . . . . . . . . . . . 13 (𝑦 = π‘Œ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑦) = (⦋𝑋 / π‘₯⦌𝐡 Β· π‘Œ))
43813, 5, 206, 213, 396, 400, 435, 263, 265, 261, 49, 436, 33, 437dvle 25895 . . . . . . . . . . . 12 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((⦋𝑋 / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑋)))
439343, 69, 70subdid 11674 . . . . . . . . . . . 12 (πœ‘ β†’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)) = ((⦋𝑋 / π‘₯⦌𝐡 Β· π‘Œ) βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· 𝑋)))
440438, 439breqtrrd 5169 . . . . . . . . . . 11 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋)))
44142, 51, 349, 440subled 11821 . . . . . . . . . 10 (πœ‘ β†’ (β¦‹π‘Œ / π‘₯⦌𝐴 βˆ’ (⦋𝑋 / π‘₯⦌𝐡 Β· (π‘Œ βˆ’ 𝑋))) ≀ ⦋𝑋 / π‘₯⦌𝐴)
442348, 441eqbrtrd 5163 . . . . . . . . 9 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴)) ≀ ⦋𝑋 / π‘₯⦌𝐴)
443322, 327, 51, 442subled 11821 . . . . . . . 8 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
444325renegcld 11645 . . . . . . . . . . . 12 (πœ‘ β†’ -((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ∈ ℝ)
445 1red 11219 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 1 ∈ ℝ)
4465, 15, 445lesubadd2d 11817 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ≀ 1 ↔ π‘Œ ≀ ((βŒŠβ€˜π‘‹) + 1)))
447310, 446mpbird 257 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ≀ 1)
44816, 445suble0d 11809 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ≀ 0 ↔ (π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) ≀ 1))
449447, 448mpbird 257 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ≀ 0)
450325le0neg1d 11789 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) ≀ 0 ↔ 0 ≀ -((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1)))
451449, 450mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ 0 ≀ -((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1))
45231, 47, 444, 451, 301lemul2ad 12158 . . . . . . . . . . 11 (πœ‘ β†’ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))
453341, 68mulneg1d 11671 . . . . . . . . . . 11 (πœ‘ β†’ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡))
454341, 343mulneg1d 11671 . . . . . . . . . . 11 (πœ‘ β†’ (-((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) = -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))
455452, 453, 4543brtr3d 5172 . . . . . . . . . 10 (πœ‘ β†’ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡))
456326, 328lenegd 11797 . . . . . . . . . 10 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ≀ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ↔ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) ≀ -(((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡)))
457455, 456mpbird 257 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) ≀ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡))
458326, 328, 42, 457lesub1dd 11834 . . . . . . . 8 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
459323, 327, 329, 443, 458letrd 11375 . . . . . . 7 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
460280, 337, 343subdird 11675 . . . . . . . . 9 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (1 Β· ⦋𝑋 / π‘₯⦌𝐡)))
461343mullidd 11236 . . . . . . . . . 10 (πœ‘ β†’ (1 Β· ⦋𝑋 / π‘₯⦌𝐡) = ⦋𝑋 / π‘₯⦌𝐡)
462461oveq2d 7421 . . . . . . . . 9 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ (1 Β· ⦋𝑋 / π‘₯⦌𝐡)) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡))
463460, 462eqtrd 2766 . . . . . . . 8 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) = (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡))
464463oveq1d 7420 . . . . . . 7 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
465279, 337, 68subdird 11675 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (1 Β· β¦‹π‘Œ / π‘₯⦌𝐡)))
46668mullidd 11236 . . . . . . . . . 10 (πœ‘ β†’ (1 Β· β¦‹π‘Œ / π‘₯⦌𝐡) = β¦‹π‘Œ / π‘₯⦌𝐡)
467466oveq2d 7421 . . . . . . . . 9 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ (1 Β· β¦‹π‘Œ / π‘₯⦌𝐡)) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
468465, 467eqtrd 2766 . . . . . . . 8 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) = (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
469468oveq1d 7420 . . . . . . 7 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) βˆ’ 1) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
470459, 464, 4693brtr3d 5172 . . . . . 6 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
47148recnd 11246 . . . . . . 7 (πœ‘ β†’ ((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) ∈ β„‚)
47251recnd 11246 . . . . . . 7 (πœ‘ β†’ ⦋𝑋 / π‘₯⦌𝐴 ∈ β„‚)
473471, 472, 343sub32d 11607 . . . . . 6 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) = ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴))
474272, 273, 68sub32d 11607 . . . . . 6 (πœ‘ β†’ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) = ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴))
475470, 473, 4743brtr4d 5173 . . . . 5 (πœ‘ β†’ ((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
476318, 319, 63, 475leadd1dd 11832 . . . 4 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) ≀ (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
47752recnd 11246 . . . . 5 (πœ‘ β†’ (((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) ∈ β„‚)
47863recnd 11246 . . . . 5 (πœ‘ β†’ Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢 ∈ β„‚)
479477, 478, 343addsubd 11596 . . . 4 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) = (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
48043recnd 11246 . . . . 5 (πœ‘ β†’ (((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) ∈ β„‚)
481480, 478, 68addsubd 11596 . . . 4 (πœ‘ β†’ (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) = (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢))
482476, 479, 4813brtr4d 5173 . . 3 (πœ‘ β†’ (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
483316oveq1d 7420 . . 3 (πœ‘ β†’ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) = (((((𝑋 βˆ’ (βŒŠβ€˜π‘‹)) Β· ⦋𝑋 / π‘₯⦌𝐡) βˆ’ ⦋𝑋 / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ ⦋𝑋 / π‘₯⦌𝐡))
484311oveq1d 7420 . . 3 (πœ‘ β†’ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡) = (((((π‘Œ βˆ’ (βŒŠβ€˜π‘‹)) Β· β¦‹π‘Œ / π‘₯⦌𝐡) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐴) + Ξ£π‘˜ ∈ (𝑀...(βŒŠβ€˜π‘‹))𝐢) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
485482, 483, 4843brtr4d 5173 . 2 (πœ‘ β†’ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡))
486317, 485jca 511 1 (πœ‘ β†’ ((π»β€˜π‘Œ) ≀ (π»β€˜π‘‹) ∧ ((π»β€˜π‘‹) βˆ’ ⦋𝑋 / π‘₯⦌𝐡) ≀ ((π»β€˜π‘Œ) βˆ’ β¦‹π‘Œ / π‘₯⦌𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  β¦‹csb 3888   βŠ† wss 3943  {cpr 4625   class class class wbr 5141  {copab 5203   ↦ cmpt 5224  dom cdm 5669  ran crn 5670   β†Ύ cres 5671  βŸΆwf 6533  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  +∞cpnf 11249  β„*cxr 11251   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  -cneg 11449  β„€cz 12562  β„€β‰₯cuz 12826  (,)cioo 13330  [,]cicc 13333  ...cfz 13490  βŒŠcfl 13761  Ξ£csu 15638  TopOpenctopn 17376  topGenctg 17392  β„‚fldccnfld 21240  β€“cnβ†’ccncf 24751   D cdv 25747
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12981  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13334  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-starv 17221  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-unif 17229  df-hom 17230  df-cco 17231  df-rest 17377  df-topn 17378  df-0g 17396  df-gsum 17397  df-topgen 17398  df-pt 17399  df-prds 17402  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-submnd 18714  df-mulg 18996  df-cntz 19233  df-cmn 19702  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22751  df-topon 22768  df-topsp 22790  df-bases 22804  df-cld 22878  df-ntr 22879  df-cls 22880  df-nei 22957  df-lp 22995  df-perf 22996  df-cn 23086  df-cnp 23087  df-haus 23174  df-cmp 23246  df-tx 23421  df-hmeo 23614  df-fil 23705  df-fm 23797  df-flim 23798  df-flf 23799  df-xms 24181  df-ms 24182  df-tms 24183  df-cncf 24753  df-limc 25750  df-dv 25751
This theorem is referenced by:  dvfsumlem3  25918
  Copyright terms: Public domain W3C validator