Step | Hyp | Ref
| Expression |
1 | | stoweidlem48.2 |
. 2
β’
β²π‘π |
2 | | stoweidlem48.12 |
. . . . . 6
β’ (π β π· β π) |
3 | 2 | sselda 3982 |
. . . . 5
β’ ((π β§ π‘ β π·) β π‘ β π) |
4 | | stoweidlem48.1 |
. . . . . 6
β’
β²ππ |
5 | | stoweidlem48.3 |
. . . . . . 7
β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
6 | | nfra1 3281 |
. . . . . . . 8
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
7 | | nfcv 2903 |
. . . . . . . 8
β’
β²π‘π΄ |
8 | 6, 7 | nfrabw 3468 |
. . . . . . 7
β’
β²π‘{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
9 | 5, 8 | nfcxfr 2901 |
. . . . . 6
β’
β²π‘π |
10 | | stoweidlem48.4 |
. . . . . 6
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
11 | | stoweidlem48.5 |
. . . . . 6
β’ π = (seq1(π, π)βπ) |
12 | | stoweidlem48.6 |
. . . . . 6
β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
13 | | stoweidlem48.7 |
. . . . . 6
β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) |
14 | | stoweidlem48.14 |
. . . . . 6
β’ (π β π β V) |
15 | | stoweidlem48.8 |
. . . . . 6
β’ (π β π β β) |
16 | | stoweidlem48.10 |
. . . . . 6
β’ (π β π:(1...π)βΆπ) |
17 | 5 | eleq2i 2825 |
. . . . . . . . 9
β’ (π β π β π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
18 | | fveq1 6890 |
. . . . . . . . . . . . 13
β’ (β = π β (ββπ‘) = (πβπ‘)) |
19 | 18 | breq2d 5160 |
. . . . . . . . . . . 12
β’ (β = π β (0 β€ (ββπ‘) β 0 β€ (πβπ‘))) |
20 | 18 | breq1d 5158 |
. . . . . . . . . . . 12
β’ (β = π β ((ββπ‘) β€ 1 β (πβπ‘) β€ 1)) |
21 | 19, 20 | anbi12d 631 |
. . . . . . . . . . 11
β’ (β = π β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
22 | 21 | ralbidv 3177 |
. . . . . . . . . 10
β’ (β = π β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
23 | 22 | elrab 3683 |
. . . . . . . . 9
β’ (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
24 | 17, 23 | sylbb 218 |
. . . . . . . 8
β’ (π β π β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
25 | 24 | simpld 495 |
. . . . . . 7
β’ (π β π β π β π΄) |
26 | | stoweidlem48.15 |
. . . . . . 7
β’ ((π β§ π β π΄) β π:πβΆβ) |
27 | 25, 26 | sylan2 593 |
. . . . . 6
β’ ((π β§ π β π) β π:πβΆβ) |
28 | | eqid 2732 |
. . . . . . 7
β’ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
29 | | stoweidlem48.16 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
30 | 1, 5, 28, 26, 29 | stoweidlem16 44722 |
. . . . . 6
β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
31 | 4, 9, 10, 11, 12, 13, 14, 15, 16, 27, 30 | fmuldfeq 44289 |
. . . . 5
β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) |
32 | 3, 31 | syldan 591 |
. . . 4
β’ ((π β§ π‘ β π·) β (πβπ‘) = (πβπ‘)) |
33 | | elnnuz 12865 |
. . . . . . . . 9
β’ (π β β β π β
(β€β₯β1)) |
34 | 15, 33 | sylib 217 |
. . . . . . . 8
β’ (π β π β
(β€β₯β1)) |
35 | 34 | adantr 481 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β π β
(β€β₯β1)) |
36 | | nfv 1917 |
. . . . . . . . . . . 12
β’
β²π π‘ β π |
37 | 4, 36 | nfan 1902 |
. . . . . . . . . . 11
β’
β²π(π β§ π‘ β π) |
38 | 16 | ffvelcdmda 7086 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
39 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = (πβπ) β (ββπ‘) = ((πβπ)βπ‘)) |
40 | 39 | breq2d 5160 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (πβπ) β (0 β€ (ββπ‘) β 0 β€ ((πβπ)βπ‘))) |
41 | 39 | breq1d 5158 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (πβπ) β ((ββπ‘) β€ 1 β ((πβπ)βπ‘) β€ 1)) |
42 | 40, 41 | anbi12d 631 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (πβπ) β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
43 | 42 | ralbidv 3177 |
. . . . . . . . . . . . . . . . 17
β’ (β = (πβπ) β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
44 | 43, 5 | elrab2 3686 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β π β ((πβπ) β π΄ β§ βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
45 | 38, 44 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((πβπ) β π΄ β§ βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
46 | 45 | simpld 495 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (πβπ) β π΄) |
47 | | simpl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β π) |
48 | 47, 46 | jca 512 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (π β§ (πβπ) β π΄)) |
49 | | eleq1 2821 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (π β π΄ β (πβπ) β π΄)) |
50 | 49 | anbi2d 629 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β ((π β§ π β π΄) β (π β§ (πβπ) β π΄))) |
51 | | feq1 6698 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (π:πβΆβ β (πβπ):πβΆβ)) |
52 | 50, 51 | imbi12d 344 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ))) |
53 | 52, 26 | vtoclg 3556 |
. . . . . . . . . . . . . 14
β’ ((πβπ) β π΄ β ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ)) |
54 | 46, 48, 53 | sylc 65 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πβπ):πβΆβ) |
55 | 54 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β π) β§ π β (1...π)) β (πβπ):πβΆβ) |
56 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β π) β§ π β (1...π)) β π‘ β π) |
57 | 55, 56 | ffvelcdmd 7087 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πβπ)βπ‘) β β) |
58 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) = (π β (1...π) β¦ ((πβπ)βπ‘)) |
59 | 37, 57, 58 | fmptdf 7116 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (π β (1...π) β¦ ((πβπ)βπ‘)):(1...π)βΆβ) |
60 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β π‘ β π) |
61 | | ovex 7441 |
. . . . . . . . . . . . 13
β’
(1...π) β
V |
62 | | mptexg 7222 |
. . . . . . . . . . . . 13
β’
((1...π) β V
β (π β (1...π) β¦ ((πβπ)βπ‘)) β V) |
63 | 61, 62 | mp1i 13 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β (π β (1...π) β¦ ((πβπ)βπ‘)) β V) |
64 | 12 | fvmpt2 7009 |
. . . . . . . . . . . 12
β’ ((π‘ β π β§ (π β (1...π) β¦ ((πβπ)βπ‘)) β V) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
65 | 60, 63, 64 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
66 | 65 | feq1d 6702 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β ((πΉβπ‘):(1...π)βΆβ β (π β (1...π) β¦ ((πβπ)βπ‘)):(1...π)βΆβ)) |
67 | 59, 66 | mpbird 256 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πΉβπ‘):(1...π)βΆβ) |
68 | 3, 67 | syldan 591 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β (πΉβπ‘):(1...π)βΆβ) |
69 | 68 | ffvelcdmda 7086 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
70 | | remulcl 11194 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π Β· π) β β) |
71 | 70 | adantl 482 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ (π β β β§ π β β)) β (π Β· π) β β) |
72 | 35, 69, 71 | seqcl 13987 |
. . . . . 6
β’ ((π β§ π‘ β π·) β (seq1( Β· , (πΉβπ‘))βπ) β β) |
73 | 13 | fvmpt2 7009 |
. . . . . 6
β’ ((π‘ β π β§ (seq1( Β· , (πΉβπ‘))βπ) β β) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
74 | 3, 72, 73 | syl2anc 584 |
. . . . 5
β’ ((π β§ π‘ β π·) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
75 | | nfcv 2903 |
. . . . . . . . 9
β’
β²ππ |
76 | | nfmpt1 5256 |
. . . . . . . . 9
β’
β²π(π β (1...π) β¦ ((πβπ)βπ‘)) |
77 | 75, 76 | nfmpt 5255 |
. . . . . . . 8
β’
β²π(π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
78 | 12, 77 | nfcxfr 2901 |
. . . . . . 7
β’
β²ππΉ |
79 | | nfcv 2903 |
. . . . . . 7
β’
β²ππ‘ |
80 | 78, 79 | nffv 6901 |
. . . . . 6
β’
β²π(πΉβπ‘) |
81 | | nfv 1917 |
. . . . . . 7
β’
β²π π‘ β π· |
82 | 4, 81 | nfan 1902 |
. . . . . 6
β’
β²π(π β§ π‘ β π·) |
83 | | nfcv 2903 |
. . . . . 6
β’
β²πseq1(
Β· , (πΉβπ‘)) |
84 | | eqid 2732 |
. . . . . 6
β’ seq1(
Β· , (πΉβπ‘)) = seq1( Β· , (πΉβπ‘)) |
85 | 15 | adantr 481 |
. . . . . 6
β’ ((π β§ π‘ β π·) β π β β) |
86 | | simpll 765 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β π) |
87 | | simpr 485 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β π β (1...π)) |
88 | 3 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β π‘ β π) |
89 | 45 | simprd 496 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1)) |
90 | 89 | r19.21bi 3248 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β π) β (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1)) |
91 | 90 | simpld 495 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) |
92 | 86, 87, 88, 91 | syl21anc 836 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β 0 β€ ((πβπ)βπ‘)) |
93 | 65 | fveq1d 6893 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) |
94 | 86, 88, 93 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) |
95 | 86, 88, 87, 57 | syl21anc 836 |
. . . . . . . . 9
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πβπ)βπ‘) β β) |
96 | 58 | fvmpt2 7009 |
. . . . . . . . 9
β’ ((π β (1...π) β§ ((πβπ)βπ‘) β β) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((πβπ)βπ‘)) |
97 | 87, 95, 96 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((πβπ)βπ‘)) |
98 | 94, 97 | eqtrd 2772 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
99 | 92, 98 | breqtrrd 5176 |
. . . . . 6
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β 0 β€ ((πΉβπ‘)βπ)) |
100 | 90 | simprd 496 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β π) β ((πβπ)βπ‘) β€ 1) |
101 | 86, 87, 88, 100 | syl21anc 836 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πβπ)βπ‘) β€ 1) |
102 | 98, 101 | eqbrtrd 5170 |
. . . . . 6
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) β€ 1) |
103 | | stoweidlem48.17 |
. . . . . . 7
β’ (π β πΈ β
β+) |
104 | 103 | adantr 481 |
. . . . . 6
β’ ((π β§ π‘ β π·) β πΈ β
β+) |
105 | | stoweidlem48.11 |
. . . . . . . . . . 11
β’ (π β π· β βͺ ran
π) |
106 | 105 | sselda 3982 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π·) β π‘ β βͺ ran
π) |
107 | | eluni 4911 |
. . . . . . . . . 10
β’ (π‘ β βͺ ran π β βπ€(π‘ β π€ β§ π€ β ran π)) |
108 | 106, 107 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β βπ€(π‘ β π€ β§ π€ β ran π)) |
109 | | stoweidlem48.9 |
. . . . . . . . . . . . . . . 16
β’ (π β π:(1...π)βΆπ) |
110 | | ffn 6717 |
. . . . . . . . . . . . . . . 16
β’ (π:(1...π)βΆπ β π Fn (1...π)) |
111 | | fvelrnb 6952 |
. . . . . . . . . . . . . . . 16
β’ (π Fn (1...π) β (π€ β ran π β βπ β (1...π)(πβπ) = π€)) |
112 | 109, 110,
111 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β (π€ β ran π β βπ β (1...π)(πβπ) = π€)) |
113 | 112 | biimpa 477 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€ β ran π) β βπ β (1...π)(πβπ) = π€) |
114 | 113 | adantrl 714 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π€ β§ π€ β ran π)) β βπ β (1...π)(πβπ) = π€) |
115 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π€) β§ (πβπ) = π€) β π‘ β π€) |
116 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π€) β§ (πβπ) = π€) β (πβπ) = π€) |
117 | 115, 116 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π‘ β π€) β§ (πβπ) = π€) β π‘ β (πβπ)) |
118 | 117 | ex 413 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β π€) β ((πβπ) = π€ β π‘ β (πβπ))) |
119 | 118 | reximdv 3170 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π€) β (βπ β (1...π)(πβπ) = π€ β βπ β (1...π)π‘ β (πβπ))) |
120 | 119 | adantrr 715 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π€ β§ π€ β ran π)) β (βπ β (1...π)(πβπ) = π€ β βπ β (1...π)π‘ β (πβπ))) |
121 | 114, 120 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ β π€ β§ π€ β ran π)) β βπ β (1...π)π‘ β (πβπ)) |
122 | 121 | ex 413 |
. . . . . . . . . . 11
β’ (π β ((π‘ β π€ β§ π€ β ran π) β βπ β (1...π)π‘ β (πβπ))) |
123 | 122 | exlimdv 1936 |
. . . . . . . . . 10
β’ (π β (βπ€(π‘ β π€ β§ π€ β ran π) β βπ β (1...π)π‘ β (πβπ))) |
124 | 123 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β (βπ€(π‘ β π€ β§ π€ β ran π) β βπ β (1...π)π‘ β (πβπ))) |
125 | 108, 124 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β βπ β (1...π)π‘ β (πβπ)) |
126 | | simplll 773 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β π) |
127 | | simplr 767 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β π β (1...π)) |
128 | | simpr 485 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β π‘ β (πβπ)) |
129 | | nfv 1917 |
. . . . . . . . . . . . . 14
β’
β²π π β (1...π) |
130 | | nfv 1917 |
. . . . . . . . . . . . . 14
β’
β²π π‘ β (πβπ) |
131 | 4, 129, 130 | nf3an 1904 |
. . . . . . . . . . . . 13
β’
β²π(π β§ π β (1...π) β§ π‘ β (πβπ)) |
132 | | nfv 1917 |
. . . . . . . . . . . . 13
β’
β²π((πβπ)βπ‘) < πΈ |
133 | 131, 132 | nfim 1899 |
. . . . . . . . . . . 12
β’
β²π((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
134 | | eleq1 2821 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β (1...π) β π β (1...π))) |
135 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
136 | 135 | eleq2d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π β (π‘ β (πβπ) β π‘ β (πβπ))) |
137 | 134, 136 | 3anbi23d 1439 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β§ π β (1...π) β§ π‘ β (πβπ)) β (π β§ π β (1...π) β§ π‘ β (πβπ)))) |
138 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
139 | 138 | fveq1d 6893 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ)βπ‘) = ((πβπ)βπ‘)) |
140 | 139 | breq1d 5158 |
. . . . . . . . . . . . 13
β’ (π = π β (((πβπ)βπ‘) < πΈ β ((πβπ)βπ‘) < πΈ)) |
141 | 137, 140 | imbi12d 344 |
. . . . . . . . . . . 12
β’ (π = π β (((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) β ((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ))) |
142 | | stoweidlem48.13 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < πΈ) |
143 | 142 | r19.21bi 3248 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
144 | 143 | 3impa 1110 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
145 | 133, 141,
144 | chvarfv 2233 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
146 | 126, 127,
128, 145 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
147 | 146 | ex 413 |
. . . . . . . . 9
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β (π‘ β (πβπ) β ((πβπ)βπ‘) < πΈ)) |
148 | 147 | reximdva 3168 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β (βπ β (1...π)π‘ β (πβπ) β βπ β (1...π)((πβπ)βπ‘) < πΈ)) |
149 | 125, 148 | mpd 15 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β βπ β (1...π)((πβπ)βπ‘) < πΈ) |
150 | 82, 129 | nfan 1902 |
. . . . . . . . . . . 12
β’
β²π((π β§ π‘ β π·) β§ π β (1...π)) |
151 | | nfcv 2903 |
. . . . . . . . . . . . . 14
β’
β²ππ |
152 | 80, 151 | nffv 6901 |
. . . . . . . . . . . . 13
β’
β²π((πΉβπ‘)βπ) |
153 | 152 | nfeq1 2918 |
. . . . . . . . . . . 12
β’
β²π((πΉβπ‘)βπ) = ((πβπ)βπ‘) |
154 | 150, 153 | nfim 1899 |
. . . . . . . . . . 11
β’
β²π(((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
155 | 134 | anbi2d 629 |
. . . . . . . . . . . 12
β’ (π = π β (((π β§ π‘ β π·) β§ π β (1...π)) β ((π β§ π‘ β π·) β§ π β (1...π)))) |
156 | | fveq2 6891 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
157 | 156, 139 | eqeq12d 2748 |
. . . . . . . . . . . 12
β’ (π = π β (((πΉβπ‘)βπ) = ((πβπ)βπ‘) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘))) |
158 | 155, 157 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π = π β ((((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) β (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)))) |
159 | 154, 158,
98 | chvarfv 2233 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
160 | 159 | breq1d 5158 |
. . . . . . . . 9
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β (((πΉβπ‘)βπ) < πΈ β ((πβπ)βπ‘) < πΈ)) |
161 | 160 | biimprd 247 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β (((πβπ)βπ‘) < πΈ β ((πΉβπ‘)βπ) < πΈ)) |
162 | 161 | reximdva 3168 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β (βπ β (1...π)((πβπ)βπ‘) < πΈ β βπ β (1...π)((πΉβπ‘)βπ) < πΈ)) |
163 | 149, 162 | mpd 15 |
. . . . . 6
β’ ((π β§ π‘ β π·) β βπ β (1...π)((πΉβπ‘)βπ) < πΈ) |
164 | 80, 82, 83, 84, 85, 68, 99, 102, 104, 163 | fmul01lt1 44292 |
. . . . 5
β’ ((π β§ π‘ β π·) β (seq1( Β· , (πΉβπ‘))βπ) < πΈ) |
165 | 74, 164 | eqbrtrd 5170 |
. . . 4
β’ ((π β§ π‘ β π·) β (πβπ‘) < πΈ) |
166 | 32, 165 | eqbrtrd 5170 |
. . 3
β’ ((π β§ π‘ β π·) β (πβπ‘) < πΈ) |
167 | 166 | ex 413 |
. 2
β’ (π β (π‘ β π· β (πβπ‘) < πΈ)) |
168 | 1, 167 | ralrimi 3254 |
1
β’ (π β βπ‘ β π· (πβπ‘) < πΈ) |