Step | Hyp | Ref
| Expression |
1 | | stoweidlem48.2 |
. 2
β’
β²π‘π |
2 | | stoweidlem48.12 |
. . . . . 6
β’ (π β π· β π) |
3 | 2 | sselda 3948 |
. . . . 5
β’ ((π β§ π‘ β π·) β π‘ β π) |
4 | | stoweidlem48.1 |
. . . . . 6
β’
β²ππ |
5 | | stoweidlem48.3 |
. . . . . . 7
β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
6 | | nfra1 3266 |
. . . . . . . 8
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
7 | | nfcv 2904 |
. . . . . . . 8
β’
β²π‘π΄ |
8 | 6, 7 | nfrabw 3442 |
. . . . . . 7
β’
β²π‘{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
9 | 5, 8 | nfcxfr 2902 |
. . . . . 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 2826 |
. . . . . . . . 9
β’ (π β π β π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
18 | | fveq1 6845 |
. . . . . . . . . . . . 13
β’ (β = π β (ββπ‘) = (πβπ‘)) |
19 | 18 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (β = π β (0 β€ (ββπ‘) β 0 β€ (πβπ‘))) |
20 | 18 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (β = π β ((ββπ‘) β€ 1 β (πβπ‘) β€ 1)) |
21 | 19, 20 | anbi12d 632 |
. . . . . . . . . . 11
β’ (β = π β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
22 | 21 | ralbidv 3171 |
. . . . . . . . . 10
β’ (β = π β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
23 | 22 | elrab 3649 |
. . . . . . . . 9
β’ (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
24 | 17, 23 | sylbb 218 |
. . . . . . . 8
β’ (π β π β (π β π΄ β§ βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
25 | 24 | simpld 496 |
. . . . . . 7
β’ (π β π β π β π΄) |
26 | | stoweidlem48.15 |
. . . . . . 7
β’ ((π β§ π β π΄) β π:πβΆβ) |
27 | 25, 26 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β π) β π:πβΆβ) |
28 | | eqid 2733 |
. . . . . . 7
β’ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
29 | | stoweidlem48.16 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
30 | 1, 5, 28, 26, 29 | stoweidlem16 44347 |
. . . . . 6
β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
31 | 4, 9, 10, 11, 12, 13, 14, 15, 16, 27, 30 | fmuldfeq 43914 |
. . . . 5
β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) |
32 | 3, 31 | syldan 592 |
. . . 4
β’ ((π β§ π‘ β π·) β (πβπ‘) = (πβπ‘)) |
33 | | elnnuz 12815 |
. . . . . . . . 9
β’ (π β β β π β
(β€β₯β1)) |
34 | 15, 33 | sylib 217 |
. . . . . . . 8
β’ (π β π β
(β€β₯β1)) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β π β
(β€β₯β1)) |
36 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π π‘ β π |
37 | 4, 36 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π(π β§ π‘ β π) |
38 | 16 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
39 | | fveq1 6845 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = (πβπ) β (ββπ‘) = ((πβπ)βπ‘)) |
40 | 39 | breq2d 5121 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (πβπ) β (0 β€ (ββπ‘) β 0 β€ ((πβπ)βπ‘))) |
41 | 39 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (πβπ) β ((ββπ‘) β€ 1 β ((πβπ)βπ‘) β€ 1)) |
42 | 40, 41 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (πβπ) β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
43 | 42 | ralbidv 3171 |
. . . . . . . . . . . . . . . . 17
β’ (β = (πβπ) β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
44 | 43, 5 | elrab2 3652 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β π β ((πβπ) β π΄ β§ βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
45 | 38, 44 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((πβπ) β π΄ β§ βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1))) |
46 | 45 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (πβπ) β π΄) |
47 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β π) |
48 | 47, 46 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (π β§ (πβπ) β π΄)) |
49 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (π β π΄ β (πβπ) β π΄)) |
50 | 49 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β ((π β§ π β π΄) β (π β§ (πβπ) β π΄))) |
51 | | feq1 6653 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (π:πβΆβ β (πβπ):πβΆβ)) |
52 | 50, 51 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ))) |
53 | 52, 26 | vtoclg 3527 |
. . . . . . . . . . . . . 14
β’ ((πβπ) β π΄ β ((π β§ (πβπ) β π΄) β (πβπ):πβΆβ)) |
54 | 46, 48, 53 | sylc 65 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πβπ):πβΆβ) |
55 | 54 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β π) β§ π β (1...π)) β (πβπ):πβΆβ) |
56 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β π) β§ π β (1...π)) β π‘ β π) |
57 | 55, 56 | ffvelcdmd 7040 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πβπ)βπ‘) β β) |
58 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) = (π β (1...π) β¦ ((πβπ)βπ‘)) |
59 | 37, 57, 58 | fmptdf 7069 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (π β (1...π) β¦ ((πβπ)βπ‘)):(1...π)βΆβ) |
60 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β π‘ β π) |
61 | | ovex 7394 |
. . . . . . . . . . . . 13
β’
(1...π) β
V |
62 | | mptexg 7175 |
. . . . . . . . . . . . 13
β’
((1...π) β V
β (π β (1...π) β¦ ((πβπ)βπ‘)) β V) |
63 | 61, 62 | mp1i 13 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β (π β (1...π) β¦ ((πβπ)βπ‘)) β V) |
64 | 12 | fvmpt2 6963 |
. . . . . . . . . . . 12
β’ ((π‘ β π β§ (π β (1...π) β¦ ((πβπ)βπ‘)) β V) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
65 | 60, 63, 64 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
66 | 65 | feq1d 6657 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β ((πΉβπ‘):(1...π)βΆβ β (π β (1...π) β¦ ((πβπ)βπ‘)):(1...π)βΆβ)) |
67 | 59, 66 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πΉβπ‘):(1...π)βΆβ) |
68 | 3, 67 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β (πΉβπ‘):(1...π)βΆβ) |
69 | 68 | ffvelcdmda 7039 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
70 | | remulcl 11144 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π Β· π) β β) |
71 | 70 | adantl 483 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ (π β β β§ π β β)) β (π Β· π) β β) |
72 | 35, 69, 71 | seqcl 13937 |
. . . . . 6
β’ ((π β§ π‘ β π·) β (seq1( Β· , (πΉβπ‘))βπ) β β) |
73 | 13 | fvmpt2 6963 |
. . . . . 6
β’ ((π‘ β π β§ (seq1( Β· , (πΉβπ‘))βπ) β β) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
74 | 3, 72, 73 | syl2anc 585 |
. . . . 5
β’ ((π β§ π‘ β π·) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
75 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
76 | | nfmpt1 5217 |
. . . . . . . . 9
β’
β²π(π β (1...π) β¦ ((πβπ)βπ‘)) |
77 | 75, 76 | nfmpt 5216 |
. . . . . . . 8
β’
β²π(π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
78 | 12, 77 | nfcxfr 2902 |
. . . . . . 7
β’
β²ππΉ |
79 | | nfcv 2904 |
. . . . . . 7
β’
β²ππ‘ |
80 | 78, 79 | nffv 6856 |
. . . . . 6
β’
β²π(πΉβπ‘) |
81 | | nfv 1918 |
. . . . . . 7
β’
β²π π‘ β π· |
82 | 4, 81 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ π‘ β π·) |
83 | | nfcv 2904 |
. . . . . 6
β’
β²πseq1(
Β· , (πΉβπ‘)) |
84 | | eqid 2733 |
. . . . . 6
β’ seq1(
Β· , (πΉβπ‘)) = seq1( Β· , (πΉβπ‘)) |
85 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π·) β π β β) |
86 | | simpll 766 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β π) |
87 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β π β (1...π)) |
88 | 3 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β π‘ β π) |
89 | 45 | simprd 497 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β βπ‘ β π (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1)) |
90 | 89 | r19.21bi 3233 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π‘ β π) β (0 β€ ((πβπ)βπ‘) β§ ((πβπ)βπ‘) β€ 1)) |
91 | 90 | simpld 496 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) |
92 | 86, 87, 88, 91 | syl21anc 837 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β 0 β€ ((πβπ)βπ‘)) |
93 | 65 | fveq1d 6848 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) |
94 | 86, 88, 93 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) |
95 | 86, 88, 87, 57 | syl21anc 837 |
. . . . . . . . 9
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πβπ)βπ‘) β β) |
96 | 58 | fvmpt2 6963 |
. . . . . . . . 9
β’ ((π β (1...π) β§ ((πβπ)βπ‘) β β) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((πβπ)βπ‘)) |
97 | 87, 95, 96 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((πβπ)βπ‘)) |
98 | 94, 97 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
99 | 92, 98 | breqtrrd 5137 |
. . . . . 6
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β 0 β€ ((πΉβπ‘)βπ)) |
100 | 90 | simprd 497 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π‘ β π) β ((πβπ)βπ‘) β€ 1) |
101 | 86, 87, 88, 100 | syl21anc 837 |
. . . . . . 7
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πβπ)βπ‘) β€ 1) |
102 | 98, 101 | eqbrtrd 5131 |
. . . . . 6
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) β€ 1) |
103 | | stoweidlem48.17 |
. . . . . . 7
β’ (π β πΈ β
β+) |
104 | 103 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π·) β πΈ β
β+) |
105 | | stoweidlem48.11 |
. . . . . . . . . . 11
β’ (π β π· β βͺ ran
π) |
106 | 105 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π·) β π‘ β βͺ ran
π) |
107 | | eluni 4872 |
. . . . . . . . . 10
β’ (π‘ β βͺ ran π β βπ€(π‘ β π€ β§ π€ β ran π)) |
108 | 106, 107 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β βπ€(π‘ β π€ β§ π€ β ran π)) |
109 | | stoweidlem48.9 |
. . . . . . . . . . . . . . . 16
β’ (π β π:(1...π)βΆπ) |
110 | | ffn 6672 |
. . . . . . . . . . . . . . . 16
β’ (π:(1...π)βΆπ β π Fn (1...π)) |
111 | | fvelrnb 6907 |
. . . . . . . . . . . . . . . 16
β’ (π Fn (1...π) β (π€ β ran π β βπ β (1...π)(πβπ) = π€)) |
112 | 109, 110,
111 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β (π€ β ran π β βπ β (1...π)(πβπ) = π€)) |
113 | 112 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€ β ran π) β βπ β (1...π)(πβπ) = π€) |
114 | 113 | adantrl 715 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π€ β§ π€ β ran π)) β βπ β (1...π)(πβπ) = π€) |
115 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π€) β§ (πβπ) = π€) β π‘ β π€) |
116 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π€) β§ (πβπ) = π€) β (πβπ) = π€) |
117 | 115, 116 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π‘ β π€) β§ (πβπ) = π€) β π‘ β (πβπ)) |
118 | 117 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β π€) β ((πβπ) = π€ β π‘ β (πβπ))) |
119 | 118 | reximdv 3164 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π€) β (βπ β (1...π)(πβπ) = π€ β βπ β (1...π)π‘ β (πβπ))) |
120 | 119 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π€ β§ π€ β ran π)) β (βπ β (1...π)(πβπ) = π€ β βπ β (1...π)π‘ β (πβπ))) |
121 | 114, 120 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ β π€ β§ π€ β ran π)) β βπ β (1...π)π‘ β (πβπ)) |
122 | 121 | ex 414 |
. . . . . . . . . . 11
β’ (π β ((π‘ β π€ β§ π€ β ran π) β βπ β (1...π)π‘ β (πβπ))) |
123 | 122 | exlimdv 1937 |
. . . . . . . . . 10
β’ (π β (βπ€(π‘ β π€ β§ π€ β ran π) β βπ β (1...π)π‘ β (πβπ))) |
124 | 123 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π·) β (βπ€(π‘ β π€ β§ π€ β ran π) β βπ β (1...π)π‘ β (πβπ))) |
125 | 108, 124 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β βπ β (1...π)π‘ β (πβπ)) |
126 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β π) |
127 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β π β (1...π)) |
128 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β π‘ β (πβπ)) |
129 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π π β (1...π) |
130 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π π‘ β (πβπ) |
131 | 4, 129, 130 | nf3an 1905 |
. . . . . . . . . . . . 13
β’
β²π(π β§ π β (1...π) β§ π‘ β (πβπ)) |
132 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π((πβπ)βπ‘) < πΈ |
133 | 131, 132 | nfim 1900 |
. . . . . . . . . . . 12
β’
β²π((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
134 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β (1...π) β π β (1...π))) |
135 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
136 | 135 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π = π β (π‘ β (πβπ) β π‘ β (πβπ))) |
137 | 134, 136 | 3anbi23d 1440 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β§ π β (1...π) β§ π‘ β (πβπ)) β (π β§ π β (1...π) β§ π‘ β (πβπ)))) |
138 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
139 | 138 | fveq1d 6848 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ)βπ‘) = ((πβπ)βπ‘)) |
140 | 139 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (π = π β (((πβπ)βπ‘) < πΈ β ((πβπ)βπ‘) < πΈ)) |
141 | 137, 140 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π β (((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) β ((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ))) |
142 | | stoweidlem48.13 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < πΈ) |
143 | 142 | r19.21bi 3233 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
144 | 143 | 3impa 1111 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
145 | 133, 141,
144 | chvarfv 2234 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
146 | 126, 127,
128, 145 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β π·) β§ π β (1...π)) β§ π‘ β (πβπ)) β ((πβπ)βπ‘) < πΈ) |
147 | 146 | ex 414 |
. . . . . . . . 9
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β (π‘ β (πβπ) β ((πβπ)βπ‘) < πΈ)) |
148 | 147 | reximdva 3162 |
. . . . . . . 8
β’ ((π β§ π‘ β π·) β (βπ β (1...π)π‘ β (πβπ) β βπ β (1...π)((πβπ)βπ‘) < πΈ)) |
149 | 125, 148 | mpd 15 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β βπ β (1...π)((πβπ)βπ‘) < πΈ) |
150 | 82, 129 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π((π β§ π‘ β π·) β§ π β (1...π)) |
151 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²ππ |
152 | 80, 151 | nffv 6856 |
. . . . . . . . . . . . 13
β’
β²π((πΉβπ‘)βπ) |
153 | 152 | nfeq1 2919 |
. . . . . . . . . . . 12
β’
β²π((πΉβπ‘)βπ) = ((πβπ)βπ‘) |
154 | 150, 153 | nfim 1900 |
. . . . . . . . . . 11
β’
β²π(((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
155 | 134 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π = π β (((π β§ π‘ β π·) β§ π β (1...π)) β ((π β§ π‘ β π·) β§ π β (1...π)))) |
156 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
157 | 156, 139 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π = π β (((πΉβπ‘)βπ) = ((πβπ)βπ‘) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘))) |
158 | 155, 157 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β ((((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) β (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)))) |
159 | 154, 158,
98 | chvarfv 2234 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((πβπ)βπ‘)) |
160 | 159 | breq1d 5119 |
. . . . . . . . 9
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β (((πΉβπ‘)βπ) < πΈ β ((πβπ)βπ‘) < πΈ)) |
161 | 160 | biimprd 248 |
. . . . . . . 8
β’ (((π β§ π‘ β π·) β§ π β (1...π)) β (((πβπ)βπ‘) < πΈ β ((πΉβπ‘)βπ) < πΈ)) |
162 | 161 | reximdva 3162 |
. . . . . . 7
β’ ((π β§ π‘ β π·) β (βπ β (1...π)((πβπ)βπ‘) < πΈ β βπ β (1...π)((πΉβπ‘)βπ) < πΈ)) |
163 | 149, 162 | mpd 15 |
. . . . . 6
β’ ((π β§ π‘ β π·) β βπ β (1...π)((πΉβπ‘)βπ) < πΈ) |
164 | 80, 82, 83, 84, 85, 68, 99, 102, 104, 163 | fmul01lt1 43917 |
. . . . 5
β’ ((π β§ π‘ β π·) β (seq1( Β· , (πΉβπ‘))βπ) < πΈ) |
165 | 74, 164 | eqbrtrd 5131 |
. . . 4
β’ ((π β§ π‘ β π·) β (πβπ‘) < πΈ) |
166 | 32, 165 | eqbrtrd 5131 |
. . 3
β’ ((π β§ π‘ β π·) β (πβπ‘) < πΈ) |
167 | 166 | ex 414 |
. 2
β’ (π β (π‘ β π· β (πβπ‘) < πΈ)) |
168 | 1, 167 | ralrimi 3239 |
1
β’ (π β βπ‘ β π· (πβπ‘) < πΈ) |