Step | Hyp | Ref
| Expression |
1 | | fperiodmullem.n |
. 2
β’ (π β π β
β0) |
2 | | oveq1 7412 |
. . . . . 6
β’ (π = 0 β (π Β· π) = (0 Β· π)) |
3 | 2 | oveq2d 7421 |
. . . . 5
β’ (π = 0 β (π + (π Β· π)) = (π + (0 Β· π))) |
4 | 3 | fveqeq2d 6896 |
. . . 4
β’ (π = 0 β ((πΉβ(π + (π Β· π))) = (πΉβπ) β (πΉβ(π + (0 Β· π))) = (πΉβπ))) |
5 | 4 | imbi2d 340 |
. . 3
β’ (π = 0 β ((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β (π β (πΉβ(π + (0 Β· π))) = (πΉβπ)))) |
6 | | oveq1 7412 |
. . . . . 6
β’ (π = π β (π Β· π) = (π Β· π)) |
7 | 6 | oveq2d 7421 |
. . . . 5
β’ (π = π β (π + (π Β· π)) = (π + (π Β· π))) |
8 | 7 | fveqeq2d 6896 |
. . . 4
β’ (π = π β ((πΉβ(π + (π Β· π))) = (πΉβπ) β (πΉβ(π + (π Β· π))) = (πΉβπ))) |
9 | 8 | imbi2d 340 |
. . 3
β’ (π = π β ((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β (π β (πΉβ(π + (π Β· π))) = (πΉβπ)))) |
10 | | oveq1 7412 |
. . . . . 6
β’ (π = (π + 1) β (π Β· π) = ((π + 1) Β· π)) |
11 | 10 | oveq2d 7421 |
. . . . 5
β’ (π = (π + 1) β (π + (π Β· π)) = (π + ((π + 1) Β· π))) |
12 | 11 | fveqeq2d 6896 |
. . . 4
β’ (π = (π + 1) β ((πΉβ(π + (π Β· π))) = (πΉβπ) β (πΉβ(π + ((π + 1) Β· π))) = (πΉβπ))) |
13 | 12 | imbi2d 340 |
. . 3
β’ (π = (π + 1) β ((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β (π β (πΉβ(π + ((π + 1) Β· π))) = (πΉβπ)))) |
14 | | oveq1 7412 |
. . . . . 6
β’ (π = π β (π Β· π) = (π Β· π)) |
15 | 14 | oveq2d 7421 |
. . . . 5
β’ (π = π β (π + (π Β· π)) = (π + (π Β· π))) |
16 | 15 | fveqeq2d 6896 |
. . . 4
β’ (π = π β ((πΉβ(π + (π Β· π))) = (πΉβπ) β (πΉβ(π + (π Β· π))) = (πΉβπ))) |
17 | 16 | imbi2d 340 |
. . 3
β’ (π = π β ((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β (π β (πΉβ(π + (π Β· π))) = (πΉβπ)))) |
18 | | fperiodmullem.t |
. . . . . . . 8
β’ (π β π β β) |
19 | 18 | recnd 11238 |
. . . . . . 7
β’ (π β π β β) |
20 | 19 | mul02d 11408 |
. . . . . 6
β’ (π β (0 Β· π) = 0) |
21 | 20 | oveq2d 7421 |
. . . . 5
β’ (π β (π + (0 Β· π)) = (π + 0)) |
22 | | fperiodmullem.x |
. . . . . . 7
β’ (π β π β β) |
23 | 22 | recnd 11238 |
. . . . . 6
β’ (π β π β β) |
24 | 23 | addridd 11410 |
. . . . 5
β’ (π β (π + 0) = π) |
25 | 21, 24 | eqtrd 2772 |
. . . 4
β’ (π β (π + (0 Β· π)) = π) |
26 | 25 | fveq2d 6892 |
. . 3
β’ (π β (πΉβ(π + (0 Β· π))) = (πΉβπ)) |
27 | | simp3 1138 |
. . . . 5
β’ ((π β β0
β§ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β π) |
28 | | simp1 1136 |
. . . . 5
β’ ((π β β0
β§ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β π β β0) |
29 | | simpr 485 |
. . . . . . 7
β’ (((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β π) |
30 | | simpl 483 |
. . . . . . 7
β’ (((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β (π β (πΉβ(π + (π Β· π))) = (πΉβπ))) |
31 | 29, 30 | mpd 15 |
. . . . . 6
β’ (((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β (πΉβ(π + (π Β· π))) = (πΉβπ)) |
32 | 31 | 3adant1 1130 |
. . . . 5
β’ ((π β β0
β§ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β (πΉβ(π + (π Β· π))) = (πΉβπ)) |
33 | | nn0cn 12478 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
34 | 33 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π β
β) |
35 | | 1cnd 11205 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β 1 β
β) |
36 | 19 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π β
β) |
37 | 34, 35, 36 | adddird 11235 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((π + 1) Β· π) = ((π Β· π) + (1 Β· π))) |
38 | 37 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π + ((π + 1) Β· π)) = (π + ((π Β· π) + (1 Β· π)))) |
39 | 23 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β π β
β) |
40 | 34, 36 | mulcld 11230 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π Β· π) β β) |
41 | 35, 36 | mulcld 11230 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (1
Β· π) β
β) |
42 | 39, 40, 41 | addassd 11232 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π + (π Β· π)) + (1 Β· π)) = (π + ((π Β· π) + (1 Β· π)))) |
43 | 36 | mullidd 11228 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (1
Β· π) = π) |
44 | 43 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π + (π Β· π)) + (1 Β· π)) = ((π + (π Β· π)) + π)) |
45 | 38, 42, 44 | 3eqtr2d 2778 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π + ((π + 1) Β· π)) = ((π + (π Β· π)) + π)) |
46 | 45 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π β β0) β (πΉβ(π + ((π + 1) Β· π))) = (πΉβ((π + (π Β· π)) + π))) |
47 | 46 | 3adant3 1132 |
. . . . . 6
β’ ((π β§ π β β0 β§ (πΉβ(π + (π Β· π))) = (πΉβπ)) β (πΉβ(π + ((π + 1) Β· π))) = (πΉβ((π + (π Β· π)) + π))) |
48 | 22 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β0) β π β
β) |
49 | | nn0re 12477 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β) |
50 | 49 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β π β
β) |
51 | 18 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β π β
β) |
52 | 50, 51 | remulcld 11240 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π Β· π) β β) |
53 | 48, 52 | readdcld 11239 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π + (π Β· π)) β β) |
54 | 53 | ex 413 |
. . . . . . . . 9
β’ (π β (π β β0 β (π + (π Β· π)) β β)) |
55 | 54 | imdistani 569 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π β§ (π + (π Β· π)) β β)) |
56 | | eleq1 2821 |
. . . . . . . . . . 11
β’ (π₯ = (π + (π Β· π)) β (π₯ β β β (π + (π Β· π)) β β)) |
57 | 56 | anbi2d 629 |
. . . . . . . . . 10
β’ (π₯ = (π + (π Β· π)) β ((π β§ π₯ β β) β (π β§ (π + (π Β· π)) β β))) |
58 | | fvoveq1 7428 |
. . . . . . . . . . 11
β’ (π₯ = (π + (π Β· π)) β (πΉβ(π₯ + π)) = (πΉβ((π + (π Β· π)) + π))) |
59 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π₯ = (π + (π Β· π)) β (πΉβπ₯) = (πΉβ(π + (π Β· π)))) |
60 | 58, 59 | eqeq12d 2748 |
. . . . . . . . . 10
β’ (π₯ = (π + (π Β· π)) β ((πΉβ(π₯ + π)) = (πΉβπ₯) β (πΉβ((π + (π Β· π)) + π)) = (πΉβ(π + (π Β· π))))) |
61 | 57, 60 | imbi12d 344 |
. . . . . . . . 9
β’ (π₯ = (π + (π Β· π)) β (((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β ((π β§ (π + (π Β· π)) β β) β (πΉβ((π + (π Β· π)) + π)) = (πΉβ(π + (π Β· π)))))) |
62 | | fperiodmullem.per |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
63 | 61, 62 | vtoclg 3556 |
. . . . . . . 8
β’ ((π + (π Β· π)) β β β ((π β§ (π + (π Β· π)) β β) β (πΉβ((π + (π Β· π)) + π)) = (πΉβ(π + (π Β· π))))) |
64 | 53, 55, 63 | sylc 65 |
. . . . . . 7
β’ ((π β§ π β β0) β (πΉβ((π + (π Β· π)) + π)) = (πΉβ(π + (π Β· π)))) |
65 | 64 | 3adant3 1132 |
. . . . . 6
β’ ((π β§ π β β0 β§ (πΉβ(π + (π Β· π))) = (πΉβπ)) β (πΉβ((π + (π Β· π)) + π)) = (πΉβ(π + (π Β· π)))) |
66 | | simp3 1138 |
. . . . . 6
β’ ((π β§ π β β0 β§ (πΉβ(π + (π Β· π))) = (πΉβπ)) β (πΉβ(π + (π Β· π))) = (πΉβπ)) |
67 | 47, 65, 66 | 3eqtrd 2776 |
. . . . 5
β’ ((π β§ π β β0 β§ (πΉβ(π + (π Β· π))) = (πΉβπ)) β (πΉβ(π + ((π + 1) Β· π))) = (πΉβπ)) |
68 | 27, 28, 32, 67 | syl3anc 1371 |
. . . 4
β’ ((π β β0
β§ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β§ π) β (πΉβ(π + ((π + 1) Β· π))) = (πΉβπ)) |
69 | 68 | 3exp 1119 |
. . 3
β’ (π β β0
β ((π β (πΉβ(π + (π Β· π))) = (πΉβπ)) β (π β (πΉβ(π + ((π + 1) Β· π))) = (πΉβπ)))) |
70 | 5, 9, 13, 17, 26, 69 | nn0ind 12653 |
. 2
β’ (π β β0
β (π β (πΉβ(π + (π Β· π))) = (πΉβπ))) |
71 | 1, 70 | mpcom 38 |
1
β’ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) |