Step | Hyp | Ref
| Expression |
1 | | stoweidlem51.5 |
. . . 4
β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
2 | | ssrab2 4038 |
. . . 4
β’ {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β π΄ |
3 | 1, 2 | eqsstri 3979 |
. . 3
β’ π β π΄ |
4 | | stoweidlem51.6 |
. . . 4
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
5 | | stoweidlem51.7 |
. . . 4
β’ π = (seq1(π, π)βπ) |
6 | | 1zzd 12539 |
. . . . 5
β’ (π β 1 β
β€) |
7 | | stoweidlem51.10 |
. . . . . 6
β’ (π β π β β) |
8 | 7 | nnzd 12531 |
. . . . 5
β’ (π β π β β€) |
9 | 7 | nnge1d 12206 |
. . . . 5
β’ (π β 1 β€ π) |
10 | 7 | nnred 12173 |
. . . . . 6
β’ (π β π β β) |
11 | 10 | leidd 11726 |
. . . . 5
β’ (π β π β€ π) |
12 | 6, 8, 8, 9, 11 | elfzd 13438 |
. . . 4
β’ (π β π β (1...π)) |
13 | | stoweidlem51.12 |
. . . 4
β’ (π β π:(1...π)βΆπ) |
14 | | stoweidlem51.2 |
. . . . 5
β’
β²π‘π |
15 | | eqid 2733 |
. . . . 5
β’ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
16 | | stoweidlem51.20 |
. . . . 5
β’ ((π β§ π β π΄) β π:πβΆβ) |
17 | | stoweidlem51.19 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
18 | 14, 1, 15, 16, 17 | stoweidlem16 44343 |
. . . 4
β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
19 | | stoweidlem51.21 |
. . . 4
β’ (π β π β V) |
20 | 4, 5, 12, 13, 18, 19 | fmulcl 43908 |
. . 3
β’ (π β π β π) |
21 | 3, 20 | sselid 3943 |
. 2
β’ (π β π β π΄) |
22 | 1 | eleq2i 2826 |
. . . . . . 7
β’ (π β π β π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
23 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²β1 |
24 | | nfrab1 3425 |
. . . . . . . . . . . . . 14
β’
β²β{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
25 | 1, 24 | nfcxfr 2902 |
. . . . . . . . . . . . 13
β’
β²βπ |
26 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²β(π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
27 | 25, 25, 26 | nfmpo 7440 |
. . . . . . . . . . . 12
β’
β²β(π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
28 | 4, 27 | nfcxfr 2902 |
. . . . . . . . . . 11
β’
β²βπ |
29 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²βπ |
30 | 23, 28, 29 | nfseq 13922 |
. . . . . . . . . 10
β’
β²βseq1(π, π) |
31 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²βπ |
32 | 30, 31 | nffv 6853 |
. . . . . . . . 9
β’
β²β(seq1(π, π)βπ) |
33 | 5, 32 | nfcxfr 2902 |
. . . . . . . 8
β’
β²βπ |
34 | | nfcv 2904 |
. . . . . . . 8
β’
β²βπ΄ |
35 | | nfcv 2904 |
. . . . . . . . 9
β’
β²βπ |
36 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²β0 |
37 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²β
β€ |
38 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²βπ‘ |
39 | 33, 38 | nffv 6853 |
. . . . . . . . . . 11
β’
β²β(πβπ‘) |
40 | 36, 37, 39 | nfbr 5153 |
. . . . . . . . . 10
β’
β²β0 β€ (πβπ‘) |
41 | 39, 37, 23 | nfbr 5153 |
. . . . . . . . . 10
β’
β²β(πβπ‘) β€ 1 |
42 | 40, 41 | nfan 1903 |
. . . . . . . . 9
β’
β²β(0 β€
(πβπ‘) β§ (πβπ‘) β€ 1) |
43 | 35, 42 | nfralw 3293 |
. . . . . . . 8
β’
β²ββπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) |
44 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π‘1 |
45 | | nfra1 3266 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
46 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘π΄ |
47 | 45, 46 | nfrabw 3439 |
. . . . . . . . . . . . . . . 16
β’
β²π‘{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
48 | 1, 47 | nfcxfr 2902 |
. . . . . . . . . . . . . . 15
β’
β²π‘π |
49 | | nfmpt1 5214 |
. . . . . . . . . . . . . . 15
β’
β²π‘(π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
50 | 48, 48, 49 | nfmpo 7440 |
. . . . . . . . . . . . . 14
β’
β²π‘(π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
51 | 4, 50 | nfcxfr 2902 |
. . . . . . . . . . . . 13
β’
β²π‘π |
52 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π‘π |
53 | 44, 51, 52 | nfseq 13922 |
. . . . . . . . . . . 12
β’
β²π‘seq1(π, π) |
54 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π‘π |
55 | 53, 54 | nffv 6853 |
. . . . . . . . . . 11
β’
β²π‘(seq1(π, π)βπ) |
56 | 5, 55 | nfcxfr 2902 |
. . . . . . . . . 10
β’
β²π‘π |
57 | 56 | nfeq2 2921 |
. . . . . . . . 9
β’
β²π‘ β = π |
58 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (β = π β (ββπ‘) = (πβπ‘)) |
59 | 58 | breq2d 5118 |
. . . . . . . . . 10
β’ (β = π β (0 β€ (ββπ‘) β 0 β€ (πβπ‘))) |
60 | 58 | breq1d 5116 |
. . . . . . . . . 10
β’ (β = π β ((ββπ‘) β€ 1 β (πβπ‘) β€ 1)) |
61 | 59, 60 | anbi12d 632 |
. . . . . . . . 9
β’ (β = π β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
62 | 57, 61 | ralbid 3255 |
. . . . . . . 8
β’ (β = π β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
63 | 33, 34, 43, 62 | elrabf 3642 |
. . . . . . 7
β’ (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
64 | 22, 63 | bitri 275 |
. . . . . 6
β’ (π β π β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
65 | 20, 64 | sylib 217 |
. . . . 5
β’ (π β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
66 | 65 | simprd 497 |
. . . 4
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
67 | | stoweidlem51.1 |
. . . . 5
β’
β²ππ |
68 | | stoweidlem51.8 |
. . . . 5
β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
69 | | stoweidlem51.9 |
. . . . 5
β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) |
70 | | stoweidlem51.11 |
. . . . 5
β’ (π β π:(1...π)βΆπ) |
71 | | stoweidlem51.14 |
. . . . 5
β’ (π β π· β βͺ ran
π) |
72 | | stoweidlem51.15 |
. . . . 5
β’ (π β π· β π) |
73 | | nfv 1918 |
. . . . . . 7
β’
β²π‘ π β (1...π) |
74 | 14, 73 | nfan 1903 |
. . . . . 6
β’
β²π‘(π β§ π β (1...π)) |
75 | 13 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
76 | | fveq1 6842 |
. . . . . . . . . . . . . . . . 17
β’ (β = (πβπ) β (ββπ‘) = ((πβπ)βπ‘)) |
77 | 76 | breq2d 5118 |
. . . . . . . . . . . . . . . 16
β’ (β = (πβπ) β (0 β€ (ββπ‘) β 0 β€ ((πβπ)βπ‘))) |
78 | 76 | breq1d 5116 |
. . . . . . . . . . . . . . . 16
β’ (β = (πβπ) β ((ββπ‘) β€ 1 β ((πβπ)βπ‘) β€ 1)) |
79 | 77, 78 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (β = (πβπ) β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
80 | 79 | ralbidv 3171 |
. . . . . . . . . . . . . 14
β’ (β = (πβπ) β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
81 | 80, 1 | elrab2 3649 |
. . . . . . . . . . . . 13
β’ ((πβπ) β π β ((πβπ) β π΄ β§ βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
82 | 81 | simplbi 499 |
. . . . . . . . . . . 12
β’ ((πβπ) β π β (πβπ) β π΄) |
83 | 75, 82 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πβπ) β π΄) |
84 | | eleq1 2822 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (π β π΄ β (πβπ) β π΄)) |
85 | 84 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β ((π β§ π β π΄) β (π β§ (πβπ) β π΄))) |
86 | | feq1 6650 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (π:πβΆβ β (πβπ):πβΆβ)) |
87 | 85, 86 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ))) |
88 | 16 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π΄ β ((π β§ π β π΄) β π:πβΆβ)) |
89 | 87, 88 | vtoclga 3533 |
. . . . . . . . . . . 12
β’ ((πβπ) β π΄ β ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ)) |
90 | 89 | anabsi7 670 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ) |
91 | 83, 90 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πβπ):πβΆβ) |
92 | 91 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β (πβπ):πβΆβ) |
93 | 70 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
94 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β π) |
95 | 94, 93 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (π β§ (πβπ) β π)) |
96 | | stoweidlem51.3 |
. . . . . . . . . . . . . 14
β’
β²π€π |
97 | | stoweidlem51.4 |
. . . . . . . . . . . . . . 15
β’
β²π€π |
98 | 97 | nfel2 2922 |
. . . . . . . . . . . . . 14
β’
β²π€(πβπ) β π |
99 | 96, 98 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π€(π β§ (πβπ) β π) |
100 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π€(πβπ) β π |
101 | 99, 100 | nfim 1900 |
. . . . . . . . . . . 12
β’
β²π€((π β§ (πβπ) β π) β (πβπ) β π) |
102 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π€ = (πβπ) β (π€ β π β (πβπ) β π)) |
103 | 102 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π€ = (πβπ) β ((π β§ π€ β π) β (π β§ (πβπ) β π))) |
104 | | sseq1 3970 |
. . . . . . . . . . . . 13
β’ (π€ = (πβπ) β (π€ β π β (πβπ) β π)) |
105 | 103, 104 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π€ = (πβπ) β (((π β§ π€ β π) β π€ β π) β ((π β§ (πβπ) β π) β (πβπ) β π))) |
106 | | stoweidlem51.13 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β π) β π€ β π) |
107 | 101, 105,
106 | vtoclg1f 3523 |
. . . . . . . . . . 11
β’ ((πβπ) β π β ((π β§ (πβπ) β π) β (πβπ) β π)) |
108 | 93, 95, 107 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
109 | 108 | sselda 3945 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β π‘ β π) |
110 | 92, 109 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) β β) |
111 | | stoweidlem51.22 |
. . . . . . . . . . 11
β’ (π β πΈ β
β+) |
112 | 111 | rpred 12962 |
. . . . . . . . . 10
β’ (π β πΈ β β) |
113 | 112 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β πΈ β β) |
114 | 10 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β π β β) |
115 | 7 | nnne0d 12208 |
. . . . . . . . . 10
β’ (π β π β 0) |
116 | 115 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β π β 0) |
117 | 113, 114,
116 | redivcld 11988 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β (πΈ / π) β β) |
118 | | stoweidlem51.17 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < (πΈ / π)) |
119 | 118 | r19.21bi 3233 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < (πΈ / π)) |
120 | | 1red 11161 |
. . . . . . . . . . . 12
β’ (π β 1 β
β) |
121 | | 0lt1 11682 |
. . . . . . . . . . . . 13
β’ 0 <
1 |
122 | 121 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 0 < 1) |
123 | 7 | nngt0d 12207 |
. . . . . . . . . . . 12
β’ (π β 0 < π) |
124 | 111 | rpregt0d 12968 |
. . . . . . . . . . . 12
β’ (π β (πΈ β β β§ 0 < πΈ)) |
125 | | lediv2 12050 |
. . . . . . . . . . . 12
β’ (((1
β β β§ 0 < 1) β§ (π β β β§ 0 < π) β§ (πΈ β β β§ 0 < πΈ)) β (1 β€ π β (πΈ / π) β€ (πΈ / 1))) |
126 | 120, 122,
10, 123, 124, 125 | syl221anc 1382 |
. . . . . . . . . . 11
β’ (π β (1 β€ π β (πΈ / π) β€ (πΈ / 1))) |
127 | 9, 126 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (πΈ / π) β€ (πΈ / 1)) |
128 | 111 | rpcnd 12964 |
. . . . . . . . . . 11
β’ (π β πΈ β β) |
129 | 128 | div1d 11928 |
. . . . . . . . . 10
β’ (π β (πΈ / 1) = πΈ) |
130 | 127, 129 | breqtrd 5132 |
. . . . . . . . 9
β’ (π β (πΈ / π) β€ πΈ) |
131 | 130 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β (πΈ / π) β€ πΈ) |
132 | 110, 117,
113, 119, 131 | ltletrd 11320 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
133 | 132 | ex 414 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (π‘ β (πβπ) β ((πβπ)βπ‘) < πΈ)) |
134 | 74, 133 | ralrimi 3239 |
. . . . 5
β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < πΈ) |
135 | 67, 14, 1, 4, 5, 68,
69, 7, 70, 13, 71, 72, 134, 19, 16, 17, 111 | stoweidlem48 44375 |
. . . 4
β’ (π β βπ‘ β π· (πβπ‘) < πΈ) |
136 | | stoweidlem51.18 |
. . . . 5
β’ ((π β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((πβπ)βπ‘)) |
137 | | stoweidlem51.23 |
. . . . 5
β’ (π β πΈ < (1 / 3)) |
138 | 3 | sseli 3941 |
. . . . . 6
β’ (π β π β π β π΄) |
139 | 138, 16 | sylan2 594 |
. . . . 5
β’ ((π β§ π β π) β π:πβΆβ) |
140 | | stoweidlem51.16 |
. . . . 5
β’ (π β π΅ β π) |
141 | 67, 14, 48, 4, 5, 68, 69, 7, 13, 136, 111, 137, 139, 18, 19, 140 | stoweidlem42 44369 |
. . . 4
β’ (π β βπ‘ β π΅ (1 β πΈ) < (πβπ‘)) |
142 | 66, 135, 141 | 3jca 1129 |
. . 3
β’ (π β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π· (πβπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (πβπ‘))) |
143 | 21, 142 | jca 513 |
. 2
β’ (π β (π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π· (πβπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (πβπ‘)))) |
144 | | eleq1 2822 |
. . . 4
β’ (π₯ = π β (π₯ β π΄ β π β π΄)) |
145 | 56 | nfeq2 2921 |
. . . . . 6
β’
β²π‘ π₯ = π |
146 | | fveq1 6842 |
. . . . . . . 8
β’ (π₯ = π β (π₯βπ‘) = (πβπ‘)) |
147 | 146 | breq2d 5118 |
. . . . . . 7
β’ (π₯ = π β (0 β€ (π₯βπ‘) β 0 β€ (πβπ‘))) |
148 | 146 | breq1d 5116 |
. . . . . . 7
β’ (π₯ = π β ((π₯βπ‘) β€ 1 β (πβπ‘) β€ 1)) |
149 | 147, 148 | anbi12d 632 |
. . . . . 6
β’ (π₯ = π β ((0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
150 | 145, 149 | ralbid 3255 |
. . . . 5
β’ (π₯ = π β (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
151 | 146 | breq1d 5116 |
. . . . . 6
β’ (π₯ = π β ((π₯βπ‘) < πΈ β (πβπ‘) < πΈ)) |
152 | 145, 151 | ralbid 3255 |
. . . . 5
β’ (π₯ = π β (βπ‘ β π· (π₯βπ‘) < πΈ β βπ‘ β π· (πβπ‘) < πΈ)) |
153 | 146 | breq2d 5118 |
. . . . . 6
β’ (π₯ = π β ((1 β πΈ) < (π₯βπ‘) β (1 β πΈ) < (πβπ‘))) |
154 | 145, 153 | ralbid 3255 |
. . . . 5
β’ (π₯ = π β (βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘) β βπ‘ β π΅ (1 β πΈ) < (πβπ‘))) |
155 | 150, 152,
154 | 3anbi123d 1437 |
. . . 4
β’ (π₯ = π β ((βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)) β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π· (πβπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (πβπ‘)))) |
156 | 144, 155 | anbi12d 632 |
. . 3
β’ (π₯ = π β ((π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) β (π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π· (πβπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (πβπ‘))))) |
157 | 156 | spcegv 3555 |
. 2
β’ (π β π΄ β ((π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π· (πβπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (πβπ‘))) β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))))) |
158 | 21, 143, 157 | sylc 65 |
1
β’ (π β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |