| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → 2
∥ (𝑋 /
π)) | 
| 2 |  | 2z 12651 | . . . . . . . . . . . 12
⊢ 2 ∈
ℤ | 
| 3 | 2 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → 2 ∈
ℤ) | 
| 4 |  | fourierswlem.x | . . . . . . . . . . . . . 14
⊢ 𝑋 ∈ ℝ | 
| 5 |  | pirp 26504 | . . . . . . . . . . . . . 14
⊢ π
∈ ℝ+ | 
| 6 |  | mod0 13917 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℝ ∧ π
∈ ℝ+) → ((𝑋 mod π) = 0 ↔ (𝑋 / π) ∈ ℤ)) | 
| 7 | 4, 5, 6 | mp2an 692 | . . . . . . . . . . . . 13
⊢ ((𝑋 mod π) = 0 ↔ (𝑋 / π) ∈
ℤ) | 
| 8 | 7 | biimpi 216 | . . . . . . . . . . . 12
⊢ ((𝑋 mod π) = 0 → (𝑋 / π) ∈
ℤ) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → (𝑋 / π) ∈
ℤ) | 
| 10 |  | divides 16293 | . . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ (𝑋 /
π) ∈ ℤ) → (2 ∥ (𝑋 / π) ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = (𝑋 / π))) | 
| 11 | 3, 9, 10 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → (2
∥ (𝑋 / π) ↔
∃𝑘 ∈ ℤ
(𝑘 · 2) = (𝑋 / π))) | 
| 12 | 1, 11 | mpbid 232 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) →
∃𝑘 ∈ ℤ
(𝑘 · 2) = (𝑋 / π)) | 
| 13 |  | 2cnd 12345 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → 2 ∈
ℂ) | 
| 14 |  | picn 26502 | . . . . . . . . . . . . . . . . . . . 20
⊢ π
∈ ℂ | 
| 15 | 14 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → π
∈ ℂ) | 
| 16 |  | zcn 12620 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) | 
| 17 | 13, 15, 16 | mulassd 11285 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → ((2
· π) · 𝑘)
= (2 · (π · 𝑘))) | 
| 18 | 15, 16 | mulcld 11282 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → (π
· 𝑘) ∈
ℂ) | 
| 19 | 13, 18 | mulcomd 11283 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → (2
· (π · 𝑘))
= ((π · 𝑘)
· 2)) | 
| 20 | 17, 19 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → ((2
· π) · 𝑘)
= ((π · 𝑘)
· 2)) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((2 ·
π) · 𝑘) = ((π
· 𝑘) ·
2)) | 
| 22 | 15, 16, 13 | mulassd 11285 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → ((π
· 𝑘) · 2) =
(π · (𝑘 ·
2))) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((π ·
𝑘) · 2) = (π
· (𝑘 ·
2))) | 
| 24 |  | id 22 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 · 2) = (𝑋 / π) → (𝑘 · 2) = (𝑋 / π)) | 
| 25 | 24 | eqcomd 2742 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 · 2) = (𝑋 / π) → (𝑋 / π) = (𝑘 · 2)) | 
| 26 | 25 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / π) = (𝑘 · 2)) | 
| 27 | 4 | recni 11276 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑋 ∈ ℂ | 
| 28 | 27 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑋 ∈
ℂ) | 
| 29 | 14 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → π ∈
ℂ) | 
| 30 | 16 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑘 ∈
ℂ) | 
| 31 |  | 2cnd 12345 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 2 ∈
ℂ) | 
| 32 | 30, 31 | mulcld 11282 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑘 · 2) ∈
ℂ) | 
| 33 |  | pire 26501 | . . . . . . . . . . . . . . . . . . . 20
⊢ π
∈ ℝ | 
| 34 |  | pipos 26503 | . . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
π | 
| 35 | 33, 34 | gt0ne0ii 11800 | . . . . . . . . . . . . . . . . . . 19
⊢ π ≠
0 | 
| 36 | 35 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → π ≠
0) | 
| 37 | 28, 29, 32, 36 | divmuld 12066 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → ((𝑋 / π) = (𝑘 · 2) ↔ (π · (𝑘 · 2)) = 𝑋)) | 
| 38 | 26, 37 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (π ·
(𝑘 · 2)) = 𝑋) | 
| 39 | 21, 23, 38 | 3eqtrrd 2781 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑋 = ((2 · π) ·
𝑘)) | 
| 40 |  | fourierswlem.t | . . . . . . . . . . . . . . . 16
⊢ 𝑇 = (2 ·
π) | 
| 41 | 40 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑇 = (2 ·
π)) | 
| 42 | 39, 41 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) = (((2 · π) · 𝑘) / (2 ·
π))) | 
| 43 | 13, 15 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (2
· π) ∈ ℂ) | 
| 44 |  | 2ne0 12371 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 | 
| 45 | 44 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → 2 ≠
0) | 
| 46 | 35 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → π ≠
0) | 
| 47 | 13, 15, 45, 46 | mulne0d 11916 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (2
· π) ≠ 0) | 
| 48 | 16, 43, 47 | divcan3d 12049 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ → (((2
· π) · 𝑘)
/ (2 · π)) = 𝑘) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (((2 ·
π) · 𝑘) / (2
· π)) = 𝑘) | 
| 50 | 42, 49 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) = 𝑘) | 
| 51 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → 𝑘 ∈
ℤ) | 
| 52 | 50, 51 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 · 2) = (𝑋 / π)) → (𝑋 / 𝑇) ∈ ℤ) | 
| 53 | 52 | ex 412 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ → ((𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ)) | 
| 54 | 53 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → (𝑘 ∈ ℤ → ((𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ))) | 
| 55 | 54 | rexlimdv 3152 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) →
(∃𝑘 ∈ ℤ
(𝑘 · 2) = (𝑋 / π) → (𝑋 / 𝑇) ∈ ℤ)) | 
| 56 | 12, 55 | mpd 15 | . . . . . . . 8
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → (𝑋 / 𝑇) ∈ ℤ) | 
| 57 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 58 | 57, 33 | remulcli 11278 | . . . . . . . . . . 11
⊢ (2
· π) ∈ ℝ | 
| 59 | 40, 58 | eqeltri 2836 | . . . . . . . . . 10
⊢ 𝑇 ∈ ℝ | 
| 60 |  | 2pos 12370 | . . . . . . . . . . . 12
⊢ 0 <
2 | 
| 61 | 57, 33, 60, 34 | mulgt0ii 11395 | . . . . . . . . . . 11
⊢ 0 < (2
· π) | 
| 62 | 61, 40 | breqtrri 5169 | . . . . . . . . . 10
⊢ 0 <
𝑇 | 
| 63 | 59, 62 | elrpii 13038 | . . . . . . . . 9
⊢ 𝑇 ∈
ℝ+ | 
| 64 |  | mod0 13917 | . . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+)
→ ((𝑋 mod 𝑇) = 0 ↔ (𝑋 / 𝑇) ∈ ℤ)) | 
| 65 | 4, 63, 64 | mp2an 692 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) = 0 ↔ (𝑋 / 𝑇) ∈ ℤ) | 
| 66 | 56, 65 | sylibr 234 | . . . . . . 7
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → (𝑋 mod 𝑇) = 0) | 
| 67 | 66 | orcd 873 | . . . . . 6
⊢ (((𝑋 mod π) = 0 ∧ 2 ∥
(𝑋 / π)) → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π)) | 
| 68 |  | odd2np1 16379 | . . . . . . . . . 10
⊢ ((𝑋 / π) ∈ ℤ →
(¬ 2 ∥ (𝑋 / π)
↔ ∃𝑘 ∈
ℤ ((2 · 𝑘) +
1) = (𝑋 /
π))) | 
| 69 | 7, 68 | sylbi 217 | . . . . . . . . 9
⊢ ((𝑋 mod π) = 0 → (¬ 2
∥ (𝑋 / π) ↔
∃𝑘 ∈ ℤ ((2
· 𝑘) + 1) = (𝑋 / π))) | 
| 70 | 69 | biimpa 476 | . . . . . . . 8
⊢ (((𝑋 mod π) = 0 ∧ ¬ 2
∥ (𝑋 / π)) →
∃𝑘 ∈ ℤ ((2
· 𝑘) + 1) = (𝑋 / π)) | 
| 71 | 13, 16 | mulcld 11282 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → (2
· 𝑘) ∈
ℂ) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (2 ·
𝑘) ∈
ℂ) | 
| 73 |  | 1cnd 11257 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → 1 ∈
ℂ) | 
| 74 | 14 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → π ∈
ℂ) | 
| 75 | 72, 73, 74 | adddird 11287 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (((2 ·
𝑘) + 1) · π) =
(((2 · 𝑘) ·
π) + (1 · π))) | 
| 76 | 13, 16 | mulcomd 11283 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → (2
· 𝑘) = (𝑘 · 2)) | 
| 77 | 76 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → ((2
· 𝑘) · π)
= ((𝑘 · 2) ·
π)) | 
| 78 | 16, 13, 15 | mulassd 11285 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → ((𝑘 · 2) · π) =
(𝑘 · (2 ·
π))) | 
| 79 | 40 | eqcomi 2745 | . . . . . . . . . . . . . . . . . . . 20
⊢ (2
· π) = 𝑇 | 
| 80 | 79 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → (2
· π) = 𝑇) | 
| 81 | 80 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → (𝑘 · (2 · π)) =
(𝑘 · 𝑇)) | 
| 82 | 77, 78, 81 | 3eqtrd 2780 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → ((2
· 𝑘) · π)
= (𝑘 · 𝑇)) | 
| 83 | 14 | mullidi 11267 | . . . . . . . . . . . . . . . . . 18
⊢ (1
· π) = π | 
| 84 | 83 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → (1
· π) = π) | 
| 85 | 82, 84 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (((2
· 𝑘) · π)
+ (1 · π)) = ((𝑘
· 𝑇) +
π)) | 
| 86 | 85 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (((2 ·
𝑘) · π) + (1
· π)) = ((𝑘
· 𝑇) +
π)) | 
| 87 | 40, 43 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → 𝑇 ∈
ℂ) | 
| 88 | 16, 87 | mulcld 11282 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → (𝑘 · 𝑇) ∈ ℂ) | 
| 89 | 88, 15 | addcomd 11464 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → ((𝑘 · 𝑇) + π) = (π + (𝑘 · 𝑇))) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → ((𝑘 · 𝑇) + π) = (π + (𝑘 · 𝑇))) | 
| 91 | 75, 86, 90 | 3eqtrrd 2781 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (π + (𝑘 · 𝑇)) = (((2 · 𝑘) + 1) · π)) | 
| 92 |  | peano2cn 11434 | . . . . . . . . . . . . . . . . 17
⊢ ((2
· 𝑘) ∈ ℂ
→ ((2 · 𝑘) + 1)
∈ ℂ) | 
| 93 | 71, 92 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → ((2
· 𝑘) + 1) ∈
ℂ) | 
| 94 | 93, 15 | mulcomd 11283 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ → (((2
· 𝑘) + 1) ·
π) = (π · ((2 · 𝑘) + 1))) | 
| 95 | 94 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (((2 ·
𝑘) + 1) · π) =
(π · ((2 · 𝑘) + 1))) | 
| 96 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (((2
· 𝑘) + 1) = (𝑋 / π) → ((2 ·
𝑘) + 1) = (𝑋 / π)) | 
| 97 | 96 | eqcomd 2742 | . . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑘) + 1) = (𝑋 / π) → (𝑋 / π) = ((2 · 𝑘) + 1)) | 
| 98 | 97 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (𝑋 / π) = ((2 · 𝑘) + 1)) | 
| 99 | 27 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → 𝑋 ∈
ℂ) | 
| 100 | 93 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → ((2 ·
𝑘) + 1) ∈
ℂ) | 
| 101 | 35 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → π ≠
0) | 
| 102 | 99, 74, 100, 101 | divmuld 12066 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → ((𝑋 / π) = ((2 · 𝑘) + 1) ↔ (π · ((2
· 𝑘) + 1)) = 𝑋)) | 
| 103 | 98, 102 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (π ·
((2 · 𝑘) + 1)) =
𝑋) | 
| 104 | 91, 95, 103 | 3eqtrrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → 𝑋 = (π + (𝑘 · 𝑇))) | 
| 105 | 104 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (𝑋 mod 𝑇) = ((π + (𝑘 · 𝑇)) mod 𝑇)) | 
| 106 |  | modcyc 13947 | . . . . . . . . . . . . . 14
⊢ ((π
∈ ℝ ∧ 𝑇
∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇)) | 
| 107 | 33, 63, 106 | mp3an12 1452 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → ((π +
(𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇)) | 
| 108 | 107 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → ((π + (𝑘 · 𝑇)) mod 𝑇) = (π mod 𝑇)) | 
| 109 | 33 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → π ∈
ℝ) | 
| 110 | 63 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → 𝑇 ∈
ℝ+) | 
| 111 |  | 0re 11264 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ | 
| 112 | 111, 33, 34 | ltleii 11385 | . . . . . . . . . . . . . 14
⊢ 0 ≤
π | 
| 113 | 112 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → 0 ≤
π) | 
| 114 |  | 2timesgt 45305 | . . . . . . . . . . . . . . . 16
⊢ (π
∈ ℝ+ → π < (2 · π)) | 
| 115 | 5, 114 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ π <
(2 · π) | 
| 116 | 115, 40 | breqtrri 5169 | . . . . . . . . . . . . . 14
⊢ π <
𝑇 | 
| 117 | 116 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → π < 𝑇) | 
| 118 |  | modid 13937 | . . . . . . . . . . . . 13
⊢ (((π
∈ ℝ ∧ 𝑇
∈ ℝ+) ∧ (0 ≤ π ∧ π < 𝑇)) → (π mod 𝑇) = π) | 
| 119 | 109, 110,
113, 117, 118 | syl22anc 838 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (π mod 𝑇) = π) | 
| 120 | 105, 108,
119 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ ((2
· 𝑘) + 1) = (𝑋 / π)) → (𝑋 mod 𝑇) = π) | 
| 121 | 120 | ex 412 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (((2
· 𝑘) + 1) = (𝑋 / π) → (𝑋 mod 𝑇) = π)) | 
| 122 | 121 | a1i 11 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ ¬ 2
∥ (𝑋 / π)) →
(𝑘 ∈ ℤ →
(((2 · 𝑘) + 1) =
(𝑋 / π) → (𝑋 mod 𝑇) = π))) | 
| 123 | 122 | rexlimdv 3152 | . . . . . . . 8
⊢ (((𝑋 mod π) = 0 ∧ ¬ 2
∥ (𝑋 / π)) →
(∃𝑘 ∈ ℤ
((2 · 𝑘) + 1) =
(𝑋 / π) → (𝑋 mod 𝑇) = π)) | 
| 124 | 70, 123 | mpd 15 | . . . . . . 7
⊢ (((𝑋 mod π) = 0 ∧ ¬ 2
∥ (𝑋 / π)) →
(𝑋 mod 𝑇) = π) | 
| 125 | 124 | olcd 874 | . . . . . 6
⊢ (((𝑋 mod π) = 0 ∧ ¬ 2
∥ (𝑋 / π)) →
((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π)) | 
| 126 | 67, 125 | pm2.61dan 812 | . . . . 5
⊢ ((𝑋 mod π) = 0 → ((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π)) | 
| 127 |  | 0xr 11309 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 128 | 33 | rexri 11320 | . . . . . . . 8
⊢ π
∈ ℝ* | 
| 129 |  | iocgtlb 45520 | . . . . . . . 8
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (0(,]π)) → 0 < (𝑋 mod 𝑇)) | 
| 130 | 127, 128,
129 | mp3an12 1452 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) ∈ (0(,]π) → 0 < (𝑋 mod 𝑇)) | 
| 131 | 130 | gt0ne0d 11828 | . . . . . 6
⊢ ((𝑋 mod 𝑇) ∈ (0(,]π) → (𝑋 mod 𝑇) ≠ 0) | 
| 132 | 131 | neneqd 2944 | . . . . 5
⊢ ((𝑋 mod 𝑇) ∈ (0(,]π) → ¬ (𝑋 mod 𝑇) = 0) | 
| 133 |  | pm2.53 851 | . . . . . 6
⊢ (((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π) → (¬ (𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) = π)) | 
| 134 | 133 | imp 406 | . . . . 5
⊢ ((((𝑋 mod 𝑇) = 0 ∨ (𝑋 mod 𝑇) = π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) = π) | 
| 135 | 126, 132,
134 | syl2anr 597 | . . . 4
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) = π) | 
| 136 | 127 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑋 mod 𝑇) = π → 0 ∈
ℝ*) | 
| 137 | 128 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑋 mod 𝑇) = π → π ∈
ℝ*) | 
| 138 |  | modcl 13914 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+)
→ (𝑋 mod 𝑇) ∈
ℝ) | 
| 139 | 4, 63, 138 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ (𝑋 mod 𝑇) ∈ ℝ | 
| 140 | 139 | rexri 11320 | . . . . . . . . . . . . 13
⊢ (𝑋 mod 𝑇) ∈
ℝ* | 
| 141 | 140 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ∈
ℝ*) | 
| 142 |  | id 22 | . . . . . . . . . . . . 13
⊢ ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) = π) | 
| 143 | 34, 142 | breqtrrid 5180 | . . . . . . . . . . . 12
⊢ ((𝑋 mod 𝑇) = π → 0 < (𝑋 mod 𝑇)) | 
| 144 | 33 | eqlei2 11373 | . . . . . . . . . . . 12
⊢ ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ≤ π) | 
| 145 | 136, 137,
141, 143, 144 | eliocd 45525 | . . . . . . . . . . 11
⊢ ((𝑋 mod 𝑇) = π → (𝑋 mod 𝑇) ∈ (0(,]π)) | 
| 146 | 145 | iftrued 4532 | . . . . . . . . . 10
⊢ ((𝑋 mod 𝑇) = π → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) =
1) | 
| 147 | 146 | adantl 481 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) =
1) | 
| 148 |  | oveq1 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → (𝑥 mod 𝑇) = (𝑋 mod 𝑇)) | 
| 149 | 148 | breq1d 5152 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → ((𝑥 mod 𝑇) < π ↔ (𝑋 mod 𝑇) < π)) | 
| 150 | 149 | ifbid 4548 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → if((𝑥 mod 𝑇) < π, 1, -1) = if((𝑋 mod 𝑇) < π, 1, -1)) | 
| 151 |  | fourierswlem.f | . . . . . . . . . . . . 13
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) | 
| 152 |  | 1ex 11258 | . . . . . . . . . . . . . 14
⊢ 1 ∈
V | 
| 153 |  | negex 11507 | . . . . . . . . . . . . . 14
⊢ -1 ∈
V | 
| 154 | 152, 153 | ifex 4575 | . . . . . . . . . . . . 13
⊢ if((𝑋 mod 𝑇) < π, 1, -1) ∈
V | 
| 155 | 150, 151,
154 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ ℝ → (𝐹‘𝑋) = if((𝑋 mod 𝑇) < π, 1, -1)) | 
| 156 | 4, 155 | ax-mp 5 | . . . . . . . . . . 11
⊢ (𝐹‘𝑋) = if((𝑋 mod 𝑇) < π, 1, -1) | 
| 157 | 139 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) ∈ ℝ) | 
| 158 |  | id 22 | . . . . . . . . . . . . . 14
⊢ ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) < π) | 
| 159 | 157, 158 | ltned 11398 | . . . . . . . . . . . . 13
⊢ ((𝑋 mod 𝑇) < π → (𝑋 mod 𝑇) ≠ π) | 
| 160 | 159 | necon2bi 2970 | . . . . . . . . . . . 12
⊢ ((𝑋 mod 𝑇) = π → ¬ (𝑋 mod 𝑇) < π) | 
| 161 | 160 | iffalsed 4535 | . . . . . . . . . . 11
⊢ ((𝑋 mod 𝑇) = π → if((𝑋 mod 𝑇) < π, 1, -1) = -1) | 
| 162 | 156, 161 | eqtrid 2788 | . . . . . . . . . 10
⊢ ((𝑋 mod 𝑇) = π → (𝐹‘𝑋) = -1) | 
| 163 | 162 | adantl 481 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (𝐹‘𝑋) = -1) | 
| 164 | 147, 163 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) = (1 + -1)) | 
| 165 |  | 1pneg1e0 12386 | . . . . . . . 8
⊢ (1 + -1)
= 0 | 
| 166 | 164, 165 | eqtrdi 2792 | . . . . . . 7
⊢ (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) = 0) | 
| 167 | 166 | oveq1d 7447 | . . . . . 6
⊢ (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = π) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) = (0 / 2)) | 
| 168 | 167 | adantll 714 | . . . . 5
⊢ ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) = (0 / 2)) | 
| 169 |  | 2cn 12342 | . . . . . . 7
⊢ 2 ∈
ℂ | 
| 170 | 169, 44 | div0i 12002 | . . . . . 6
⊢ (0 / 2) =
0 | 
| 171 | 170 | a1i 11 | . . . . 5
⊢ ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → (0 / 2) =
0) | 
| 172 |  | fourierswlem.y | . . . . . . 7
⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) | 
| 173 |  | iftrue 4530 | . . . . . . 7
⊢ ((𝑋 mod π) = 0 → if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) = 0) | 
| 174 | 172, 173 | eqtr2id 2789 | . . . . . 6
⊢ ((𝑋 mod π) = 0 → 0 = 𝑌) | 
| 175 | 174 | ad2antlr 727 | . . . . 5
⊢ ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → 0 = 𝑌) | 
| 176 | 168, 171,
175 | 3eqtrrd 2781 | . . . 4
⊢ ((((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) ∧ (𝑋 mod 𝑇) = π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 177 | 135, 176 | mpdan 687 | . . 3
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod π) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 178 |  | iftrue 4530 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) ∈ (0(,]π) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) =
1) | 
| 179 | 178 | adantr 480 | . . . . . 6
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) =
1) | 
| 180 | 139 | a1i 11 | . . . . . . . 8
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) ∈ ℝ) | 
| 181 | 33 | a1i 11 | . . . . . . . 8
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → π
∈ ℝ) | 
| 182 |  | iocleub 45521 | . . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (0(,]π)) → (𝑋 mod 𝑇) ≤ π) | 
| 183 | 127, 128,
182 | mp3an12 1452 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (0(,]π) → (𝑋 mod 𝑇) ≤ π) | 
| 184 | 183 | adantr 480 | . . . . . . . 8
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) ≤ π) | 
| 185 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ | 
| 186 | 185, 14 | mulcomi 11270 | . . . . . . . . . . . . . . . . . . 19
⊢ (1
· π) = (π · 1) | 
| 187 | 83, 186 | eqtr3i 2766 | . . . . . . . . . . . . . . . . . 18
⊢ π =
(π · 1) | 
| 188 | 187 | oveq1i 7442 | . . . . . . . . . . . . . . . . 17
⊢ (π +
(π · (2 · (⌊‘(𝑋 / 𝑇))))) = ((π · 1) + (π ·
(2 · (⌊‘(𝑋 / 𝑇))))) | 
| 189 | 169, 14 | mulcomi 11270 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· π) = (π · 2) | 
| 190 | 40, 189 | eqtri 2764 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑇 = (π ·
2) | 
| 191 | 190 | oveq1i 7442 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 · (⌊‘(𝑋 / 𝑇))) = ((π · 2) ·
(⌊‘(𝑋 / 𝑇))) | 
| 192 | 111, 62 | gtneii 11374 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑇 ≠ 0 | 
| 193 | 4, 59, 192 | redivcli 12035 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑋 / 𝑇) ∈ ℝ | 
| 194 |  | flcl 13836 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 / 𝑇) ∈ ℝ →
(⌊‘(𝑋 / 𝑇)) ∈
ℤ) | 
| 195 | 193, 194 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(⌊‘(𝑋 /
𝑇)) ∈
ℤ | 
| 196 |  | zcn 12620 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⌊‘(𝑋 /
𝑇)) ∈ ℤ →
(⌊‘(𝑋 / 𝑇)) ∈
ℂ) | 
| 197 | 195, 196 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢
(⌊‘(𝑋 /
𝑇)) ∈
ℂ | 
| 198 | 14, 169, 197 | mulassi 11273 | . . . . . . . . . . . . . . . . . . 19
⊢ ((π
· 2) · (⌊‘(𝑋 / 𝑇))) = (π · (2 ·
(⌊‘(𝑋 / 𝑇)))) | 
| 199 | 191, 198 | eqtri 2764 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 · (⌊‘(𝑋 / 𝑇))) = (π · (2 ·
(⌊‘(𝑋 / 𝑇)))) | 
| 200 | 199 | oveq2i 7443 | . . . . . . . . . . . . . . . . 17
⊢ (π +
(𝑇 ·
(⌊‘(𝑋 / 𝑇)))) = (π + (π · (2
· (⌊‘(𝑋
/ 𝑇))))) | 
| 201 | 169, 197 | mulcli 11269 | . . . . . . . . . . . . . . . . . 18
⊢ (2
· (⌊‘(𝑋
/ 𝑇))) ∈
ℂ | 
| 202 | 14, 185, 201 | adddii 11274 | . . . . . . . . . . . . . . . . 17
⊢ (π
· (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = ((π · 1) + (π ·
(2 · (⌊‘(𝑋 / 𝑇))))) | 
| 203 | 188, 200,
202 | 3eqtr4ri 2775 | . . . . . . . . . . . . . . . 16
⊢ (π
· (1 + (2 · (⌊‘(𝑋 / 𝑇))))) = (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))) | 
| 204 | 203 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (π =
(𝑋 mod 𝑇) → (π · (1 + (2 ·
(⌊‘(𝑋 / 𝑇))))) = (π + (𝑇 · (⌊‘(𝑋 / 𝑇))))) | 
| 205 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (π =
(𝑋 mod 𝑇) → π = (𝑋 mod 𝑇)) | 
| 206 |  | modval 13912 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+)
→ (𝑋 mod 𝑇) = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇))))) | 
| 207 | 4, 63, 206 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 mod 𝑇) = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) | 
| 208 | 205, 207 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (π =
(𝑋 mod 𝑇) → π = (𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇))))) | 
| 209 | 208 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (π =
(𝑋 mod 𝑇) → (π + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = ((𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) + (𝑇 · (⌊‘(𝑋 / 𝑇))))) | 
| 210 | 27 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (π =
(𝑋 mod 𝑇) → 𝑋 ∈ ℂ) | 
| 211 | 59 | recni 11276 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑇 ∈ ℂ | 
| 212 | 211, 197 | mulcli 11269 | . . . . . . . . . . . . . . . . 17
⊢ (𝑇 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ | 
| 213 | 212 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (π =
(𝑋 mod 𝑇) → (𝑇 · (⌊‘(𝑋 / 𝑇))) ∈ ℂ) | 
| 214 | 210, 213 | npcand 11625 | . . . . . . . . . . . . . . 15
⊢ (π =
(𝑋 mod 𝑇) → ((𝑋 − (𝑇 · (⌊‘(𝑋 / 𝑇)))) + (𝑇 · (⌊‘(𝑋 / 𝑇)))) = 𝑋) | 
| 215 | 204, 209,
214 | 3eqtrrd 2781 | . . . . . . . . . . . . . 14
⊢ (π =
(𝑋 mod 𝑇) → 𝑋 = (π · (1 + (2 ·
(⌊‘(𝑋 / 𝑇)))))) | 
| 216 | 215 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (π =
(𝑋 mod 𝑇) → (𝑋 / π) = ((π · (1 + (2 ·
(⌊‘(𝑋 / 𝑇))))) / π)) | 
| 217 | 185, 201 | addcli 11268 | . . . . . . . . . . . . . 14
⊢ (1 + (2
· (⌊‘(𝑋
/ 𝑇)))) ∈
ℂ | 
| 218 | 217, 14, 35 | divcan3i 12014 | . . . . . . . . . . . . 13
⊢ ((π
· (1 + (2 · (⌊‘(𝑋 / 𝑇))))) / π) = (1 + (2 ·
(⌊‘(𝑋 / 𝑇)))) | 
| 219 | 216, 218 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ (π =
(𝑋 mod 𝑇) → (𝑋 / π) = (1 + (2 ·
(⌊‘(𝑋 / 𝑇))))) | 
| 220 |  | 1z 12649 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ | 
| 221 |  | zmulcl 12668 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (⌊‘(𝑋 / 𝑇)) ∈ ℤ) → (2 ·
(⌊‘(𝑋 / 𝑇))) ∈
ℤ) | 
| 222 | 2, 195, 221 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ (2
· (⌊‘(𝑋
/ 𝑇))) ∈
ℤ | 
| 223 |  | zaddcl 12659 | . . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ (2 · (⌊‘(𝑋 / 𝑇))) ∈ ℤ) → (1 + (2 ·
(⌊‘(𝑋 / 𝑇)))) ∈
ℤ) | 
| 224 | 220, 222,
223 | mp2an 692 | . . . . . . . . . . . . 13
⊢ (1 + (2
· (⌊‘(𝑋
/ 𝑇)))) ∈
ℤ | 
| 225 | 224 | a1i 11 | . . . . . . . . . . . 12
⊢ (π =
(𝑋 mod 𝑇) → (1 + (2 ·
(⌊‘(𝑋 / 𝑇)))) ∈
ℤ) | 
| 226 | 219, 225 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (π =
(𝑋 mod 𝑇) → (𝑋 / π) ∈ ℤ) | 
| 227 | 226, 7 | sylibr 234 | . . . . . . . . . 10
⊢ (π =
(𝑋 mod 𝑇) → (𝑋 mod π) = 0) | 
| 228 | 227 | necon3bi 2966 | . . . . . . . . 9
⊢ (¬
(𝑋 mod π) = 0 →
π ≠ (𝑋 mod 𝑇)) | 
| 229 | 228 | adantl 481 | . . . . . . . 8
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → π ≠
(𝑋 mod 𝑇)) | 
| 230 | 180, 181,
184, 229 | leneltd 11416 | . . . . . . 7
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝑋 mod 𝑇) < π) | 
| 231 |  | iftrue 4530 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) < π → if((𝑋 mod 𝑇) < π, 1, -1) = 1) | 
| 232 | 156, 231 | eqtrid 2788 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) < π → (𝐹‘𝑋) = 1) | 
| 233 | 230, 232 | syl 17 | . . . . . 6
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝐹‘𝑋) = 1) | 
| 234 | 179, 233 | oveq12d 7450 | . . . . 5
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) →
(if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) +
(𝐹‘𝑋)) = (1 + 1)) | 
| 235 | 234 | oveq1d 7447 | . . . 4
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) →
((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) +
(𝐹‘𝑋)) / 2) = ((1 + 1) / 2)) | 
| 236 |  | 1p1e2 12392 | . . . . . . 7
⊢ (1 + 1) =
2 | 
| 237 | 236 | oveq1i 7442 | . . . . . 6
⊢ ((1 + 1)
/ 2) = (2 / 2) | 
| 238 |  | 2div2e1 12408 | . . . . . 6
⊢ (2 / 2) =
1 | 
| 239 | 237, 238 | eqtr2i 2765 | . . . . 5
⊢ 1 = ((1 +
1) / 2) | 
| 240 | 233, 239 | eqtr2di 2793 | . . . 4
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → ((1 + 1)
/ 2) = (𝐹‘𝑋)) | 
| 241 |  | iffalse 4533 | . . . . . 6
⊢ (¬
(𝑋 mod π) = 0 →
if((𝑋 mod π) = 0, 0,
(𝐹‘𝑋)) = (𝐹‘𝑋)) | 
| 242 | 172, 241 | eqtr2id 2789 | . . . . 5
⊢ (¬
(𝑋 mod π) = 0 →
(𝐹‘𝑋) = 𝑌) | 
| 243 | 242 | adantl 481 | . . . 4
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → (𝐹‘𝑋) = 𝑌) | 
| 244 | 235, 240,
243 | 3eqtrrd 2781 | . . 3
⊢ (((𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod π) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 245 | 177, 244 | pm2.61dan 812 | . 2
⊢ ((𝑋 mod 𝑇) ∈ (0(,]π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 246 | 131 | necon2bi 2970 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) = 0 → ¬ (𝑋 mod 𝑇) ∈ (0(,]π)) | 
| 247 | 246 | iffalsed 4535 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) = 0 → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) =
-1) | 
| 248 |  | id 22 | . . . . . . . . . 10
⊢ ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) = 0) | 
| 249 | 248, 34 | eqbrtrdi 5181 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) < π) | 
| 250 | 249 | iftrued 4532 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) = 0 → if((𝑋 mod 𝑇) < π, 1, -1) = 1) | 
| 251 | 156, 250 | eqtrid 2788 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) = 0 → (𝐹‘𝑋) = 1) | 
| 252 | 247, 251 | oveq12d 7450 | . . . . . 6
⊢ ((𝑋 mod 𝑇) = 0 → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) = (-1 + 1)) | 
| 253 | 252 | oveq1d 7447 | . . . . 5
⊢ ((𝑋 mod 𝑇) = 0 → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) = ((-1 + 1) / 2)) | 
| 254 |  | neg1cn 12381 | . . . . . . . . 9
⊢ -1 ∈
ℂ | 
| 255 | 185, 254,
165 | addcomli 11454 | . . . . . . . 8
⊢ (-1 + 1)
= 0 | 
| 256 | 255 | oveq1i 7442 | . . . . . . 7
⊢ ((-1 + 1)
/ 2) = (0 / 2) | 
| 257 | 256, 170 | eqtri 2764 | . . . . . 6
⊢ ((-1 + 1)
/ 2) = 0 | 
| 258 | 257 | a1i 11 | . . . . 5
⊢ ((𝑋 mod 𝑇) = 0 → ((-1 + 1) / 2) =
0) | 
| 259 | 40 | oveq2i 7443 | . . . . . . . . . . . . 13
⊢ (𝑋 / 𝑇) = (𝑋 / (2 · π)) | 
| 260 |  | 2cnne0 12477 | . . . . . . . . . . . . . 14
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 261 | 14, 35 | pm3.2i 470 | . . . . . . . . . . . . . 14
⊢ (π
∈ ℂ ∧ π ≠ 0) | 
| 262 |  | divdiv1 11979 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) →
((𝑋 / 2) / π) = (𝑋 / (2 ·
π))) | 
| 263 | 27, 260, 261, 262 | mp3an 1462 | . . . . . . . . . . . . 13
⊢ ((𝑋 / 2) / π) = (𝑋 / (2 ·
π)) | 
| 264 | 27, 169, 14, 44, 35 | divdiv32i 12023 | . . . . . . . . . . . . 13
⊢ ((𝑋 / 2) / π) = ((𝑋 / π) / 2) | 
| 265 | 259, 263,
264 | 3eqtr2i 2770 | . . . . . . . . . . . 12
⊢ (𝑋 / 𝑇) = ((𝑋 / π) / 2) | 
| 266 | 265 | oveq2i 7443 | . . . . . . . . . . 11
⊢ (2
· (𝑋 / 𝑇)) = (2 · ((𝑋 / π) / 2)) | 
| 267 | 27, 14, 35 | divcli 12010 | . . . . . . . . . . . 12
⊢ (𝑋 / π) ∈
ℂ | 
| 268 | 267, 169,
44 | divcan2i 12011 | . . . . . . . . . . 11
⊢ (2
· ((𝑋 / π) / 2))
= (𝑋 /
π) | 
| 269 | 266, 268 | eqtr2i 2765 | . . . . . . . . . 10
⊢ (𝑋 / π) = (2 · (𝑋 / 𝑇)) | 
| 270 | 2 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑋 / 𝑇) ∈ ℤ → 2 ∈
ℤ) | 
| 271 |  | id 22 | . . . . . . . . . . 11
⊢ ((𝑋 / 𝑇) ∈ ℤ → (𝑋 / 𝑇) ∈ ℤ) | 
| 272 | 270, 271 | zmulcld 12730 | . . . . . . . . . 10
⊢ ((𝑋 / 𝑇) ∈ ℤ → (2 · (𝑋 / 𝑇)) ∈ ℤ) | 
| 273 | 269, 272 | eqeltrid 2844 | . . . . . . . . 9
⊢ ((𝑋 / 𝑇) ∈ ℤ → (𝑋 / π) ∈ ℤ) | 
| 274 | 65, 273 | sylbi 217 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) = 0 → (𝑋 / π) ∈ ℤ) | 
| 275 | 274, 7 | sylibr 234 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) = 0 → (𝑋 mod π) = 0) | 
| 276 | 275 | iftrued 4532 | . . . . . 6
⊢ ((𝑋 mod 𝑇) = 0 → if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) = 0) | 
| 277 | 172, 276 | eqtr2id 2789 | . . . . 5
⊢ ((𝑋 mod 𝑇) = 0 → 0 = 𝑌) | 
| 278 | 253, 258,
277 | 3eqtrrd 2781 | . . . 4
⊢ ((𝑋 mod 𝑇) = 0 → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 279 | 278 | adantl 481 | . . 3
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ (𝑋 mod 𝑇) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 280 | 128 | a1i 11 | . . . . 5
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈
ℝ*) | 
| 281 | 59 | rexri 11320 | . . . . . 6
⊢ 𝑇 ∈
ℝ* | 
| 282 | 281 | a1i 11 | . . . . 5
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → 𝑇 ∈
ℝ*) | 
| 283 | 139 | a1i 11 | . . . . 5
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ ℝ) | 
| 284 |  | pm4.56 990 | . . . . . . . 8
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) ↔ ¬ ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0)) | 
| 285 | 284 | biimpi 216 | . . . . . . 7
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → ¬ ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0)) | 
| 286 |  | olc 868 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) = 0 → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0)) | 
| 287 | 286 | adantl 481 | . . . . . . . 8
⊢ (((𝑋 mod 𝑇) ≤ π ∧ (𝑋 mod 𝑇) = 0) → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0)) | 
| 288 | 127 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → 0 ∈
ℝ*) | 
| 289 | 128 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈
ℝ*) | 
| 290 | 140 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈
ℝ*) | 
| 291 |  | 0red 11265 | . . . . . . . . . . . 12
⊢ (¬
(𝑋 mod 𝑇) = 0 → 0 ∈
ℝ) | 
| 292 | 139 | a1i 11 | . . . . . . . . . . . 12
⊢ (¬
(𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ∈ ℝ) | 
| 293 |  | modge0 13920 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+)
→ 0 ≤ (𝑋 mod 𝑇)) | 
| 294 | 4, 63, 293 | mp2an 692 | . . . . . . . . . . . . 13
⊢ 0 ≤
(𝑋 mod 𝑇) | 
| 295 | 294 | a1i 11 | . . . . . . . . . . . 12
⊢ (¬
(𝑋 mod 𝑇) = 0 → 0 ≤ (𝑋 mod 𝑇)) | 
| 296 |  | neqne 2947 | . . . . . . . . . . . 12
⊢ (¬
(𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ≠ 0) | 
| 297 | 291, 292,
295, 296 | leneltd 11416 | . . . . . . . . . . 11
⊢ (¬
(𝑋 mod 𝑇) = 0 → 0 < (𝑋 mod 𝑇)) | 
| 298 | 297 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → 0 < (𝑋 mod 𝑇)) | 
| 299 |  | simpl 482 | . . . . . . . . . 10
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π) | 
| 300 | 288, 289,
290, 298, 299 | eliocd 45525 | . . . . . . . . 9
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ (0(,]π)) | 
| 301 | 300 | orcd 873 | . . . . . . . 8
⊢ (((𝑋 mod 𝑇) ≤ π ∧ ¬ (𝑋 mod 𝑇) = 0) → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0)) | 
| 302 | 287, 301 | pm2.61dan 812 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) ≤ π → ((𝑋 mod 𝑇) ∈ (0(,]π) ∨ (𝑋 mod 𝑇) = 0)) | 
| 303 | 285, 302 | nsyl 140 | . . . . . 6
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → ¬ (𝑋 mod 𝑇) ≤ π) | 
| 304 | 33 | a1i 11 | . . . . . . 7
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π ∈
ℝ) | 
| 305 | 304, 283 | ltnled 11409 | . . . . . 6
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (π < (𝑋 mod 𝑇) ↔ ¬ (𝑋 mod 𝑇) ≤ π)) | 
| 306 | 303, 305 | mpbird 257 | . . . . 5
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → π < (𝑋 mod 𝑇)) | 
| 307 |  | modlt 13921 | . . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+)
→ (𝑋 mod 𝑇) < 𝑇) | 
| 308 | 4, 63, 307 | mp2an 692 | . . . . . 6
⊢ (𝑋 mod 𝑇) < 𝑇 | 
| 309 | 308 | a1i 11 | . . . . 5
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) < 𝑇) | 
| 310 | 280, 282,
283, 306, 309 | eliood 45516 | . . . 4
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ∈ (π(,)𝑇)) | 
| 311 | 127 | a1i 11 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 0 ∈
ℝ*) | 
| 312 | 33 | a1i 11 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → π ∈
ℝ) | 
| 313 | 140 | a1i 11 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝑋 mod 𝑇) ∈
ℝ*) | 
| 314 |  | ioogtlb 45513 | . . . . . . . . . 10
⊢ ((π
∈ ℝ* ∧ 𝑇 ∈ ℝ* ∧ (𝑋 mod 𝑇) ∈ (π(,)𝑇)) → π < (𝑋 mod 𝑇)) | 
| 315 | 128, 281,
314 | mp3an12 1452 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → π < (𝑋 mod 𝑇)) | 
| 316 | 311, 312,
313, 315 | gtnelioc 45509 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) ∈ (0(,]π)) | 
| 317 | 316 | iffalsed 4535 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) =
-1) | 
| 318 | 139 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝑋 mod 𝑇) ∈ ℝ) | 
| 319 | 312, 318,
315 | ltnsymd 11411 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) < π) | 
| 320 | 319 | iffalsed 4535 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod 𝑇) < π, 1, -1) = -1) | 
| 321 | 156, 320 | eqtrid 2788 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (𝐹‘𝑋) = -1) | 
| 322 | 317, 321 | oveq12d 7450 | . . . . . 6
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) = (-1 + -1)) | 
| 323 | 322 | oveq1d 7447 | . . . . 5
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) = ((-1 + -1) / 2)) | 
| 324 |  | df-2 12330 | . . . . . . . . . 10
⊢ 2 = (1 +
1) | 
| 325 | 324 | negeqi 11502 | . . . . . . . . 9
⊢ -2 = -(1
+ 1) | 
| 326 | 185, 185 | negdii 11594 | . . . . . . . . 9
⊢ -(1 + 1)
= (-1 + -1) | 
| 327 | 325, 326 | eqtr2i 2765 | . . . . . . . 8
⊢ (-1 + -1)
= -2 | 
| 328 | 327 | oveq1i 7442 | . . . . . . 7
⊢ ((-1 +
-1) / 2) = (-2 / 2) | 
| 329 |  | divneg 11960 | . . . . . . . 8
⊢ ((2
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(2 / 2) = (-2 /
2)) | 
| 330 | 169, 169,
44, 329 | mp3an 1462 | . . . . . . 7
⊢ -(2 / 2)
= (-2 / 2) | 
| 331 | 238 | negeqi 11502 | . . . . . . 7
⊢ -(2 / 2)
= -1 | 
| 332 | 328, 330,
331 | 3eqtr2i 2770 | . . . . . 6
⊢ ((-1 +
-1) / 2) = -1 | 
| 333 | 332 | a1i 11 | . . . . 5
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ((-1 + -1) / 2) =
-1) | 
| 334 | 172 | a1i 11 | . . . . . 6
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋))) | 
| 335 | 312, 318 | ltnled 11409 | . . . . . . . . 9
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → (π < (𝑋 mod 𝑇) ↔ ¬ (𝑋 mod 𝑇) ≤ π)) | 
| 336 | 315, 335 | mpbid 232 | . . . . . . . 8
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod 𝑇) ≤ π) | 
| 337 | 248, 112 | eqbrtrdi 5181 | . . . . . . . . . 10
⊢ ((𝑋 mod 𝑇) = 0 → (𝑋 mod 𝑇) ≤ π) | 
| 338 | 337 | adantl 481 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ (𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π) | 
| 339 | 126 | orcanai 1004 | . . . . . . . . . 10
⊢ (((𝑋 mod π) = 0 ∧ ¬
(𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) = π) | 
| 340 | 339, 144 | syl 17 | . . . . . . . . 9
⊢ (((𝑋 mod π) = 0 ∧ ¬
(𝑋 mod 𝑇) = 0) → (𝑋 mod 𝑇) ≤ π) | 
| 341 | 338, 340 | pm2.61dan 812 | . . . . . . . 8
⊢ ((𝑋 mod π) = 0 → (𝑋 mod 𝑇) ≤ π) | 
| 342 | 336, 341 | nsyl 140 | . . . . . . 7
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → ¬ (𝑋 mod π) = 0) | 
| 343 | 342 | iffalsed 4535 | . . . . . 6
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) = (𝐹‘𝑋)) | 
| 344 | 334, 343,
321 | 3eqtrrd 2781 | . . . . 5
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → -1 = 𝑌) | 
| 345 | 323, 333,
344 | 3eqtrrd 2781 | . . . 4
⊢ ((𝑋 mod 𝑇) ∈ (π(,)𝑇) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 346 | 310, 345 | syl 17 | . . 3
⊢ ((¬
(𝑋 mod 𝑇) ∈ (0(,]π) ∧ ¬ (𝑋 mod 𝑇) = 0) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 347 | 279, 346 | pm2.61dan 812 | . 2
⊢ (¬
(𝑋 mod 𝑇) ∈ (0(,]π) → 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2)) | 
| 348 | 245, 347 | pm2.61i 182 | 1
⊢ 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) |