Step | Hyp | Ref
| Expression |
1 | | axcontlem8.1 |
. . . . . . . . 9
β’ π· = {π β (πΌβπ) β£ (π Btwn β¨π, πβ© β¨ π Btwn β¨π, πβ©)} |
2 | | axcontlem8.2 |
. . . . . . . . 9
β’ πΉ = {β¨π₯, π‘β© β£ (π₯ β π· β§ (π‘ β (0[,)+β) β§ βπ β (1...π)(π₯βπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (πβπ)))))} |
3 | 1, 2 | axcontlem6 27960 |
. . . . . . . 8
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ π β π·) β ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) |
4 | 3 | ex 414 |
. . . . . . 7
β’ (((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β (π β π· β ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))))) |
5 | 1, 2 | axcontlem6 27960 |
. . . . . . . 8
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ π β π·) β ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) |
6 | 5 | ex 414 |
. . . . . . 7
β’ (((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β (π β π· β ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))))) |
7 | 1, 2 | axcontlem6 27960 |
. . . . . . . 8
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ π
β π·) β ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) |
8 | 7 | ex 414 |
. . . . . . 7
β’ (((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β (π
β π· β ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
9 | 4, 6, 8 | 3anim123d 1444 |
. . . . . 6
β’ (((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β ((π β π· β§ π β π· β§ π
β π·) β (((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
10 | 9 | imp 408 |
. . . . 5
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β (((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
11 | 10 | adantr 482 |
. . . 4
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β (((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
12 | | 3an6 1447 |
. . . . 5
β’ ((((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β (((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β)) β§
(βπ β
(1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
13 | | 0elunit 13392 |
. . . . . . . . . . . 12
β’ 0 β
(0[,]1) |
14 | | simplr1 1216 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β (πΉβπ) β (0[,)+β)) |
15 | 14 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β (0[,)+β)) |
16 | | elrege0 13377 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β (0[,)+β) β ((πΉβπ) β β β§ 0 β€ (πΉβπ))) |
17 | 16 | simplbi 499 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (0[,)+β) β (πΉβπ) β β) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β β) |
19 | 18 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β β) |
20 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β€ (πΉβπ)) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β€ (πΉβπ)) |
22 | | simprrr 781 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β€ (πΉβπ
)) |
23 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) = (πΉβπ
)) |
24 | 22, 23 | breqtrrd 5134 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β€ (πΉβπ)) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β€ (πΉβπ)) |
26 | | simplr2 1217 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β (πΉβπ) β (0[,)+β)) |
27 | 26 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β (0[,)+β)) |
28 | | elrege0 13377 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) β (0[,)+β) β ((πΉβπ) β β β§ 0 β€ (πΉβπ))) |
29 | 28 | simplbi 499 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β (0[,)+β) β (πΉβπ) β β) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β β) |
31 | 18, 30 | letri3d 11302 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β ((πΉβπ) = (πΉβπ) β ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ)))) |
32 | 21, 25, 31 | mpbir2and 712 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) = (πΉβπ)) |
33 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) = (πΉβπ
)) |
34 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β π β (πΌβπ)) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β π β (πΌβπ)) |
36 | 35 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β π β (πΌβπ)) |
37 | | fveecn 27893 |
. . . . . . . . . . . . . . 15
β’ ((π β (πΌβπ) β§ π β (1...π)) β (πβπ) β β) |
38 | 36, 37 | sylancom 589 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πβπ) β β) |
39 | | simpll3 1215 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β π β (πΌβπ)) |
40 | 39 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β π β (πΌβπ)) |
41 | 40 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β π β (πΌβπ)) |
42 | | fveecn 27893 |
. . . . . . . . . . . . . . 15
β’ ((π β (πΌβπ) β§ π β (1...π)) β (πβπ) β β) |
43 | 41, 42 | sylancom 589 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πβπ) β β) |
44 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β |
45 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ) β β) |
46 | | subcl 11405 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((1
β β β§ (πΉβπ) β β) β (1 β (πΉβπ)) β β) |
47 | 44, 45, 46 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (1 β (πΉβπ)) β β) |
48 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (πβπ) β β) |
49 | 47, 48 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β (πΉβπ)) Β· (πβπ)) β β) |
50 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉβπ) β β β§ (πβπ) β β) β ((πΉβπ) Β· (πβπ)) β β) |
51 | 50 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· (πβπ)) β β) |
52 | 49, 51 | addcld 11179 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β β) |
53 | 52 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (1 Β· (((1
β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) |
54 | 52 | mul02d 11358 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (0 Β· (((1
β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) = 0) |
55 | 53, 54 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 Β· (((1
β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) = ((((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) + 0)) |
56 | 52 | addid1d 11360 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) + 0) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) |
57 | 55, 56 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β β β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))))) |
58 | 57 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β β β§ ((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ
)) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))))) |
59 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) = (πΉβπ) β (1 β (πΉβπ)) = (1 β (πΉβπ))) |
60 | 59 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = (πΉβπ) β ((1 β (πΉβπ)) Β· (πβπ)) = ((1 β (πΉβπ)) Β· (πβπ))) |
61 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = (πΉβπ) β ((πΉβπ) Β· (πβπ)) = ((πΉβπ) Β· (πβπ))) |
62 | 60, 61 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) = (πΉβπ) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) |
63 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉβπ) = (πΉβπ
) β (1 β (πΉβπ)) = (1 β (πΉβπ
))) |
64 | 63 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβπ) = (πΉβπ
) β ((1 β (πΉβπ)) Β· (πβπ)) = ((1 β (πΉβπ
)) Β· (πβπ))) |
65 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβπ) = (πΉβπ
) β ((πΉβπ) Β· (πβπ)) = ((πΉβπ
) Β· (πβπ))) |
66 | 64, 65 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) = (πΉβπ
) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) |
67 | 66 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = (πΉβπ
) β (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) = (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) |
68 | 67 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) = (πΉβπ
) β ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
69 | 62, 68 | eqeqan12d 2747 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ
)) β ((((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
70 | 69 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β β β§ ((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ
)) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
71 | 58, 70 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ ((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ
)) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
72 | 19, 32, 33, 38, 43, 71 | syl122anc 1380 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
73 | 72 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
74 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = 0 β (1 β π‘) = (1 β
0)) |
75 | | 1m0e1 12279 |
. . . . . . . . . . . . . . . . . 18
β’ (1
β 0) = 1 |
76 | 74, 75 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = 0 β (1 β π‘) = 1) |
77 | 76 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = 0 β ((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) = (1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) |
78 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = 0 β (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) = (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) |
79 | 77, 78 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
β’ (π‘ = 0 β (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
80 | 79 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π‘ = 0 β ((((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
81 | 80 | ralbidv 3171 |
. . . . . . . . . . . . 13
β’ (π‘ = 0 β (βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
82 | 81 | rspcev 3580 |
. . . . . . . . . . . 12
β’ ((0
β (0[,]1) β§ βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = ((1 Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (0 Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
83 | 13, 73, 82 | sylancr 588 |
. . . . . . . . . . 11
β’ (((πΉβπ) = (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
84 | 83 | ex 414 |
. . . . . . . . . 10
β’ ((πΉβπ) = (πΉβπ
) β (((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
85 | 26 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β (0[,)+β)) |
86 | 85, 29 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β β) |
87 | | simplr3 1218 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β (πΉβπ
) β (0[,)+β)) |
88 | 87 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ
) β (0[,)+β)) |
89 | | elrege0 13377 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ
) β (0[,)+β) β ((πΉβπ
) β β β§ 0 β€ (πΉβπ
))) |
90 | 89 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ
) β (0[,)+β) β (πΉβπ
) β β) |
91 | 88, 90 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ
) β β) |
92 | 14 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β (0[,)+β)) |
93 | 92, 17 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β β) |
94 | | simprrr 781 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β€ (πΉβπ
)) |
95 | 86, 91, 93, 94 | lesub1dd 11776 |
. . . . . . . . . . . . 13
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β ((πΉβπ) β (πΉβπ)) β€ ((πΉβπ
) β (πΉβπ))) |
96 | 86, 93 | resubcld 11588 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β ((πΉβπ) β (πΉβπ)) β β) |
97 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β€ (πΉβπ)) |
98 | 86, 93 | subge0d 11750 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (0 β€ ((πΉβπ) β (πΉβπ)) β (πΉβπ) β€ (πΉβπ))) |
99 | 97, 98 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β 0 β€ ((πΉβπ) β (πΉβπ))) |
100 | 91, 93 | resubcld 11588 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β ((πΉβπ
) β (πΉβπ)) β β) |
101 | 93, 86, 91, 97, 94 | letrd 11317 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β€ (πΉβπ
)) |
102 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) β (πΉβπ
)) |
103 | 102 | necomd 2996 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ
) β (πΉβπ)) |
104 | 93, 91, 101, 103 | leneltd 11314 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (πΉβπ) < (πΉβπ
)) |
105 | 93, 91 | posdifd 11747 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β ((πΉβπ) < (πΉβπ
) β 0 < ((πΉβπ
) β (πΉβπ)))) |
106 | 104, 105 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β 0 < ((πΉβπ
) β (πΉβπ))) |
107 | | divelunit 13417 |
. . . . . . . . . . . . . 14
β’
(((((πΉβπ) β (πΉβπ)) β β β§ 0 β€ ((πΉβπ) β (πΉβπ))) β§ (((πΉβπ
) β (πΉβπ)) β β β§ 0 < ((πΉβπ
) β (πΉβπ)))) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (0[,]1) β ((πΉβπ) β (πΉβπ)) β€ ((πΉβπ
) β (πΉβπ)))) |
108 | 96, 99, 100, 106, 107 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (0[,]1) β ((πΉβπ) β (πΉβπ)) β€ ((πΉβπ
) β (πΉβπ)))) |
109 | 95, 108 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (0[,]1)) |
110 | 14 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β (0[,)+β)) |
111 | 17 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β (0[,)+β) β (πΉβπ) β β) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β β) |
113 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β (πΉβπ
)) |
114 | 26 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β (0[,)+β)) |
115 | 29 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β (0[,)+β) β (πΉβπ) β β) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ) β β) |
117 | 87 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ
) β (0[,)+β)) |
118 | 90 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ
) β (0[,)+β) β (πΉβπ
) β β) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πΉβπ
) β β) |
120 | 34 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β π β (πΌβπ)) |
121 | 120, 37 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πβπ) β β) |
122 | 39 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β π β (πΌβπ)) |
123 | 122, 42 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (πβπ) β β) |
124 | | simp2r 1201 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ
) β β) |
125 | | simp2l 1200 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ) β β) |
126 | 124, 125 | subcld 11517 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ
) β (πΉβπ)) β β) |
127 | | simp1l 1198 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ) β β) |
128 | 44, 127, 46 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (1 β (πΉβπ)) β β) |
129 | 126, 128 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) β β) |
130 | 125, 127 | subcld 11517 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) β (πΉβπ)) β β) |
131 | | subcl 11405 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((1
β β β§ (πΉβπ
) β β) β (1 β (πΉβπ
)) β β) |
132 | 44, 124, 131 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (1 β (πΉβπ
)) β β) |
133 | 130, 132 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) β β) |
134 | 124, 127 | subcld 11517 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ
) β (πΉβπ)) β β) |
135 | | simp1r 1199 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ) β (πΉβπ
)) |
136 | 135 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ
) β (πΉβπ)) |
137 | 124, 127,
136 | subne0d 11526 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ
) β (πΉβπ)) β 0) |
138 | 129, 133,
134, 137 | divdird 11974 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))) / ((πΉβπ
) β (πΉβπ))) = (((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) / ((πΉβπ
) β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) / ((πΉβπ
) β (πΉβπ))))) |
139 | 134 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· 1) = ((πΉβπ
) β (πΉβπ))) |
140 | 134, 125 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) = ((πΉβπ) Β· ((πΉβπ
) β (πΉβπ)))) |
141 | 125, 124,
127 | subdid 11616 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· ((πΉβπ
) β (πΉβπ))) = (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) |
142 | 140, 141 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) = (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) |
143 | 139, 142 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ))) = (((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))))) |
144 | | subdi 11593 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ
) β (πΉβπ)) β β β§ 1 β β
β§ (πΉβπ) β β) β
(((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)))) |
145 | 44, 144 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ
) β (πΉβπ)) β β β§ (πΉβπ) β β) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)))) |
146 | 134, 125,
145 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)))) |
147 | | subdi 11593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉβπ
) β (πΉβπ)) β β β§ 1 β β
β§ (πΉβπ) β β) β
(((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)))) |
148 | 44, 147 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ
) β (πΉβπ)) β β β§ (πΉβπ) β β) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)))) |
149 | 126, 127,
148 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)))) |
150 | 126 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· 1) = ((πΉβπ
) β (πΉβπ))) |
151 | 124, 125,
127 | subdird 11617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) = (((πΉβπ
) Β· (πΉβπ)) β ((πΉβπ) Β· (πΉβπ)))) |
152 | 124, 127 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ
) Β· (πΉβπ)) = ((πΉβπ) Β· (πΉβπ
))) |
153 | 152 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) Β· (πΉβπ)) β ((πΉβπ) Β· (πΉβπ))) = (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) |
154 | 151, 153 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) = (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) |
155 | 150, 154 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· 1) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ))) = (((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))))) |
156 | 149, 155 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = (((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))))) |
157 | | subdi 11593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉβπ) β (πΉβπ)) β β β§ 1 β β
β§ (πΉβπ
) β β) β
(((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) = ((((πΉβπ) β (πΉβπ)) Β· 1) β (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)))) |
158 | 44, 157 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ) β (πΉβπ)) β β β§ (πΉβπ
) β β) β (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) = ((((πΉβπ) β (πΉβπ)) Β· 1) β (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)))) |
159 | 130, 124,
158 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) = ((((πΉβπ) β (πΉβπ)) Β· 1) β (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)))) |
160 | 130 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) Β· 1) = ((πΉβπ) β (πΉβπ))) |
161 | 125, 127,
124 | subdird 11617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)) = (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
)))) |
162 | 160, 161 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) Β· 1) β (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))) = (((πΉβπ) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
))))) |
163 | 159, 162 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) = (((πΉβπ) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
))))) |
164 | 156, 163 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))) = ((((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) + (((πΉβπ) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
)))))) |
165 | 127, 124 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· (πΉβπ
)) β β) |
166 | 125, 127 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· (πΉβπ)) β β) |
167 | 165, 166 | subcld 11517 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))) β β) |
168 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉβπ) β β β§ (πΉβπ
) β β) β ((πΉβπ) Β· (πΉβπ
)) β β) |
169 | 168 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· (πΉβπ
)) β β) |
170 | 169, 165 | subcld 11517 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
))) β β) |
171 | 126, 130,
167, 170 | addsub4d 11564 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) + ((πΉβπ) β (πΉβπ))) β ((((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))) + (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
))))) = ((((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) + (((πΉβπ) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
)))))) |
172 | 124, 125,
127 | npncand 11541 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) + ((πΉβπ) β (πΉβπ))) = ((πΉβπ
) β (πΉβπ))) |
173 | 165, 166,
169 | npncan3d 11553 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))) + (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
)))) = (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ)))) |
174 | 172, 173 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) + ((πΉβπ) β (πΉβπ))) β ((((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))) + (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
))))) = (((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))))) |
175 | 164, 171,
174 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))) = (((πΉβπ
) β (πΉβπ)) β (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))))) |
176 | 143, 146,
175 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))))) |
177 | 129, 133 | addcld 11179 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))) β β) |
178 | | subcl 11405 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((1
β β β§ (πΉβπ) β β) β (1 β (πΉβπ)) β β) |
179 | 44, 125, 178 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (1 β (πΉβπ)) β β) |
180 | 177, 134,
179, 137 | divmuld 11958 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))) / ((πΉβπ
) β (πΉβπ))) = (1 β (πΉβπ)) β (((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))))) |
181 | 176, 180 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) + (((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
)))) / ((πΉβπ
) β (πΉβπ))) = (1 β (πΉβπ))) |
182 | 126, 128,
134, 137 | div23d 11973 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) / ((πΉβπ
) β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ)))) |
183 | 134, 130,
134, 137 | divsubdird 11975 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) β ((πΉβπ) β (πΉβπ))) / ((πΉβπ
) β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))))) |
184 | 124, 125,
127 | nnncan2d 11552 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) β ((πΉβπ) β (πΉβπ))) = ((πΉβπ
) β (πΉβπ))) |
185 | 184 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) β ((πΉβπ) β (πΉβπ))) / ((πΉβπ
) β (πΉβπ))) = (((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) |
186 | 134, 137 | dividd 11934 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) = 1) |
187 | 186 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) = (1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))))) |
188 | 183, 185,
187 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) = (1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))))) |
189 | 188 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ))) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ)))) |
190 | 182, 189 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) / ((πΉβπ
) β (πΉβπ))) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ)))) |
191 | 130, 132,
134, 137 | div23d 11973 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) / ((πΉβπ
) β (πΉβπ))) = ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
)))) |
192 | 190, 191 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ
) β (πΉβπ)) Β· (1 β (πΉβπ))) / ((πΉβπ
) β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) Β· (1 β (πΉβπ
))) / ((πΉβπ
) β (πΉβπ)))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
))))) |
193 | 138, 181,
192 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (1 β (πΉβπ)) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
))))) |
194 | 193 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β (πΉβπ)) Β· (πβπ)) = ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
)))) Β· (πβπ))) |
195 | 126, 127 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) β β) |
196 | 130, 124 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)) β β) |
197 | 195, 196,
134, 137 | divdird 11974 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))) / ((πΉβπ
) β (πΉβπ))) = (((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)) / ((πΉβπ
) β (πΉβπ))))) |
198 | 154, 161 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))) = ((((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ))) + (((πΉβπ) Β· (πΉβπ
)) β ((πΉβπ) Β· (πΉβπ
))))) |
199 | 173, 198,
142 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) = ((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)))) |
200 | 195, 196 | addcld 11179 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))) β β) |
201 | 200, 134,
125, 137 | divmuld 11958 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))) / ((πΉβπ
) β (πΉβπ))) = (πΉβπ) β (((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) = ((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))))) |
202 | 199, 201 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) + (((πΉβπ) β (πΉβπ)) Β· (πΉβπ
))) / ((πΉβπ
) β (πΉβπ))) = (πΉβπ)) |
203 | 126, 127,
134, 137 | div23d 11973 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) = ((((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ))) |
204 | 188 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ)) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ))) |
205 | 203, 204 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ))) |
206 | 130, 124,
134, 137 | div23d 11973 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)) / ((πΉβπ
) β (πΉβπ))) = ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
))) |
207 | 205, 206 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ
) β (πΉβπ)) Β· (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) Β· (πΉβπ
)) / ((πΉβπ
) β (πΉβπ)))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
)))) |
208 | 197, 202,
207 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πΉβπ) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
)))) |
209 | 208 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· (πβπ)) = ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
))) Β· (πβπ))) |
210 | 194, 209 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
)))) Β· (πβπ)) + ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
))) Β· (πβπ)))) |
211 | 130, 134,
137 | divcld 11936 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β β) |
212 | | subcl 11405 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1
β β β§ (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β β) β (1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) β β) |
213 | 44, 211, 212 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) β β) |
214 | | simp3l 1202 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πβπ) β β) |
215 | 128, 214 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β (πΉβπ)) Β· (πβπ)) β β) |
216 | 213, 215 | mulcld 11180 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) β β) |
217 | 132, 214 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β (πΉβπ
)) Β· (πβπ)) β β) |
218 | 211, 217 | mulcld 11180 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ))) β β) |
219 | | simp3r 1203 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (πβπ) β β) |
220 | 127, 219 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ) Β· (πβπ)) β β) |
221 | 213, 220 | mulcld 11180 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ))) β β) |
222 | 124, 219 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((πΉβπ
) Β· (πβπ)) β β) |
223 | 211, 222 | mulcld 11180 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ))) β β) |
224 | 216, 218,
221, 223 | add4d 11388 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ)))) + (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ))))) = ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ)))) + (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ)))))) |
225 | 213, 128 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) β β) |
226 | 211, 132 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
))) β β) |
227 | 213, 128,
214 | mulassd 11183 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) Β· (πβπ)) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ)))) |
228 | 211, 132,
214 | mulassd 11183 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
))) Β· (πβπ)) = ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ)))) |
229 | 227, 228 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) Β· (πβπ)) + (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
))) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ))))) |
230 | 225, 214,
226, 229 | joinlmuladdmuld 11187 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
)))) Β· (πβπ)) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ))))) |
231 | 213, 127 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) β β) |
232 | 211, 124 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
)) β β) |
233 | 213, 127,
219 | mulassd 11183 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) Β· (πβπ)) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ)))) |
234 | 211, 124,
219 | mulassd 11183 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
)) Β· (πβπ)) = ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ)))) |
235 | 233, 234 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) Β· (πβπ)) + (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
)) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ))))) |
236 | 231, 219,
232, 235 | joinlmuladdmuld 11187 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
))) Β· (πβπ)) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ))))) |
237 | 230, 236 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
)))) Β· (πβπ)) + ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
))) Β· (πβπ))) = ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ)))) + (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ)))))) |
238 | 213, 215,
220 | adddid 11184 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ))))) |
239 | 211, 217,
222 | adddid 11184 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) = (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ))))) |
240 | 238, 239 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) = ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((1 β (πΉβπ)) Β· (πβπ))) + ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· ((πΉβπ) Β· (πβπ)))) + (((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((1 β (πΉβπ
)) Β· (πβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· ((πΉβπ
) Β· (πβπ)))))) |
241 | 224, 237,
240 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . 15
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β
(((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) = (((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (1 β (πΉβπ))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (1 β (πΉβπ
)))) Β· (πβπ)) + ((((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (πΉβπ)) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (πΉβπ
))) Β· (πβπ)))) |
242 | 210, 241 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((((πΉβπ) β β β§ (πΉβπ) β (πΉβπ
)) β§ ((πΉβπ) β β β§ (πΉβπ
) β β) β§ ((πβπ) β β β§ (πβπ) β β)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
243 | 112, 113,
116, 119, 121, 123, 242 | syl222anc 1387 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β§ π β (1...π)) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
244 | 243 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
245 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (1 β π‘) = (1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))))) |
246 | 245 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β ((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) = ((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) |
247 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) = ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) |
248 | 246, 247 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
β’ (π‘ = (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
249 | 248 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π‘ = (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β ((((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
250 | 249 | ralbidv 3171 |
. . . . . . . . . . . . 13
β’ (π‘ = (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
251 | 250 | rspcev 3580 |
. . . . . . . . . . . 12
β’
(((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) β (0[,]1) β§ βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β (((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ)))) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + ((((πΉβπ) β (πΉβπ)) / ((πΉβπ
) β (πΉβπ))) Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
252 | 109, 244,
251 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((πΉβπ) β (πΉβπ
) β§ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
253 | 252 | ex 414 |
. . . . . . . . . 10
β’ ((πΉβπ) β (πΉβπ
) β (((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
254 | 84, 253 | pm2.61ine 3025 |
. . . . . . . . 9
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
255 | | r19.26-3 3112 |
. . . . . . . . . 10
β’
(βπ β
(1...π)((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β (βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) |
256 | | simp2 1138 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) |
257 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β ((1 β π‘) Β· (πβπ)) = ((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))))) |
258 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ ((π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))) β (π‘ Β· (π
βπ)) = (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) |
259 | 257, 258 | oveqan12d 7377 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
260 | 259 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) |
261 | 256, 260 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
β’ (((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β ((πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
262 | 261 | ralimi 3083 |
. . . . . . . . . . . . 13
β’
(βπ β
(1...π)((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β βπ β (1...π)((πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
263 | | ralbi 3103 |
. . . . . . . . . . . . 13
β’
(βπ β
(1...π)((πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) β (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))))) β (βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) β βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
264 | 262, 263 | syl 17 |
. . . . . . . . . . . 12
β’
(βπ β
(1...π)((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β (βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) β βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
265 | 264 | rexbidv 3172 |
. . . . . . . . . . 11
β’
(βπ β
(1...π)((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β (βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))) β βπ‘ β (0[,]1)βπ β (1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))))) |
266 | 265 | biimprcd 250 |
. . . . . . . . . 10
β’
(βπ‘ β
(0[,]1)βπ β
(1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β (βπ β (1...π)((πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ (π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
267 | 255, 266 | biimtrrid 242 |
. . . . . . . . 9
β’
(βπ‘ β
(0[,]1)βπ β
(1...π)(((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) = (((1 β π‘) Β· (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) + (π‘ Β· (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β ((βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
268 | 254, 267 | syl 17 |
. . . . . . . 8
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β ((βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
269 | 268 | an32s 651 |
. . . . . . 7
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β§ ((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β))) β
((βπ β
(1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ)))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
270 | 269 | expimpd 455 |
. . . . . 6
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β ((((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β)) β§
(βπ β
(1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
271 | 270 | adantlr 714 |
. . . . 5
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β ((((πΉβπ) β (0[,)+β) β§ (πΉβπ) β (0[,)+β) β§ (πΉβπ
) β (0[,)+β)) β§
(βπ β
(1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ))) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
272 | 12, 271 | biimtrid 241 |
. . . 4
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β ((((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ) β (0[,)+β) β§ βπ β (1...π)(πβπ) = (((1 β (πΉβπ)) Β· (πβπ)) + ((πΉβπ) Β· (πβπ)))) β§ ((πΉβπ
) β (0[,)+β) β§ βπ β (1...π)(π
βπ) = (((1 β (πΉβπ
)) Β· (πβπ)) + ((πΉβπ
) Β· (πβπ))))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
273 | 11, 272 | mpd 15 |
. . 3
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ)))) |
274 | | simpl1 1192 |
. . . . 5
β’ (((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β π β β) |
275 | 1 | ssrab3 4041 |
. . . . . . . 8
β’ π· β (πΌβπ) |
276 | 275 | sseli 3941 |
. . . . . . 7
β’ (π β π· β π β (πΌβπ)) |
277 | 275 | sseli 3941 |
. . . . . . 7
β’ (π β π· β π β (πΌβπ)) |
278 | 275 | sseli 3941 |
. . . . . . 7
β’ (π
β π· β π
β (πΌβπ)) |
279 | 276, 277,
278 | 3anim123i 1152 |
. . . . . 6
β’ ((π β π· β§ π β π· β§ π
β π·) β (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ))) |
280 | 279 | 3com12 1124 |
. . . . 5
β’ ((π β π· β§ π β π· β§ π
β π·) β (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ))) |
281 | | brbtwn 27890 |
. . . . . 6
β’ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β (π Btwn β¨π, π
β© β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
282 | 281 | adantl 483 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ))) β (π Btwn β¨π, π
β© β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
283 | 274, 280,
282 | syl2an 597 |
. . . 4
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β (π Btwn β¨π, π
β© β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
284 | 283 | adantr 482 |
. . 3
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β (π Btwn β¨π, π
β© β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (πβπ)) + (π‘ Β· (π
βπ))))) |
285 | 273, 284 | mpbird 257 |
. 2
β’
(((((π β
β β§ π β
(πΌβπ) β§
π β
(πΌβπ)) β§
π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β§ ((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
))) β π Btwn β¨π, π
β©) |
286 | 285 | ex 414 |
1
β’ ((((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ π β π) β§ (π β π· β§ π β π· β§ π
β π·)) β (((πΉβπ) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβπ
)) β π Btwn β¨π, π
β©)) |