Step | Hyp | Ref
| Expression |
1 | | nnuz 12814 |
. . . . 5
β’ β =
(β€β₯β1) |
2 | | 1zzd 12542 |
. . . . 5
β’ (π β 1 β
β€) |
3 | | stoweidlem7.7 |
. . . . 5
β’ (π β πΈ β
β+) |
4 | | stoweidlem7.2 |
. . . . . 6
β’ πΊ = (π β β0 β¦ (π΅βπ)) |
5 | | oveq2 7369 |
. . . . . 6
β’ (π = π β (π΅βπ) = (π΅βπ)) |
6 | | nnnn0 12428 |
. . . . . . 7
β’ (π β β β π β
β0) |
7 | 6 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β π β β0) |
8 | | stoweidlem7.5 |
. . . . . . . . 9
β’ (π β π΅ β
β+) |
9 | 8 | rpcnd 12967 |
. . . . . . . 8
β’ (π β π΅ β β) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π΅ β β) |
11 | 10, 7 | expcld 14060 |
. . . . . 6
β’ ((π β§ π β β) β (π΅βπ) β β) |
12 | 4, 5, 7, 11 | fvmptd3 6975 |
. . . . 5
β’ ((π β§ π β β) β (πΊβπ) = (π΅βπ)) |
13 | | 1red 11164 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
14 | 13 | renegcld 11590 |
. . . . . . . . 9
β’ (π β -1 β
β) |
15 | | 0red 11166 |
. . . . . . . . 9
β’ (π β 0 β
β) |
16 | 8 | rpred 12965 |
. . . . . . . . 9
β’ (π β π΅ β β) |
17 | | neg1lt0 12278 |
. . . . . . . . . 10
β’ -1 <
0 |
18 | 17 | a1i 11 |
. . . . . . . . 9
β’ (π β -1 <
0) |
19 | 8 | rpgt0d 12968 |
. . . . . . . . 9
β’ (π β 0 < π΅) |
20 | 14, 15, 16, 18, 19 | lttrd 11324 |
. . . . . . . 8
β’ (π β -1 < π΅) |
21 | | stoweidlem7.6 |
. . . . . . . 8
β’ (π β π΅ < 1) |
22 | 16, 13 | absltd 15323 |
. . . . . . . 8
β’ (π β ((absβπ΅) < 1 β (-1 < π΅ β§ π΅ < 1))) |
23 | 20, 21, 22 | mpbir2and 712 |
. . . . . . 7
β’ (π β (absβπ΅) < 1) |
24 | 9, 23 | expcnv 15757 |
. . . . . 6
β’ (π β (π β β0 β¦ (π΅βπ)) β 0) |
25 | 4, 24 | eqbrtrid 5144 |
. . . . 5
β’ (π β πΊ β 0) |
26 | 1, 2, 3, 12, 25 | climi 15401 |
. . . 4
β’ (π β βπ β β βπ β (β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) |
27 | | r19.26 3111 |
. . . . . . . . . . . . . 14
β’
(βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ) β (βπ β (β€β₯βπ)(π΅βπ) β β β§ βπ β
(β€β₯βπ)(absβ((π΅βπ) β 0)) < πΈ)) |
28 | 27 | simprbi 498 |
. . . . . . . . . . . . 13
β’
(βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ) β βπ β (β€β₯βπ)(absβ((π΅βπ) β 0)) < πΈ) |
29 | 28 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β βπ β
(β€β₯βπ)(absβ((π΅βπ) β 0)) < πΈ) |
30 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΅βπ) = (π΅βπ)) |
31 | 30 | oveq1d 7376 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π΅βπ) β 0) = ((π΅βπ) β 0)) |
32 | 31 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π = π β (absβ((π΅βπ) β 0)) = (absβ((π΅βπ) β 0))) |
33 | 32 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (π = π β ((absβ((π΅βπ) β 0)) < πΈ β (absβ((π΅βπ) β 0)) < πΈ)) |
34 | 33 | rspccva 3582 |
. . . . . . . . . . . 12
β’
((βπ β
(β€β₯βπ)(absβ((π΅βπ) β 0)) < πΈ β§ π β (β€β₯βπ)) β (absβ((π΅βπ) β 0)) < πΈ) |
35 | 29, 34 | sylancom 589 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β (absβ((π΅βπ) β 0)) < πΈ) |
36 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π) |
37 | 36, 8 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π΅ β
β+) |
38 | 37 | rpred 12965 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π΅ β β) |
39 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π β β) |
40 | | nnnn0 12428 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β0) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π β β0) |
42 | | eluznn0 12850 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π β
(β€β₯βπ)) β π β β0) |
43 | 41, 42 | sylancom 589 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π β β0) |
44 | 38, 43 | reexpcld 14077 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β (π΅βπ) β β) |
45 | | rpre 12931 |
. . . . . . . . . . . . 13
β’ (πΈ β β+
β πΈ β
β) |
46 | 36, 3, 45 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β πΈ β β) |
47 | | recn 11149 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅βπ) β β β (π΅βπ) β β) |
48 | 47 | subid1d 11509 |
. . . . . . . . . . . . . . . 16
β’ ((π΅βπ) β β β ((π΅βπ) β 0) = (π΅βπ)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π΅βπ) β β β§ πΈ β β) β ((π΅βπ) β 0) = (π΅βπ)) |
50 | 49 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (((π΅βπ) β β β§ πΈ β β) β (absβ((π΅βπ) β 0)) = (absβ(π΅βπ))) |
51 | 50 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (((π΅βπ) β β β§ πΈ β β) β ((absβ((π΅βπ) β 0)) < πΈ β (absβ(π΅βπ)) < πΈ)) |
52 | | abslt 15208 |
. . . . . . . . . . . . 13
β’ (((π΅βπ) β β β§ πΈ β β) β ((absβ(π΅βπ)) < πΈ β (-πΈ < (π΅βπ) β§ (π΅βπ) < πΈ))) |
53 | 51, 52 | bitrd 279 |
. . . . . . . . . . . 12
β’ (((π΅βπ) β β β§ πΈ β β) β ((absβ((π΅βπ) β 0)) < πΈ β (-πΈ < (π΅βπ) β§ (π΅βπ) < πΈ))) |
54 | 44, 46, 53 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β ((absβ((π΅βπ) β 0)) < πΈ β (-πΈ < (π΅βπ) β§ (π΅βπ) < πΈ))) |
55 | 35, 54 | mpbid 231 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β (-πΈ < (π΅βπ) β§ (π΅βπ) < πΈ)) |
56 | 55 | simprd 497 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β (π΅βπ) < πΈ) |
57 | | eluznn 12851 |
. . . . . . . . . . 11
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
58 | 39, 57 | sylancom 589 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β π β β) |
59 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π΅ β β) |
60 | | nnnn0 12428 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
61 | 60 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β0) |
62 | 59, 61 | reexpcld 14077 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π΅βπ) β β) |
63 | 3 | rpred 12965 |
. . . . . . . . . . . 12
β’ (π β πΈ β β) |
64 | 63 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΈ β β) |
65 | | 1red 11164 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 1 β
β) |
66 | 62, 64, 65 | ltsub2d 11773 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π΅βπ) < πΈ β (1 β πΈ) < (1 β (π΅βπ)))) |
67 | 36, 58, 66 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β ((π΅βπ) < πΈ β (1 β πΈ) < (1 β (π΅βπ)))) |
68 | 56, 67 | mpbid 231 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β§ π β (β€β₯βπ)) β (1 β πΈ) < (1 β (π΅βπ))) |
69 | 68 | ralrimiva 3140 |
. . . . . . 7
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ))) |
70 | 30 | oveq2d 7377 |
. . . . . . . . 9
β’ (π = π β (1 β (π΅βπ)) = (1 β (π΅βπ))) |
71 | 70 | breq2d 5121 |
. . . . . . . 8
β’ (π = π β ((1 β πΈ) < (1 β (π΅βπ)) β (1 β πΈ) < (1 β (π΅βπ)))) |
72 | 71 | cbvralvw 3224 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ)) β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ))) |
73 | 69, 72 | sylibr 233 |
. . . . . 6
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ)) β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ))) |
74 | 73 | ex 414 |
. . . . 5
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ) β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ)))) |
75 | 74 | reximdva 3162 |
. . . 4
β’ (π β (βπ β β βπ β (β€β₯βπ)((π΅βπ) β β β§ (absβ((π΅βπ) β 0)) < πΈ) β βπ β β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ)))) |
76 | 26, 75 | mpd 15 |
. . 3
β’ (π β βπ β β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ))) |
77 | | stoweidlem7.1 |
. . . . . 6
β’ πΉ = (π β β0 β¦ ((1 /
π΄)βπ)) |
78 | | oveq2 7369 |
. . . . . 6
β’ (π = π β ((1 / π΄)βπ) = ((1 / π΄)βπ)) |
79 | | stoweidlem7.3 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
80 | 79 | recnd 11191 |
. . . . . . . . 9
β’ (π β π΄ β β) |
81 | | 0lt1 11685 |
. . . . . . . . . . . 12
β’ 0 <
1 |
82 | 81 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 0 < 1) |
83 | | stoweidlem7.4 |
. . . . . . . . . . 11
β’ (π β 1 < π΄) |
84 | 15, 13, 79, 82, 83 | lttrd 11324 |
. . . . . . . . . 10
β’ (π β 0 < π΄) |
85 | 84 | gt0ne0d 11727 |
. . . . . . . . 9
β’ (π β π΄ β 0) |
86 | 80, 85 | reccld 11932 |
. . . . . . . 8
β’ (π β (1 / π΄) β β) |
87 | 86 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β (1 / π΄) β
β) |
88 | 87, 7 | expcld 14060 |
. . . . . 6
β’ ((π β§ π β β) β ((1 / π΄)βπ) β β) |
89 | 77, 78, 7, 88 | fvmptd3 6975 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ) = ((1 / π΄)βπ)) |
90 | 79, 85 | rereccld 11990 |
. . . . . . . . 9
β’ (π β (1 / π΄) β β) |
91 | 79, 84 | recgt0d 12097 |
. . . . . . . . 9
β’ (π β 0 < (1 / π΄)) |
92 | 14, 15, 90, 18, 91 | lttrd 11324 |
. . . . . . . 8
β’ (π β -1 < (1 / π΄)) |
93 | | ltdiv23 12054 |
. . . . . . . . . . 11
β’ ((1
β β β§ (π΄
β β β§ 0 < π΄) β§ (1 β β β§ 0 < 1))
β ((1 / π΄) < 1
β (1 / 1) < π΄)) |
94 | 13, 79, 84, 13, 82, 93 | syl122anc 1380 |
. . . . . . . . . 10
β’ (π β ((1 / π΄) < 1 β (1 / 1) < π΄)) |
95 | | 1cnd 11158 |
. . . . . . . . . . . 12
β’ (π β 1 β
β) |
96 | 95 | div1d 11931 |
. . . . . . . . . . 11
β’ (π β (1 / 1) =
1) |
97 | 96 | breq1d 5119 |
. . . . . . . . . 10
β’ (π β ((1 / 1) < π΄ β 1 < π΄)) |
98 | 94, 97 | bitrd 279 |
. . . . . . . . 9
β’ (π β ((1 / π΄) < 1 β 1 < π΄)) |
99 | 83, 98 | mpbird 257 |
. . . . . . . 8
β’ (π β (1 / π΄) < 1) |
100 | 90, 13 | absltd 15323 |
. . . . . . . 8
β’ (π β ((absβ(1 / π΄)) < 1 β (-1 < (1 /
π΄) β§ (1 / π΄) < 1))) |
101 | 92, 99, 100 | mpbir2and 712 |
. . . . . . 7
β’ (π β (absβ(1 / π΄)) < 1) |
102 | 86, 101 | expcnv 15757 |
. . . . . 6
β’ (π β (π β β0 β¦ ((1 /
π΄)βπ)) β 0) |
103 | 77, 102 | eqbrtrid 5144 |
. . . . 5
β’ (π β πΉ β 0) |
104 | 1, 2, 3, 89, 103 | climi2 15402 |
. . . 4
β’ (π β βπ β β βπ β (β€β₯βπ)(absβ(((1 / π΄)βπ) β 0)) < πΈ) |
105 | | simpll 766 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π) |
106 | | uznnssnn 12828 |
. . . . . . . . 9
β’ (π β β β
(β€β₯βπ) β β) |
107 | 106 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β
(β€β₯βπ) β β) |
108 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
109 | 107, 108 | sseldd 3949 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β) |
110 | 88 | subid1d 11509 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((1 / π΄)βπ) β 0) = ((1 / π΄)βπ)) |
111 | 110 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (absβ(((1 /
π΄)βπ) β 0)) = (absβ((1 / π΄)βπ))) |
112 | 90 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (1 / π΄) β
β) |
113 | 112, 7 | reexpcld 14077 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((1 / π΄)βπ) β β) |
114 | 15, 90, 91 | ltled 11311 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ (1 / π΄)) |
115 | 114 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 0 β€ (1 / π΄)) |
116 | 112, 7, 115 | expge0d 14078 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 β€ ((1 / π΄)βπ)) |
117 | 113, 116 | absidd 15316 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (absβ((1 /
π΄)βπ)) = ((1 / π΄)βπ)) |
118 | 111, 117 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β β) β (absβ(((1 /
π΄)βπ) β 0)) = ((1 / π΄)βπ)) |
119 | 118 | breq1d 5119 |
. . . . . . . 8
β’ ((π β§ π β β) β ((absβ(((1 /
π΄)βπ) β 0)) < πΈ β ((1 / π΄)βπ) < πΈ)) |
120 | 119 | biimpd 228 |
. . . . . . 7
β’ ((π β§ π β β) β ((absβ(((1 /
π΄)βπ) β 0)) < πΈ β ((1 / π΄)βπ) < πΈ)) |
121 | 105, 109,
120 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((absβ(((1 /
π΄)βπ) β 0)) < πΈ β ((1 / π΄)βπ) < πΈ)) |
122 | 121 | ralimdva 3161 |
. . . . 5
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)(absβ(((1 / π΄)βπ) β 0)) < πΈ β βπ β (β€β₯βπ)((1 / π΄)βπ) < πΈ)) |
123 | 122 | reximdva 3162 |
. . . 4
β’ (π β (βπ β β βπ β (β€β₯βπ)(absβ(((1 / π΄)βπ) β 0)) < πΈ β βπ β β βπ β (β€β₯βπ)((1 / π΄)βπ) < πΈ)) |
124 | 104, 123 | mpd 15 |
. . 3
β’ (π β βπ β β βπ β (β€β₯βπ)((1 / π΄)βπ) < πΈ) |
125 | 1 | rexanuz2 15243 |
. . 3
β’
(βπ β
β βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ) β (βπ β β βπ β (β€β₯βπ)(1 β πΈ) < (1 β (π΅βπ)) β§ βπ β β βπ β (β€β₯βπ)((1 / π΄)βπ) < πΈ)) |
126 | 76, 124, 125 | sylanbrc 584 |
. 2
β’ (π β βπ β β βπ β (β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) |
127 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) β βπ β (β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) |
128 | | nnz 12528 |
. . . . . . . 8
β’ (π β β β π β
β€) |
129 | | uzid 12786 |
. . . . . . . 8
β’ (π β β€ β π β
(β€β₯βπ)) |
130 | 128, 129 | syl 17 |
. . . . . . 7
β’ (π β β β π β
(β€β₯βπ)) |
131 | 130 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) β π β (β€β₯βπ)) |
132 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = π β (π΅βπ) = (π΅βπ)) |
133 | 132 | oveq2d 7377 |
. . . . . . . . 9
β’ (π = π β (1 β (π΅βπ)) = (1 β (π΅βπ))) |
134 | 133 | breq2d 5121 |
. . . . . . . 8
β’ (π = π β ((1 β πΈ) < (1 β (π΅βπ)) β (1 β πΈ) < (1 β (π΅βπ)))) |
135 | | oveq2 7369 |
. . . . . . . . 9
β’ (π = π β ((1 / π΄)βπ) = ((1 / π΄)βπ)) |
136 | 135 | breq1d 5119 |
. . . . . . . 8
β’ (π = π β (((1 / π΄)βπ) < πΈ β ((1 / π΄)βπ) < πΈ)) |
137 | 134, 136 | anbi12d 632 |
. . . . . . 7
β’ (π = π β (((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ) β ((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ))) |
138 | 137 | rspccva 3582 |
. . . . . 6
β’
((βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ) β§ π β (β€β₯βπ)) β ((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) |
139 | 127, 131,
138 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) β ((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) |
140 | | 1cnd 11158 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 1 β
β) |
141 | 80, 85 | jca 513 |
. . . . . . . . . . 11
β’ (π β (π΄ β β β§ π΄ β 0)) |
142 | 141 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π΄ β β β§ π΄ β 0)) |
143 | 40 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β0) |
144 | | expdiv 14028 |
. . . . . . . . . 10
β’ ((1
β β β§ (π΄
β β β§ π΄ β
0) β§ π β
β0) β ((1 / π΄)βπ) = ((1βπ) / (π΄βπ))) |
145 | 140, 142,
143, 144 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((1 / π΄)βπ) = ((1βπ) / (π΄βπ))) |
146 | 128 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β€) |
147 | | 1exp 14006 |
. . . . . . . . . . 11
β’ (π β β€ β
(1βπ) =
1) |
148 | 146, 147 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1βπ) = 1) |
149 | 148 | oveq1d 7376 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((1βπ) / (π΄βπ)) = (1 / (π΄βπ))) |
150 | 145, 149 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β β) β ((1 / π΄)βπ) = (1 / (π΄βπ))) |
151 | 150 | breq1d 5119 |
. . . . . . 7
β’ ((π β§ π β β) β (((1 / π΄)βπ) < πΈ β (1 / (π΄βπ)) < πΈ)) |
152 | 151 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) β (((1 / π΄)βπ) < πΈ β (1 / (π΄βπ)) < πΈ)) |
153 | 152 | anbi2d 630 |
. . . . 5
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) β (((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ) β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ))) |
154 | 139, 153 | mpbid 231 |
. . . 4
β’ (((π β§ π β β) β§ βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ)) β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ)) |
155 | 154 | ex 414 |
. . 3
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ) β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ))) |
156 | 155 | reximdva 3162 |
. 2
β’ (π β (βπ β β βπ β (β€β₯βπ)((1 β πΈ) < (1 β (π΅βπ)) β§ ((1 / π΄)βπ) < πΈ) β βπ β β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ))) |
157 | 126, 156 | mpd 15 |
1
β’ (π β βπ β β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ)) |