Step | Hyp | Ref
| Expression |
1 | | fperiodmullem.n |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑛 · 𝑇) = (0 · 𝑇)) |
3 | 2 | oveq2d 6666 |
. . . . . 6
⊢ (𝑛 = 0 → (𝑋 + (𝑛 · 𝑇)) = (𝑋 + (0 · 𝑇))) |
4 | 3 | fveq2d 6195 |
. . . . 5
⊢ (𝑛 = 0 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘(𝑋 + (0 · 𝑇)))) |
5 | 4 | eqeq1d 2624 |
. . . 4
⊢ (𝑛 = 0 → ((𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋) ↔ (𝐹‘(𝑋 + (0 · 𝑇))) = (𝐹‘𝑋))) |
6 | 5 | imbi2d 330 |
. . 3
⊢ (𝑛 = 0 → ((𝜑 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋)) ↔ (𝜑 → (𝐹‘(𝑋 + (0 · 𝑇))) = (𝐹‘𝑋)))) |
7 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑇) = (𝑚 · 𝑇)) |
8 | 7 | oveq2d 6666 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑋 + (𝑛 · 𝑇)) = (𝑋 + (𝑚 · 𝑇))) |
9 | 8 | fveq2d 6195 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘(𝑋 + (𝑚 · 𝑇)))) |
10 | 9 | eqeq1d 2624 |
. . . 4
⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋) ↔ (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋))) |
11 | 10 | imbi2d 330 |
. . 3
⊢ (𝑛 = 𝑚 → ((𝜑 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋)) ↔ (𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)))) |
12 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · 𝑇) = ((𝑚 + 1) · 𝑇)) |
13 | 12 | oveq2d 6666 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑋 + (𝑛 · 𝑇)) = (𝑋 + ((𝑚 + 1) · 𝑇))) |
14 | 13 | fveq2d 6195 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇)))) |
15 | 14 | eqeq1d 2624 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋) ↔ (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘𝑋))) |
16 | 15 | imbi2d 330 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋)) ↔ (𝜑 → (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘𝑋)))) |
17 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 · 𝑇) = (𝑁 · 𝑇)) |
18 | 17 | oveq2d 6666 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑋 + (𝑛 · 𝑇)) = (𝑋 + (𝑁 · 𝑇))) |
19 | 18 | fveq2d 6195 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘(𝑋 + (𝑁 · 𝑇)))) |
20 | 19 | eqeq1d 2624 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋) ↔ (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋))) |
21 | 20 | imbi2d 330 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝜑 → (𝐹‘(𝑋 + (𝑛 · 𝑇))) = (𝐹‘𝑋)) ↔ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)))) |
22 | | fperiodmullem.t |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℝ) |
23 | 22 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℂ) |
24 | 23 | mul02d 10234 |
. . . . . 6
⊢ (𝜑 → (0 · 𝑇) = 0) |
25 | 24 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (𝑋 + (0 · 𝑇)) = (𝑋 + 0)) |
26 | | fperiodmullem.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) |
27 | 26 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℂ) |
28 | 27 | addid1d 10236 |
. . . . 5
⊢ (𝜑 → (𝑋 + 0) = 𝑋) |
29 | 25, 28 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (𝑋 + (0 · 𝑇)) = 𝑋) |
30 | 29 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (𝐹‘(𝑋 + (0 · 𝑇))) = (𝐹‘𝑋)) |
31 | | simp3 1063 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → 𝜑) |
32 | | simp1 1061 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → 𝑚 ∈ ℕ0) |
33 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → 𝜑) |
34 | | simpl 473 |
. . . . . . 7
⊢ (((𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → (𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋))) |
35 | 33, 34 | mpd 15 |
. . . . . 6
⊢ (((𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) |
36 | 35 | 3adant1 1079 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) |
37 | | nn0cn 11302 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
38 | 37 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) |
39 | | 1cnd 10056 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) |
40 | 23 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑇 ∈
ℂ) |
41 | 38, 39, 40 | adddird 10065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑇) = ((𝑚 · 𝑇) + (1 · 𝑇))) |
42 | 41 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑋 + ((𝑚 + 1) · 𝑇)) = (𝑋 + ((𝑚 · 𝑇) + (1 · 𝑇)))) |
43 | 27 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈
ℂ) |
44 | 38, 40 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑇) ∈ ℂ) |
45 | 39, 40 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (1
· 𝑇) ∈
ℂ) |
46 | 43, 44, 45 | addassd 10062 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑋 + (𝑚 · 𝑇)) + (1 · 𝑇)) = (𝑋 + ((𝑚 · 𝑇) + (1 · 𝑇)))) |
47 | 40 | mulid2d 10058 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (1
· 𝑇) = 𝑇) |
48 | 47 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑋 + (𝑚 · 𝑇)) + (1 · 𝑇)) = ((𝑋 + (𝑚 · 𝑇)) + 𝑇)) |
49 | 42, 46, 48 | 3eqtr2d 2662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑋 + ((𝑚 + 1) · 𝑇)) = ((𝑋 + (𝑚 · 𝑇)) + 𝑇)) |
50 | 49 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇))) |
51 | 50 | 3adant3 1081 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) → (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇))) |
52 | 26 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈
ℝ) |
53 | | nn0re 11301 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
54 | 53 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℝ) |
55 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑇 ∈
ℝ) |
56 | 54, 55 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑇) ∈ ℝ) |
57 | 52, 56 | readdcld 10069 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑋 + (𝑚 · 𝑇)) ∈ ℝ) |
58 | 57 | ex 450 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ ℕ0 → (𝑋 + (𝑚 · 𝑇)) ∈ ℝ)) |
59 | 58 | imdistani 726 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝜑 ∧ (𝑋 + (𝑚 · 𝑇)) ∈ ℝ)) |
60 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → (𝑥 ∈ ℝ ↔ (𝑋 + (𝑚 · 𝑇)) ∈ ℝ)) |
61 | 60 | anbi2d 740 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑋 + (𝑚 · 𝑇)) ∈ ℝ))) |
62 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → (𝑥 + 𝑇) = ((𝑋 + (𝑚 · 𝑇)) + 𝑇)) |
63 | 62 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇))) |
64 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → (𝐹‘𝑥) = (𝐹‘(𝑋 + (𝑚 · 𝑇)))) |
65 | 63, 64 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇)) = (𝐹‘(𝑋 + (𝑚 · 𝑇))))) |
66 | 61, 65 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = (𝑋 + (𝑚 · 𝑇)) → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ (𝑋 + (𝑚 · 𝑇)) ∈ ℝ) → (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇)) = (𝐹‘(𝑋 + (𝑚 · 𝑇)))))) |
67 | | fperiodmullem.per |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
68 | 66, 67 | vtoclg 3266 |
. . . . . . . 8
⊢ ((𝑋 + (𝑚 · 𝑇)) ∈ ℝ → ((𝜑 ∧ (𝑋 + (𝑚 · 𝑇)) ∈ ℝ) → (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇)) = (𝐹‘(𝑋 + (𝑚 · 𝑇))))) |
69 | 57, 59, 68 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇)) = (𝐹‘(𝑋 + (𝑚 · 𝑇)))) |
70 | 69 | 3adant3 1081 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) → (𝐹‘((𝑋 + (𝑚 · 𝑇)) + 𝑇)) = (𝐹‘(𝑋 + (𝑚 · 𝑇)))) |
71 | | simp3 1063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) |
72 | 51, 70, 71 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) → (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘𝑋)) |
73 | 31, 32, 36, 72 | syl3anc 1326 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) ∧ 𝜑) → (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘𝑋)) |
74 | 73 | 3exp 1264 |
. . 3
⊢ (𝑚 ∈ ℕ0
→ ((𝜑 → (𝐹‘(𝑋 + (𝑚 · 𝑇))) = (𝐹‘𝑋)) → (𝜑 → (𝐹‘(𝑋 + ((𝑚 + 1) · 𝑇))) = (𝐹‘𝑋)))) |
75 | 6, 11, 16, 21, 30, 74 | nn0ind 11472 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋))) |
76 | 1, 75 | mpcom 38 |
1
⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) |