Step | Hyp | Ref
| Expression |
1 | | stoweidlem19.7 |
. 2
β’ (π β π β
β0) |
2 | | oveq2 7401 |
. . . . . 6
β’ (π = 0 β ((πΉβπ‘)βπ) = ((πΉβπ‘)β0)) |
3 | 2 | mpteq2dv 5243 |
. . . . 5
β’ (π = 0 β (π‘ β π β¦ ((πΉβπ‘)βπ)) = (π‘ β π β¦ ((πΉβπ‘)β0))) |
4 | 3 | eleq1d 2817 |
. . . 4
β’ (π = 0 β ((π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄ β (π‘ β π β¦ ((πΉβπ‘)β0)) β π΄)) |
5 | 4 | imbi2d 340 |
. . 3
β’ (π = 0 β ((π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π β (π‘ β π β¦ ((πΉβπ‘)β0)) β π΄))) |
6 | | oveq2 7401 |
. . . . . 6
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
7 | 6 | mpteq2dv 5243 |
. . . . 5
β’ (π = π β (π‘ β π β¦ ((πΉβπ‘)βπ)) = (π‘ β π β¦ ((πΉβπ‘)βπ))) |
8 | 7 | eleq1d 2817 |
. . . 4
β’ (π = π β ((π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄ β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) |
9 | 8 | imbi2d 340 |
. . 3
β’ (π = π β ((π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄))) |
10 | | oveq2 7401 |
. . . . . 6
β’ (π = (π + 1) β ((πΉβπ‘)βπ) = ((πΉβπ‘)β(π + 1))) |
11 | 10 | mpteq2dv 5243 |
. . . . 5
β’ (π = (π + 1) β (π‘ β π β¦ ((πΉβπ‘)βπ)) = (π‘ β π β¦ ((πΉβπ‘)β(π + 1)))) |
12 | 11 | eleq1d 2817 |
. . . 4
β’ (π = (π + 1) β ((π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄ β (π‘ β π β¦ ((πΉβπ‘)β(π + 1))) β π΄)) |
13 | 12 | imbi2d 340 |
. . 3
β’ (π = (π + 1) β ((π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π β (π‘ β π β¦ ((πΉβπ‘)β(π + 1))) β π΄))) |
14 | | oveq2 7401 |
. . . . . 6
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
15 | 14 | mpteq2dv 5243 |
. . . . 5
β’ (π = π β (π‘ β π β¦ ((πΉβπ‘)βπ)) = (π‘ β π β¦ ((πΉβπ‘)βπ))) |
16 | 15 | eleq1d 2817 |
. . . 4
β’ (π = π β ((π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄ β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) |
17 | 16 | imbi2d 340 |
. . 3
β’ (π = π β ((π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄))) |
18 | | stoweidlem19.2 |
. . . . 5
β’
β²π‘π |
19 | | stoweidlem19.6 |
. . . . . . . . 9
β’ (π β πΉ β π΄) |
20 | 19 | ancli 549 |
. . . . . . . . 9
β’ (π β (π β§ πΉ β π΄)) |
21 | | eleq1 2820 |
. . . . . . . . . . . 12
β’ (π = πΉ β (π β π΄ β πΉ β π΄)) |
22 | 21 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π = πΉ β ((π β§ π β π΄) β (π β§ πΉ β π΄))) |
23 | | feq1 6685 |
. . . . . . . . . . 11
β’ (π = πΉ β (π:πβΆβ β πΉ:πβΆβ)) |
24 | 22, 23 | imbi12d 344 |
. . . . . . . . . 10
β’ (π = πΉ β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ πΉ β π΄) β πΉ:πβΆβ))) |
25 | | stoweidlem19.3 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π:πβΆβ) |
26 | 24, 25 | vtoclg 3553 |
. . . . . . . . 9
β’ (πΉ β π΄ β ((π β§ πΉ β π΄) β πΉ:πβΆβ)) |
27 | 19, 20, 26 | sylc 65 |
. . . . . . . 8
β’ (π β πΉ:πβΆβ) |
28 | 27 | ffvelcdmda 7071 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
29 | | recn 11182 |
. . . . . . 7
β’ ((πΉβπ‘) β β β (πΉβπ‘) β β) |
30 | | exp0 14013 |
. . . . . . 7
β’ ((πΉβπ‘) β β β ((πΉβπ‘)β0) = 1) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((πΉβπ‘)β0) = 1) |
32 | 31 | eqcomd 2737 |
. . . . 5
β’ ((π β§ π‘ β π) β 1 = ((πΉβπ‘)β0)) |
33 | 18, 32 | mpteq2da 5239 |
. . . 4
β’ (π β (π‘ β π β¦ 1) = (π‘ β π β¦ ((πΉβπ‘)β0))) |
34 | | 1re 11196 |
. . . . 5
β’ 1 β
β |
35 | | stoweidlem19.5 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
36 | 35 | stoweidlem4 44493 |
. . . . 5
β’ ((π β§ 1 β β) β
(π‘ β π β¦ 1) β π΄) |
37 | 34, 36 | mpan2 689 |
. . . 4
β’ (π β (π‘ β π β¦ 1) β π΄) |
38 | 33, 37 | eqeltrrd 2833 |
. . 3
β’ (π β (π‘ β π β¦ ((πΉβπ‘)β0)) β π΄) |
39 | | simpr 485 |
. . . . 5
β’ (((π β β0
β§ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) β§ π) β π) |
40 | | simpll 765 |
. . . . 5
β’ (((π β β0
β§ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) β§ π) β π β β0) |
41 | | simplr 767 |
. . . . . 6
β’ (((π β β0
β§ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) β§ π) β (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) |
42 | 39, 41 | mpd 15 |
. . . . 5
β’ (((π β β0
β§ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) β§ π) β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) |
43 | | nfv 1917 |
. . . . . . . 8
β’
β²π‘ π β
β0 |
44 | | nfmpt1 5249 |
. . . . . . . . 9
β’
β²π‘(π‘ β π β¦ ((πΉβπ‘)βπ)) |
45 | 44 | nfel1 2918 |
. . . . . . . 8
β’
β²π‘(π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄ |
46 | 18, 43, 45 | nf3an 1904 |
. . . . . . 7
β’
β²π‘(π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) |
47 | | simpl1 1191 |
. . . . . . . . 9
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β π) |
48 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β π‘ β π) |
49 | 28 | recnd 11224 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
50 | 47, 48, 49 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β (πΉβπ‘) β β) |
51 | | simpl2 1192 |
. . . . . . . 8
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β π β β0) |
52 | 50, 51 | expp1d 14094 |
. . . . . . 7
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β ((πΉβπ‘)β(π + 1)) = (((πΉβπ‘)βπ) Β· (πΉβπ‘))) |
53 | 46, 52 | mpteq2da 5239 |
. . . . . 6
β’ ((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π‘ β π β¦ ((πΉβπ‘)β(π + 1))) = (π‘ β π β¦ (((πΉβπ‘)βπ) Β· (πΉβπ‘)))) |
54 | 28 | 3adant2 1131 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0 β§ π‘ β π) β (πΉβπ‘) β β) |
55 | | simp2 1137 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0 β§ π‘ β π) β π β β0) |
56 | 54, 55 | reexpcld 14110 |
. . . . . . . . . . 11
β’ ((π β§ π β β0 β§ π‘ β π) β ((πΉβπ‘)βπ) β β) |
57 | 47, 51, 48, 56 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β ((πΉβπ‘)βπ) β β) |
58 | | eqid 2731 |
. . . . . . . . . . . 12
β’ (π‘ β π β¦ ((πΉβπ‘)βπ)) = (π‘ β π β¦ ((πΉβπ‘)βπ)) |
59 | 58 | fvmpt2 6995 |
. . . . . . . . . . 11
β’ ((π‘ β π β§ ((πΉβπ‘)βπ) β β) β ((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘) = ((πΉβπ‘)βπ)) |
60 | 59 | eqcomd 2737 |
. . . . . . . . . 10
β’ ((π‘ β π β§ ((πΉβπ‘)βπ) β β) β ((πΉβπ‘)βπ) = ((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘)) |
61 | 48, 57, 60 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β ((πΉβπ‘)βπ) = ((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘)) |
62 | 61 | oveq1d 7408 |
. . . . . . . 8
β’ (((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β§ π‘ β π) β (((πΉβπ‘)βπ) Β· (πΉβπ‘)) = (((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘) Β· (πΉβπ‘))) |
63 | 46, 62 | mpteq2da 5239 |
. . . . . . 7
β’ ((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π‘ β π β¦ (((πΉβπ‘)βπ) Β· (πΉβπ‘))) = (π‘ β π β¦ (((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘) Β· (πΉβπ‘)))) |
64 | 19 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β πΉ β π΄) |
65 | 44 | nfeq2 2919 |
. . . . . . . . . 10
β’
β²π‘ π = (π‘ β π β¦ ((πΉβπ‘)βπ)) |
66 | | stoweidlem19.1 |
. . . . . . . . . . 11
β’
β²π‘πΉ |
67 | 66 | nfeq2 2919 |
. . . . . . . . . 10
β’
β²π‘ π = πΉ |
68 | | stoweidlem19.4 |
. . . . . . . . . 10
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
69 | 65, 67, 68 | stoweidlem6 44495 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄ β§ πΉ β π΄) β (π‘ β π β¦ (((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘) Β· (πΉβπ‘))) β π΄) |
70 | 64, 69 | mpd3an3 1462 |
. . . . . . . 8
β’ ((π β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘) Β· (πΉβπ‘))) β π΄) |
71 | 70 | 3adant2 1131 |
. . . . . . 7
β’ ((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ ((πΉβπ‘)βπ))βπ‘) Β· (πΉβπ‘))) β π΄) |
72 | 63, 71 | eqeltrd 2832 |
. . . . . 6
β’ ((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π‘ β π β¦ (((πΉβπ‘)βπ) Β· (πΉβπ‘))) β π΄) |
73 | 53, 72 | eqeltrd 2832 |
. . . . 5
β’ ((π β§ π β β0 β§ (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π‘ β π β¦ ((πΉβπ‘)β(π + 1))) β π΄) |
74 | 39, 40, 42, 73 | syl3anc 1371 |
. . . 4
β’ (((π β β0
β§ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) β§ π) β (π‘ β π β¦ ((πΉβπ‘)β(π + 1))) β π΄) |
75 | 74 | exp31 420 |
. . 3
β’ (π β β0
β ((π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) β (π β (π‘ β π β¦ ((πΉβπ‘)β(π + 1))) β π΄))) |
76 | 5, 9, 13, 17, 38, 75 | nn0ind 12639 |
. 2
β’ (π β β0
β (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄)) |
77 | 1, 76 | mpcom 38 |
1
β’ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) |