Step | Hyp | Ref
| Expression |
1 | | stoweidlem40.3 |
. . 3
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))βπ)) |
2 | | stoweidlem40.2 |
. . . 4
β’
β²π‘π |
3 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π‘ β π) β π‘ β π) |
4 | | 1red 11164 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β 1 β β) |
5 | | stoweidlem40.8 |
. . . . . . . . . 10
β’ (π β π:πβΆβ) |
6 | 5 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πβπ‘) β β) |
7 | | stoweidlem40.13 |
. . . . . . . . . . 11
β’ (π β π β β) |
8 | 7 | nnnn0d 12481 |
. . . . . . . . . 10
β’ (π β π β
β0) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π β
β0) |
10 | 6, 9 | reexpcld 14077 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β ((πβπ‘)βπ) β β) |
11 | 4, 10 | resubcld 11591 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) β β) |
12 | | stoweidlem40.4 |
. . . . . . . 8
β’ πΉ = (π‘ β π β¦ (1 β ((πβπ‘)βπ))) |
13 | 12 | fvmpt2 6963 |
. . . . . . 7
β’ ((π‘ β π β§ (1 β ((πβπ‘)βπ)) β β) β (πΉβπ‘) = (1 β ((πβπ‘)βπ))) |
14 | 3, 11, 13 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΉβπ‘) = (1 β ((πβπ‘)βπ))) |
15 | 14 | eqcomd 2739 |
. . . . 5
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) = (πΉβπ‘)) |
16 | 15 | oveq1d 7376 |
. . . 4
β’ ((π β§ π‘ β π) β ((1 β ((πβπ‘)βπ))βπ) = ((πΉβπ‘)βπ)) |
17 | 2, 16 | mpteq2da 5207 |
. . 3
β’ (π β (π‘ β π β¦ ((1 β ((πβπ‘)βπ))βπ)) = (π‘ β π β¦ ((πΉβπ‘)βπ))) |
18 | 1, 17 | eqtrid 2785 |
. 2
β’ (π β π = (π‘ β π β¦ ((πΉβπ‘)βπ))) |
19 | | nfmpt1 5217 |
. . . 4
β’
β²π‘(π‘ β π β¦ (1 β ((πβπ‘)βπ))) |
20 | 12, 19 | nfcxfr 2902 |
. . 3
β’
β²π‘πΉ |
21 | | stoweidlem40.9 |
. . 3
β’ ((π β§ π β π΄) β π:πβΆβ) |
22 | | stoweidlem40.11 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
23 | | stoweidlem40.12 |
. . 3
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
24 | | 1re 11163 |
. . . . . . . . . 10
β’ 1 β
β |
25 | | stoweidlem40.5 |
. . . . . . . . . . 11
β’ πΊ = (π‘ β π β¦ 1) |
26 | 25 | fvmpt2 6963 |
. . . . . . . . . 10
β’ ((π‘ β π β§ 1 β β) β (πΊβπ‘) = 1) |
27 | 24, 26 | mpan2 690 |
. . . . . . . . 9
β’ (π‘ β π β (πΊβπ‘) = 1) |
28 | 27 | eqcomd 2739 |
. . . . . . . 8
β’ (π‘ β π β 1 = (πΊβπ‘)) |
29 | 28 | adantl 483 |
. . . . . . 7
β’ ((π β§ π‘ β π) β 1 = (πΊβπ‘)) |
30 | | stoweidlem40.6 |
. . . . . . . . . 10
β’ π» = (π‘ β π β¦ ((πβπ‘)βπ)) |
31 | 30 | fvmpt2 6963 |
. . . . . . . . 9
β’ ((π‘ β π β§ ((πβπ‘)βπ) β β) β (π»βπ‘) = ((πβπ‘)βπ)) |
32 | 3, 10, 31 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π»βπ‘) = ((πβπ‘)βπ)) |
33 | 32 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((πβπ‘)βπ) = (π»βπ‘)) |
34 | 29, 33 | oveq12d 7379 |
. . . . . 6
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) = ((πΊβπ‘) β (π»βπ‘))) |
35 | 2, 34 | mpteq2da 5207 |
. . . . 5
β’ (π β (π‘ β π β¦ (1 β ((πβπ‘)βπ))) = (π‘ β π β¦ ((πΊβπ‘) β (π»βπ‘)))) |
36 | 12, 35 | eqtrid 2785 |
. . . 4
β’ (π β πΉ = (π‘ β π β¦ ((πΊβπ‘) β (π»βπ‘)))) |
37 | 23 | stoweidlem4 44335 |
. . . . . . 7
β’ ((π β§ 1 β β) β
(π‘ β π β¦ 1) β π΄) |
38 | 24, 37 | mpan2 690 |
. . . . . 6
β’ (π β (π‘ β π β¦ 1) β π΄) |
39 | 25, 38 | eqeltrid 2838 |
. . . . 5
β’ (π β πΊ β π΄) |
40 | | stoweidlem40.1 |
. . . . . . 7
β’
β²π‘π |
41 | | stoweidlem40.7 |
. . . . . . 7
β’ (π β π β π΄) |
42 | 40, 2, 21, 22, 23, 41, 8 | stoweidlem19 44350 |
. . . . . 6
β’ (π β (π‘ β π β¦ ((πβπ‘)βπ)) β π΄) |
43 | 30, 42 | eqeltrid 2838 |
. . . . 5
β’ (π β π» β π΄) |
44 | | nfmpt1 5217 |
. . . . . . 7
β’
β²π‘(π‘ β π β¦ 1) |
45 | 25, 44 | nfcxfr 2902 |
. . . . . 6
β’
β²π‘πΊ |
46 | | nfmpt1 5217 |
. . . . . . 7
β’
β²π‘(π‘ β π β¦ ((πβπ‘)βπ)) |
47 | 30, 46 | nfcxfr 2902 |
. . . . . 6
β’
β²π‘π» |
48 | | stoweidlem40.10 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
49 | 45, 47, 2, 21, 48, 22, 23 | stoweidlem33 44364 |
. . . . 5
β’ ((π β§ πΊ β π΄ β§ π» β π΄) β (π‘ β π β¦ ((πΊβπ‘) β (π»βπ‘))) β π΄) |
50 | 39, 43, 49 | mpd3an23 1464 |
. . . 4
β’ (π β (π‘ β π β¦ ((πΊβπ‘) β (π»βπ‘))) β π΄) |
51 | 36, 50 | eqeltrd 2834 |
. . 3
β’ (π β πΉ β π΄) |
52 | | stoweidlem40.14 |
. . . 4
β’ (π β π β β) |
53 | 52 | nnnn0d 12481 |
. . 3
β’ (π β π β
β0) |
54 | 20, 2, 21, 22, 23, 51, 53 | stoweidlem19 44350 |
. 2
β’ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) |
55 | 18, 54 | eqeltrd 2834 |
1
β’ (π β π β π΄) |