Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ+ β πΉ:π΄βΆβ+) |
2 | | rpssre 12946 |
. . . . . . . . . . . . 13
β’
β+ β β |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ+ β
β+ β β) |
4 | 1, 3 | fssd 6706 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆβ+ β πΉ:π΄βΆβ) |
5 | 4 | 3ad2ant3 1135 |
. . . . . . . . . 10
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β πΉ:π΄βΆβ) |
6 | 5 | adantr 481 |
. . . . . . . . 9
β’ (((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β πΉ:π΄βΆβ) |
7 | 6 | ffvelcdmda 7055 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β (πΉβπ¦) β β) |
8 | | simplrr 776 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β π β β) |
9 | | simpl2 1192 |
. . . . . . . . . 10
β’ (((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β πΊ:π΄βΆβ+) |
10 | 9 | ffvelcdmda 7055 |
. . . . . . . . 9
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β (πΊβπ¦) β
β+) |
11 | 10 | rpregt0d 12987 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β ((πΊβπ¦) β β β§ 0 < (πΊβπ¦))) |
12 | 7, 8, 11 | 3jca 1128 |
. . . . . . 7
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β ((πΉβπ¦) β β β§ π β β β§ ((πΊβπ¦) β β β§ 0 < (πΊβπ¦)))) |
13 | | ledivmul2 12058 |
. . . . . . . 8
β’ (((πΉβπ¦) β β β§ π β β β§ ((πΊβπ¦) β β β§ 0 < (πΊβπ¦))) β (((πΉβπ¦) / (πΊβπ¦)) β€ π β (πΉβπ¦) β€ (π Β· (πΊβπ¦)))) |
14 | 13 | bicomd 222 |
. . . . . . 7
β’ (((πΉβπ¦) β β β§ π β β β§ ((πΊβπ¦) β β β§ 0 < (πΊβπ¦))) β ((πΉβπ¦) β€ (π Β· (πΊβπ¦)) β ((πΉβπ¦) / (πΊβπ¦)) β€ π)) |
15 | 12, 14 | syl 17 |
. . . . . 6
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β ((πΉβπ¦) β€ (π Β· (πΊβπ¦)) β ((πΉβπ¦) / (πΊβπ¦)) β€ π)) |
16 | | id 22 |
. . . . . . . . . . . . 13
β’ (πΊ:π΄βΆβ+ β πΊ:π΄βΆβ+) |
17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
β’ (πΊ:π΄βΆβ+ β
β+ β β) |
18 | 16, 17 | fssd 6706 |
. . . . . . . . . . . 12
β’ (πΊ:π΄βΆβ+ β πΊ:π΄βΆβ) |
19 | 18 | 3ad2ant2 1134 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β πΊ:π΄βΆβ) |
20 | | reex 11166 |
. . . . . . . . . . . . 13
β’ β
β V |
21 | 20 | ssex 5298 |
. . . . . . . . . . . 12
β’ (π΄ β β β π΄ β V) |
22 | 21 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β π΄ β V) |
23 | 5, 19, 22 | 3jca 1128 |
. . . . . . . . . 10
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β (πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β V)) |
24 | 23 | adantr 481 |
. . . . . . . . 9
β’ (((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β (πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β V)) |
25 | 24 | adantr 481 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β (πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β V)) |
26 | | ffun 6691 |
. . . . . . . . . . . . . . . 16
β’ (πΊ:π΄βΆβ+ β Fun πΊ) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β Fun
πΊ) |
28 | 21 | anim1ci 616 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β (πΊ:π΄βΆβ+ β§ π΄ β V)) |
29 | | fex 7196 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ:π΄βΆβ+ β§ π΄ β V) β πΊ β V) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β πΊ β V) |
31 | | 0red 11182 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β 0 β
β) |
32 | | frn 6695 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ:π΄βΆβ+ β ran πΊ β
β+) |
33 | | 0nrp 12974 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬ 0
β β+ |
34 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (ran
πΊ β
β+ β ran πΊ β
β+) |
35 | 34 | ssneld 3964 |
. . . . . . . . . . . . . . . . . . 19
β’ (ran
πΊ β
β+ β (Β¬ 0 β β+ β Β¬ 0
β ran πΊ)) |
36 | 33, 35 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
β’ (ran
πΊ β
β+ β Β¬ 0 β ran πΊ) |
37 | | df-nel 3046 |
. . . . . . . . . . . . . . . . . 18
β’ (0
β ran πΊ β Β¬
0 β ran πΊ) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (ran
πΊ β
β+ β 0 β ran πΊ) |
39 | 32, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (πΊ:π΄βΆβ+ β 0 β
ran πΊ) |
40 | 39 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β 0
β ran πΊ) |
41 | | suppdm 46744 |
. . . . . . . . . . . . . . 15
β’ (((Fun
πΊ β§ πΊ β V β§ 0 β β) β§ 0
β ran πΊ) β
(πΊ supp 0) = dom πΊ) |
42 | 27, 30, 31, 40, 41 | syl31anc 1373 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β (πΊ supp 0) = dom πΊ) |
43 | | fdm 6697 |
. . . . . . . . . . . . . . 15
β’ (πΊ:π΄βΆβ+ β dom πΊ = π΄) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β dom
πΊ = π΄) |
45 | 42, 44 | eqtrd 2771 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ πΊ:π΄βΆβ+) β (πΊ supp 0) = π΄) |
46 | 45 | 3adant3 1132 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β (πΊ supp 0) = π΄) |
47 | 46 | eqcomd 2737 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β π΄ = (πΊ supp 0)) |
48 | 47 | adantr 481 |
. . . . . . . . . 10
β’ (((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β π΄ = (πΊ supp 0)) |
49 | 48 | eleq2d 2818 |
. . . . . . . . 9
β’ (((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β (π¦ β π΄ β π¦ β (πΊ supp 0))) |
50 | 49 | biimpa 477 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β π¦ β (πΊ supp 0)) |
51 | | refdivmptfv 46785 |
. . . . . . . 8
β’ (((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β V) β§ π¦ β (πΊ supp 0)) β ((πΉ /f πΊ)βπ¦) = ((πΉβπ¦) / (πΊβπ¦))) |
52 | 25, 50, 51 | syl2anc 584 |
. . . . . . 7
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β ((πΉ /f πΊ)βπ¦) = ((πΉβπ¦) / (πΊβπ¦))) |
53 | 52 | breq1d 5135 |
. . . . . 6
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β (((πΉ /f πΊ)βπ¦) β€ π β ((πΉβπ¦) / (πΊβπ¦)) β€ π)) |
54 | 15, 53 | bitr4d 281 |
. . . . 5
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β ((πΉβπ¦) β€ (π Β· (πΊβπ¦)) β ((πΉ /f πΊ)βπ¦) β€ π)) |
55 | 54 | imbi2d 340 |
. . . 4
β’ ((((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β§ π¦ β π΄) β ((π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))) β (π₯ β€ π¦ β ((πΉ /f πΊ)βπ¦) β€ π))) |
56 | 55 | ralbidva 3174 |
. . 3
β’ (((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β§ (π₯ β β β§ π β β)) β
(βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))) β βπ¦ β π΄ (π₯ β€ π¦ β ((πΉ /f πΊ)βπ¦) β€ π))) |
57 | 56 | 2rexbidva 3216 |
. 2
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β
(βπ₯ β β
βπ β β
βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β ((πΉ /f πΊ)βπ¦) β€ π))) |
58 | | simp1 1136 |
. . 3
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β π΄ β
β) |
59 | | ssidd 3985 |
. . 3
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β π΄ β π΄) |
60 | | elbigo2 46791 |
. . 3
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΄βΆβ β§ π΄ β π΄)) β (πΉ β (ΞβπΊ) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
61 | 19, 58, 5, 59, 60 | syl22anc 837 |
. 2
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β (πΉ β (ΞβπΊ) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) |
62 | | refdivmptf 46781 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β V) β (πΉ /f πΊ):(πΊ supp 0)βΆβ) |
63 | 23, 62 | syl 17 |
. . . 4
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β (πΉ /f πΊ):(πΊ supp 0)βΆβ) |
64 | 47 | feq2d 6674 |
. . . 4
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β ((πΉ /f πΊ):π΄βΆβ β (πΉ /f πΊ):(πΊ supp 0)βΆβ)) |
65 | 63, 64 | mpbird 256 |
. . 3
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β (πΉ /f πΊ):π΄βΆβ) |
66 | | ello12 15425 |
. . 3
β’ (((πΉ /f πΊ):π΄βΆβ β§ π΄ β β) β ((πΉ /f πΊ) β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β π΄ (π₯ β€ π¦ β ((πΉ /f πΊ)βπ¦) β€ π))) |
67 | 65, 58, 66 | syl2anc 584 |
. 2
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β ((πΉ /f πΊ) β β€π(1) β
βπ₯ β β
βπ β β
βπ¦ β π΄ (π₯ β€ π¦ β ((πΉ /f πΊ)βπ¦) β€ π))) |
68 | 57, 61, 67 | 3bitr4d 310 |
1
β’ ((π΄ β β β§ πΊ:π΄βΆβ+ β§ πΉ:π΄βΆβ+) β (πΉ β (ΞβπΊ) β (πΉ /f πΊ) β β€π(1))) |