Step | Hyp | Ref
| Expression |
1 | | stoweidlem41.1 |
. . . . 5
β’
β²π‘π |
2 | | 1re 11163 |
. . . . . . . 8
β’ 1 β
β |
3 | | stoweidlem41.3 |
. . . . . . . . 9
β’ πΉ = (π‘ β π β¦ 1) |
4 | 3 | fvmpt2 6963 |
. . . . . . . 8
β’ ((π‘ β π β§ 1 β β) β (πΉβπ‘) = 1) |
5 | 2, 4 | mpan2 690 |
. . . . . . 7
β’ (π‘ β π β (πΉβπ‘) = 1) |
6 | 5 | adantl 483 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΉβπ‘) = 1) |
7 | 6 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πΉβπ‘) β (π¦βπ‘)) = (1 β (π¦βπ‘))) |
8 | 1, 7 | mpteq2da 5207 |
. . . 4
β’ (π β (π‘ β π β¦ ((πΉβπ‘) β (π¦βπ‘))) = (π‘ β π β¦ (1 β (π¦βπ‘)))) |
9 | | stoweidlem41.2 |
. . . 4
β’ π = (π‘ β π β¦ (1 β (π¦βπ‘))) |
10 | 8, 9 | eqtr4di 2791 |
. . 3
β’ (π β (π‘ β π β¦ ((πΉβπ‘) β (π¦βπ‘))) = π) |
11 | | stoweidlem41.10 |
. . . . . . 7
β’ ((π β§ π€ β β) β (π‘ β π β¦ π€) β π΄) |
12 | 11 | stoweidlem4 44335 |
. . . . . 6
β’ ((π β§ 1 β β) β
(π‘ β π β¦ 1) β π΄) |
13 | 2, 12 | mpan2 690 |
. . . . 5
β’ (π β (π‘ β π β¦ 1) β π΄) |
14 | 3, 13 | eqeltrid 2838 |
. . . 4
β’ (π β πΉ β π΄) |
15 | | stoweidlem41.5 |
. . . 4
β’ (π β π¦ β π΄) |
16 | | nfmpt1 5217 |
. . . . . 6
β’
β²π‘(π‘ β π β¦ 1) |
17 | 3, 16 | nfcxfr 2902 |
. . . . 5
β’
β²π‘πΉ |
18 | | nfcv 2904 |
. . . . 5
β’
β²π‘π¦ |
19 | | stoweidlem41.7 |
. . . . 5
β’ ((π β§ π β π΄) β π:πβΆβ) |
20 | | stoweidlem41.8 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
21 | | stoweidlem41.9 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
22 | 17, 18, 1, 19, 20, 21, 11 | stoweidlem33 44364 |
. . . 4
β’ ((π β§ πΉ β π΄ β§ π¦ β π΄) β (π‘ β π β¦ ((πΉβπ‘) β (π¦βπ‘))) β π΄) |
23 | 14, 15, 22 | mpd3an23 1464 |
. . 3
β’ (π β (π‘ β π β¦ ((πΉβπ‘) β (π¦βπ‘))) β π΄) |
24 | 10, 23 | eqeltrrd 2835 |
. 2
β’ (π β π β π΄) |
25 | | stoweidlem41.6 |
. . . . . . . 8
β’ (π β π¦:πβΆβ) |
26 | 25 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (π¦βπ‘) β β) |
27 | | 1red 11164 |
. . . . . . 7
β’ ((π β§ π‘ β π) β 1 β β) |
28 | | 0red 11166 |
. . . . . . 7
β’ ((π β§ π‘ β π) β 0 β β) |
29 | | stoweidlem41.12 |
. . . . . . . . . 10
β’ (π β βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)) |
30 | 29 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)) |
31 | 30 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π¦βπ‘) β€ 1) |
32 | | 1m0e1 12282 |
. . . . . . . 8
β’ (1
β 0) = 1 |
33 | 31, 32 | breqtrrdi 5151 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (π¦βπ‘) β€ (1 β 0)) |
34 | 26, 27, 28, 33 | lesubd 11767 |
. . . . . 6
β’ ((π β§ π‘ β π) β 0 β€ (1 β (π¦βπ‘))) |
35 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π‘ β π) β π‘ β π) |
36 | 27, 26 | resubcld 11591 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (1 β (π¦βπ‘)) β β) |
37 | 9 | fvmpt2 6963 |
. . . . . . 7
β’ ((π‘ β π β§ (1 β (π¦βπ‘)) β β) β (πβπ‘) = (1 β (π¦βπ‘))) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πβπ‘) = (1 β (π¦βπ‘))) |
39 | 34, 38 | breqtrrd 5137 |
. . . . 5
β’ ((π β§ π‘ β π) β 0 β€ (πβπ‘)) |
40 | 30 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β 0 β€ (π¦βπ‘)) |
41 | 28, 26, 27, 40 | lesub2dd 11780 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (1 β (π¦βπ‘)) β€ (1 β 0)) |
42 | 41, 32 | breqtrdi 5150 |
. . . . . 6
β’ ((π β§ π‘ β π) β (1 β (π¦βπ‘)) β€ 1) |
43 | 38, 42 | eqbrtrd 5131 |
. . . . 5
β’ ((π β§ π‘ β π) β (πβπ‘) β€ 1) |
44 | 39, 43 | jca 513 |
. . . 4
β’ ((π β§ π‘ β π) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
45 | 44 | ex 414 |
. . 3
β’ (π β (π‘ β π β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
46 | 1, 45 | ralrimi 3239 |
. 2
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
47 | | stoweidlem41.4 |
. . . . . . 7
β’ π β π |
48 | 47 | sseli 3944 |
. . . . . 6
β’ (π‘ β π β π‘ β π) |
49 | 48, 38 | sylan2 594 |
. . . . 5
β’ ((π β§ π‘ β π) β (πβπ‘) = (1 β (π¦βπ‘))) |
50 | | 1red 11164 |
. . . . . 6
β’ ((π β§ π‘ β π) β 1 β β) |
51 | | stoweidlem41.11 |
. . . . . . . 8
β’ (π β πΈ β
β+) |
52 | 51 | rpred 12965 |
. . . . . . 7
β’ (π β πΈ β β) |
53 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β πΈ β β) |
54 | 48, 26 | sylan2 594 |
. . . . . 6
β’ ((π β§ π‘ β π) β (π¦βπ‘) β β) |
55 | | stoweidlem41.13 |
. . . . . . 7
β’ (π β βπ‘ β π (1 β πΈ) < (π¦βπ‘)) |
56 | 55 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π‘ β π) β (1 β πΈ) < (π¦βπ‘)) |
57 | 50, 53, 54, 56 | ltsub23d 11768 |
. . . . 5
β’ ((π β§ π‘ β π) β (1 β (π¦βπ‘)) < πΈ) |
58 | 49, 57 | eqbrtrd 5131 |
. . . 4
β’ ((π β§ π‘ β π) β (πβπ‘) < πΈ) |
59 | 58 | ex 414 |
. . 3
β’ (π β (π‘ β π β (πβπ‘) < πΈ)) |
60 | 1, 59 | ralrimi 3239 |
. 2
β’ (π β βπ‘ β π (πβπ‘) < πΈ) |
61 | | eldifi 4090 |
. . . . . . 7
β’ (π‘ β (π β π) β π‘ β π) |
62 | 61, 26 | sylan2 594 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β (π¦βπ‘) β β) |
63 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β πΈ β β) |
64 | | 1red 11164 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β 1 β β) |
65 | | stoweidlem41.14 |
. . . . . . 7
β’ (π β βπ‘ β (π β π)(π¦βπ‘) < πΈ) |
66 | 65 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β (π¦βπ‘) < πΈ) |
67 | 62, 63, 64, 66 | ltsub2dd 11776 |
. . . . 5
β’ ((π β§ π‘ β (π β π)) β (1 β πΈ) < (1 β (π¦βπ‘))) |
68 | 61, 38 | sylan2 594 |
. . . . 5
β’ ((π β§ π‘ β (π β π)) β (πβπ‘) = (1 β (π¦βπ‘))) |
69 | 67, 68 | breqtrrd 5137 |
. . . 4
β’ ((π β§ π‘ β (π β π)) β (1 β πΈ) < (πβπ‘)) |
70 | 69 | ex 414 |
. . 3
β’ (π β (π‘ β (π β π) β (1 β πΈ) < (πβπ‘))) |
71 | 1, 70 | ralrimi 3239 |
. 2
β’ (π β βπ‘ β (π β π)(1 β πΈ) < (πβπ‘)) |
72 | | nfmpt1 5217 |
. . . . . . 7
β’
β²π‘(π‘ β π β¦ (1 β (π¦βπ‘))) |
73 | 9, 72 | nfcxfr 2902 |
. . . . . 6
β’
β²π‘π |
74 | 73 | nfeq2 2921 |
. . . . 5
β’
β²π‘ π₯ = π |
75 | | fveq1 6845 |
. . . . . . 7
β’ (π₯ = π β (π₯βπ‘) = (πβπ‘)) |
76 | 75 | breq2d 5121 |
. . . . . 6
β’ (π₯ = π β (0 β€ (π₯βπ‘) β 0 β€ (πβπ‘))) |
77 | 75 | breq1d 5119 |
. . . . . 6
β’ (π₯ = π β ((π₯βπ‘) β€ 1 β (πβπ‘) β€ 1)) |
78 | 76, 77 | anbi12d 632 |
. . . . 5
β’ (π₯ = π β ((0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
79 | 74, 78 | ralbid 3255 |
. . . 4
β’ (π₯ = π β (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
80 | 75 | breq1d 5119 |
. . . . 5
β’ (π₯ = π β ((π₯βπ‘) < πΈ β (πβπ‘) < πΈ)) |
81 | 74, 80 | ralbid 3255 |
. . . 4
β’ (π₯ = π β (βπ‘ β π (π₯βπ‘) < πΈ β βπ‘ β π (πβπ‘) < πΈ)) |
82 | 75 | breq2d 5121 |
. . . . 5
β’ (π₯ = π β ((1 β πΈ) < (π₯βπ‘) β (1 β πΈ) < (πβπ‘))) |
83 | 74, 82 | ralbid 3255 |
. . . 4
β’ (π₯ = π β (βπ‘ β (π β π)(1 β πΈ) < (π₯βπ‘) β βπ‘ β (π β π)(1 β πΈ) < (πβπ‘))) |
84 | 79, 81, 83 | 3anbi123d 1437 |
. . 3
β’ (π₯ = π β ((βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (π₯βπ‘)) β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π (πβπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (πβπ‘)))) |
85 | 84 | rspcev 3583 |
. 2
β’ ((π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π (πβπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (πβπ‘))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (π₯βπ‘))) |
86 | 24, 46, 60, 71, 85 | syl13anc 1373 |
1
β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (π₯βπ‘))) |