Step | Hyp | Ref
| Expression |
1 | | ostth3.5 |
. . . 4
β’ π
= -((logβ(πΉβπ)) / (logβπ)) |
2 | | ostth.1 |
. . . . . . . . 9
β’ (π β πΉ β π΄) |
3 | | ostth3.3 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
4 | | prmuz2 16577 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β2)) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β
(β€β₯β2)) |
6 | | eluz2b2 12851 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
7 | 5, 6 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π β β β§ 1 < π)) |
8 | 7 | simpld 496 |
. . . . . . . . . 10
β’ (π β π β β) |
9 | | nnq 12892 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
11 | | qabsabv.a |
. . . . . . . . . 10
β’ π΄ = (AbsValβπ) |
12 | | qrng.q |
. . . . . . . . . . 11
β’ π = (βfld
βΎs β) |
13 | 12 | qrngbas 26983 |
. . . . . . . . . 10
β’ β =
(Baseβπ) |
14 | 11, 13 | abvcl 20297 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
15 | 2, 10, 14 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΉβπ) β β) |
16 | 8 | nnne0d 12208 |
. . . . . . . . 9
β’ (π β π β 0) |
17 | 12 | qrng0 26985 |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
18 | 11, 13, 17 | abvgt0 20301 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ π β β β§ π β 0) β 0 < (πΉβπ)) |
19 | 2, 10, 16, 18 | syl3anc 1372 |
. . . . . . . 8
β’ (π β 0 < (πΉβπ)) |
20 | 15, 19 | elrpd 12959 |
. . . . . . 7
β’ (π β (πΉβπ) β
β+) |
21 | 20 | relogcld 25994 |
. . . . . 6
β’ (π β (logβ(πΉβπ)) β β) |
22 | 8 | nnred 12173 |
. . . . . . 7
β’ (π β π β β) |
23 | 7 | simprd 497 |
. . . . . . 7
β’ (π β 1 < π) |
24 | 22, 23 | rplogcld 26000 |
. . . . . 6
β’ (π β (logβπ) β
β+) |
25 | 21, 24 | rerpdivcld 12993 |
. . . . 5
β’ (π β ((logβ(πΉβπ)) / (logβπ)) β β) |
26 | 25 | renegcld 11587 |
. . . 4
β’ (π β -((logβ(πΉβπ)) / (logβπ)) β β) |
27 | 1, 26 | eqeltrid 2838 |
. . 3
β’ (π β π
β β) |
28 | | ostth3.4 |
. . . . . . . . 9
β’ (π β (πΉβπ) < 1) |
29 | | 1rp 12924 |
. . . . . . . . . 10
β’ 1 β
β+ |
30 | | logltb 25971 |
. . . . . . . . . 10
β’ (((πΉβπ) β β+ β§ 1 β
β+) β ((πΉβπ) < 1 β (logβ(πΉβπ)) < (logβ1))) |
31 | 20, 29, 30 | sylancl 587 |
. . . . . . . . 9
β’ (π β ((πΉβπ) < 1 β (logβ(πΉβπ)) < (logβ1))) |
32 | 28, 31 | mpbid 231 |
. . . . . . . 8
β’ (π β (logβ(πΉβπ)) < (logβ1)) |
33 | | log1 25957 |
. . . . . . . 8
β’
(logβ1) = 0 |
34 | 32, 33 | breqtrdi 5147 |
. . . . . . 7
β’ (π β (logβ(πΉβπ)) < 0) |
35 | 24 | rpcnd 12964 |
. . . . . . . 8
β’ (π β (logβπ) β
β) |
36 | 35 | mul01d 11359 |
. . . . . . 7
β’ (π β ((logβπ) Β· 0) =
0) |
37 | 34, 36 | breqtrrd 5134 |
. . . . . 6
β’ (π β (logβ(πΉβπ)) < ((logβπ) Β· 0)) |
38 | | 0red 11163 |
. . . . . . 7
β’ (π β 0 β
β) |
39 | 21, 38, 24 | ltdivmuld 13013 |
. . . . . 6
β’ (π β (((logβ(πΉβπ)) / (logβπ)) < 0 β (logβ(πΉβπ)) < ((logβπ) Β· 0))) |
40 | 37, 39 | mpbird 257 |
. . . . 5
β’ (π β ((logβ(πΉβπ)) / (logβπ)) < 0) |
41 | 25 | lt0neg1d 11729 |
. . . . 5
β’ (π β (((logβ(πΉβπ)) / (logβπ)) < 0 β 0 < -((logβ(πΉβπ)) / (logβπ)))) |
42 | 40, 41 | mpbid 231 |
. . . 4
β’ (π β 0 < -((logβ(πΉβπ)) / (logβπ))) |
43 | 42, 1 | breqtrrdi 5148 |
. . 3
β’ (π β 0 < π
) |
44 | 27, 43 | elrpd 12959 |
. 2
β’ (π β π
β
β+) |
45 | | padic.j |
. . . . 5
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
46 | 12, 11, 45 | padicabvcxp 26996 |
. . . 4
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ
)) β π΄) |
47 | 3, 44, 46 | syl2anc 585 |
. . 3
β’ (π β (π¦ β β β¦ (((π½βπ)βπ¦)βππ
)) β π΄) |
48 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π¦ = π β ((π½βπ)βπ¦) = ((π½βπ)βπ)) |
49 | 48 | oveq1d 7373 |
. . . . . . . . 9
β’ (π¦ = π β (((π½βπ)βπ¦)βππ
) = (((π½βπ)βπ)βππ
)) |
50 | | eqid 2733 |
. . . . . . . . 9
β’ (π¦ β β β¦ (((π½βπ)βπ¦)βππ
)) = (π¦ β β β¦ (((π½βπ)βπ¦)βππ
)) |
51 | | ovex 7391 |
. . . . . . . . 9
β’ (((π½βπ)βπ)βππ
) β V |
52 | 49, 50, 51 | fvmpt 6949 |
. . . . . . . 8
β’ (π β β β ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ) = (((π½βπ)βπ)βππ
)) |
53 | 10, 52 | syl 17 |
. . . . . . 7
β’ (π β ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ) = (((π½βπ)βπ)βππ
)) |
54 | 45 | padicval 26981 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β ((π½βπ)βπ) = if(π = 0, 0, (πβ-(π pCnt π)))) |
55 | 3, 10, 54 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((π½βπ)βπ) = if(π = 0, 0, (πβ-(π pCnt π)))) |
56 | 16 | neneqd 2945 |
. . . . . . . . . 10
β’ (π β Β¬ π = 0) |
57 | 56 | iffalsed 4498 |
. . . . . . . . 9
β’ (π β if(π = 0, 0, (πβ-(π pCnt π))) = (πβ-(π pCnt π))) |
58 | 8 | nncnd 12174 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
59 | 58 | exp1d 14052 |
. . . . . . . . . . . . . 14
β’ (π β (πβ1) = π) |
60 | 59 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π β (π pCnt (πβ1)) = (π pCnt π)) |
61 | | 1z 12538 |
. . . . . . . . . . . . . 14
β’ 1 β
β€ |
62 | | pcid 16750 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ 1 β
β€) β (π pCnt
(πβ1)) =
1) |
63 | 3, 61, 62 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β (π pCnt (πβ1)) = 1) |
64 | 60, 63 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (π β (π pCnt π) = 1) |
65 | 64 | negeqd 11400 |
. . . . . . . . . . 11
β’ (π β -(π pCnt π) = -1) |
66 | 65 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β (πβ-(π pCnt π)) = (πβ-1)) |
67 | | neg1z 12544 |
. . . . . . . . . . . 12
β’ -1 β
β€ |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
β’ (π β -1 β
β€) |
69 | 58, 16, 68 | cxpexpzd 26082 |
. . . . . . . . . 10
β’ (π β (πβπ-1) = (πβ-1)) |
70 | 66, 69 | eqtr4d 2776 |
. . . . . . . . 9
β’ (π β (πβ-(π pCnt π)) = (πβπ-1)) |
71 | 55, 57, 70 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β ((π½βπ)βπ) = (πβπ-1)) |
72 | 71 | oveq1d 7373 |
. . . . . . 7
β’ (π β (((π½βπ)βπ)βππ
) = ((πβπ-1)βππ
)) |
73 | 27 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β π
β β) |
74 | 73 | mulm1d 11612 |
. . . . . . . . . 10
β’ (π β (-1 Β· π
) = -π
) |
75 | 1 | negeqi 11399 |
. . . . . . . . . . 11
β’ -π
= --((logβ(πΉβπ)) / (logβπ)) |
76 | 25 | recnd 11188 |
. . . . . . . . . . . 12
β’ (π β ((logβ(πΉβπ)) / (logβπ)) β β) |
77 | 76 | negnegd 11508 |
. . . . . . . . . . 11
β’ (π β --((logβ(πΉβπ)) / (logβπ)) = ((logβ(πΉβπ)) / (logβπ))) |
78 | 75, 77 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β -π
= ((logβ(πΉβπ)) / (logβπ))) |
79 | 74, 78 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (-1 Β· π
) = ((logβ(πΉβπ)) / (logβπ))) |
80 | 79 | oveq2d 7374 |
. . . . . . . 8
β’ (π β (πβπ(-1 Β· π
)) = (πβπ((logβ(πΉβπ)) / (logβπ)))) |
81 | 8 | nnrpd 12960 |
. . . . . . . . 9
β’ (π β π β
β+) |
82 | | neg1rr 12273 |
. . . . . . . . . 10
β’ -1 β
β |
83 | 82 | a1i 11 |
. . . . . . . . 9
β’ (π β -1 β
β) |
84 | 81, 83, 73 | cxpmuld 26107 |
. . . . . . . 8
β’ (π β (πβπ(-1 Β· π
)) = ((πβπ-1)βππ
)) |
85 | 58, 16, 76 | cxpefd 26083 |
. . . . . . . . 9
β’ (π β (πβπ((logβ(πΉβπ)) / (logβπ))) = (expβ(((logβ(πΉβπ)) / (logβπ)) Β· (logβπ)))) |
86 | 21 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β (logβ(πΉβπ)) β β) |
87 | 24 | rpne0d 12967 |
. . . . . . . . . . 11
β’ (π β (logβπ) β 0) |
88 | 86, 35, 87 | divcan1d 11937 |
. . . . . . . . . 10
β’ (π β (((logβ(πΉβπ)) / (logβπ)) Β· (logβπ)) = (logβ(πΉβπ))) |
89 | 88 | fveq2d 6847 |
. . . . . . . . 9
β’ (π β
(expβ(((logβ(πΉβπ)) / (logβπ)) Β· (logβπ))) = (expβ(logβ(πΉβπ)))) |
90 | 20 | reeflogd 25995 |
. . . . . . . . 9
β’ (π β
(expβ(logβ(πΉβπ))) = (πΉβπ)) |
91 | 85, 89, 90 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (πβπ((logβ(πΉβπ)) / (logβπ))) = (πΉβπ)) |
92 | 80, 84, 91 | 3eqtr3d 2781 |
. . . . . . 7
β’ (π β ((πβπ-1)βππ
) = (πΉβπ)) |
93 | 53, 72, 92 | 3eqtrrd 2778 |
. . . . . 6
β’ (π β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ)) |
94 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
95 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ)) |
96 | 94, 95 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β ((πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ) β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ))) |
97 | 93, 96 | syl5ibcom 244 |
. . . . 5
β’ (π β (π = π β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ))) |
98 | 97 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β (π = π β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ))) |
99 | | prmnn 16555 |
. . . . . . . . 9
β’ (π β β β π β
β) |
100 | 99 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β π β β) |
101 | | nnq 12892 |
. . . . . . . 8
β’ (π β β β π β
β) |
102 | 100, 101 | syl 17 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β π β β) |
103 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = π β ((π½βπ)βπ¦) = ((π½βπ)βπ)) |
104 | 103 | oveq1d 7373 |
. . . . . . . 8
β’ (π¦ = π β (((π½βπ)βπ¦)βππ
) = (((π½βπ)βπ)βππ
)) |
105 | | ovex 7391 |
. . . . . . . 8
β’ (((π½βπ)βπ)βππ
) β V |
106 | 104, 50, 105 | fvmpt 6949 |
. . . . . . 7
β’ (π β β β ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ) = (((π½βπ)βπ)βππ
)) |
107 | 102, 106 | syl 17 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ) = (((π½βπ)βπ)βππ
)) |
108 | 73 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β π
β β) |
109 | 108 | 1cxpd 26078 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (1βππ
) = 1) |
110 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β π β β) |
111 | 45 | padicval 26981 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β ((π½βπ)βπ) = if(π = 0, 0, (πβ-(π pCnt π)))) |
112 | 110, 102,
111 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β ((π½βπ)βπ) = if(π = 0, 0, (πβ-(π pCnt π)))) |
113 | 100 | nnne0d 12208 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β π β 0) |
114 | 113 | neneqd 2945 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β Β¬ π = 0) |
115 | 114 | iffalsed 4498 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β if(π = 0, 0, (πβ-(π pCnt π))) = (πβ-(π pCnt π))) |
116 | | pceq0 16748 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β ((π pCnt π) = 0 β Β¬ π β₯ π)) |
117 | 3, 99, 116 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((π pCnt π) = 0 β Β¬ π β₯ π)) |
118 | | dvdsprm 16584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β2) β§ π β β) β (π β₯ π β π = π)) |
119 | 5, 118 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (π β₯ π β π = π)) |
120 | 119 | necon3bbid 2978 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (Β¬ π β₯ π β π β π)) |
121 | 117, 120 | bitrd 279 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π pCnt π) = 0 β π β π)) |
122 | 121 | biimpar 479 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β (π pCnt π) = 0) |
123 | 122 | negeqd 11400 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π) β -(π pCnt π) = -0) |
124 | | neg0 11452 |
. . . . . . . . . . . 12
β’ -0 =
0 |
125 | 123, 124 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β -(π pCnt π) = 0) |
126 | 125 | oveq2d 7374 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β (πβ-(π pCnt π)) = (πβ0)) |
127 | 58 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β π β β) |
128 | 127 | exp0d 14051 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π) β (πβ0) = 1) |
129 | 126, 128 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β (πβ-(π pCnt π)) = 1) |
130 | 112, 115,
129 | 3eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β ((π½βπ)βπ) = 1) |
131 | 130 | oveq1d 7373 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (((π½βπ)βπ)βππ
) = (1βππ
)) |
132 | | 2re 12232 |
. . . . . . . . . . . . 13
β’ 2 β
β |
133 | 132 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β 2 β
β) |
134 | | ostth3.6 |
. . . . . . . . . . . . . 14
β’ π = if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) |
135 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β π) β πΉ β π΄) |
136 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
137 | 135, 102,
136 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β π) β (πΉβπ) β β) |
138 | 11, 13, 17 | abvgt0 20301 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β π΄ β§ π β β β§ π β 0) β 0 < (πΉβπ)) |
139 | 135, 102,
113, 138 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β π) β 0 < (πΉβπ)) |
140 | 137, 139 | elrpd 12959 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β π) β (πΉβπ) β
β+) |
141 | 140 | adantrr 716 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (πΉβπ) β
β+) |
142 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (πΉβπ) β
β+) |
143 | 141, 142 | ifcld 4533 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) β
β+) |
144 | 134, 143 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β
β+) |
145 | 144 | rprecred 12973 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (1 / π) β β) |
146 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (πΉβπ) < 1) |
147 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (πΉβπ) < 1) |
148 | | breq1 5109 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) = if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) β ((πΉβπ) < 1 β if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) < 1)) |
149 | | breq1 5109 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) = if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) β ((πΉβπ) < 1 β if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) < 1)) |
150 | 148, 149 | ifboth 4526 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) < 1 β§ (πΉβπ) < 1) β if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) < 1) |
151 | 146, 147,
150 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ)) < 1) |
152 | 134, 151 | eqbrtrid 5141 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π < 1) |
153 | 144 | reclt1d 12975 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (π < 1 β 1 < (1 / π))) |
154 | 152, 153 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β 1 < (1 / π)) |
155 | | expnbnd 14141 |
. . . . . . . . . . . 12
β’ ((2
β β β§ (1 / π) β β β§ 1 < (1 / π)) β βπ β β 2 < ((1 /
π)βπ)) |
156 | 133, 145,
154, 155 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β βπ β β 2 < ((1 / π)βπ)) |
157 | 144 | rpcnd 12964 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β β) |
158 | 157 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β π β β) |
159 | 144 | rpne0d 12967 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β 0) |
160 | 159 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β π β 0) |
161 | | nnz 12525 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β€) |
162 | 161 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β π β β€) |
163 | 158, 160,
162 | exprecd 14065 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((1 / π)βπ) = (1 / (πβπ))) |
164 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β πΉ β π΄) |
165 | | ax-1ne0 11125 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
0 |
166 | 12 | qrng1 26986 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 =
(1rβπ) |
167 | 11, 166, 17 | abv1z 20305 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β π΄ β§ 1 β 0) β (πΉβ1) = 1) |
168 | 164, 165,
167 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πΉβ1) = 1) |
169 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β β) |
170 | | nnnn0 12425 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β0) |
171 | | nnexpcl 13986 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
172 | 169, 170,
171 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β β) |
173 | 172 | nnzd 12531 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β β€) |
174 | 99 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β β) |
175 | | nnexpcl 13986 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
176 | 174, 170,
175 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β β) |
177 | 176 | nnzd 12531 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β β€) |
178 | | bezout 16429 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ) β β€ β§ (πβπ) β β€) β βπ β β€ βπ β β€ ((πβπ) gcd (πβπ)) = (((πβπ) Β· π) + ((πβπ) Β· π))) |
179 | 173, 177,
178 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β βπ β β€ βπ β β€ ((πβπ) gcd (πβπ)) = (((πβπ) Β· π) + ((πβπ) Β· π))) |
180 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β π) |
181 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β β) |
182 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β β) |
183 | | prmrp 16593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β β§ π β β) β ((π gcd π) = 1 β π β π)) |
184 | 181, 182,
183 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β ((π gcd π) = 1 β π β π)) |
185 | 180, 184 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (π gcd π) = 1) |
186 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (π gcd π) = 1) |
187 | 169 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β π β β) |
188 | 174 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β π β β) |
189 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β π β β) |
190 | | rppwr 16445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β β§ π β β β§ π β β) β ((π gcd π) = 1 β ((πβπ) gcd (πβπ)) = 1)) |
191 | 187, 188,
189, 190 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((π gcd π) = 1 β ((πβπ) gcd (πβπ)) = 1)) |
192 | 186, 191 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((πβπ) gcd (πβπ)) = 1) |
193 | 192 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πβπ) gcd (πβπ)) = 1) |
194 | 193 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πβπ) gcd (πβπ)) = (((πβπ) Β· π) + ((πβπ) Β· π)) β 1 = (((πβπ) Β· π) + ((πβπ) Β· π)))) |
195 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β πΉ β π΄) |
196 | 172 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πβπ) β β) |
197 | | nnq 12892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β β β (πβπ) β β) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πβπ) β β) |
199 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β€) |
200 | | zq 12884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β€ β π β
β) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β) |
202 | | qmulcl 12897 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πβπ) β β β§ π β β) β ((πβπ) Β· π) β β) |
203 | 198, 201,
202 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πβπ) Β· π) β β) |
204 | 176 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πβπ) β β) |
205 | | nnq 12892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β β β (πβπ) β β) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πβπ) β β) |
207 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β€) |
208 | | zq 12884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β€ β π β
β) |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β) |
210 | | qmulcl 12897 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πβπ) β β β§ π β β) β ((πβπ) Β· π) β β) |
211 | 206, 209,
210 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πβπ) Β· π) β β) |
212 | | qaddcl 12895 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πβπ) Β· π) β β β§ ((πβπ) Β· π) β β) β (((πβπ) Β· π) + ((πβπ) Β· π)) β β) |
213 | 203, 211,
212 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πβπ) Β· π) + ((πβπ) Β· π)) β β) |
214 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ β π΄ β§ (((πβπ) Β· π) + ((πβπ) Β· π)) β β) β (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π))) β β) |
215 | 195, 213,
214 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π))) β β) |
216 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ β π΄ β§ ((πβπ) Β· π) β β) β (πΉβ((πβπ) Β· π)) β β) |
217 | 195, 203,
216 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) β β) |
218 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ β π΄ β§ ((πβπ) Β· π) β β) β (πΉβ((πβπ) Β· π)) β β) |
219 | 195, 211,
218 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) β β) |
220 | 217, 219 | readdcld 11189 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβ((πβπ) Β· π)) + (πΉβ((πβπ) Β· π))) β β) |
221 | | rpexpcl 13992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β+
β§ π β β€)
β (πβπ) β
β+) |
222 | 144, 161,
221 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β
β+) |
223 | 222 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β β) |
224 | 223 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πβπ) β β) |
225 | | remulcl 11141 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((2
β β β§ (πβπ) β β) β (2 Β· (πβπ)) β β) |
226 | 132, 224,
225 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (2 Β· (πβπ)) β β) |
227 | | qex 12891 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ β
β V |
228 | | cnfldadd 20817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ + =
(+gββfld) |
229 | 12, 228 | ressplusg 17176 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (β
β V β + = (+gβπ)) |
230 | 227, 229 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ + =
(+gβπ) |
231 | 11, 13, 230 | abvtri 20303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ β π΄ β§ ((πβπ) Β· π) β β β§ ((πβπ) Β· π) β β) β (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π))) β€ ((πΉβ((πβπ) Β· π)) + (πΉβ((πβπ) Β· π)))) |
232 | 195, 203,
211, 231 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π))) β€ ((πΉβ((πβπ) Β· π)) + (πΉβ((πβπ) Β· π)))) |
233 | | cnfldmul 20818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ Β·
= (.rββfld) |
234 | 12, 233 | ressmulr 17193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (β
β V β Β· = (.rβπ)) |
235 | 227, 234 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ Β·
= (.rβπ) |
236 | 11, 13, 235 | abvmul 20302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΉ β π΄ β§ (πβπ) β β β§ π β β) β (πΉβ((πβπ) Β· π)) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
237 | 195, 198,
201, 236 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
238 | 10 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β) |
239 | 170 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β0) |
240 | 12, 11 | qabvexp 26990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉ β π΄ β§ π β β β§ π β β0) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
241 | 195, 238,
239, 240 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
242 | 241 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβ(πβπ)) Β· (πΉβπ)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
243 | 237, 242 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
244 | 195, 238,
14 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β β) |
245 | 244, 239 | reexpcld 14074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ)βπ) β β) |
246 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
247 | 195, 201,
246 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β β) |
248 | 245, 247 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β β) |
249 | | elz 12506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β€ β (π β β β§ (π = 0 β¨ π β β β¨ -π β β))) |
250 | 249 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β β€ β (π = 0 β¨ π β β β¨ -π β β)) |
251 | 250 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β β€) β (π = 0 β¨ π β β β¨ -π β β)) |
252 | 11, 17 | abv0 20304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (πΉ β π΄ β (πΉβ0) = 0) |
253 | 2, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β (πΉβ0) = 0) |
254 | | 0le1 11683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ 0 β€
1 |
255 | 253, 254 | eqbrtrdi 5145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β (πΉβ0) β€ 1) |
256 | 255 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ π β β€) β (πΉβ0) β€ 1) |
257 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = 0 β (πΉβπ) = (πΉβ0)) |
258 | 257 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = 0 β ((πΉβπ) β€ 1 β (πΉβ0) β€ 1)) |
259 | 256, 258 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π β β€) β (π = 0 β (πΉβπ) β€ 1)) |
260 | | ostth3.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β βπ β β Β¬ 1 < (πΉβπ)) |
261 | | nnq 12892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β β β π β
β) |
262 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
263 | 2, 261, 262 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ π β β) β (πΉβπ) β β) |
264 | | 1re 11160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ 1 β
β |
265 | | lenlt 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((πΉβπ) β β β§ 1 β β)
β ((πΉβπ) β€ 1 β Β¬ 1 <
(πΉβπ))) |
266 | 263, 264,
265 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π β β) β ((πΉβπ) β€ 1 β Β¬ 1 < (πΉβπ))) |
267 | 266 | ralbidva 3169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β (βπ β β (πΉβπ) β€ 1 β βπ β β Β¬ 1 < (πΉβπ))) |
268 | 260, 267 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β βπ β β (πΉβπ) β€ 1) |
269 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π = π β (πΉβπ) = (πΉβπ)) |
270 | 269 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π = π β ((πΉβπ) β€ 1 β (πΉβπ) β€ 1)) |
271 | 270 | rspccv 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(βπ β
β (πΉβπ) β€ 1 β (π β β β (πΉβπ) β€ 1)) |
272 | 268, 271 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β (π β β β (πΉβπ) β€ 1)) |
273 | 272 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π β β€) β (π β β β (πΉβπ) β€ 1)) |
274 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ (π β β€ β§ -π β β)) β πΉ β π΄) |
275 | 200 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ (π β β€ β§ -π β β)) β π β β) |
276 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(invgβπ) = (invgβπ) |
277 | 11, 13, 276 | abvneg 20307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΉ β π΄ β§ π β β) β (πΉβ((invgβπ)βπ)) = (πΉβπ)) |
278 | 274, 275,
277 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ (π β β€ β§ -π β β)) β (πΉβ((invgβπ)βπ)) = (πΉβπ)) |
279 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π = ((invgβπ)βπ) β (πΉβπ) = (πΉβ((invgβπ)βπ))) |
280 | 279 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π = ((invgβπ)βπ) β ((πΉβπ) β€ 1 β (πΉβ((invgβπ)βπ)) β€ 1)) |
281 | 268 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ (π β β€ β§ -π β β)) β βπ β β (πΉβπ) β€ 1) |
282 | 12 | qrngneg 26987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β β β
((invgβπ)βπ) = -π) |
283 | 275, 282 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ (π β β€ β§ -π β β)) β
((invgβπ)βπ) = -π) |
284 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ (π β β€ β§ -π β β)) β -π β β) |
285 | 283, 284 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ (π β β€ β§ -π β β)) β
((invgβπ)βπ) β β) |
286 | 280, 281,
285 | rspcdva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ (π β β€ β§ -π β β)) β (πΉβ((invgβπ)βπ)) β€ 1) |
287 | 278, 286 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ (π β β€ β§ -π β β)) β (πΉβπ) β€ 1) |
288 | 287 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π β β€) β (-π β β β (πΉβπ) β€ 1)) |
289 | 259, 273,
288 | 3jaod 1429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β β€) β ((π = 0 β¨ π β β β¨ -π β β) β (πΉβπ) β€ 1)) |
290 | 251, 289 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β€) β (πΉβπ) β€ 1) |
291 | 290 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β βπ β β€ (πΉβπ) β€ 1) |
292 | 291 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β βπ β β€ (πΉβπ) β€ 1) |
293 | | rsp 3229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(βπ β
β€ (πΉβπ) β€ 1 β (π β β€ β (πΉβπ) β€ 1)) |
294 | 292, 199,
293 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β€ 1) |
295 | 264 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 1 β
β) |
296 | 161 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β€) |
297 | 19 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 0 < (πΉβπ)) |
298 | | expgt0 14007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((πΉβπ) β β β§ π β β€ β§ 0 < (πΉβπ)) β 0 < ((πΉβπ)βπ)) |
299 | 244, 296,
297, 298 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 0 < ((πΉβπ)βπ)) |
300 | | lemul2 12013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πΉβπ) β β β§ 1 β β β§
(((πΉβπ)βπ) β β β§ 0 < ((πΉβπ)βπ))) β ((πΉβπ) β€ 1 β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (((πΉβπ)βπ) Β· 1))) |
301 | 247, 295,
245, 299, 300 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ) β€ 1 β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (((πΉβπ)βπ) Β· 1))) |
302 | 294, 301 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (((πΉβπ)βπ) Β· 1)) |
303 | 245 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ)βπ) β β) |
304 | 303 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· 1) = ((πΉβπ)βπ)) |
305 | 302, 304 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β€ ((πΉβπ)βπ)) |
306 | 144 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β π β β) |
307 | 306 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β) |
308 | 142 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β
β+) |
309 | 308 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 0 β€ (πΉβπ)) |
310 | 174 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β) |
311 | 310, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β β) |
312 | 195, 311,
136 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β β) |
313 | | max1 13110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (πΉβπ) β€ if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ))) |
314 | 244, 312,
313 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β€ if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ))) |
315 | 314, 134 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β€ π) |
316 | | leexp1a 14086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΉβπ) β β β§ π β β β§ π β β0) β§ (0 β€
(πΉβπ) β§ (πΉβπ) β€ π)) β ((πΉβπ)βπ) β€ (πβπ)) |
317 | 244, 307,
239, 309, 315, 316 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ)βπ) β€ (πβπ)) |
318 | 248, 245,
224, 305, 317 | letrd 11317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (πβπ)) |
319 | 243, 318 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) β€ (πβπ)) |
320 | 11, 13, 235 | abvmul 20302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΉ β π΄ β§ (πβπ) β β β§ π β β) β (πΉβ((πβπ) Β· π)) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
321 | 195, 206,
209, 320 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) = ((πΉβ(πβπ)) Β· (πΉβπ))) |
322 | 12, 11 | qabvexp 26990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉ β π΄ β§ π β β β§ π β β0) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
323 | 195, 311,
239, 322 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
324 | 323 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβ(πβπ)) Β· (πΉβπ)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
325 | 321, 324 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) = (((πΉβπ)βπ) Β· (πΉβπ))) |
326 | 312, 239 | reexpcld 14074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ)βπ) β β) |
327 | 11, 13 | abvcl 20297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
328 | 195, 209,
327 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β β) |
329 | 326, 328 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β β) |
330 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (πΉβπ) = (πΉβπ)) |
331 | 330 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β ((πΉβπ) β€ 1 β (πΉβπ) β€ 1)) |
332 | 331, 292,
207 | rspcdva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β€ 1) |
333 | 310 | nnne0d 12208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β π β 0) |
334 | 195, 311,
333, 138 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 0 < (πΉβπ)) |
335 | | expgt0 14007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((πΉβπ) β β β§ π β β€ β§ 0 < (πΉβπ)) β 0 < ((πΉβπ)βπ)) |
336 | 312, 296,
334, 335 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 0 < ((πΉβπ)βπ)) |
337 | | lemul2 12013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πΉβπ) β β β§ 1 β β β§
(((πΉβπ)βπ) β β β§ 0 < ((πΉβπ)βπ))) β ((πΉβπ) β€ 1 β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (((πΉβπ)βπ) Β· 1))) |
338 | 328, 295,
326, 336, 337 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ) β€ 1 β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (((πΉβπ)βπ) Β· 1))) |
339 | 332, 338 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (((πΉβπ)βπ) Β· 1)) |
340 | 326 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ)βπ) β β) |
341 | 340 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· 1) = ((πΉβπ)βπ)) |
342 | 339, 341 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β€ ((πΉβπ)βπ)) |
343 | 141 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β
β+) |
344 | 343 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β 0 β€ (πΉβπ)) |
345 | | max2 13112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (πΉβπ) β€ if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ))) |
346 | 244, 312,
345 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β€ if((πΉβπ) β€ (πΉβπ), (πΉβπ), (πΉβπ))) |
347 | 346, 134 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβπ) β€ π) |
348 | | leexp1a 14086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΉβπ) β β β§ π β β β§ π β β0) β§ (0 β€
(πΉβπ) β§ (πΉβπ) β€ π)) β ((πΉβπ)βπ) β€ (πβπ)) |
349 | 312, 307,
239, 344, 347, 348 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβπ)βπ) β€ (πβπ)) |
350 | 329, 326,
224, 342, 349 | letrd 11317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πΉβπ)βπ) Β· (πΉβπ)) β€ (πβπ)) |
351 | 325, 350 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ((πβπ) Β· π)) β€ (πβπ)) |
352 | 217, 219,
224, 224, 319, 351 | le2addd 11779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβ((πβπ) Β· π)) + (πΉβ((πβπ) Β· π))) β€ ((πβπ) + (πβπ))) |
353 | 222 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πβπ) β β) |
354 | 353 | 2timesd 12401 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (2 Β· (πβπ)) = ((πβπ) + (πβπ))) |
355 | 354 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (2 Β· (πβπ)) = ((πβπ) + (πβπ))) |
356 | 352, 355 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β ((πΉβ((πβπ) Β· π)) + (πΉβ((πβπ) Β· π))) β€ (2 Β· (πβπ))) |
357 | 215, 220,
226, 232, 356 | letrd 11317 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π))) β€ (2 Β· (πβπ))) |
358 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (1 =
(((πβπ) Β· π) + ((πβπ) Β· π)) β (πΉβ1) = (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π)))) |
359 | 358 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 =
(((πβπ) Β· π) + ((πβπ) Β· π)) β ((πΉβ1) β€ (2 Β· (πβπ)) β (πΉβ(((πβπ) Β· π) + ((πβπ) Β· π))) β€ (2 Β· (πβπ)))) |
360 | 357, 359 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (1 = (((πβπ) Β· π) + ((πβπ) Β· π)) β (πΉβ1) β€ (2 Β· (πβπ)))) |
361 | 194, 360 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ (π β β β§ (π β β€ β§ π β β€))) β (((πβπ) gcd (πβπ)) = (((πβπ) Β· π) + ((πβπ) Β· π)) β (πΉβ1) β€ (2 Β· (πβπ)))) |
362 | 361 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β§ (π β β€ β§ π β β€)) β (((πβπ) gcd (πβπ)) = (((πβπ) Β· π) + ((πβπ) Β· π)) β (πΉβ1) β€ (2 Β· (πβπ)))) |
363 | 362 | rexlimdvva 3202 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (βπ β β€ βπ β β€ ((πβπ) gcd (πβπ)) = (((πβπ) Β· π) + ((πβπ) Β· π)) β (πΉβ1) β€ (2 Β· (πβπ)))) |
364 | 179, 363 | mpd 15 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (πΉβ1) β€ (2 Β· (πβπ))) |
365 | 168, 364 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β 1 β€ (2 Β·
(πβπ))) |
366 | 222 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((πβπ) β β β§ 0 < (πβπ))) |
367 | | ledivmul2 12039 |
. . . . . . . . . . . . . . . . 17
β’ ((1
β β β§ 2 β β β§ ((πβπ) β β β§ 0 < (πβπ))) β ((1 / (πβπ)) β€ 2 β 1 β€ (2 Β· (πβπ)))) |
368 | 264, 132,
366, 367 | mp3an12i 1466 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((1 / (πβπ)) β€ 2 β 1 β€ (2 Β· (πβπ)))) |
369 | 365, 368 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (1 / (πβπ)) β€ 2) |
370 | 163, 369 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((1 / π)βπ) β€ 2) |
371 | | reexpcl 13990 |
. . . . . . . . . . . . . . . 16
β’ (((1 /
π) β β β§
π β
β0) β ((1 / π)βπ) β β) |
372 | 145, 170,
371 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β ((1 / π)βπ) β β) |
373 | | lenlt 11238 |
. . . . . . . . . . . . . . 15
β’ ((((1 /
π)βπ) β β β§ 2 β β)
β (((1 / π)βπ) β€ 2 β Β¬ 2 < ((1
/ π)βπ))) |
374 | 372, 132,
373 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (((1 / π)βπ) β€ 2 β Β¬ 2 < ((1 / π)βπ))) |
375 | 370, 374 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β Β¬ 2 < ((1 /
π)βπ)) |
376 | 375 | pm2.21d 121 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β§ π β β) β (2 < ((1 / π)βπ) β Β¬ (πΉβπ) < 1)) |
377 | 376 | rexlimdva 3149 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β (βπ β β 2 < ((1 / π)βπ) β Β¬ (πΉβπ) < 1)) |
378 | 156, 377 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π β π β§ (πΉβπ) < 1)) β Β¬ (πΉβπ) < 1) |
379 | 378 | expr 458 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β ((πΉβπ) < 1 β Β¬ (πΉβπ) < 1)) |
380 | 379 | pm2.01d 189 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β Β¬ (πΉβπ) < 1) |
381 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π β (πΉβπ) = (πΉβπ)) |
382 | 381 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = π β (1 < (πΉβπ) β 1 < (πΉβπ))) |
383 | 382 | notbid 318 |
. . . . . . . . 9
β’ (π = π β (Β¬ 1 < (πΉβπ) β Β¬ 1 < (πΉβπ))) |
384 | 260 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π) β βπ β β Β¬ 1 < (πΉβπ)) |
385 | 383, 384,
100 | rspcdva 3581 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β Β¬ 1 < (πΉβπ)) |
386 | | lttri3 11243 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ 1 β β)
β ((πΉβπ) = 1 β (Β¬ (πΉβπ) < 1 β§ Β¬ 1 < (πΉβπ)))) |
387 | 137, 264,
386 | sylancl 587 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π) β ((πΉβπ) = 1 β (Β¬ (πΉβπ) < 1 β§ Β¬ 1 < (πΉβπ)))) |
388 | 380, 385,
387 | mpbir2and 712 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π) β (πΉβπ) = 1) |
389 | 109, 131,
388 | 3eqtr4d 2783 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π) β (((π½βπ)βπ)βππ
) = (πΉβπ)) |
390 | 107, 389 | eqtr2d 2774 |
. . . . 5
β’ (((π β§ π β β) β§ π β π) β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ)) |
391 | 390 | ex 414 |
. . . 4
β’ ((π β§ π β β) β (π β π β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ))) |
392 | 98, 391 | pm2.61dne 3028 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = ((π¦ β β β¦ (((π½βπ)βπ¦)βππ
))βπ)) |
393 | 12, 11, 2, 47, 392 | ostthlem2 26992 |
. 2
β’ (π β πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ
))) |
394 | | oveq2 7366 |
. . . 4
β’ (π = π
β (((π½βπ)βπ¦)βππ) = (((π½βπ)βπ¦)βππ
)) |
395 | 394 | mpteq2dv 5208 |
. . 3
β’ (π = π
β (π¦ β β β¦ (((π½βπ)βπ¦)βππ)) = (π¦ β β β¦ (((π½βπ)βπ¦)βππ
))) |
396 | 395 | rspceeqv 3596 |
. 2
β’ ((π
β β+
β§ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ
))) β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |
397 | 44, 393, 396 | syl2anc 585 |
1
β’ (π β βπ β β+ πΉ = (π¦ β β β¦ (((π½βπ)βπ¦)βππ))) |