Step | Hyp | Ref
| Expression |
1 | | o1cxp.4 |
. . 3
β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) |
2 | | o1f 15473 |
. . . . 5
β’ ((π₯ β π΄ β¦ π΅) β π(1) β (π₯ β π΄ β¦ π΅):dom (π₯ β π΄ β¦ π΅)βΆβ) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β (π₯ β π΄ β¦ π΅):dom (π₯ β π΄ β¦ π΅)βΆβ) |
4 | | o1cxp.3 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β π΅ β π) |
5 | 4 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ₯ β π΄ π΅ β π) |
6 | | dmmptg 6242 |
. . . . . 6
β’
(βπ₯ β
π΄ π΅ β π β dom (π₯ β π΄ β¦ π΅) = π΄) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β dom (π₯ β π΄ β¦ π΅) = π΄) |
8 | 7 | feq2d 6704 |
. . . 4
β’ (π β ((π₯ β π΄ β¦ π΅):dom (π₯ β π΄ β¦ π΅)βΆβ β (π₯ β π΄ β¦ π΅):π΄βΆβ)) |
9 | 3, 8 | mpbid 231 |
. . 3
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
10 | | o1bdd 15475 |
. . 3
β’ (((π₯ β π΄ β¦ π΅) β π(1) β§ (π₯ β π΄ β¦ π΅):π΄βΆβ) β βπ¦ β β βπ β β βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) |
11 | 1, 9, 10 | syl2anc 585 |
. 2
β’ (π β βπ¦ β β βπ β β βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) |
12 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
13 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
14 | 13 | fvmpt2 7010 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π΄ β§ π΅ β π) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
15 | 12, 4, 14 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
16 | 15 | oveq1d 7424 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = (π΅βππΆ)) |
17 | | ovex 7442 |
. . . . . . . . . . . . . . 15
β’ (π΅βππΆ) β V |
18 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π΄ β¦ (π΅βππΆ)) = (π₯ β π΄ β¦ (π΅βππΆ)) |
19 | 18 | fvmpt2 7010 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π΄ β§ (π΅βππΆ) β V) β ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯) = (π΅βππΆ)) |
20 | 12, 17, 19 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯) = (π΅βππΆ)) |
21 | 16, 20 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯)) |
22 | 21 | ralrimiva 3147 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π΄ (((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯)) |
23 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π§(((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯) |
24 | | nffvmpt1 6903 |
. . . . . . . . . . . . . . 15
β’
β²π₯((π₯ β π΄ β¦ π΅)βπ§) |
25 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π₯βπ |
26 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π₯πΆ |
27 | 24, 25, 26 | nfov 7439 |
. . . . . . . . . . . . . 14
β’
β²π₯(((π₯ β π΄ β¦ π΅)βπ§)βππΆ) |
28 | | nffvmpt1 6903 |
. . . . . . . . . . . . . 14
β’
β²π₯((π₯ β π΄ β¦ (π΅βππΆ))βπ§) |
29 | 27, 28 | nfeq 2917 |
. . . . . . . . . . . . 13
β’
β²π₯(((π₯ β π΄ β¦ π΅)βπ§)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§) |
30 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β ((π₯ β π΄ β¦ π΅)βπ₯) = ((π₯ β π΄ β¦ π΅)βπ§)) |
31 | 30 | oveq1d 7424 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = (((π₯ β π΄ β¦ π΅)βπ§)βππΆ)) |
32 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) |
33 | 31, 32 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β ((((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯) β (((π₯ β π΄ β¦ π΅)βπ§)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§))) |
34 | 23, 29, 33 | cbvralw 3304 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π΄ (((π₯ β π΄ β¦ π΅)βπ₯)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ₯) β βπ§ β π΄ (((π₯ β π΄ β¦ π΅)βπ§)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) |
35 | 22, 34 | sylib 217 |
. . . . . . . . . . 11
β’ (π β βπ§ β π΄ (((π₯ β π΄ β¦ π΅)βπ§)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) |
36 | 35 | r19.21bi 3249 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (((π₯ β π΄ β¦ π΅)βπ§)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) |
37 | 36 | ad2ant2r 746 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (((π₯ β π΄ β¦ π΅)βπ§)βππΆ) = ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) |
38 | 37 | fveq2d 6896 |
. . . . . . . 8
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (absβ(((π₯ β π΄ β¦ π΅)βπ§)βππΆ)) = (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§))) |
39 | 9 | ffvelcdmda 7087 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β ((π₯ β π΄ β¦ π΅)βπ§) β β) |
40 | 39 | ad2ant2r 746 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β ((π₯ β π΄ β¦ π΅)βπ§) β β) |
41 | | o1cxp.1 |
. . . . . . . . . 10
β’ (π β πΆ β β) |
42 | 41 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β πΆ β β) |
43 | | o1cxp.2 |
. . . . . . . . . 10
β’ (π β 0 β€ (ββπΆ)) |
44 | 43 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β 0 β€ (ββπΆ)) |
45 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β β β§ π β β)) β π β β) |
46 | | 0re 11216 |
. . . . . . . . . . 11
β’ 0 β
β |
47 | | ifcl 4574 |
. . . . . . . . . . 11
β’ ((π β β β§ 0 β
β) β if(0 β€ π, π, 0) β β) |
48 | 45, 46, 47 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β β β§ π β β)) β if(0 β€ π, π, 0) β β) |
49 | 48 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β if(0 β€ π, π, 0) β β) |
50 | 40 | abscld 15383 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β β) |
51 | 45 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β π β β) |
52 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π) |
53 | | max2 13166 |
. . . . . . . . . . . 12
β’ ((0
β β β§ π
β β) β π
β€ if(0 β€ π, π, 0)) |
54 | 46, 45, 53 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β β β§ π β β)) β π β€ if(0 β€ π, π, 0)) |
55 | 54 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β π β€ if(0 β€ π, π, 0)) |
56 | 50, 51, 49, 52, 55 | letrd 11371 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ if(0 β€ π, π, 0)) |
57 | 40, 42, 44, 49, 56 | abscxpbnd 26261 |
. . . . . . . 8
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (absβ(((π₯ β π΄ β¦ π΅)βπ§)βππΆ)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β·
Ο)))) |
58 | 38, 57 | eqbrtrrd 5173 |
. . . . . . 7
β’ (((π β§ (π¦ β β β§ π β β)) β§ (π§ β π΄ β§ (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π)) β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β·
Ο)))) |
59 | 58 | expr 458 |
. . . . . 6
β’ (((π β§ (π¦ β β β§ π β β)) β§ π§ β π΄) β ((absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β·
Ο))))) |
60 | 59 | imim2d 57 |
. . . . 5
β’ (((π β§ (π¦ β β β§ π β β)) β§ π§ β π΄) β ((π¦ β€ π§ β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π) β (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β·
Ο)))))) |
61 | 60 | ralimdva 3168 |
. . . 4
β’ ((π β§ (π¦ β β β§ π β β)) β (βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π) β βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β·
Ο)))))) |
62 | 4, 1 | o1mptrcl 15567 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β π΅ β β) |
63 | 41 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β πΆ β β) |
64 | 62, 63 | cxpcld 26216 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (π΅βππΆ) β β) |
65 | 64 | fmpttd 7115 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (π΅βππΆ)):π΄βΆβ) |
66 | 65 | adantr 482 |
. . . . 5
β’ ((π β§ (π¦ β β β§ π β β)) β (π₯ β π΄ β¦ (π΅βππΆ)):π΄βΆβ) |
67 | | o1dm 15474 |
. . . . . . . 8
β’ ((π₯ β π΄ β¦ π΅) β π(1) β dom (π₯ β π΄ β¦ π΅) β β) |
68 | 1, 67 | syl 17 |
. . . . . . 7
β’ (π β dom (π₯ β π΄ β¦ π΅) β β) |
69 | 7, 68 | eqsstrrd 4022 |
. . . . . 6
β’ (π β π΄ β β) |
70 | 69 | adantr 482 |
. . . . 5
β’ ((π β§ (π¦ β β β§ π β β)) β π΄ β β) |
71 | | simprl 770 |
. . . . 5
β’ ((π β§ (π¦ β β β§ π β β)) β π¦ β β) |
72 | | max1 13164 |
. . . . . . . 8
β’ ((0
β β β§ π
β β) β 0 β€ if(0 β€ π, π, 0)) |
73 | 46, 45, 72 | sylancr 588 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π β β)) β 0 β€ if(0 β€
π, π, 0)) |
74 | 41 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β β β§ π β β)) β πΆ β β) |
75 | 74 | recld 15141 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π β β)) β (ββπΆ) β
β) |
76 | 48, 73, 75 | recxpcld 26231 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ π β β)) β (if(0 β€ π, π,
0)βπ(ββπΆ)) β β) |
77 | 74 | abscld 15383 |
. . . . . . . 8
β’ ((π β§ (π¦ β β β§ π β β)) β (absβπΆ) β
β) |
78 | | pire 25968 |
. . . . . . . 8
β’ Ο
β β |
79 | | remulcl 11195 |
. . . . . . . 8
β’
(((absβπΆ)
β β β§ Ο β β) β ((absβπΆ) Β· Ο) β
β) |
80 | 77, 78, 79 | sylancl 587 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ π β β)) β ((absβπΆ) Β· Ο) β
β) |
81 | 80 | reefcld 16031 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ π β β)) β
(expβ((absβπΆ)
Β· Ο)) β β) |
82 | 76, 81 | remulcld 11244 |
. . . . 5
β’ ((π β§ (π¦ β β β§ π β β)) β ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β· Ο))) β
β) |
83 | | elo12r 15472 |
. . . . . 6
β’ ((((π₯ β π΄ β¦ (π΅βππΆ)):π΄βΆβ β§ π΄ β β) β§ (π¦ β β β§ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β· Ο))) β
β) β§ βπ§
β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β· Ο))))) β
(π₯ β π΄ β¦ (π΅βππΆ)) β π(1)) |
84 | 83 | 3expia 1122 |
. . . . 5
β’ ((((π₯ β π΄ β¦ (π΅βππΆ)):π΄βΆβ β§ π΄ β β) β§ (π¦ β β β§ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β· Ο))) β
β)) β (βπ§
β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β· Ο)))) β
(π₯ β π΄ β¦ (π΅βππΆ)) β π(1))) |
85 | 66, 70, 71, 82, 84 | syl22anc 838 |
. . . 4
β’ ((π β§ (π¦ β β β§ π β β)) β (βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ (π΅βππΆ))βπ§)) β€ ((if(0 β€ π, π,
0)βπ(ββπΆ)) Β· (expβ((absβπΆ) Β· Ο)))) β
(π₯ β π΄ β¦ (π΅βππΆ)) β π(1))) |
86 | 61, 85 | syld 47 |
. . 3
β’ ((π β§ (π¦ β β β§ π β β)) β (βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π) β (π₯ β π΄ β¦ (π΅βππΆ)) β π(1))) |
87 | 86 | rexlimdvva 3212 |
. 2
β’ (π β (βπ¦ β β βπ β β βπ§ β π΄ (π¦ β€ π§ β (absβ((π₯ β π΄ β¦ π΅)βπ§)) β€ π) β (π₯ β π΄ β¦ (π΅βππΆ)) β π(1))) |
88 | 11, 87 | mpd 15 |
1
β’ (π β (π₯ β π΄ β¦ (π΅βππΆ)) β π(1)) |