Step | Hyp | Ref
| Expression |
1 | | mulcl 11136 |
. . 3
β’ ((π΄ β β β§ π₯ β β) β (π΄ Β· π₯) β β) |
2 | | mulc1cncf.1 |
. . 3
β’ πΉ = (π₯ β β β¦ (π΄ Β· π₯)) |
3 | 1, 2 | fmptd 7063 |
. 2
β’ (π΄ β β β πΉ:ββΆβ) |
4 | | simprr 772 |
. . . . 5
β’ ((π΄ β β β§ (π¦ β β β§ π§ β β+))
β π§ β
β+) |
5 | | simpl 484 |
. . . . 5
β’ ((π΄ β β β§ (π¦ β β β§ π§ β β+))
β π΄ β
β) |
6 | | simprl 770 |
. . . . 5
β’ ((π΄ β β β§ (π¦ β β β§ π§ β β+))
β π¦ β
β) |
7 | | mulcn2 15479 |
. . . . 5
β’ ((π§ β β+
β§ π΄ β β
β§ π¦ β β)
β βπ‘ β
β+ βπ€ β β+ βπ£ β β βπ’ β β
(((absβ(π£ β
π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§)) |
8 | 4, 5, 6, 7 | syl3anc 1372 |
. . . 4
β’ ((π΄ β β β§ (π¦ β β β§ π§ β β+))
β βπ‘ β
β+ βπ€ β β+ βπ£ β β βπ’ β β
(((absβ(π£ β
π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§)) |
9 | | fvoveq1 7381 |
. . . . . . . . . . . . . 14
β’ (π£ = π΄ β (absβ(π£ β π΄)) = (absβ(π΄ β π΄))) |
10 | 9 | breq1d 5116 |
. . . . . . . . . . . . 13
β’ (π£ = π΄ β ((absβ(π£ β π΄)) < π‘ β (absβ(π΄ β π΄)) < π‘)) |
11 | 10 | anbi1d 631 |
. . . . . . . . . . . 12
β’ (π£ = π΄ β (((absβ(π£ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β ((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€))) |
12 | | oveq1 7365 |
. . . . . . . . . . . . . 14
β’ (π£ = π΄ β (π£ Β· π’) = (π΄ Β· π’)) |
13 | 12 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
β’ (π£ = π΄ β (absβ((π£ Β· π’) β (π΄ Β· π¦))) = (absβ((π΄ Β· π’) β (π΄ Β· π¦)))) |
14 | 13 | breq1d 5116 |
. . . . . . . . . . . 12
β’ (π£ = π΄ β ((absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§ β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§)) |
15 | 11, 14 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π£ = π΄ β ((((absβ(π£ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
16 | 15 | ralbidv 3175 |
. . . . . . . . . 10
β’ (π£ = π΄ β (βπ’ β β (((absβ(π£ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ’ β β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
17 | 16 | rspcv 3578 |
. . . . . . . . 9
β’ (π΄ β β β
(βπ£ β β
βπ’ β β
(((absβ(π£ β
π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ’ β β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
18 | 17 | ad2antrr 725 |
. . . . . . . 8
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ (π‘ β
β+ β§ π€
β β+)) β (βπ£ β β βπ’ β β (((absβ(π£ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ’ β β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
19 | | subid 11421 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β (π΄ β π΄) = 0) |
20 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (π΄ β π΄) = 0) |
21 | 20 | abs00bd 15177 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (absβ(π΄ β π΄)) = 0) |
22 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β π‘ β β+) |
23 | 22 | rpgt0d 12961 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β 0 < π‘) |
24 | 21, 23 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (absβ(π΄ β π΄)) < π‘) |
25 | 24 | biantrurd 534 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β ((absβ(π’ β π¦)) < π€ β ((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€))) |
26 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β π’ β β) |
27 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π’ β (π΄ Β· π₯) = (π΄ Β· π’)) |
28 | | ovex 7391 |
. . . . . . . . . . . . . . . 16
β’ (π΄ Β· π’) β V |
29 | 27, 2, 28 | fvmpt 6949 |
. . . . . . . . . . . . . . 15
β’ (π’ β β β (πΉβπ’) = (π΄ Β· π’)) |
30 | 26, 29 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (πΉβπ’) = (π΄ Β· π’)) |
31 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β π¦ β β) |
32 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (π΄ Β· π₯) = (π΄ Β· π¦)) |
33 | | ovex 7391 |
. . . . . . . . . . . . . . . 16
β’ (π΄ Β· π¦) β V |
34 | 32, 2, 33 | fvmpt 6949 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (πΉβπ¦) = (π΄ Β· π¦)) |
35 | 31, 34 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (πΉβπ¦) = (π΄ Β· π¦)) |
36 | 30, 35 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β ((πΉβπ’) β (πΉβπ¦)) = ((π΄ Β· π’) β (π΄ Β· π¦))) |
37 | 36 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (absβ((πΉβπ’) β (πΉβπ¦))) = (absβ((π΄ Β· π’) β (π΄ Β· π¦)))) |
38 | 37 | breq1d 5116 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β ((absβ((πΉβπ’) β (πΉβπ¦))) < π§ β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§)) |
39 | 25, 38 | imbi12d 345 |
. . . . . . . . . 10
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ ((π‘ β
β+ β§ π€
β β+) β§ π’ β β)) β (((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§) β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
40 | 39 | anassrs 469 |
. . . . . . . . 9
β’ ((((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ (π‘ β
β+ β§ π€
β β+)) β§ π’ β β) β (((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§) β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
41 | 40 | ralbidva 3173 |
. . . . . . . 8
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ (π‘ β
β+ β§ π€
β β+)) β (βπ’ β β ((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§) β βπ’ β β (((absβ(π΄ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π΄ Β· π’) β (π΄ Β· π¦))) < π§))) |
42 | 18, 41 | sylibrd 259 |
. . . . . . 7
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ (π‘ β
β+ β§ π€
β β+)) β (βπ£ β β βπ’ β β (((absβ(π£ β π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ’ β β ((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§))) |
43 | 42 | anassrs 469 |
. . . . . 6
β’ ((((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ π‘ β
β+) β§ π€ β β+) β
(βπ£ β β
βπ’ β β
(((absβ(π£ β
π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ’ β β ((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§))) |
44 | 43 | reximdva 3166 |
. . . . 5
β’ (((π΄ β β β§ (π¦ β β β§ π§ β β+))
β§ π‘ β
β+) β (βπ€ β β+ βπ£ β β βπ’ β β
(((absβ(π£ β
π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ€ β β+ βπ’ β β
((absβ(π’ β
π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§))) |
45 | 44 | rexlimdva 3153 |
. . . 4
β’ ((π΄ β β β§ (π¦ β β β§ π§ β β+))
β (βπ‘ β
β+ βπ€ β β+ βπ£ β β βπ’ β β
(((absβ(π£ β
π΄)) < π‘ β§ (absβ(π’ β π¦)) < π€) β (absβ((π£ Β· π’) β (π΄ Β· π¦))) < π§) β βπ€ β β+ βπ’ β β
((absβ(π’ β
π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§))) |
46 | 8, 45 | mpd 15 |
. . 3
β’ ((π΄ β β β§ (π¦ β β β§ π§ β β+))
β βπ€ β
β+ βπ’ β β ((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§)) |
47 | 46 | ralrimivva 3198 |
. 2
β’ (π΄ β β β
βπ¦ β β
βπ§ β
β+ βπ€ β β+ βπ’ β β
((absβ(π’ β
π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§)) |
48 | | ssid 3967 |
. . 3
β’ β
β β |
49 | | elcncf2 24256 |
. . 3
β’ ((β
β β β§ β β β) β (πΉ β (ββcnββ) β (πΉ:ββΆβ β§ βπ¦ β β βπ§ β β+
βπ€ β
β+ βπ’ β β ((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§)))) |
50 | 48, 48, 49 | mp2an 691 |
. 2
β’ (πΉ β (ββcnββ) β (πΉ:ββΆβ β§ βπ¦ β β βπ§ β β+
βπ€ β
β+ βπ’ β β ((absβ(π’ β π¦)) < π€ β (absβ((πΉβπ’) β (πΉβπ¦))) < π§))) |
51 | 3, 47, 50 | sylanbrc 584 |
1
β’ (π΄ β β β πΉ β (ββcnββ)) |