Step | Hyp | Ref
| Expression |
1 | | qrng.q |
. . . . . 6
β’ π = (βfld
βΎs β) |
2 | | qabsabv.a |
. . . . . 6
β’ π΄ = (AbsValβπ) |
3 | | padic.j |
. . . . . 6
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
4 | | ostth.k |
. . . . . 6
β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) |
5 | | simpl 484 |
. . . . . 6
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β πΉ β π΄) |
6 | | 1re 11163 |
. . . . . . . . . . 11
β’ 1 β
β |
7 | 6 | ltnri 11272 |
. . . . . . . . . 10
β’ Β¬ 1
< 1 |
8 | | ax-1ne0 11128 |
. . . . . . . . . . . 12
β’ 1 β
0 |
9 | 1 | qrng1 26993 |
. . . . . . . . . . . . 13
β’ 1 =
(1rβπ) |
10 | 1 | qrng0 26992 |
. . . . . . . . . . . . 13
β’ 0 =
(0gβπ) |
11 | 2, 9, 10 | abv1z 20334 |
. . . . . . . . . . . 12
β’ ((πΉ β π΄ β§ 1 β 0) β (πΉβ1) = 1) |
12 | 8, 11 | mpan2 690 |
. . . . . . . . . . 11
β’ (πΉ β π΄ β (πΉβ1) = 1) |
13 | 12 | breq2d 5121 |
. . . . . . . . . 10
β’ (πΉ β π΄ β (1 < (πΉβ1) β 1 < 1)) |
14 | 7, 13 | mtbiri 327 |
. . . . . . . . 9
β’ (πΉ β π΄ β Β¬ 1 < (πΉβ1)) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β Β¬ 1 < (πΉβ1)) |
16 | | simprr 772 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β 1 < (πΉβπ)) |
17 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = 1 β (πΉβπ) = (πΉβ1)) |
18 | 17 | breq2d 5121 |
. . . . . . . . 9
β’ (π = 1 β (1 < (πΉβπ) β 1 < (πΉβ1))) |
19 | 16, 18 | syl5ibcom 244 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β (π = 1 β 1 < (πΉβ1))) |
20 | 15, 19 | mtod 197 |
. . . . . . 7
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β Β¬ π = 1) |
21 | | simprl 770 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β π β β) |
22 | | elnn1uz2 12858 |
. . . . . . . . 9
β’ (π β β β (π = 1 β¨ π β
(β€β₯β2))) |
23 | 21, 22 | sylib 217 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β (π = 1 β¨ π β
(β€β₯β2))) |
24 | 23 | ord 863 |
. . . . . . 7
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β (Β¬ π = 1 β π β
(β€β₯β2))) |
25 | 20, 24 | mpd 15 |
. . . . . 6
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β π β
(β€β₯β2)) |
26 | | eqid 2733 |
. . . . . 6
β’
((logβ(πΉβπ)) / (logβπ)) = ((logβ(πΉβπ)) / (logβπ)) |
27 | 1, 2, 3, 4, 5, 25,
16, 26 | ostth2 27008 |
. . . . 5
β’ ((πΉ β π΄ β§ (π β β β§ 1 < (πΉβπ))) β βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ))) |
28 | 27 | rexlimdvaa 3150 |
. . . 4
β’ (πΉ β π΄ β (βπ β β 1 < (πΉβπ) β βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)))) |
29 | | 3mix2 1332 |
. . . 4
β’
(βπ β
(0(,]1)πΉ = (π¦ β β β¦
((absβπ¦)βππ)) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |
30 | 28, 29 | syl6 35 |
. . 3
β’ (πΉ β π΄ β (βπ β β 1 < (πΉβπ) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))))) |
31 | | ralnex 3072 |
. . . 4
β’
(βπ β
β Β¬ 1 < (πΉβπ) β Β¬ βπ β β 1 < (πΉβπ)) |
32 | | simpll 766 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ (π β β β§ (πΉβπ) < 1)) β πΉ β π΄) |
33 | | simplr 768 |
. . . . . . . . . . 11
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ (π β β β§ (πΉβπ) < 1)) β βπ β β Β¬ 1 < (πΉβπ)) |
34 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
35 | 34 | breq2d 5121 |
. . . . . . . . . . . . 13
β’ (π = π β (1 < (πΉβπ) β 1 < (πΉβπ))) |
36 | 35 | notbid 318 |
. . . . . . . . . . . 12
β’ (π = π β (Β¬ 1 < (πΉβπ) β Β¬ 1 < (πΉβπ))) |
37 | 36 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ β
β Β¬ 1 < (πΉβπ) β βπ β β Β¬ 1 < (πΉβπ)) |
38 | 33, 37 | sylib 217 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ (π β β β§ (πΉβπ) < 1)) β βπ β β Β¬ 1 < (πΉβπ)) |
39 | | simprl 770 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ (π β β β§ (πΉβπ) < 1)) β π β β) |
40 | | simprr 772 |
. . . . . . . . . 10
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ (π β β β§ (πΉβπ) < 1)) β (πΉβπ) < 1) |
41 | | eqid 2733 |
. . . . . . . . . 10
β’
-((logβ(πΉβπ)) / (logβπ)) = -((logβ(πΉβπ)) / (logβπ)) |
42 | | eqid 2733 |
. . . . . . . . . 10
β’ if((πΉβπ) β€ (πΉβπ§), (πΉβπ§), (πΉβπ)) = if((πΉβπ) β€ (πΉβπ§), (πΉβπ§), (πΉβπ)) |
43 | 1, 2, 3, 4, 32, 38, 39, 40, 41, 42 | ostth3 27009 |
. . . . . . . . 9
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ (π β β β§ (πΉβπ) < 1)) β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
44 | 43 | expr 458 |
. . . . . . . 8
β’ (((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β§ π β β) β ((πΉβπ) < 1 β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)))) |
45 | 44 | reximdva 3162 |
. . . . . . 7
β’ ((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β (βπ β β (πΉβπ) < 1 β βπ β β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)))) |
46 | 1, 2, 3 | padicabvf 27002 |
. . . . . . . . . . 11
β’ π½:ββΆπ΄ |
47 | | ffn 6672 |
. . . . . . . . . . 11
β’ (π½:ββΆπ΄ β π½ Fn β) |
48 | | fveq1 6845 |
. . . . . . . . . . . . . . 15
β’ (π = (π½βπ) β (πβπ¦) = ((π½βπ)βπ¦)) |
49 | 48 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (π = (π½βπ) β ((πβπ¦)βππ) = (((π½βπ)βπ¦)βππ)) |
50 | 49 | mpteq2dv 5211 |
. . . . . . . . . . . . 13
β’ (π = (π½βπ) β (π¦ β β β¦ ((πβπ¦)βππ)) = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
51 | 50 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = (π½βπ) β (πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)))) |
52 | 51 | rexrn 7041 |
. . . . . . . . . . 11
β’ (π½ Fn β β (βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β βπ β β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)))) |
53 | 46, 47, 52 | mp2b 10 |
. . . . . . . . . 10
β’
(βπ β ran
π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β βπ β β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
54 | 53 | rexbii 3094 |
. . . . . . . . 9
β’
(βπ β
β+ βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β βπ β β+ βπ β β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
55 | | rexcom 3272 |
. . . . . . . . 9
β’
(βπ β
β+ βπ β β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)) β βπ β β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
56 | 54, 55 | bitri 275 |
. . . . . . . 8
β’
(βπ β
β+ βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β βπ β β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
57 | | 3mix3 1333 |
. . . . . . . 8
β’
(βπ β
β+ βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |
58 | 56, 57 | sylbir 234 |
. . . . . . 7
β’
(βπ β
β βπ β
β+ πΉ =
(π¦ β β β¦
(((π½βπ)βπ¦)βππ)) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |
59 | 45, 58 | syl6 35 |
. . . . . 6
β’ ((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β (βπ β β (πΉβπ) < 1 β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))))) |
60 | | ralnex 3072 |
. . . . . . 7
β’
(βπ β
β Β¬ (πΉβπ) < 1 β Β¬ βπ β β (πΉβπ) < 1) |
61 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β πΉ β π΄) |
62 | | simprl 770 |
. . . . . . . . . . 11
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β βπ β β Β¬ 1 < (πΉβπ)) |
63 | 62, 37 | sylib 217 |
. . . . . . . . . 10
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β βπ β β Β¬ 1 < (πΉβπ)) |
64 | | simprr 772 |
. . . . . . . . . . 11
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β βπ β β Β¬ (πΉβπ) < 1) |
65 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
66 | 65 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ) < 1 β (πΉβπ) < 1)) |
67 | 66 | notbid 318 |
. . . . . . . . . . . 12
β’ (π = π β (Β¬ (πΉβπ) < 1 β Β¬ (πΉβπ) < 1)) |
68 | 67 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ β
β Β¬ (πΉβπ) < 1 β βπ β β Β¬ (πΉβπ) < 1) |
69 | 64, 68 | sylib 217 |
. . . . . . . . . 10
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β βπ β β Β¬ (πΉβπ) < 1) |
70 | 1, 2, 3, 4, 61, 63, 69 | ostth1 27004 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β πΉ = πΎ) |
71 | 70 | 3mix1d 1337 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ (βπ β β Β¬ 1 < (πΉβπ) β§ βπ β β Β¬ (πΉβπ) < 1)) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |
72 | 71 | expr 458 |
. . . . . . 7
β’ ((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β (βπ β β Β¬ (πΉβπ) < 1 β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))))) |
73 | 60, 72 | biimtrrid 242 |
. . . . . 6
β’ ((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β (Β¬ βπ β β (πΉβπ) < 1 β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))))) |
74 | 59, 73 | pm2.61d 179 |
. . . . 5
β’ ((πΉ β π΄ β§ βπ β β Β¬ 1 < (πΉβπ)) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |
75 | 74 | ex 414 |
. . . 4
β’ (πΉ β π΄ β (βπ β β Β¬ 1 < (πΉβπ) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))))) |
76 | 31, 75 | biimtrrid 242 |
. . 3
β’ (πΉ β π΄ β (Β¬ βπ β β 1 < (πΉβπ) β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))))) |
77 | 30, 76 | pm2.61d 179 |
. 2
β’ (πΉ β π΄ β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |
78 | | id 22 |
. . . 4
β’ (πΉ = πΎ β πΉ = πΎ) |
79 | 1 | qdrng 26991 |
. . . . 5
β’ π β DivRing |
80 | 1 | qrngbas 26990 |
. . . . . 6
β’ β =
(Baseβπ) |
81 | 2, 80, 10, 4 | abvtriv 20343 |
. . . . 5
β’ (π β DivRing β πΎ β π΄) |
82 | 79, 81 | ax-mp 5 |
. . . 4
β’ πΎ β π΄ |
83 | 78, 82 | eqeltrdi 2842 |
. . 3
β’ (πΉ = πΎ β πΉ β π΄) |
84 | 1, 2 | qabsabv 27000 |
. . . . . 6
β’ (abs
βΎ β) β π΄ |
85 | | fvres 6865 |
. . . . . . . . . 10
β’ (π¦ β β β ((abs
βΎ β)βπ¦) =
(absβπ¦)) |
86 | 85 | oveq1d 7376 |
. . . . . . . . 9
β’ (π¦ β β β (((abs
βΎ β)βπ¦)βππ) = ((absβπ¦)βππ)) |
87 | 86 | mpteq2ia 5212 |
. . . . . . . 8
β’ (π¦ β β β¦ (((abs
βΎ β)βπ¦)βππ)) = (π¦ β β β¦ ((absβπ¦)βππ)) |
88 | 87 | eqcomi 2742 |
. . . . . . 7
β’ (π¦ β β β¦
((absβπ¦)βππ)) = (π¦ β β β¦ (((abs βΎ
β)βπ¦)βππ)) |
89 | 2, 80, 88 | abvcxp 26986 |
. . . . . 6
β’ (((abs
βΎ β) β π΄
β§ π β (0(,]1))
β (π¦ β β
β¦ ((absβπ¦)βππ)) β π΄) |
90 | 84, 89 | mpan 689 |
. . . . 5
β’ (π β (0(,]1) β (π¦ β β β¦
((absβπ¦)βππ)) β π΄) |
91 | | eleq1 2822 |
. . . . 5
β’ (πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β (πΉ β π΄ β (π¦ β β β¦ ((absβπ¦)βππ)) β π΄)) |
92 | 90, 91 | syl5ibrcom 247 |
. . . 4
β’ (π β (0(,]1) β (πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β πΉ β π΄)) |
93 | 92 | rexlimiv 3142 |
. . 3
β’
(βπ β
(0(,]1)πΉ = (π¦ β β β¦
((absβπ¦)βππ)) β πΉ β π΄) |
94 | 1, 2, 3 | padicabvcxp 27003 |
. . . . . . 7
β’ ((π β β β§ π β β+)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ)) β π΄) |
95 | 94 | ancoms 460 |
. . . . . 6
β’ ((π β β+
β§ π β β)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ)) β π΄) |
96 | | eleq1 2822 |
. . . . . 6
β’ (πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)) β (πΉ β π΄ β (π¦ β β β¦ (((π½βπ)βπ¦)βππ)) β π΄)) |
97 | 95, 96 | syl5ibrcom 247 |
. . . . 5
β’ ((π β β+
β§ π β β)
β (πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)) β πΉ β π΄)) |
98 | 97 | rexlimivv 3193 |
. . . 4
β’
(βπ β
β+ βπ β β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ)) β πΉ β π΄) |
99 | 54, 98 | sylbi 216 |
. . 3
β’
(βπ β
β+ βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)) β πΉ β π΄) |
100 | 83, 93, 99 | 3jaoi 1428 |
. 2
β’ ((πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ))) β πΉ β π΄) |
101 | 77, 100 | impbii 208 |
1
β’ (πΉ β π΄ β (πΉ = πΎ β¨ βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ)) β¨ βπ β β+
βπ β ran π½ πΉ = (π¦ β β β¦ ((πβπ¦)βππ)))) |