Step | Hyp | Ref
| Expression |
1 | | mulcncflem.s |
. . . . 5
β’ (π β π β
β+) |
2 | 1 | rpred 9698 |
. . . 4
β’ (π β π β β) |
3 | | mulcncflem.t |
. . . . 5
β’ (π β π β
β+) |
4 | 3 | rpred 9698 |
. . . 4
β’ (π β π β β) |
5 | | mincl 11241 |
. . . 4
β’ ((π β β β§ π β β) β
inf({π, π}, β, < ) β
β) |
6 | 2, 4, 5 | syl2anc 411 |
. . 3
β’ (π β inf({π, π}, β, < ) β
β) |
7 | 1 | rpgt0d 9701 |
. . . 4
β’ (π β 0 < π) |
8 | 3 | rpgt0d 9701 |
. . . 4
β’ (π β 0 < π) |
9 | | 0red 7960 |
. . . . 5
β’ (π β 0 β
β) |
10 | | ltmininf 11245 |
. . . . 5
β’ ((0
β β β§ π
β β β§ π
β β) β (0 < inf({π, π}, β, < ) β (0 < π β§ 0 < π))) |
11 | 9, 2, 4, 10 | syl3anc 1238 |
. . . 4
β’ (π β (0 < inf({π, π}, β, < ) β (0 < π β§ 0 < π))) |
12 | 7, 8, 11 | mpbir2and 944 |
. . 3
β’ (π β 0 < inf({π, π}, β, < )) |
13 | 6, 12 | elrpd 9695 |
. 2
β’ (π β inf({π, π}, β, < ) β
β+) |
14 | | simplr 528 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π§ β π) |
15 | | simpr 110 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π) β π§ β π) |
16 | | mulcncflem.a |
. . . . . . . . . . . . . . . . 17
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) |
17 | | cncff 14149 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β¦ π΄) β (πβcnββ) β (π₯ β π β¦ π΄):πβΆβ) |
18 | 16, 17 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ (π β (π₯ β π β¦ π΄):πβΆβ) |
19 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
20 | 19 | fmpt 5668 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯ β
π π΄ β β β (π₯ β π β¦ π΄):πβΆβ) |
21 | 18, 20 | sylibr 134 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β π π΄ β β) |
22 | | mulcncflem.b |
. . . . . . . . . . . . . . . . 17
β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) |
23 | | cncff 14149 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β¦ π΅) β (πβcnββ) β (π₯ β π β¦ π΅):πβΆβ) |
24 | 22, 23 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ (π β (π₯ β π β¦ π΅):πβΆβ) |
25 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
26 | 25 | fmpt 5668 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯ β
π π΅ β β β (π₯ β π β¦ π΅):πβΆβ) |
27 | 24, 26 | sylibr 134 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β π π΅ β β) |
28 | | r19.26 2603 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
π (π΄ β β β§ π΅ β β) β (βπ₯ β π π΄ β β β§ βπ₯ β π π΅ β β)) |
29 | 21, 27, 28 | sylanbrc 417 |
. . . . . . . . . . . . . 14
β’ (π β βπ₯ β π (π΄ β β β§ π΅ β β)) |
30 | | mulcl 7940 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β· π΅) β β) |
31 | 30 | ralimi 2540 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
π (π΄ β β β§ π΅ β β) β βπ₯ β π (π΄ Β· π΅) β β) |
32 | 29, 31 | syl 14 |
. . . . . . . . . . . . 13
β’ (π β βπ₯ β π (π΄ Β· π΅) β β) |
33 | 32 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π) β βπ₯ β π (π΄ Β· π΅) β β) |
34 | | rspcsbela 3118 |
. . . . . . . . . . . 12
β’ ((π§ β π β§ βπ₯ β π (π΄ Β· π΅) β β) β
β¦π§ / π₯β¦(π΄ Β· π΅) β β) |
35 | 15, 33, 34 | syl2anc 411 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π) β β¦π§ / π₯β¦(π΄ Β· π΅) β β) |
36 | 35 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
β¦π§ / π₯β¦(π΄ Β· π΅) β β) |
37 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π₯ β π β¦ (π΄ Β· π΅)) = (π₯ β π β¦ (π΄ Β· π΅)) |
38 | 37 | fvmpts 5596 |
. . . . . . . . . 10
β’ ((π§ β π β§ β¦π§ / π₯β¦(π΄ Β· π΅) β β) β ((π₯ β π β¦ (π΄ Β· π΅))βπ§) = β¦π§ / π₯β¦(π΄ Β· π΅)) |
39 | 14, 36, 38 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β ((π₯ β π β¦ (π΄ Β· π΅))βπ§) = β¦π§ / π₯β¦(π΄ Β· π΅)) |
40 | | csbov12g 5916 |
. . . . . . . . . 10
β’ (π§ β π β β¦π§ / π₯β¦(π΄ Β· π΅) = (β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅)) |
41 | 14, 40 | syl 14 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
β¦π§ / π₯β¦(π΄ Β· π΅) = (β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅)) |
42 | 39, 41 | eqtrd 2210 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β ((π₯ β π β¦ (π΄ Β· π΅))βπ§) = (β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅)) |
43 | | mulcncflem.v |
. . . . . . . . . . 11
β’ (π β π β π) |
44 | 43 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π β π) |
45 | | rspcsbela 3118 |
. . . . . . . . . . . 12
β’ ((π β π β§ βπ₯ β π (π΄ Β· π΅) β β) β
β¦π / π₯β¦(π΄ Β· π΅) β β) |
46 | 43, 32, 45 | syl2anc 411 |
. . . . . . . . . . 11
β’ (π β β¦π / π₯β¦(π΄ Β· π΅) β β) |
47 | 46 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
β¦π / π₯β¦(π΄ Β· π΅) β β) |
48 | 37 | fvmpts 5596 |
. . . . . . . . . 10
β’ ((π β π β§ β¦π / π₯β¦(π΄ Β· π΅) β β) β ((π₯ β π β¦ (π΄ Β· π΅))βπ) = β¦π / π₯β¦(π΄ Β· π΅)) |
49 | 44, 47, 48 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β ((π₯ β π β¦ (π΄ Β· π΅))βπ) = β¦π / π₯β¦(π΄ Β· π΅)) |
50 | | csbov12g 5916 |
. . . . . . . . . 10
β’ (π β π β β¦π / π₯β¦(π΄ Β· π΅) = (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅)) |
51 | 44, 50 | syl 14 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
β¦π / π₯β¦(π΄ Β· π΅) = (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅)) |
52 | 49, 51 | eqtrd 2210 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β ((π₯ β π β¦ (π΄ Β· π΅))βπ) = (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅)) |
53 | 42, 52 | oveq12d 5895 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β (((π₯ β π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ)) = ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) |
54 | 53 | fveq2d 5521 |
. . . . . 6
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) = (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅)))) |
55 | | simpr 110 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β (absβ(π§ β π)) < inf({π, π}, β, < )) |
56 | | cncfrss 14147 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β¦ π΄) β (πβcnββ) β π β β) |
57 | 16, 56 | syl 14 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
58 | 57 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π β β) |
59 | 58, 14 | sseldd 3158 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π§ β
β) |
60 | 57, 43 | sseldd 3158 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
61 | 60 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π β β) |
62 | 59, 61 | subcld 8270 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β (π§ β π) β β) |
63 | 62 | abscld 11192 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β (absβ(π§ β π)) β β) |
64 | 2 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π β β) |
65 | 4 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β π β β) |
66 | | ltmininf 11245 |
. . . . . . . . . 10
β’
(((absβ(π§
β π)) β β
β§ π β β
β§ π β β)
β ((absβ(π§
β π)) < inf({π, π}, β, < ) β ((absβ(π§ β π)) < π β§ (absβ(π§ β π)) < π))) |
67 | 63, 64, 65, 66 | syl3anc 1238 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
((absβ(π§ β
π)) < inf({π, π}, β, < ) β ((absβ(π§ β π)) < π β§ (absβ(π§ β π)) < π))) |
68 | 55, 67 | mpbid 147 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
((absβ(π§ β
π)) < π β§ (absβ(π§ β π)) < π)) |
69 | | mulcncflem.acn |
. . . . . . . . . . . . 13
β’ (π β βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ))) < πΉ)) |
70 | | fvoveq1 5900 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π§ β (absβ(π’ β π)) = (absβ(π§ β π))) |
71 | 70 | breq1d 4015 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β ((absβ(π’ β π)) < π β (absβ(π§ β π)) < π)) |
72 | 71 | imbrov2fvoveq 5902 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β (((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ))) < πΉ) β ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ))) < πΉ))) |
73 | 72 | cbvralv 2705 |
. . . . . . . . . . . . 13
β’
(βπ’ β
π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ))) < πΉ) β βπ§ β π ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ))) < πΉ)) |
74 | 69, 73 | sylib 122 |
. . . . . . . . . . . 12
β’ (π β βπ§ β π ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ))) < πΉ)) |
75 | 74 | r19.21bi 2565 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π) β ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ))) < πΉ)) |
76 | 21 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π) β βπ₯ β π π΄ β β) |
77 | | rspcsbela 3118 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β π β§ βπ₯ β π π΄ β β) β β¦π§ / π₯β¦π΄ β β) |
78 | 15, 76, 77 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π) β β¦π§ / π₯β¦π΄ β β) |
79 | 19 | fvmpts 5596 |
. . . . . . . . . . . . . . 15
β’ ((π§ β π β§ β¦π§ / π₯β¦π΄ β β) β ((π₯ β π β¦ π΄)βπ§) = β¦π§ / π₯β¦π΄) |
80 | 15, 78, 79 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π) β ((π₯ β π β¦ π΄)βπ§) = β¦π§ / π₯β¦π΄) |
81 | 43 | adantr 276 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π) β π β π) |
82 | | rspcsbela 3118 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ βπ₯ β π π΄ β β) β β¦π / π₯β¦π΄ β β) |
83 | 81, 76, 82 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π) β β¦π / π₯β¦π΄ β β) |
84 | 19 | fvmpts 5596 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ β¦π / π₯β¦π΄ β β) β ((π₯ β π β¦ π΄)βπ) = β¦π / π₯β¦π΄) |
85 | 81, 83, 84 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π) β ((π₯ β π β¦ π΄)βπ) = β¦π / π₯β¦π΄) |
86 | 80, 85 | oveq12d 5895 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π) β (((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ)) = (β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) |
87 | 86 | fveq2d 5521 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π) β (absβ(((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ))) = (absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄))) |
88 | 87 | breq1d 4015 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π) β ((absβ(((π₯ β π β¦ π΄)βπ§) β ((π₯ β π β¦ π΄)βπ))) < πΉ β (absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ)) |
89 | 75, 88 | sylibd 149 |
. . . . . . . . . 10
β’ ((π β§ π§ β π) β ((absβ(π§ β π)) < π β (absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ)) |
90 | | mulcncflem.bcn |
. . . . . . . . . . . . 13
β’ (π β βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ))) < πΊ)) |
91 | 70 | breq1d 4015 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β ((absβ(π’ β π)) < π β (absβ(π§ β π)) < π)) |
92 | 91 | imbrov2fvoveq 5902 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β (((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ))) < πΊ) β ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ))) < πΊ))) |
93 | 92 | cbvralv 2705 |
. . . . . . . . . . . . 13
β’
(βπ’ β
π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ))) < πΊ) β βπ§ β π ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ))) < πΊ)) |
94 | 90, 93 | sylib 122 |
. . . . . . . . . . . 12
β’ (π β βπ§ β π ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ))) < πΊ)) |
95 | 94 | r19.21bi 2565 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π) β ((absβ(π§ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ))) < πΊ)) |
96 | 27 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π) β βπ₯ β π π΅ β β) |
97 | | rspcsbela 3118 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β π β§ βπ₯ β π π΅ β β) β β¦π§ / π₯β¦π΅ β β) |
98 | 15, 96, 97 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π) β β¦π§ / π₯β¦π΅ β β) |
99 | 25 | fvmpts 5596 |
. . . . . . . . . . . . . . 15
β’ ((π§ β π β§ β¦π§ / π₯β¦π΅ β β) β ((π₯ β π β¦ π΅)βπ§) = β¦π§ / π₯β¦π΅) |
100 | 15, 98, 99 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π) β ((π₯ β π β¦ π΅)βπ§) = β¦π§ / π₯β¦π΅) |
101 | | rspcsbela 3118 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ βπ₯ β π π΅ β β) β β¦π / π₯β¦π΅ β β) |
102 | 81, 96, 101 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π) β β¦π / π₯β¦π΅ β β) |
103 | 25 | fvmpts 5596 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ β¦π / π₯β¦π΅ β β) β ((π₯ β π β¦ π΅)βπ) = β¦π / π₯β¦π΅) |
104 | 81, 102, 103 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π) β ((π₯ β π β¦ π΅)βπ) = β¦π / π₯β¦π΅) |
105 | 100, 104 | oveq12d 5895 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π) β (((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ)) = (β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) |
106 | 105 | fveq2d 5521 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π) β (absβ(((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ))) = (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅))) |
107 | 106 | breq1d 4015 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π) β ((absβ(((π₯ β π β¦ π΅)βπ§) β ((π₯ β π β¦ π΅)βπ))) < πΊ β (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ)) |
108 | 95, 107 | sylibd 149 |
. . . . . . . . . 10
β’ ((π β§ π§ β π) β ((absβ(π§ β π)) < π β (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ)) |
109 | 89, 108 | anim12d 335 |
. . . . . . . . 9
β’ ((π β§ π§ β π) β (((absβ(π§ β π)) < π β§ (absβ(π§ β π)) < π) β ((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ))) |
110 | 109 | adantr 276 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
(((absβ(π§ β
π)) < π β§ (absβ(π§ β π)) < π) β ((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ))) |
111 | 68, 110 | mpd 13 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ)) |
112 | | mulcncflem.cn |
. . . . . . . . . 10
β’ (π β βπ’ β π (((absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) |
113 | | csbeq1 3062 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β β¦π’ / π₯β¦π΄ = β¦π§ / π₯β¦π΄) |
114 | 113 | fvoveq1d 5899 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β (absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄))) |
115 | 114 | breq1d 4015 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β ((absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β (absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ)) |
116 | | csbeq1 3062 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β β¦π’ / π₯β¦π΅ = β¦π§ / π₯β¦π΅) |
117 | 116 | fvoveq1d 5899 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β (absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) = (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅))) |
118 | 117 | breq1d 4015 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β ((absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ β (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ)) |
119 | 115, 118 | anbi12d 473 |
. . . . . . . . . . . 12
β’ (π’ = π§ β (((absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β ((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ))) |
120 | 113, 116 | oveq12d 5895 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β (β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) = (β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅)) |
121 | 120 | fvoveq1d 5899 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) = (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅)))) |
122 | 121 | breq1d 4015 |
. . . . . . . . . . . 12
β’ (π’ = π§ β ((absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ β (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) |
123 | 119, 122 | imbi12d 234 |
. . . . . . . . . . 11
β’ (π’ = π§ β ((((absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ) β (((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ))) |
124 | 123 | cbvralv 2705 |
. . . . . . . . . 10
β’
(βπ’ β
π
(((absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ) β βπ§ β π (((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) |
125 | 112, 124 | sylib 122 |
. . . . . . . . 9
β’ (π β βπ§ β π (((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) |
126 | 125 | r19.21bi 2565 |
. . . . . . . 8
β’ ((π β§ π§ β π) β (((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) |
127 | 126 | adantr 276 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
(((absβ(β¦π§ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π§ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) |
128 | 111, 127 | mpd 13 |
. . . . . 6
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
(absβ((β¦π§ / π₯β¦π΄ Β· β¦π§ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ) |
129 | 54, 128 | eqbrtrd 4027 |
. . . . 5
β’ (((π β§ π§ β π) β§ (absβ(π§ β π)) < inf({π, π}, β, < )) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ) |
130 | 129 | ex 115 |
. . . 4
β’ ((π β§ π§ β π) β ((absβ(π§ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |
131 | 130 | ralrimiva 2550 |
. . 3
β’ (π β βπ§ β π ((absβ(π§ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |
132 | | fvoveq1 5900 |
. . . . . 6
β’ (π§ = π’ β (absβ(π§ β π)) = (absβ(π’ β π))) |
133 | 132 | breq1d 4015 |
. . . . 5
β’ (π§ = π’ β ((absβ(π§ β π)) < inf({π, π}, β, < ) β (absβ(π’ β π)) < inf({π, π}, β, < ))) |
134 | 133 | imbrov2fvoveq 5902 |
. . . 4
β’ (π§ = π’ β (((absβ(π§ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ) β ((absβ(π’ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ))) |
135 | 134 | cbvralv 2705 |
. . 3
β’
(βπ§ β
π ((absβ(π§ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ§) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ) β βπ’ β π ((absβ(π’ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |
136 | 131, 135 | sylib 122 |
. 2
β’ (π β βπ’ β π ((absβ(π’ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |
137 | | breq2 4009 |
. . 3
β’ (π = inf({π, π}, β, < ) β ((absβ(π’ β π)) < π β (absβ(π’ β π)) < inf({π, π}, β, < ))) |
138 | 137 | rspceaimv 2851 |
. 2
β’
((inf({π, π}, β, < ) β
β+ β§ βπ’ β π ((absβ(π’ β π)) < inf({π, π}, β, < ) β
(absβ(((π₯ β
π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) β βπ β β+ βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |
139 | 13, 136, 138 | syl2anc 411 |
1
β’ (π β βπ β β+ βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |