Step | Hyp | Ref
| Expression |
1 | | stoweidlem42.2 |
. 2
β’
β²π‘π |
2 | | 1red 11163 |
. . . . . . . 8
β’ (π β 1 β
β) |
3 | | stoweidlem42.11 |
. . . . . . . . 9
β’ (π β πΈ β
β+) |
4 | 3 | rpred 12964 |
. . . . . . . 8
β’ (π β πΈ β β) |
5 | 2, 4 | resubcld 11590 |
. . . . . . 7
β’ (π β (1 β πΈ) β
β) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π΅) β (1 β πΈ) β β) |
7 | | stoweidlem42.8 |
. . . . . . . . . 10
β’ (π β π β β) |
8 | 4, 7 | nndivred 12214 |
. . . . . . . . 9
β’ (π β (πΈ / π) β β) |
9 | 2, 8 | resubcld 11590 |
. . . . . . . 8
β’ (π β (1 β (πΈ / π)) β β) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π΅) β (1 β (πΈ / π)) β β) |
11 | 7 | nnnn0d 12480 |
. . . . . . . 8
β’ (π β π β
β0) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π΅) β π β
β0) |
13 | 10, 12 | reexpcld 14075 |
. . . . . 6
β’ ((π β§ π‘ β π΅) β ((1 β (πΈ / π))βπ) β β) |
14 | | elnnuz 12814 |
. . . . . . . . 9
β’ (π β β β π β
(β€β₯β1)) |
15 | 7, 14 | sylib 217 |
. . . . . . . 8
β’ (π β π β
(β€β₯β1)) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π΅) β π β
(β€β₯β1)) |
17 | | stoweidlem42.1 |
. . . . . . . . . . 11
β’
β²ππ |
18 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π‘ β π΅ |
19 | 17, 18 | nfan 1903 |
. . . . . . . . . 10
β’
β²π(π β§ π‘ β π΅) |
20 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π β (1...π) |
21 | 19, 20 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ π‘ β π΅) β§ π β (1...π)) |
22 | | stoweidlem42.6 |
. . . . . . . . . . . . 13
β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
23 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²ππ |
24 | | nfmpt1 5218 |
. . . . . . . . . . . . . 14
β’
β²π(π β (1...π) β¦ ((πβπ)βπ‘)) |
25 | 23, 24 | nfmpt 5217 |
. . . . . . . . . . . . 13
β’
β²π(π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
26 | 22, 25 | nfcxfr 2906 |
. . . . . . . . . . . 12
β’
β²ππΉ |
27 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²ππ‘ |
28 | 26, 27 | nffv 6857 |
. . . . . . . . . . 11
β’
β²π(πΉβπ‘) |
29 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²ππ |
30 | 28, 29 | nffv 6857 |
. . . . . . . . . 10
β’
β²π((πΉβπ‘)βπ) |
31 | 30 | nfel1 2924 |
. . . . . . . . 9
β’
β²π((πΉβπ‘)βπ) β β |
32 | 21, 31 | nfim 1900 |
. . . . . . . 8
β’
β²π(((π β§ π‘ β π΅) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
33 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = π β (π β (1...π) β π β (1...π))) |
34 | 33 | anbi2d 630 |
. . . . . . . . 9
β’ (π = π β (((π β§ π‘ β π΅) β§ π β (1...π)) β ((π β§ π‘ β π΅) β§ π β (1...π)))) |
35 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
36 | 35 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = π β (((πΉβπ‘)βπ) β β β ((πΉβπ‘)βπ) β β)) |
37 | 34, 36 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((((π β§ π‘ β π΅) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) β (((π β§ π‘ β π΅) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β))) |
38 | | stoweidlem42.16 |
. . . . . . . . . . . 12
β’ (π β π΅ β π) |
39 | 38 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π΅) β π‘ β π) |
40 | | ovex 7395 |
. . . . . . . . . . . 12
β’
(1...π) β
V |
41 | | mptexg 7176 |
. . . . . . . . . . . 12
β’
((1...π) β V
β (π β (1...π) β¦ ((πβπ)βπ‘)) β V) |
42 | 40, 41 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π΅) β (π β (1...π) β¦ ((πβπ)βπ‘)) β V) |
43 | 22 | fvmpt2 6964 |
. . . . . . . . . . 11
β’ ((π‘ β π β§ (π β (1...π) β¦ ((πβπ)βπ‘)) β V) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
44 | 39, 42, 43 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π΅) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
45 | | stoweidlem42.9 |
. . . . . . . . . . . . . 14
β’ (π β π:(1...π)βΆπ) |
46 | 45 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
47 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β π) |
48 | 47, 46 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (π β§ (πβπ) β π)) |
49 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (π β π β (πβπ) β π)) |
50 | 49 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β ((π β§ π β π) β (π β§ (πβπ) β π))) |
51 | | feq1 6654 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (π:πβΆβ β (πβπ):πβΆβ)) |
52 | 50, 51 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (((π β§ π β π) β π:πβΆβ) β ((π β§ (πβπ) β π) β (πβπ):πβΆβ))) |
53 | | stoweidlem42.13 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π:πβΆβ) |
54 | 52, 53 | vtoclg 3528 |
. . . . . . . . . . . . 13
β’ ((πβπ) β π β ((π β§ (πβπ) β π) β (πβπ):πβΆβ)) |
55 | 46, 48, 54 | sylc 65 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (πβπ):πβΆβ) |
56 | 55 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β (πβπ):πβΆβ) |
57 | 39 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β π‘ β π) |
58 | 56, 57 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β ((πβπ)βπ‘) β β) |
59 | 44, 58 | fvmpt2d 6966 |
. . . . . . . . 9
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
60 | 59, 58 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
61 | 32, 37, 60 | chvarfv 2234 |
. . . . . . 7
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
62 | | remulcl 11143 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π Β· π) β β) |
63 | 62 | adantl 483 |
. . . . . . 7
β’ (((π β§ π‘ β π΅) β§ (π β β β§ π β β)) β (π Β· π) β β) |
64 | 16, 61, 63 | seqcl 13935 |
. . . . . 6
β’ ((π β§ π‘ β π΅) β (seq1( Β· , (πΉβπ‘))βπ) β β) |
65 | 3 | rpcnd 12966 |
. . . . . . . . . . . 12
β’ (π β πΈ β β) |
66 | 7 | nncnd 12176 |
. . . . . . . . . . . 12
β’ (π β π β β) |
67 | 7 | nnne0d 12210 |
. . . . . . . . . . . 12
β’ (π β π β 0) |
68 | 65, 66, 67 | divcan1d 11939 |
. . . . . . . . . . 11
β’ (π β ((πΈ / π) Β· π) = πΈ) |
69 | 68 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β πΈ = ((πΈ / π) Β· π)) |
70 | 69 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β (1 β πΈ) = (1 β ((πΈ / π) Β· π))) |
71 | | 1cnd 11157 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
72 | 65, 66, 67 | divcld 11938 |
. . . . . . . . . . 11
β’ (π β (πΈ / π) β β) |
73 | 72, 66 | mulcld 11182 |
. . . . . . . . . 10
β’ (π β ((πΈ / π) Β· π) β β) |
74 | 71, 73 | negsubd 11525 |
. . . . . . . . 9
β’ (π β (1 + -((πΈ / π) Β· π)) = (1 β ((πΈ / π) Β· π))) |
75 | 72, 66 | mulneg1d 11615 |
. . . . . . . . . . 11
β’ (π β (-(πΈ / π) Β· π) = -((πΈ / π) Β· π)) |
76 | 75 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β -((πΈ / π) Β· π) = (-(πΈ / π) Β· π)) |
77 | 76 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β (1 + -((πΈ / π) Β· π)) = (1 + (-(πΈ / π) Β· π))) |
78 | 70, 74, 77 | 3eqtr2d 2783 |
. . . . . . . 8
β’ (π β (1 β πΈ) = (1 + (-(πΈ / π) Β· π))) |
79 | 8 | renegcld 11589 |
. . . . . . . . . 10
β’ (π β -(πΈ / π) β β) |
80 | 7 | nnred 12175 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
81 | | 3re 12240 |
. . . . . . . . . . . . . . . . . 18
β’ 3 β
β |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β 3 β
β) |
83 | | 3ne0 12266 |
. . . . . . . . . . . . . . . . . 18
β’ 3 β
0 |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β 3 β 0) |
85 | 82, 84 | rereccld 11989 |
. . . . . . . . . . . . . . . 16
β’ (π β (1 / 3) β
β) |
86 | | stoweidlem42.12 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ < (1 / 3)) |
87 | | 1lt3 12333 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 <
3 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 1 < 3) |
89 | | 0lt1 11684 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 <
1 |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 < 1) |
91 | | 3pos 12265 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 <
3 |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 < 3) |
93 | | ltdiv2 12048 |
. . . . . . . . . . . . . . . . . . 19
β’ (((1
β β β§ 0 < 1) β§ (3 β β β§ 0 < 3) β§ (1
β β β§ 0 < 1)) β (1 < 3 β (1 / 3) < (1 /
1))) |
94 | 2, 90, 82, 92, 2, 90, 93 | syl222anc 1387 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1 < 3 β (1 / 3)
< (1 / 1))) |
95 | 88, 94 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1 / 3) < (1 /
1)) |
96 | | 1div1e1 11852 |
. . . . . . . . . . . . . . . . 17
β’ (1 / 1) =
1 |
97 | 95, 96 | breqtrdi 5151 |
. . . . . . . . . . . . . . . 16
β’ (π β (1 / 3) <
1) |
98 | 4, 85, 2, 86, 97 | lttrd 11323 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ < 1) |
99 | 7 | nnge1d 12208 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β€ π) |
100 | 4, 2, 80, 98, 99 | ltletrd 11322 |
. . . . . . . . . . . . . 14
β’ (π β πΈ < π) |
101 | 4, 80, 100 | ltled 11310 |
. . . . . . . . . . . . 13
β’ (π β πΈ β€ π) |
102 | 3 | rpregt0d 12970 |
. . . . . . . . . . . . . 14
β’ (π β (πΈ β β β§ 0 < πΈ)) |
103 | 7 | nngt0d 12209 |
. . . . . . . . . . . . . 14
β’ (π β 0 < π) |
104 | | lediv2 12052 |
. . . . . . . . . . . . . 14
β’ (((πΈ β β β§ 0 <
πΈ) β§ (π β β β§ 0 < π) β§ (πΈ β β β§ 0 < πΈ)) β (πΈ β€ π β (πΈ / π) β€ (πΈ / πΈ))) |
105 | 102, 80, 103, 102, 104 | syl121anc 1376 |
. . . . . . . . . . . . 13
β’ (π β (πΈ β€ π β (πΈ / π) β€ (πΈ / πΈ))) |
106 | 101, 105 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (πΈ / π) β€ (πΈ / πΈ)) |
107 | 3 | rpcnne0d 12973 |
. . . . . . . . . . . . 13
β’ (π β (πΈ β β β§ πΈ β 0)) |
108 | | divid 11849 |
. . . . . . . . . . . . 13
β’ ((πΈ β β β§ πΈ β 0) β (πΈ / πΈ) = 1) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (πΈ / πΈ) = 1) |
110 | 106, 109 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (π β (πΈ / π) β€ 1) |
111 | 8, 2 | lenegd 11741 |
. . . . . . . . . . 11
β’ (π β ((πΈ / π) β€ 1 β -1 β€ -(πΈ / π))) |
112 | 110, 111 | mpbid 231 |
. . . . . . . . . 10
β’ (π β -1 β€ -(πΈ / π)) |
113 | | bernneq 14139 |
. . . . . . . . . 10
β’ ((-(πΈ / π) β β β§ π β β0 β§ -1 β€
-(πΈ / π)) β (1 + (-(πΈ / π) Β· π)) β€ ((1 + -(πΈ / π))βπ)) |
114 | 79, 11, 112, 113 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (1 + (-(πΈ / π) Β· π)) β€ ((1 + -(πΈ / π))βπ)) |
115 | 71, 72 | negsubd 11525 |
. . . . . . . . . 10
β’ (π β (1 + -(πΈ / π)) = (1 β (πΈ / π))) |
116 | 115 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β ((1 + -(πΈ / π))βπ) = ((1 β (πΈ / π))βπ)) |
117 | 114, 116 | breqtrd 5136 |
. . . . . . . 8
β’ (π β (1 + (-(πΈ / π) Β· π)) β€ ((1 β (πΈ / π))βπ)) |
118 | 78, 117 | eqbrtrd 5132 |
. . . . . . 7
β’ (π β (1 β πΈ) β€ ((1 β (πΈ / π))βπ)) |
119 | 118 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π΅) β (1 β πΈ) β€ ((1 β (πΈ / π))βπ)) |
120 | | eqid 2737 |
. . . . . . 7
β’ seq1(
Β· , (πΉβπ‘)) = seq1( Β· , (πΉβπ‘)) |
121 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π΅) β π β β) |
122 | | eqid 2737 |
. . . . . . . . 9
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) = (π β (1...π) β¦ ((πβπ)βπ‘)) |
123 | 19, 58, 122 | fmptdf 7070 |
. . . . . . . 8
β’ ((π β§ π‘ β π΅) β (π β (1...π) β¦ ((πβπ)βπ‘)):(1...π)βΆβ) |
124 | 44 | feq1d 6658 |
. . . . . . . 8
β’ ((π β§ π‘ β π΅) β ((πΉβπ‘):(1...π)βΆβ β (π β (1...π) β¦ ((πβπ)βπ‘)):(1...π)βΆβ)) |
125 | 123, 124 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π‘ β π΅) β (πΉβπ‘):(1...π)βΆβ) |
126 | | stoweidlem42.10 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((πβπ)βπ‘)) |
127 | 126 | r19.21bi 3237 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β π΅) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) |
128 | 127 | an32s 651 |
. . . . . . . 8
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) |
129 | 128, 59 | breqtrrd 5138 |
. . . . . . 7
β’ (((π β§ π‘ β π΅) β§ π β (1...π)) β (1 β (πΈ / π)) < ((πΉβπ‘)βπ)) |
130 | 72 | addid2d 11363 |
. . . . . . . . . . 11
β’ (π β (0 + (πΈ / π)) = (πΈ / π)) |
131 | | lediv2 12052 |
. . . . . . . . . . . . . . 15
β’ (((1
β β β§ 0 < 1) β§ (π β β β§ 0 < π) β§ (πΈ β β β§ 0 < πΈ)) β (1 β€ π β (πΈ / π) β€ (πΈ / 1))) |
132 | 2, 90, 80, 103, 102, 131 | syl221anc 1382 |
. . . . . . . . . . . . . 14
β’ (π β (1 β€ π β (πΈ / π) β€ (πΈ / 1))) |
133 | 99, 132 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (πΈ / π) β€ (πΈ / 1)) |
134 | 65 | div1d 11930 |
. . . . . . . . . . . . 13
β’ (π β (πΈ / 1) = πΈ) |
135 | 133, 134 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (π β (πΈ / π) β€ πΈ) |
136 | 8, 4, 2, 135, 98 | lelttrd 11320 |
. . . . . . . . . . 11
β’ (π β (πΈ / π) < 1) |
137 | 130, 136 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ (π β (0 + (πΈ / π)) < 1) |
138 | | 0red 11165 |
. . . . . . . . . . 11
β’ (π β 0 β
β) |
139 | 138, 8, 2 | ltaddsubd 11762 |
. . . . . . . . . 10
β’ (π β ((0 + (πΈ / π)) < 1 β 0 < (1 β (πΈ / π)))) |
140 | 137, 139 | mpbid 231 |
. . . . . . . . 9
β’ (π β 0 < (1 β (πΈ / π))) |
141 | 9, 140 | elrpd 12961 |
. . . . . . . 8
β’ (π β (1 β (πΈ / π)) β
β+) |
142 | 141 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π΅) β (1 β (πΈ / π)) β
β+) |
143 | 28, 19, 120, 121, 125, 129, 142 | stoweidlem3 44318 |
. . . . . 6
β’ ((π β§ π‘ β π΅) β ((1 β (πΈ / π))βπ) < (seq1( Β· , (πΉβπ‘))βπ)) |
144 | 6, 13, 64, 119, 143 | lelttrd 11320 |
. . . . 5
β’ ((π β§ π‘ β π΅) β (1 β πΈ) < (seq1( Β· , (πΉβπ‘))βπ)) |
145 | | stoweidlem42.7 |
. . . . . . 7
β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) |
146 | 145 | fvmpt2 6964 |
. . . . . 6
β’ ((π‘ β π β§ (seq1( Β· , (πΉβπ‘))βπ) β β) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
147 | 39, 64, 146 | syl2anc 585 |
. . . . 5
β’ ((π β§ π‘ β π΅) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
148 | 144, 147 | breqtrrd 5138 |
. . . 4
β’ ((π β§ π‘ β π΅) β (1 β πΈ) < (πβπ‘)) |
149 | | simpl 484 |
. . . . 5
β’ ((π β§ π‘ β π΅) β π) |
150 | | stoweidlem42.3 |
. . . . . 6
β’
β²π‘π |
151 | | stoweidlem42.4 |
. . . . . 6
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
152 | | stoweidlem42.5 |
. . . . . 6
β’ π = (seq1(π, π)βπ) |
153 | | stoweidlem42.15 |
. . . . . 6
β’ (π β π β V) |
154 | | stoweidlem42.14 |
. . . . . 6
β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
155 | 17, 150, 151, 152, 22, 145, 153, 7, 45, 53, 154 | fmuldfeq 43898 |
. . . . 5
β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) |
156 | 149, 39, 155 | syl2anc 585 |
. . . 4
β’ ((π β§ π‘ β π΅) β (πβπ‘) = (πβπ‘)) |
157 | 148, 156 | breqtrrd 5138 |
. . 3
β’ ((π β§ π‘ β π΅) β (1 β πΈ) < (πβπ‘)) |
158 | 157 | ex 414 |
. 2
β’ (π β (π‘ β π΅ β (1 β πΈ) < (πβπ‘))) |
159 | 1, 158 | ralrimi 3243 |
1
β’ (π β βπ‘ β π΅ (1 β πΈ) < (πβπ‘)) |