Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β π₯ β πΆ) |
2 | | efif1o.2 |
. . . . . . 7
β’ πΆ = (β‘abs β {1}) |
3 | 1, 2 | eleqtrdi 2844 |
. . . . . 6
β’ ((π β§ π₯ β πΆ) β π₯ β (β‘abs β {1})) |
4 | | absf 15228 |
. . . . . . 7
β’
abs:ββΆβ |
5 | | ffn 6669 |
. . . . . . 7
β’
(abs:ββΆβ β abs Fn β) |
6 | | fniniseg 7011 |
. . . . . . 7
β’ (abs Fn
β β (π₯ β
(β‘abs β {1}) β (π₯ β β β§
(absβπ₯) =
1))) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . 6
β’ (π₯ β (β‘abs β {1}) β (π₯ β β β§ (absβπ₯) = 1)) |
8 | 3, 7 | sylib 217 |
. . . . 5
β’ ((π β§ π₯ β πΆ) β (π₯ β β β§ (absβπ₯) = 1)) |
9 | 8 | simpld 496 |
. . . 4
β’ ((π β§ π₯ β πΆ) β π₯ β β) |
10 | 9 | sqrtcld 15328 |
. . 3
β’ ((π β§ π₯ β πΆ) β (ββπ₯) β β) |
11 | 10 | imcld 15086 |
. 2
β’ ((π β§ π₯ β πΆ) β (ββ(ββπ₯)) β
β) |
12 | | absimle 15200 |
. . . . . 6
β’
((ββπ₯)
β β β (absβ(ββ(ββπ₯))) β€
(absβ(ββπ₯))) |
13 | 10, 12 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β πΆ) β
(absβ(ββ(ββπ₯))) β€ (absβ(ββπ₯))) |
14 | 9 | sqsqrtd 15330 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β ((ββπ₯)β2) = π₯) |
15 | 14 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π₯ β πΆ) β (absβ((ββπ₯)β2)) = (absβπ₯)) |
16 | | 2nn0 12435 |
. . . . . . . . 9
β’ 2 β
β0 |
17 | | absexp 15195 |
. . . . . . . . 9
β’
(((ββπ₯)
β β β§ 2 β β0) β
(absβ((ββπ₯)β2)) = ((absβ(ββπ₯))β2)) |
18 | 10, 16, 17 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π₯ β πΆ) β (absβ((ββπ₯)β2)) =
((absβ(ββπ₯))β2)) |
19 | 8 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π₯ β πΆ) β (absβπ₯) = 1) |
20 | 15, 18, 19 | 3eqtr3d 2781 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β ((absβ(ββπ₯))β2) = 1) |
21 | | sq1 14105 |
. . . . . . 7
β’
(1β2) = 1 |
22 | 20, 21 | eqtr4di 2791 |
. . . . . 6
β’ ((π β§ π₯ β πΆ) β ((absβ(ββπ₯))β2) =
(1β2)) |
23 | 10 | abscld 15327 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β (absβ(ββπ₯)) β
β) |
24 | 10 | absge0d 15335 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β 0 β€
(absβ(ββπ₯))) |
25 | | 1re 11160 |
. . . . . . . 8
β’ 1 β
β |
26 | | 0le1 11683 |
. . . . . . . 8
β’ 0 β€
1 |
27 | | sq11 14042 |
. . . . . . . 8
β’
((((absβ(ββπ₯)) β β β§ 0 β€
(absβ(ββπ₯))) β§ (1 β β β§ 0 β€ 1))
β (((absβ(ββπ₯))β2) = (1β2) β
(absβ(ββπ₯)) = 1)) |
28 | 25, 26, 27 | mpanr12 704 |
. . . . . . 7
β’
(((absβ(ββπ₯)) β β β§ 0 β€
(absβ(ββπ₯))) β (((absβ(ββπ₯))β2) = (1β2) β
(absβ(ββπ₯)) = 1)) |
29 | 23, 24, 28 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β πΆ) β (((absβ(ββπ₯))β2) = (1β2) β
(absβ(ββπ₯)) = 1)) |
30 | 22, 29 | mpbid 231 |
. . . . 5
β’ ((π β§ π₯ β πΆ) β (absβ(ββπ₯)) = 1) |
31 | 13, 30 | breqtrd 5132 |
. . . 4
β’ ((π β§ π₯ β πΆ) β
(absβ(ββ(ββπ₯))) β€ 1) |
32 | | absle 15206 |
. . . . 5
β’
(((ββ(ββπ₯)) β β β§ 1 β β)
β ((absβ(ββ(ββπ₯))) β€ 1 β (-1 β€
(ββ(ββπ₯)) β§ (ββ(ββπ₯)) β€ 1))) |
33 | 11, 25, 32 | sylancl 587 |
. . . 4
β’ ((π β§ π₯ β πΆ) β
((absβ(ββ(ββπ₯))) β€ 1 β (-1 β€
(ββ(ββπ₯)) β§ (ββ(ββπ₯)) β€ 1))) |
34 | 31, 33 | mpbid 231 |
. . 3
β’ ((π β§ π₯ β πΆ) β (-1 β€
(ββ(ββπ₯)) β§ (ββ(ββπ₯)) β€ 1)) |
35 | 34 | simpld 496 |
. 2
β’ ((π β§ π₯ β πΆ) β -1 β€
(ββ(ββπ₯))) |
36 | 34 | simprd 497 |
. 2
β’ ((π β§ π₯ β πΆ) β (ββ(ββπ₯)) β€ 1) |
37 | | neg1rr 12273 |
. . 3
β’ -1 β
β |
38 | 37, 25 | elicc2i 13336 |
. 2
β’
((ββ(ββπ₯)) β (-1[,]1) β
((ββ(ββπ₯)) β β β§ -1 β€
(ββ(ββπ₯)) β§ (ββ(ββπ₯)) β€ 1)) |
39 | 11, 35, 36, 38 | syl3anbrc 1344 |
1
β’ ((π β§ π₯ β πΆ) β (ββ(ββπ₯)) β
(-1[,]1)) |