Step | Hyp | Ref
| Expression |
1 | | ax-hv0cl 30234 |
. . 3
β’
0β β β |
2 | | nlelch.1 |
. . . . . . 7
β’ π β LinFn |
3 | 2 | lnfnfi 31272 |
. . . . . 6
β’ π:
ββΆβ |
4 | | fveq2 6888 |
. . . . . . . . 9
β’
((β₯β(nullβπ)) = 0β β
(β₯β(β₯β(nullβπ))) =
(β₯β0β)) |
5 | | nlelch.2 |
. . . . . . . . . . 11
β’ π β ContFn |
6 | 2, 5 | nlelchi 31292 |
. . . . . . . . . 10
β’
(nullβπ)
β Cβ |
7 | 6 | ococi 30636 |
. . . . . . . . 9
β’
(β₯β(β₯β(nullβπ))) = (nullβπ) |
8 | | choc0 30557 |
. . . . . . . . 9
β’
(β₯β0β) = β |
9 | 4, 7, 8 | 3eqtr3g 2796 |
. . . . . . . 8
β’
((β₯β(nullβπ)) = 0β β
(nullβπ) =
β) |
10 | 9 | eleq2d 2820 |
. . . . . . 7
β’
((β₯β(nullβπ)) = 0β β (π£ β (nullβπ) β π£ β β)) |
11 | 10 | biimpar 479 |
. . . . . 6
β’
(((β₯β(nullβπ)) = 0β β§ π£ β β) β π£ β (nullβπ)) |
12 | | elnlfn2 31160 |
. . . . . 6
β’ ((π: ββΆβ β§
π£ β (nullβπ)) β (πβπ£) = 0) |
13 | 3, 11, 12 | sylancr 588 |
. . . . 5
β’
(((β₯β(nullβπ)) = 0β β§ π£ β β) β (πβπ£) = 0) |
14 | | hi02 30328 |
. . . . . 6
β’ (π£ β β β (π£
Β·ih 0β) = 0) |
15 | 14 | adantl 483 |
. . . . 5
β’
(((β₯β(nullβπ)) = 0β β§ π£ β β) β (π£
Β·ih 0β) = 0) |
16 | 13, 15 | eqtr4d 2776 |
. . . 4
β’
(((β₯β(nullβπ)) = 0β β§ π£ β β) β (πβπ£) = (π£ Β·ih
0β)) |
17 | 16 | ralrimiva 3147 |
. . 3
β’
((β₯β(nullβπ)) = 0β β
βπ£ β β
(πβπ£) = (π£ Β·ih
0β)) |
18 | | oveq2 7412 |
. . . . . 6
β’ (π€ = 0β β
(π£
Β·ih π€) = (π£ Β·ih
0β)) |
19 | 18 | eqeq2d 2744 |
. . . . 5
β’ (π€ = 0β β
((πβπ£) = (π£ Β·ih π€) β (πβπ£) = (π£ Β·ih
0β))) |
20 | 19 | ralbidv 3178 |
. . . 4
β’ (π€ = 0β β
(βπ£ β β
(πβπ£) = (π£ Β·ih π€) β βπ£ β β (πβπ£) = (π£ Β·ih
0β))) |
21 | 20 | rspcev 3612 |
. . 3
β’
((0β β β β§ βπ£ β β (πβπ£) = (π£ Β·ih
0β)) β βπ€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€)) |
22 | 1, 17, 21 | sylancr 588 |
. 2
β’
((β₯β(nullβπ)) = 0β β βπ€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€)) |
23 | 6 | choccli 30538 |
. . . 4
β’
(β₯β(nullβπ)) β
Cβ |
24 | 23 | chne0i 30684 |
. . 3
β’
((β₯β(nullβπ)) β 0β β
βπ’ β
(β₯β(nullβπ))π’ β 0β) |
25 | 23 | cheli 30463 |
. . . . 5
β’ (π’ β
(β₯β(nullβπ)) β π’ β β) |
26 | 3 | ffvelcdmi 7081 |
. . . . . . . . . . . 12
β’ (π’ β β β (πβπ’) β β) |
27 | 26 | adantr 482 |
. . . . . . . . . . 11
β’ ((π’ β β β§ π’ β 0β)
β (πβπ’) β
β) |
28 | | hicl 30311 |
. . . . . . . . . . . . 13
β’ ((π’ β β β§ π’ β β) β (π’
Β·ih π’) β β) |
29 | 28 | anidms 568 |
. . . . . . . . . . . 12
β’ (π’ β β β (π’
Β·ih π’) β β) |
30 | 29 | adantr 482 |
. . . . . . . . . . 11
β’ ((π’ β β β§ π’ β 0β)
β (π’
Β·ih π’) β β) |
31 | | his6 30330 |
. . . . . . . . . . . . 13
β’ (π’ β β β ((π’
Β·ih π’) = 0 β π’ = 0β)) |
32 | 31 | necon3bid 2986 |
. . . . . . . . . . . 12
β’ (π’ β β β ((π’
Β·ih π’) β 0 β π’ β 0β)) |
33 | 32 | biimpar 479 |
. . . . . . . . . . 11
β’ ((π’ β β β§ π’ β 0β)
β (π’
Β·ih π’) β 0) |
34 | 27, 30, 33 | divcld 11986 |
. . . . . . . . . 10
β’ ((π’ β β β§ π’ β 0β)
β ((πβπ’) / (π’ Β·ih π’)) β
β) |
35 | 34 | cjcld 15139 |
. . . . . . . . 9
β’ ((π’ β β β§ π’ β 0β)
β (ββ((πβπ’) / (π’ Β·ih π’))) β
β) |
36 | | simpl 484 |
. . . . . . . . 9
β’ ((π’ β β β§ π’ β 0β)
β π’ β
β) |
37 | | hvmulcl 30244 |
. . . . . . . . 9
β’
(((ββ((πβπ’) / (π’ Β·ih π’))) β β β§ π’ β β) β
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β β) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . . 8
β’ ((π’ β β β§ π’ β 0β)
β ((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β β) |
39 | 38 | adantll 713 |
. . . . . . 7
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β β) |
40 | | hvmulcl 30244 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ’) β β β§ π£ β β) β ((πβπ’) Β·β π£) β
β) |
41 | 26, 40 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β ((πβπ’) Β·β π£) β
β) |
42 | 3 | ffvelcdmi 7081 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β β β (πβπ£) β β) |
43 | | hvmulcl 30244 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ£) β β β§ π’ β β) β ((πβπ£) Β·β π’) β
β) |
44 | 42, 43 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ β β β§ π’ β β) β ((πβπ£) Β·β π’) β
β) |
45 | 44 | ancoms 460 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β ((πβπ£) Β·β π’) β
β) |
46 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β π’ β
β) |
47 | | his2sub 30323 |
. . . . . . . . . . . . . . . 16
β’ ((((πβπ’) Β·β π£) β β β§ ((πβπ£) Β·β π’) β β β§ π’ β β) β
((((πβπ’)
Β·β π£) ββ ((πβπ£) Β·β π’))
Β·ih π’) = ((((πβπ’) Β·β π£)
Β·ih π’) β (((πβπ£) Β·β π’)
Β·ih π’))) |
48 | 41, 45, 46, 47 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π’ β β β§ π£ β β) β
((((πβπ’)
Β·β π£) ββ ((πβπ£) Β·β π’))
Β·ih π’) = ((((πβπ’) Β·β π£)
Β·ih π’) β (((πβπ£) Β·β π’)
Β·ih π’))) |
49 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β β§ π£ β β) β (πβπ’) β β) |
50 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β β§ π£ β β) β π£ β
β) |
51 | | ax-his3 30315 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ’) β β β§ π£ β β β§ π’ β β) β (((πβπ’) Β·β π£)
Β·ih π’) = ((πβπ’) Β· (π£ Β·ih π’))) |
52 | 49, 50, 46, 51 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β (((πβπ’) Β·β π£)
Β·ih π’) = ((πβπ’) Β· (π£ Β·ih π’))) |
53 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β β§ π£ β β) β (πβπ£) β β) |
54 | | ax-his3 30315 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ£) β β β§ π’ β β β§ π’ β β) β (((πβπ£) Β·β π’)
Β·ih π’) = ((πβπ£) Β· (π’ Β·ih π’))) |
55 | 53, 46, 46, 54 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β (((πβπ£) Β·β π’)
Β·ih π’) = ((πβπ£) Β· (π’ Β·ih π’))) |
56 | 52, 55 | oveq12d 7422 |
. . . . . . . . . . . . . . 15
β’ ((π’ β β β§ π£ β β) β
((((πβπ’)
Β·β π£) Β·ih π’) β (((πβπ£) Β·β π’)
Β·ih π’)) = (((πβπ’) Β· (π£ Β·ih π’)) β ((πβπ£) Β· (π’ Β·ih π’)))) |
57 | 48, 56 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
β’ ((π’ β β β§ π£ β β) β (((πβπ’) Β· (π£ Β·ih π’)) β ((πβπ£) Β· (π’ Β·ih π’))) = ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’)) |
58 | 57 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π£ β β) β (((πβπ’) Β· (π£ Β·ih π’)) β ((πβπ£) Β· (π’ Β·ih π’))) = ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’)) |
59 | | hvsubcl 30248 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πβπ’) Β·β π£) β β β§ ((πβπ£) Β·β π’) β β) β
(((πβπ’)
Β·β π£) ββ ((πβπ£) Β·β π’)) β
β) |
60 | 41, 45, 59 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β β§ π£ β β) β (((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) β β) |
61 | 2 | lnfnsubi 31277 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πβπ’) Β·β π£) β β β§ ((πβπ£) Β·β π’) β β) β (πβ(((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’))) = ((πβ((πβπ’) Β·β π£)) β (πβ((πβπ£) Β·β π’)))) |
62 | 41, 45, 61 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β β β§ π£ β β) β (πβ(((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’))) = ((πβ((πβπ’) Β·β π£)) β (πβ((πβπ£) Β·β π’)))) |
63 | 2 | lnfnmuli 31275 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβπ’) β β β§ π£ β β) β (πβ((πβπ’) Β·β π£)) = ((πβπ’) Β· (πβπ£))) |
64 | 26, 63 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π’ β β β§ π£ β β) β (πβ((πβπ’) Β·β π£)) = ((πβπ’) Β· (πβπ£))) |
65 | 2 | lnfnmuli 31275 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβπ£) β β β§ π’ β β) β (πβ((πβπ£) Β·β π’)) = ((πβπ£) Β· (πβπ’))) |
66 | | mulcom 11192 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ£) β β β§ (πβπ’) β β) β ((πβπ£) Β· (πβπ’)) = ((πβπ’) Β· (πβπ£))) |
67 | 26, 66 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβπ£) β β β§ π’ β β) β ((πβπ£) Β· (πβπ’)) = ((πβπ’) Β· (πβπ£))) |
68 | 65, 67 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβπ£) β β β§ π’ β β) β (πβ((πβπ£) Β·β π’)) = ((πβπ’) Β· (πβπ£))) |
69 | 42, 68 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π£ β β β§ π’ β β) β (πβ((πβπ£) Β·β π’)) = ((πβπ’) Β· (πβπ£))) |
70 | 69 | ancoms 460 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π’ β β β§ π£ β β) β (πβ((πβπ£) Β·β π’)) = ((πβπ’) Β· (πβπ£))) |
71 | 64, 70 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β β β§ π£ β β) β ((πβ((πβπ’) Β·β π£)) β (πβ((πβπ£) Β·β π’))) = (((πβπ’) Β· (πβπ£)) β ((πβπ’) Β· (πβπ£)))) |
72 | | mulcl 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβπ’) β β β§ (πβπ£) β β) β ((πβπ’) Β· (πβπ£)) β β) |
73 | 26, 42, 72 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π’ β β β§ π£ β β) β ((πβπ’) Β· (πβπ£)) β β) |
74 | 73 | subidd 11555 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β β β§ π£ β β) β (((πβπ’) Β· (πβπ£)) β ((πβπ’) Β· (πβπ£))) = 0) |
75 | 62, 71, 74 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β β§ π£ β β) β (πβ(((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’))) = 0) |
76 | | elnlfn 31159 |
. . . . . . . . . . . . . . . . . 18
β’ (π: ββΆβ β
((((πβπ’)
Β·β π£) ββ ((πβπ£) Β·β π’)) β (nullβπ) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) β β β§ (πβ(((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’))) = 0))) |
77 | 3, 76 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) β (nullβπ) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) β β β§ (πβ(((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’))) = 0)) |
78 | 60, 75, 77 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β (((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) β (nullβπ)) |
79 | 6 | chssii 30462 |
. . . . . . . . . . . . . . . . 17
β’
(nullβπ)
β β |
80 | | ocorth 30522 |
. . . . . . . . . . . . . . . . 17
β’
((nullβπ)
β β β (((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) β (nullβπ) β§ π’ β (β₯β(nullβπ))) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’) = 0)) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(((((πβπ’)
Β·β π£) ββ ((πβπ£) Β·β π’)) β (nullβπ) β§ π’ β (β₯β(nullβπ))) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’) = 0) |
82 | 78, 81 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π’ β β β§ π£ β β) β§ π’ β
(β₯β(nullβπ))) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’) = 0) |
83 | 82 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ ((π’ β
(β₯β(nullβπ)) β§ (π’ β β β§ π£ β β)) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’) = 0) |
84 | 83 | anassrs 469 |
. . . . . . . . . . . . 13
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π£ β β) β ((((πβπ’) Β·β π£) ββ
((πβπ£)
Β·β π’)) Β·ih π’) = 0) |
85 | 58, 84 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π£ β β) β (((πβπ’) Β· (π£ Β·ih π’)) β ((πβπ£) Β· (π’ Β·ih π’))) = 0) |
86 | | hicl 30311 |
. . . . . . . . . . . . . . . 16
β’ ((π£ β β β§ π’ β β) β (π£
Β·ih π’) β β) |
87 | 86 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((π’ β β β§ π£ β β) β (π£
Β·ih π’) β β) |
88 | 49, 87 | mulcld 11230 |
. . . . . . . . . . . . . 14
β’ ((π’ β β β§ π£ β β) β ((πβπ’) Β· (π£ Β·ih π’)) β
β) |
89 | | mulcl 11190 |
. . . . . . . . . . . . . . 15
β’ (((πβπ£) β β β§ (π’ Β·ih π’) β β) β ((πβπ£) Β· (π’ Β·ih π’)) β
β) |
90 | 42, 29, 89 | syl2anr 598 |
. . . . . . . . . . . . . 14
β’ ((π’ β β β§ π£ β β) β ((πβπ£) Β· (π’ Β·ih π’)) β
β) |
91 | 88, 90 | subeq0ad 11577 |
. . . . . . . . . . . . 13
β’ ((π’ β β β§ π£ β β) β
((((πβπ’) Β· (π£ Β·ih π’)) β ((πβπ£) Β· (π’ Β·ih π’))) = 0 β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’)))) |
92 | 91 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π£ β β) β ((((πβπ’) Β· (π£ Β·ih π’)) β ((πβπ£) Β· (π’ Β·ih π’))) = 0 β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’)))) |
93 | 85, 92 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π£ β β) β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’))) |
94 | 93 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β§ π£ β β) β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’))) |
95 | 88 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β ((πβπ’) Β· (π£ Β·ih π’)) β
β) |
96 | 42 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β (πβπ£) β
β) |
97 | 30, 33 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π’ β β β§ π’ β 0β)
β ((π’
Β·ih π’) β β β§ (π’ Β·ih π’) β 0)) |
98 | 97 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β ((π’
Β·ih π’) β β β§ (π’ Β·ih π’) β 0)) |
99 | | divmul3 11873 |
. . . . . . . . . . . 12
β’ ((((πβπ’) Β· (π£ Β·ih π’)) β β β§ (πβπ£) β β β§ ((π’ Β·ih π’) β β β§ (π’
Β·ih π’) β 0)) β ((((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (πβπ£) β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’)))) |
100 | 95, 96, 98, 99 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β ((((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (πβπ£) β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’)))) |
101 | 100 | adantlll 717 |
. . . . . . . . . 10
β’ ((((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β§ π£ β β) β
((((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (πβπ£) β ((πβπ’) Β· (π£ Β·ih π’)) = ((πβπ£) Β· (π’ Β·ih π’)))) |
102 | 94, 101 | mpbird 257 |
. . . . . . . . 9
β’ ((((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β§ π£ β β) β (((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (πβπ£)) |
103 | 27 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β (πβπ’) β
β) |
104 | 87 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β (π£
Β·ih π’) β β) |
105 | | div23 11887 |
. . . . . . . . . . . 12
β’ (((πβπ’) β β β§ (π£ Β·ih π’) β β β§ ((π’
Β·ih π’) β β β§ (π’ Β·ih π’) β 0)) β (((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (((πβπ’) / (π’ Β·ih π’)) Β· (π£ Β·ih π’))) |
106 | 103, 104,
98, 105 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β (((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (((πβπ’) / (π’ Β·ih π’)) Β· (π£ Β·ih π’))) |
107 | 34 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β ((πβπ’) / (π’ Β·ih π’)) β
β) |
108 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β π£ β
β) |
109 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β π’ β
β) |
110 | | his52 30318 |
. . . . . . . . . . . 12
β’ ((((πβπ’) / (π’ Β·ih π’)) β β β§ π£ β β β§ π’ β β) β (π£
Β·ih ((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’)) = (((πβπ’) / (π’ Β·ih π’)) Β· (π£ Β·ih π’))) |
111 | 107, 108,
109, 110 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β (π£
Β·ih ((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’)) = (((πβπ’) / (π’ Β·ih π’)) Β· (π£ Β·ih π’))) |
112 | 106, 111 | eqtr4d 2776 |
. . . . . . . . . 10
β’ (((π’ β β β§ π’ β 0β)
β§ π£ β β)
β (((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’))) |
113 | 112 | adantlll 717 |
. . . . . . . . 9
β’ ((((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β§ π£ β β) β (((πβπ’) Β· (π£ Β·ih π’)) / (π’ Β·ih π’)) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’))) |
114 | 102, 113 | eqtr3d 2775 |
. . . . . . . 8
β’ ((((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β§ π£ β β) β (πβπ£) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’))) |
115 | 114 | ralrimiva 3147 |
. . . . . . 7
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β
βπ£ β β
(πβπ£) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’))) |
116 | | oveq2 7412 |
. . . . . . . . . 10
β’ (π€ = ((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β (π£ Β·ih π€) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’))) |
117 | 116 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π€ = ((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β ((πβπ£) = (π£ Β·ih π€) β (πβπ£) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’)))) |
118 | 117 | ralbidv 3178 |
. . . . . . . 8
β’ (π€ = ((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β (βπ£ β β (πβπ£) = (π£ Β·ih π€) β βπ£ β β (πβπ£) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’)))) |
119 | 118 | rspcev 3612 |
. . . . . . 7
β’
((((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’) β β β§ βπ£ β β (πβπ£) = (π£ Β·ih
((ββ((πβπ’) / (π’ Β·ih π’)))
Β·β π’))) β βπ€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€)) |
120 | 39, 115, 119 | syl2anc 585 |
. . . . . 6
β’ (((π’ β
(β₯β(nullβπ)) β§ π’ β β) β§ π’ β 0β) β
βπ€ β β
βπ£ β β
(πβπ£) = (π£ Β·ih π€)) |
121 | 120 | ex 414 |
. . . . 5
β’ ((π’ β
(β₯β(nullβπ)) β§ π’ β β) β (π’ β 0β β
βπ€ β β
βπ£ β β
(πβπ£) = (π£ Β·ih π€))) |
122 | 25, 121 | mpdan 686 |
. . . 4
β’ (π’ β
(β₯β(nullβπ)) β (π’ β 0β β
βπ€ β β
βπ£ β β
(πβπ£) = (π£ Β·ih π€))) |
123 | 122 | rexlimiv 3149 |
. . 3
β’
(βπ’ β
(β₯β(nullβπ))π’ β 0β β
βπ€ β β
βπ£ β β
(πβπ£) = (π£ Β·ih π€)) |
124 | 24, 123 | sylbi 216 |
. 2
β’
((β₯β(nullβπ)) β 0β β
βπ€ β β
βπ£ β β
(πβπ£) = (π£ Β·ih π€)) |
125 | 22, 124 | pm2.61ine 3026 |
1
β’
βπ€ β
β βπ£ β
β (πβπ£) = (π£ Β·ih π€) |