Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lcmineqlem12 Structured version   Visualization version   GIF version

Theorem lcmineqlem12 41563
Description: Base case for induction. (Contributed by metakunt, 12-May-2024.)
Hypothesis
Ref Expression
lcmineqlem12.1 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
Assertion
Ref Expression
lcmineqlem12 (๐œ‘ โ†’ โˆซ(0[,]1)((๐‘กโ†‘(1 โˆ’ 1)) ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) d๐‘ก = (1 / (1 ยท (๐‘C1))))
Distinct variable groups:   ๐‘ก,๐‘   ๐œ‘,๐‘ก

Proof of Theorem lcmineqlem12
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elunitcn 13472 . . . 4 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โˆˆ โ„‚)
2 1m1e0 12309 . . . . . . . 8 (1 โˆ’ 1) = 0
32oveq2i 7424 . . . . . . 7 (๐‘กโ†‘(1 โˆ’ 1)) = (๐‘กโ†‘0)
4 simpr 483 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ๐‘ก โˆˆ โ„‚)
54exp0d 14131 . . . . . . 7 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (๐‘กโ†‘0) = 1)
63, 5eqtrid 2777 . . . . . 6 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (๐‘กโ†‘(1 โˆ’ 1)) = 1)
76oveq1d 7428 . . . . 5 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((๐‘กโ†‘(1 โˆ’ 1)) ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) = (1 ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))))
8 1cnd 11234 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ 1 โˆˆ โ„‚)
98, 4subcld 11596 . . . . . . 7 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
10 lcmineqlem12.1 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
11 nnm1nn0 12538 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
1210, 11syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
1312adantr 479 . . . . . . 7 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
149, 13expcld 14137 . . . . . 6 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) โˆˆ โ„‚)
1514mullidd 11257 . . . . 5 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (1 ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
167, 15eqtrd 2765 . . . 4 ((๐œ‘ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((๐‘กโ†‘(1 โˆ’ 1)) ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
171, 16sylan2 591 . . 3 ((๐œ‘ โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ((๐‘กโ†‘(1 โˆ’ 1)) ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
1817itgeq2dv 25724 . 2 (๐œ‘ โ†’ โˆซ(0[,]1)((๐‘กโ†‘(1 โˆ’ 1)) ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) d๐‘ก = โˆซ(0[,]1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก)
19 0red 11242 . . . . 5 (๐œ‘ โ†’ 0 โˆˆ โ„)
20 1red 11240 . . . . 5 (๐œ‘ โ†’ 1 โˆˆ โ„)
211, 14sylan2 591 . . . . 5 ((๐œ‘ โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) โˆˆ โ„‚)
2219, 20, 21itgioo 25758 . . . 4 (๐œ‘ โ†’ โˆซ(0(,)1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก = โˆซ(0[,]1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก)
23 eqidd 2726 . . . . . . 7 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ (๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = (๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
24 oveq2 7421 . . . . . . . . . 10 (๐‘ฅ = ๐‘ก โ†’ (1 โˆ’ ๐‘ฅ) = (1 โˆ’ ๐‘ก))
2524oveq1d 7428 . . . . . . . . 9 (๐‘ฅ = ๐‘ก โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
2625adantl 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ = ๐‘ก) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
2726adantlr 713 . . . . . . 7 (((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โˆง ๐‘ฅ = ๐‘ก) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
28 simpr 483 . . . . . . 7 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ ๐‘ก โˆˆ (0(,)1))
29 1cnd 11234 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ 1 โˆˆ โ„‚)
30 elioore 13381 . . . . . . . . . 10 (๐‘ก โˆˆ (0(,)1) โ†’ ๐‘ก โˆˆ โ„)
31 recn 11223 . . . . . . . . . 10 (๐‘ก โˆˆ โ„ โ†’ ๐‘ก โˆˆ โ„‚)
3228, 30, 313syl 18 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ ๐‘ก โˆˆ โ„‚)
3329, 32subcld 11596 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
3412adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
3533, 34expcld 14137 . . . . . . 7 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) โˆˆ โ„‚)
3623, 27, 28, 35fvmptd 7005 . . . . . 6 ((๐œ‘ โˆง ๐‘ก โˆˆ (0(,)1)) โ†’ ((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก) = ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)))
3736itgeq2dv 25724 . . . . 5 (๐œ‘ โ†’ โˆซ(0(,)1)((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก) d๐‘ก = โˆซ(0(,)1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก)
38 cnelprrecn 11226 . . . . . . . . . . . . 13 โ„‚ โˆˆ {โ„, โ„‚}
3938a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ โ„‚ โˆˆ {โ„, โ„‚})
40 1cnd 11234 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ 1 โˆˆ โ„‚)
41 simpr 483 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ๐‘ฅ โˆˆ โ„‚)
4240, 41subcld 11596 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ฅ) โˆˆ โ„‚)
43 nnnn0 12504 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0)
4410, 43syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
4544adantr 479 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„•0)
4642, 45expcld 14137 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘) โˆˆ โ„‚)
4745nn0cnd 12559 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„‚)
4812adantr 479 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
4942, 48expcld 14137 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)) โˆˆ โ„‚)
5047, 49mulcld 11259 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ โ„‚)
5140negcld 11583 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ -1 โˆˆ โ„‚)
5250, 51mulcld 11259 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1) โˆˆ โ„‚)
53 simpr 483 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ๐‘ฆ โˆˆ โ„‚)
5444adantr 479 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„•0)
5553, 54expcld 14137 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ฆโ†‘๐‘) โˆˆ โ„‚)
5654nn0cnd 12559 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„‚)
5712adantr 479 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
5853, 57expcld 14137 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ฆโ†‘(๐‘ โˆ’ 1)) โˆˆ โ„‚)
5956, 58mulcld 11259 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ ยท (๐‘ฆโ†‘(๐‘ โˆ’ 1))) โˆˆ โ„‚)
60 0cnd 11232 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ 0 โˆˆ โ„‚)
61 1cnd 11234 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
6239, 61dvmptc 25903 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ 1)) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ 0))
6339dvmptid 25902 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ ๐‘ฅ)) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ 1))
6439, 40, 60, 62, 41, 40, 63dvmptsub 25912 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ (1 โˆ’ ๐‘ฅ))) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ (0 โˆ’ 1)))
65 df-neg 11472 . . . . . . . . . . . . . . . 16 -1 = (0 โˆ’ 1)
6665a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ -1 = (0 โˆ’ 1))
6766mpteq2dv 5246 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ -1) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ (0 โˆ’ 1)))
6864, 67eqtr4d 2768 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ (1 โˆ’ ๐‘ฅ))) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ -1))
69 dvexp 25898 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ (โ„‚ D (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘๐‘))) = (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ ยท (๐‘ฆโ†‘(๐‘ โˆ’ 1)))))
7010, 69syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โ„‚ D (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘๐‘))) = (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ ยท (๐‘ฆโ†‘(๐‘ โˆ’ 1)))))
71 oveq1 7420 . . . . . . . . . . . . 13 (๐‘ฆ = (1 โˆ’ ๐‘ฅ) โ†’ (๐‘ฆโ†‘๐‘) = ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))
72 oveq1 7420 . . . . . . . . . . . . . 14 (๐‘ฆ = (1 โˆ’ ๐‘ฅ) โ†’ (๐‘ฆโ†‘(๐‘ โˆ’ 1)) = ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))
7372oveq2d 7429 . . . . . . . . . . . . 13 (๐‘ฆ = (1 โˆ’ ๐‘ฅ) โ†’ (๐‘ ยท (๐‘ฆโ†‘(๐‘ โˆ’ 1))) = (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
7439, 39, 42, 51, 55, 59, 68, 70, 71, 73dvmptco 25917 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)))
7561negcld 11583 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -1 โˆˆ โ„‚)
7610nncnd 12253 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
7710nnne0d 12287 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ โ‰  0)
7875, 76, 77divcld 12015 . . . . . . . . . . . 12 (๐œ‘ โ†’ (-1 / ๐‘) โˆˆ โ„‚)
7939, 46, 52, 74, 78dvmptcmul 25909 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))))
8078adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (-1 / ๐‘) โˆˆ โ„‚)
8180, 50, 51mulassd 11262 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (((-1 / ๐‘) ยท (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))) ยท -1) = ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)))
8281eqcomd 2731 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)) = (((-1 / ๐‘) ยท (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))) ยท -1))
8380, 47, 49mulassd 11262 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (((-1 / ๐‘) ยท ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = ((-1 / ๐‘) ยท (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))))
8483oveq1d 7428 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((((-1 / ๐‘) ยท ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1) = (((-1 / ๐‘) ยท (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))) ยท -1))
8584eqcomd 2731 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (((-1 / ๐‘) ยท (๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))) ยท -1) = ((((-1 / ๐‘) ยท ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))
8682, 85eqtrd 2765 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)) = ((((-1 / ๐‘) ยท ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))
8777adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ๐‘ โ‰  0)
8851, 47, 87divcan1d 12016 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ๐‘) = -1)
8988oveq1d 7428 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (((-1 / ๐‘) ยท ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = (-1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
9089oveq1d 7428 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((((-1 / ๐‘) ยท ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1) = ((-1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))
9186, 90eqtrd 2765 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)) = ((-1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))
9251, 51, 49mul32d 11449 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 ยท -1) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = ((-1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))
9392eqcomd 2731 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1) = ((-1 ยท -1) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
9491, 93eqtrd 2765 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)) = ((-1 ยท -1) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
9540, 40mul2negd 11694 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (-1 ยท -1) = (1 ยท 1))
96 1t1e1 12399 . . . . . . . . . . . . . . . 16 (1 ยท 1) = 1
9795, 96eqtrdi 2781 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (-1 ยท -1) = 1)
9897oveq1d 7428 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 ยท -1) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = (1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
9949mullidd 11257 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (1 ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))
10098, 99eqtrd 2765 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 ยท -1) ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) = ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))
10194, 100eqtrd 2765 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1)) = ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))
102101mpteq2dva 5244 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((-1 / ๐‘) ยท ((๐‘ ยท ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) ยท -1))) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
10379, 102eqtrd 2765 . . . . . . . . . 10 (๐œ‘ โ†’ (โ„‚ D (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))) = (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
10480, 46mulcld 11259 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) โˆˆ โ„‚)
105103, 104, 49resdvopclptsd 41551 . . . . . . . . 9 (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))) = (๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))))
106105fveq1d 6892 . . . . . . . 8 (๐œ‘ โ†’ ((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) = ((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก))
107106ralrimivw 3140 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ก โˆˆ (0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) = ((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก))
108 itgeq2 25720 . . . . . . 7 (โˆ€๐‘ก โˆˆ (0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) = ((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก) โ†’ โˆซ(0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) d๐‘ก = โˆซ(0(,)1)((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก) d๐‘ก)
109107, 108syl 17 . . . . . 6 (๐œ‘ โ†’ โˆซ(0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) d๐‘ก = โˆซ(0(,)1)((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก) d๐‘ก)
110 0le1 11762 . . . . . . . . . 10 0 โ‰ค 1
111110a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค 1)
112 nfv 1909 . . . . . . . . . . . 12 โ„ฒ๐‘ฅ๐œ‘
113 ax-1cn 11191 . . . . . . . . . . . . . . 15 1 โˆˆ โ„‚
114 ssid 3996 . . . . . . . . . . . . . . 15 โ„‚ โІ โ„‚
115 cncfmptc 24845 . . . . . . . . . . . . . . 15 ((1 โˆˆ โ„‚ โˆง โ„‚ โІ โ„‚ โˆง โ„‚ โІ โ„‚) โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ 1) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
116113, 114, 114, 115mp3an 1457 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ โ„‚ โ†ฆ 1) โˆˆ (โ„‚โ€“cnโ†’โ„‚)
117116a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ 1) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
118 cncfmptid 24846 . . . . . . . . . . . . . . 15 ((โ„‚ โІ โ„‚ โˆง โ„‚ โІ โ„‚) โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ๐‘ฅ) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
119114, 114, 118mp2an 690 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ โ„‚ โ†ฆ ๐‘ฅ) โˆˆ (โ„‚โ€“cnโ†’โ„‚)
120119a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ๐‘ฅ) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
121117, 120subcncf 25386 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ (1 โˆ’ ๐‘ฅ)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
122 expcncf 24860 . . . . . . . . . . . . 13 ((๐‘ โˆ’ 1) โˆˆ โ„•0 โ†’ (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘(๐‘ โˆ’ 1))) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
12312, 122syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘(๐‘ โˆ’ 1))) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
124 ssidd 3997 . . . . . . . . . . . 12 (๐œ‘ โ†’ โ„‚ โІ โ„‚)
125112, 121, 123, 124, 72cncfcompt2 24841 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
126125resopunitintvd 41549 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ((0(,)1)โ€“cnโ†’โ„‚))
127105eleq1d 2810 . . . . . . . . . 10 (๐œ‘ โ†’ ((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))) โˆˆ ((0(,)1)โ€“cnโ†’โ„‚) โ†” (๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ((0(,)1)โ€“cnโ†’โ„‚)))
128126, 127mpbird 256 . . . . . . . . 9 (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))) โˆˆ ((0(,)1)โ€“cnโ†’โ„‚))
129 ioossicc 13437 . . . . . . . . . . . 12 (0(,)1) โІ (0[,]1)
130129a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (0(,)1) โІ (0[,]1))
131 ioombl 25507 . . . . . . . . . . . 12 (0(,)1) โˆˆ dom vol
132131a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (0(,)1) โˆˆ dom vol)
133 elunitcn 13472 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ (0[,]1) โ†’ ๐‘ฅ โˆˆ โ„‚)
134133, 49sylan2 591 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (0[,]1)) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)) โˆˆ โ„‚)
135114a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ โ„‚ โІ โ„‚)
136112, 121, 123, 135, 72cncfcompt2 24841 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
137136resclunitintvd 41550 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ((0[,]1)โ€“cnโ†’โ„‚))
13819, 20, 1373jca 1125 . . . . . . . . . . . 12 (๐œ‘ โ†’ (0 โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ((0[,]1)โ€“cnโ†’โ„‚)))
139 cnicciblnc 25785 . . . . . . . . . . . 12 ((0 โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ((0[,]1)โ€“cnโ†’โ„‚)) โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ๐ฟ1)
140138, 139syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ๐ฟ1)
141130, 132, 134, 140iblss 25747 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1))) โˆˆ ๐ฟ1)
142105, 141eqeltrd 2825 . . . . . . . . 9 (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))) โˆˆ ๐ฟ1)
143 cncfmptc 24845 . . . . . . . . . . . . 13 (((-1 / ๐‘) โˆˆ โ„‚ โˆง โ„‚ โІ โ„‚ โˆง โ„‚ โІ โ„‚) โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ (-1 / ๐‘)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
144114, 114, 143mp3an23 1449 . . . . . . . . . . . 12 ((-1 / ๐‘) โˆˆ โ„‚ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ (-1 / ๐‘)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
14578, 144syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ (-1 / ๐‘)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
146145resclunitintvd 41550 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ (-1 / ๐‘)) โˆˆ ((0[,]1)โ€“cnโ†’โ„‚))
147 expcncf 24860 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„•0 โ†’ (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘๐‘)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
14844, 147syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฆ โˆˆ โ„‚ โ†ฆ (๐‘ฆโ†‘๐‘)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
149112, 121, 148, 124, 71cncfcompt2 24841 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) โˆˆ (โ„‚โ€“cnโ†’โ„‚))
150149resclunitintvd 41550 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) โˆˆ ((0[,]1)โ€“cnโ†’โ„‚))
151146, 150mulcncf 25387 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))) โˆˆ ((0[,]1)โ€“cnโ†’โ„‚))
15219, 20, 111, 128, 142, 151ftc2 25992 . . . . . . . 8 (๐œ‘ โ†’ โˆซ(0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) d๐‘ก = (((๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))โ€˜1) โˆ’ ((๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))โ€˜0)))
153 eqidd 2726 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))) = (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))
154 simpr 483 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ ๐‘ฅ = 1)
155154oveq2d 7429 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ (1 โˆ’ ๐‘ฅ) = (1 โˆ’ 1))
156155, 2eqtrdi 2781 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ (1 โˆ’ ๐‘ฅ) = 0)
157156oveq1d 7428 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘) = (0โ†‘๐‘))
158 0exp 14089 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ โ„• โ†’ (0โ†‘๐‘) = 0)
15910, 158syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (0โ†‘๐‘) = 0)
160159adantr 479 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ (0โ†‘๐‘) = 0)
161157, 160eqtrd 2765 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘) = 0)
162161oveq2d 7429 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) = ((-1 / ๐‘) ยท 0))
16378mul01d 11438 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((-1 / ๐‘) ยท 0) = 0)
164163adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ ((-1 / ๐‘) ยท 0) = 0)
165162, 164eqtrd 2765 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ = 1) โ†’ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) = 0)
166 1elunit 13474 . . . . . . . . . . 11 1 โˆˆ (0[,]1)
167166a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โˆˆ (0[,]1))
168 0cnd 11232 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โˆˆ โ„‚)
169153, 165, 167, 168fvmptd 7005 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))โ€˜1) = 0)
170 simpr 483 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ ๐‘ฅ = 0)
171170oveq2d 7429 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ (1 โˆ’ ๐‘ฅ) = (1 โˆ’ 0))
172 1m0e1 12358 . . . . . . . . . . . . . . 15 (1 โˆ’ 0) = 1
173171, 172eqtrdi 2781 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ (1 โˆ’ ๐‘ฅ) = 1)
174173oveq1d 7428 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘) = (1โ†‘๐‘))
17544nn0zd 12609 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
176 1exp 14083 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ โ„ค โ†’ (1โ†‘๐‘) = 1)
177175, 176syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1โ†‘๐‘) = 1)
178177adantr 479 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ (1โ†‘๐‘) = 1)
179174, 178eqtrd 2765 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ ((1 โˆ’ ๐‘ฅ)โ†‘๐‘) = 1)
180179oveq2d 7429 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) = ((-1 / ๐‘) ยท 1))
18178adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ (-1 / ๐‘) โˆˆ โ„‚)
182181mulridd 11256 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ ((-1 / ๐‘) ยท 1) = (-1 / ๐‘))
183180, 182eqtrd 2765 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ = 0) โ†’ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)) = (-1 / ๐‘))
184 0elunit 13473 . . . . . . . . . . 11 0 โˆˆ (0[,]1)
185184a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โˆˆ (0[,]1))
186153, 183, 185, 78fvmptd 7005 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))โ€˜0) = (-1 / ๐‘))
187169, 186oveq12d 7431 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))โ€˜1) โˆ’ ((๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘)))โ€˜0)) = (0 โˆ’ (-1 / ๐‘)))
188152, 187eqtrd 2765 . . . . . . 7 (๐œ‘ โ†’ โˆซ(0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) d๐‘ก = (0 โˆ’ (-1 / ๐‘)))
189 df-neg 11472 . . . . . . . . . 10 --(1 / ๐‘) = (0 โˆ’ -(1 / ๐‘))
190189a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ --(1 / ๐‘) = (0 โˆ’ -(1 / ๐‘)))
19161, 76, 77divnegd 12028 . . . . . . . . . 10 (๐œ‘ โ†’ -(1 / ๐‘) = (-1 / ๐‘))
192191oveq2d 7429 . . . . . . . . 9 (๐œ‘ โ†’ (0 โˆ’ -(1 / ๐‘)) = (0 โˆ’ (-1 / ๐‘)))
193190, 192eqtr2d 2766 . . . . . . . 8 (๐œ‘ โ†’ (0 โˆ’ (-1 / ๐‘)) = --(1 / ๐‘))
19476, 77reccld 12008 . . . . . . . . 9 (๐œ‘ โ†’ (1 / ๐‘) โˆˆ โ„‚)
195194negnegd 11587 . . . . . . . 8 (๐œ‘ โ†’ --(1 / ๐‘) = (1 / ๐‘))
196193, 195eqtrd 2765 . . . . . . 7 (๐œ‘ โ†’ (0 โˆ’ (-1 / ๐‘)) = (1 / ๐‘))
197188, 196eqtrd 2765 . . . . . 6 (๐œ‘ โ†’ โˆซ(0(,)1)((โ„ D (๐‘ฅ โˆˆ (0[,]1) โ†ฆ ((-1 / ๐‘) ยท ((1 โˆ’ ๐‘ฅ)โ†‘๐‘))))โ€˜๐‘ก) d๐‘ก = (1 / ๐‘))
198109, 197eqtr3d 2767 . . . . 5 (๐œ‘ โ†’ โˆซ(0(,)1)((๐‘ฅ โˆˆ (0(,)1) โ†ฆ ((1 โˆ’ ๐‘ฅ)โ†‘(๐‘ โˆ’ 1)))โ€˜๐‘ก) d๐‘ก = (1 / ๐‘))
19937, 198eqtr3d 2767 . . . 4 (๐œ‘ โ†’ โˆซ(0(,)1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก = (1 / ๐‘))
20022, 199eqtr3d 2767 . . 3 (๐œ‘ โ†’ โˆซ(0[,]1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก = (1 / ๐‘))
201 bcn1 14299 . . . . . . 7 (๐‘ โˆˆ โ„•0 โ†’ (๐‘C1) = ๐‘)
20244, 201syl 17 . . . . . 6 (๐œ‘ โ†’ (๐‘C1) = ๐‘)
203202oveq2d 7429 . . . . 5 (๐œ‘ โ†’ (1 ยท (๐‘C1)) = (1 ยท ๐‘))
20476mullidd 11257 . . . . 5 (๐œ‘ โ†’ (1 ยท ๐‘) = ๐‘)
205203, 204eqtrd 2765 . . . 4 (๐œ‘ โ†’ (1 ยท (๐‘C1)) = ๐‘)
206205oveq2d 7429 . . 3 (๐œ‘ โ†’ (1 / (1 ยท (๐‘C1))) = (1 / ๐‘))
207200, 206eqtr4d 2768 . 2 (๐œ‘ โ†’ โˆซ(0[,]1)((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1)) d๐‘ก = (1 / (1 ยท (๐‘C1))))
20818, 207eqtrd 2765 1 (๐œ‘ โ†’ โˆซ(0[,]1)((๐‘กโ†‘(1 โˆ’ 1)) ยท ((1 โˆ’ ๐‘ก)โ†‘(๐‘ โˆ’ 1))) d๐‘ก = (1 / (1 ยท (๐‘C1))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 394   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930  โˆ€wral 3051   โІ wss 3941  {cpr 4627   class class class wbr 5144   โ†ฆ cmpt 5227  dom cdm 5673  โ€˜cfv 6543  (class class class)co 7413  โ„‚cc 11131  โ„cr 11132  0cc0 11133  1c1 11134   ยท cmul 11138   โ‰ค cle 11274   โˆ’ cmin 11469  -cneg 11470   / cdiv 11896  โ„•cn 12237  โ„•0cn0 12497  โ„คcz 12583  (,)cioo 13351  [,]cicc 13354  โ†‘cexp 14053  Ccbc 14288  โ€“cnโ†’ccncf 24809  volcvol 25405  ๐ฟ1cibl 25559  โˆซcitg 25560   D cdv 25805
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 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cc 10453  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211  ax-addf 11212
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 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-symdif 4238  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-disj 5110  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  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 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-ofr 7680  df-om 7866  df-1st 7987  df-2nd 7988  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-omul 8485  df-er 8718  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9381  df-fi 9429  df-sup 9460  df-inf 9461  df-oi 9528  df-dju 9919  df-card 9957  df-acn 9960  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-z 12584  df-dec 12703  df-uz 12848  df-q 12958  df-rp 13002  df-xneg 13119  df-xadd 13120  df-xmul 13121  df-ioo 13355  df-ioc 13356  df-ico 13357  df-icc 13358  df-fz 13512  df-fzo 13655  df-fl 13784  df-mod 13862  df-seq 13994  df-exp 14054  df-fac 14260  df-bc 14289  df-hash 14317  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-clim 15459  df-rlim 15460  df-sum 15660  df-struct 17110  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-rest 17398  df-topn 17399  df-0g 17417  df-gsum 17418  df-topgen 17419  df-pt 17420  df-prds 17423  df-xrs 17478  df-qtop 17483  df-imas 17484  df-xps 17486  df-mre 17560  df-mrc 17561  df-acs 17563  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-submnd 18735  df-mulg 19023  df-cntz 19267  df-cmn 19736  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-fbas 21275  df-fg 21276  df-cnfld 21279  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-perf 23054  df-cn 23144  df-cnp 23145  df-haus 23232  df-cmp 23304  df-tx 23479  df-hmeo 23672  df-fil 23763  df-fm 23855  df-flim 23856  df-flf 23857  df-xms 24239  df-ms 24240  df-tms 24241  df-cncf 24811  df-ovol 25406  df-vol 25407  df-mbf 25561  df-itg1 25562  df-itg2 25563  df-ibl 25564  df-itg 25565  df-0p 25612  df-limc 25808  df-dv 25809
This theorem is referenced by:  lcmineqlem13  41564
  Copyright terms: Public domain W3C validator