Step | Hyp | Ref
| Expression |
1 | | mulcncf.1 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) |
2 | | cncff 14103 |
. . . . . . 7
β’ ((π₯ β π β¦ π΄) β (πβcnββ) β (π₯ β π β¦ π΄):πβΆβ) |
3 | 1, 2 | syl 14 |
. . . . . 6
β’ (π β (π₯ β π β¦ π΄):πβΆβ) |
4 | | eqid 2177 |
. . . . . . 7
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
5 | 4 | fmpt 5668 |
. . . . . 6
β’
(βπ₯ β
π π΄ β β β (π₯ β π β¦ π΄):πβΆβ) |
6 | 3, 5 | sylibr 134 |
. . . . 5
β’ (π β βπ₯ β π π΄ β β) |
7 | 6 | r19.21bi 2565 |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β β) |
8 | | mulcncf.2 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) |
9 | | cncff 14103 |
. . . . . . 7
β’ ((π₯ β π β¦ π΅) β (πβcnββ) β (π₯ β π β¦ π΅):πβΆβ) |
10 | 8, 9 | syl 14 |
. . . . . 6
β’ (π β (π₯ β π β¦ π΅):πβΆβ) |
11 | | eqid 2177 |
. . . . . . 7
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
12 | 11 | fmpt 5668 |
. . . . . 6
β’
(βπ₯ β
π π΅ β β β (π₯ β π β¦ π΅):πβΆβ) |
13 | 10, 12 | sylibr 134 |
. . . . 5
β’ (π β βπ₯ β π π΅ β β) |
14 | 13 | r19.21bi 2565 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β β) |
15 | 7, 14 | mulcld 7980 |
. . 3
β’ ((π β§ π₯ β π) β (π΄ Β· π΅) β β) |
16 | 15 | fmpttd 5673 |
. 2
β’ (π β (π₯ β π β¦ (π΄ Β· π΅)):πβΆβ) |
17 | | simpr 110 |
. . . . . 6
β’ (((π β§ π£ β π) β§ π β β+) β π β
β+) |
18 | | simplr 528 |
. . . . . . 7
β’ (((π β§ π£ β π) β§ π β β+) β π£ β π) |
19 | 6 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ π£ β π) β§ π β β+) β
βπ₯ β π π΄ β β) |
20 | | rspcsbela 3118 |
. . . . . . 7
β’ ((π£ β π β§ βπ₯ β π π΄ β β) β β¦π£ / π₯β¦π΄ β β) |
21 | 18, 19, 20 | syl2anc 411 |
. . . . . 6
β’ (((π β§ π£ β π) β§ π β β+) β
β¦π£ / π₯β¦π΄ β β) |
22 | 13 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ π£ β π) β§ π β β+) β
βπ₯ β π π΅ β β) |
23 | | rspcsbela 3118 |
. . . . . . 7
β’ ((π£ β π β§ βπ₯ β π π΅ β β) β β¦π£ / π₯β¦π΅ β β) |
24 | 18, 22, 23 | syl2anc 411 |
. . . . . 6
β’ (((π β§ π£ β π) β§ π β β+) β
β¦π£ / π₯β¦π΅ β β) |
25 | | mulcn2 11322 |
. . . . . 6
β’ ((π β β+
β§ β¦π£ /
π₯β¦π΄ β β β§
β¦π£ / π₯β¦π΅ β β) β βπ β β+
βπ β
β+ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
26 | 17, 21, 24, 25 | syl3anc 1238 |
. . . . 5
β’ (((π β§ π£ β π) β§ π β β+) β
βπ β
β+ βπ β β+ βπ β β βπ β β
(((absβ(π β
β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
27 | 1 | ad3antrrr 492 |
. . . . . . . 8
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β (π₯ β π β¦ π΄) β (πβcnββ)) |
28 | | simpr 110 |
. . . . . . . . 9
β’ ((π β§ π£ β π) β π£ β π) |
29 | 28 | ad2antrr 488 |
. . . . . . . 8
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β π£ β π) |
30 | | simprl 529 |
. . . . . . . 8
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β π β β+) |
31 | | cncfi 14104 |
. . . . . . . 8
β’ (((π₯ β π β¦ π΄) β (πβcnββ) β§ π£ β π β§ π β β+) β
βπ β
β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π)) |
32 | 27, 29, 30, 31 | syl3anc 1238 |
. . . . . . 7
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β βπ β β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π)) |
33 | 8 | ad3antrrr 492 |
. . . . . . . . . 10
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β (π₯ β π β¦ π΅) β (πβcnββ)) |
34 | | simprr 531 |
. . . . . . . . . 10
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β π β β+) |
35 | | cncfi 14104 |
. . . . . . . . . 10
β’ (((π₯ β π β¦ π΅) β (πβcnββ) β§ π£ β π β§ π β β+) β
βπ‘ β
β+ βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π)) |
36 | 33, 29, 34, 35 | syl3anc 1238 |
. . . . . . . . 9
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β βπ‘ β β+ βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π)) |
37 | 36 | adantr 276 |
. . . . . . . 8
β’
(((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β βπ‘ β β+ βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π)) |
38 | 27 | ad3antrrr 492 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β (π₯ β π β¦ π΄) β (πβcnββ)) |
39 | 33 | ad3antrrr 492 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β (π₯ β π β¦ π΅) β (πβcnββ)) |
40 | 29 | ad3antrrr 492 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β π£ β π) |
41 | | simp-5r 544 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β π β β+) |
42 | 30 | ad3antrrr 492 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β π β β+) |
43 | 34 | ad3antrrr 492 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β π β β+) |
44 | | simprl 529 |
. . . . . . . . . . 11
β’
(((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β π β β+) |
45 | 44 | ad2antrr 488 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β π β β+) |
46 | | simplrl 535 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β π‘ β β+) |
47 | | simprr 531 |
. . . . . . . . . . 11
β’
(((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π)) |
48 | 47 | ad2antrr 488 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π)) |
49 | | simplrr 536 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π)) |
50 | | nfv 1528 |
. . . . . . . . . . . . . 14
β’
β²π’(((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) |
51 | | nfv 1528 |
. . . . . . . . . . . . . . 15
β’
β²π’ π β
β+ |
52 | | nfra1 2508 |
. . . . . . . . . . . . . . 15
β’
β²π’βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π) |
53 | 51, 52 | nfan 1565 |
. . . . . . . . . . . . . 14
β’
β²π’(π β β+
β§ βπ’ β
π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π)) |
54 | 50, 53 | nfan 1565 |
. . . . . . . . . . . . 13
β’
β²π’((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) |
55 | | nfv 1528 |
. . . . . . . . . . . . . 14
β’
β²π’ π‘ β
β+ |
56 | | nfra1 2508 |
. . . . . . . . . . . . . 14
β’
β²π’βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π) |
57 | 55, 56 | nfan 1565 |
. . . . . . . . . . . . 13
β’
β²π’(π‘ β β+
β§ βπ’ β
π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π)) |
58 | 54, 57 | nfan 1565 |
. . . . . . . . . . . 12
β’
β²π’(((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) |
59 | | nfv 1528 |
. . . . . . . . . . . 12
β’
β²π’βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) |
60 | 58, 59 | nfan 1565 |
. . . . . . . . . . 11
β’
β²π’((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
61 | | simpr 110 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β π’ β π) |
62 | 19 | ad5antr 496 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β βπ₯ β π π΄ β β) |
63 | | rspcsbela 3118 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ βπ₯ β π π΄ β β) β β¦π’ / π₯β¦π΄ β β) |
64 | 61, 62, 63 | syl2anc 411 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β β¦π’ / π₯β¦π΄ β β) |
65 | 22 | ad5antr 496 |
. . . . . . . . . . . . . 14
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β βπ₯ β π π΅ β β) |
66 | | rspcsbela 3118 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ βπ₯ β π π΅ β β) β β¦π’ / π₯β¦π΅ β β) |
67 | 61, 65, 66 | syl2anc 411 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β β¦π’ / π₯β¦π΅ β β) |
68 | | simplr 528 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
69 | | fvoveq1 5900 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¦π’ / π₯β¦π΄ β (absβ(π β β¦π£ / π₯β¦π΄)) = (absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄))) |
70 | 69 | breq1d 4015 |
. . . . . . . . . . . . . . . 16
β’ (π = β¦π’ / π₯β¦π΄ β ((absβ(π β β¦π£ / π₯β¦π΄)) < π β (absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π)) |
71 | 70 | anbi1d 465 |
. . . . . . . . . . . . . . 15
β’ (π = β¦π’ / π₯β¦π΄ β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β ((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π))) |
72 | | oveq1 5884 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¦π’ / π₯β¦π΄ β (π Β· π) = (β¦π’ / π₯β¦π΄ Β· π)) |
73 | 72 | fvoveq1d 5899 |
. . . . . . . . . . . . . . . 16
β’ (π = β¦π’ / π₯β¦π΄ β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) = (absβ((β¦π’ / π₯β¦π΄ Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅)))) |
74 | 73 | breq1d 4015 |
. . . . . . . . . . . . . . 15
β’ (π = β¦π’ / π₯β¦π΄ β ((absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π β (absβ((β¦π’ / π₯β¦π΄ Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
75 | 71, 74 | imbi12d 234 |
. . . . . . . . . . . . . 14
β’ (π = β¦π’ / π₯β¦π΄ β ((((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) β (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π))) |
76 | | fvoveq1 5900 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¦π’ / π₯β¦π΅ β (absβ(π β β¦π£ / π₯β¦π΅)) = (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅))) |
77 | 76 | breq1d 4015 |
. . . . . . . . . . . . . . . 16
β’ (π = β¦π’ / π₯β¦π΅ β ((absβ(π β β¦π£ / π₯β¦π΅)) < π β (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π)) |
78 | 77 | anbi2d 464 |
. . . . . . . . . . . . . . 15
β’ (π = β¦π’ / π₯β¦π΅ β (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β ((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π))) |
79 | | oveq2 5885 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¦π’ / π₯β¦π΅ β (β¦π’ / π₯β¦π΄ Β· π) = (β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅)) |
80 | 79 | fvoveq1d 5899 |
. . . . . . . . . . . . . . . 16
β’ (π = β¦π’ / π₯β¦π΅ β (absβ((β¦π’ / π₯β¦π΄ Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) = (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅)))) |
81 | 80 | breq1d 4015 |
. . . . . . . . . . . . . . 15
β’ (π = β¦π’ / π₯β¦π΅ β ((absβ((β¦π’ / π₯β¦π΄ Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
82 | 78, 81 | imbi12d 234 |
. . . . . . . . . . . . . 14
β’ (π = β¦π’ / π₯β¦π΅ β ((((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) β (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π))) |
83 | 75, 82 | rspc2va 2857 |
. . . . . . . . . . . . 13
β’
(((β¦π’
/ π₯β¦π΄ β β β§
β¦π’ / π₯β¦π΅ β β) β§ βπ β β βπ β β
(((absβ(π β
β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
84 | 64, 67, 68, 83 | syl21anc 1237 |
. . . . . . . . . . . 12
β’
((((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β§ π’ β π) β (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
85 | 84 | ex 115 |
. . . . . . . . . . 11
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β (π’ β π β (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π))) |
86 | 60, 85 | ralrimi 2548 |
. . . . . . . . . 10
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β βπ’ β π (((absβ(β¦π’ / π₯β¦π΄ β β¦π£ / π₯β¦π΄)) < π β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π£ / π₯β¦π΅)) < π) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) |
87 | 38, 39, 40, 41, 42, 43, 45, 46, 48, 49, 86 | mulcncflem 14129 |
. . . . . . . . 9
β’
(((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β§ βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π)) β βπ β β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π)) |
88 | 87 | ex 115 |
. . . . . . . 8
β’
((((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β§ (π‘ β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π‘ β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ£))) < π))) β (βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) β βπ β β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π))) |
89 | 37, 88 | rexlimddv 2599 |
. . . . . . 7
β’
(((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β§ (π β β+ β§
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ£))) < π))) β (βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) β βπ β β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π))) |
90 | 32, 89 | rexlimddv 2599 |
. . . . . 6
β’ ((((π β§ π£ β π) β§ π β β+) β§ (π β β+
β§ π β
β+)) β (βπ β β βπ β β (((absβ(π β β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) β βπ β β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π))) |
91 | 90 | rexlimdvva 2602 |
. . . . 5
β’ (((π β§ π£ β π) β§ π β β+) β
(βπ β
β+ βπ β β+ βπ β β βπ β β
(((absβ(π β
β¦π£ / π₯β¦π΄)) < π β§ (absβ(π β β¦π£ / π₯β¦π΅)) < π) β (absβ((π Β· π) β (β¦π£ / π₯β¦π΄ Β· β¦π£ / π₯β¦π΅))) < π) β βπ β β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π))) |
92 | 26, 91 | mpd 13 |
. . . 4
β’ (((π β§ π£ β π) β§ π β β+) β
βπ β
β+ βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π)) |
93 | 92 | ralrimiva 2550 |
. . 3
β’ ((π β§ π£ β π) β βπ β β+ βπ β β+
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π)) |
94 | 93 | ralrimiva 2550 |
. 2
β’ (π β βπ£ β π βπ β β+ βπ β β+
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π)) |
95 | | cncfrss 14101 |
. . . 4
β’ ((π₯ β π β¦ π΄) β (πβcnββ) β π β β) |
96 | 1, 95 | syl 14 |
. . 3
β’ (π β π β β) |
97 | | ssidd 3178 |
. . 3
β’ (π β β β
β) |
98 | | elcncf2 14100 |
. . 3
β’ ((π β β β§ β
β β) β ((π₯
β π β¦ (π΄ Β· π΅)) β (πβcnββ) β ((π₯ β π β¦ (π΄ Β· π΅)):πβΆβ β§ βπ£ β π βπ β β+ βπ β β+
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π)))) |
99 | 96, 97, 98 | syl2anc 411 |
. 2
β’ (π β ((π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ) β ((π₯ β π β¦ (π΄ Β· π΅)):πβΆβ β§ βπ£ β π βπ β β+ βπ β β+
βπ’ β π ((absβ(π’ β π£)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ£))) < π)))) |
100 | 16, 94, 99 | mpbir2and 944 |
1
β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ)) |