Metamath Proof Explorer

Theorem fourierswlem

Description: The Fourier series for the square wave F converges to Y , a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierswlem.t ⊢ 𝑇 = ( 2 · π )
fourierswlem.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
fourierswlem.x ⊢ 𝑋 ∈ ℝ
fourierswlem.y ⊢ 𝑌 = if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) )
Assertion fourierswlem 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 )

Proof

Step Hyp Ref Expression
1 fourierswlem.t ⊢ 𝑇 = ( 2 · π )
2 fourierswlem.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
3 fourierswlem.x ⊢ 𝑋 ∈ ℝ
4 fourierswlem.y ⊢ 𝑌 = if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) )
5 simpr ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → 2 ∥ ( 𝑋 / π ) )
6 2z ⊢ 2 ∈ ℤ
7 6 a1i ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → 2 ∈ ℤ )
8 pirp ⊢ π ∈ ℝ+
9 mod0 ⊢ ( ( 𝑋 ∈ ℝ ∧ π ∈ ℝ+ ) → ( ( 𝑋 mod π ) = 0 ↔ ( 𝑋 / π ) ∈ ℤ ) )
10 3 8 9 mp2an ⊢ ( ( 𝑋 mod π ) = 0 ↔ ( 𝑋 / π ) ∈ ℤ )
11 10 biimpi ⊢ ( ( 𝑋 mod π ) = 0 → ( 𝑋 / π ) ∈ ℤ )
12 11 adantr ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( 𝑋 / π ) ∈ ℤ )
13 divides ⊢ ( ( 2 ∈ ℤ ∧ ( 𝑋 / π ) ∈ ℤ ) → ( 2 ∥ ( 𝑋 / π ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) )
14 7 12 13 syl2anc ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( 2 ∥ ( 𝑋 / π ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) )
15 5 14 mpbid ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑋 / π ) )
16 2cnd ⊢ ( 𝑘 ∈ ℤ → 2 ∈ ℂ )
17 picn ⊢ π ∈ ℂ
18 17 a1i ⊢ ( 𝑘 ∈ ℤ → π ∈ ℂ )
19 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
20 16 18 19 mulassd ⊢ ( 𝑘 ∈ ℤ → ( ( 2 · π ) · 𝑘 ) = ( 2 · ( π · 𝑘 ) ) )
21 18 19 mulcld ⊢ ( 𝑘 ∈ ℤ → ( π · 𝑘 ) ∈ ℂ )
22 16 21 mulcomd ⊢ ( 𝑘 ∈ ℤ → ( 2 · ( π · 𝑘 ) ) = ( ( π · 𝑘 ) · 2 ) )
23 20 22 eqtrd ⊢ ( 𝑘 ∈ ℤ → ( ( 2 · π ) · 𝑘 ) = ( ( π · 𝑘 ) · 2 ) )
24 23 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( ( 2 · π ) · 𝑘 ) = ( ( π · 𝑘 ) · 2 ) )
25 18 19 16 mulassd ⊢ ( 𝑘 ∈ ℤ → ( ( π · 𝑘 ) · 2 ) = ( π · ( 𝑘 · 2 ) ) )
26 25 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( ( π · 𝑘 ) · 2 ) = ( π · ( 𝑘 · 2 ) ) )
27 id ⊢ ( ( 𝑘 · 2 ) = ( 𝑋 / π ) → ( 𝑘 · 2 ) = ( 𝑋 / π ) )
28 27 eqcomd ⊢ ( ( 𝑘 · 2 ) = ( 𝑋 / π ) → ( 𝑋 / π ) = ( 𝑘 · 2 ) )
29 28 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( 𝑋 / π ) = ( 𝑘 · 2 ) )
30 3 recni ⊢ 𝑋 ∈ ℂ
31 30 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → 𝑋 ∈ ℂ )
32 17 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → π ∈ ℂ )
33 19 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → 𝑘 ∈ ℂ )
34 2cnd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → 2 ∈ ℂ )
35 33 34 mulcld ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( 𝑘 · 2 ) ∈ ℂ )
36 pire ⊢ π ∈ ℝ
37 pipos ⊢ 0 < π
38 36 37 gt0ne0ii ⊢ π ≠ 0
39 38 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → π ≠ 0 )
40 31 32 35 39 divmuld ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( ( 𝑋 / π ) = ( 𝑘 · 2 ) ↔ ( π · ( 𝑘 · 2 ) ) = 𝑋 ) )
41 29 40 mpbid ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( π · ( 𝑘 · 2 ) ) = 𝑋 )
42 24 26 41 3eqtrrd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → 𝑋 = ( ( 2 · π ) · 𝑘 ) )
43 1 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → 𝑇 = ( 2 · π ) )
44 42 43 oveq12d ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( 𝑋 / 𝑇 ) = ( ( ( 2 · π ) · 𝑘 ) / ( 2 · π ) ) )
45 16 18 mulcld ⊢ ( 𝑘 ∈ ℤ → ( 2 · π ) ∈ ℂ )
46 2ne0 ⊢ 2 ≠ 0
47 46 a1i ⊢ ( 𝑘 ∈ ℤ → 2 ≠ 0 )
48 38 a1i ⊢ ( 𝑘 ∈ ℤ → π ≠ 0 )
49 16 18 47 48 mulne0d ⊢ ( 𝑘 ∈ ℤ → ( 2 · π ) ≠ 0 )
50 19 45 49 divcan3d ⊢ ( 𝑘 ∈ ℤ → ( ( ( 2 · π ) · 𝑘 ) / ( 2 · π ) ) = 𝑘 )
51 50 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( ( ( 2 · π ) · 𝑘 ) / ( 2 · π ) ) = 𝑘 )
52 44 51 eqtrd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( 𝑋 / 𝑇 ) = 𝑘 )
53 simpl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → 𝑘 ∈ ℤ )
54 52 53 eqeltrd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 · 2 ) = ( 𝑋 / π ) ) → ( 𝑋 / 𝑇 ) ∈ ℤ )
55 54 ex ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 · 2 ) = ( 𝑋 / π ) → ( 𝑋 / 𝑇 ) ∈ ℤ ) )
56 55 a1i ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( 𝑘 ∈ ℤ → ( ( 𝑘 · 2 ) = ( 𝑋 / π ) → ( 𝑋 / 𝑇 ) ∈ ℤ ) ) )
57 56 rexlimdv ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑋 / π ) → ( 𝑋 / 𝑇 ) ∈ ℤ ) )
58 15 57 mpd ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( 𝑋 / 𝑇 ) ∈ ℤ )
59 2re ⊢ 2 ∈ ℝ
60 59 36 remulcli ⊢ ( 2 · π ) ∈ ℝ
61 1 60 eqeltri ⊢ 𝑇 ∈ ℝ
62 2pos ⊢ 0 < 2
63 59 36 62 37 mulgt0ii ⊢ 0 < ( 2 · π )
64 63 1 breqtrri ⊢ 0 < 𝑇
65 61 64 elrpii ⊢ 𝑇 ∈ ℝ+
66 mod0 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) → ( ( 𝑋 mod 𝑇 ) = 0 ↔ ( 𝑋 / 𝑇 ) ∈ ℤ ) )
67 3 65 66 mp2an ⊢ ( ( 𝑋 mod 𝑇 ) = 0 ↔ ( 𝑋 / 𝑇 ) ∈ ℤ )
68 58 67 sylibr ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( 𝑋 mod 𝑇 ) = 0 )
69 68 orcd ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ 2 ∥ ( 𝑋 / π ) ) → ( ( 𝑋 mod 𝑇 ) = 0 ∨ ( 𝑋 mod 𝑇 ) = π ) )
70 odd2np1 ⊢ ( ( 𝑋 / π ) ∈ ℤ → ( ¬ 2 ∥ ( 𝑋 / π ) ↔ ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) )
71 10 70 sylbi ⊢ ( ( 𝑋 mod π ) = 0 → ( ¬ 2 ∥ ( 𝑋 / π ) ↔ ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) )
72 71 biimpa ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ 2 ∥ ( 𝑋 / π ) ) → ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) )
73 16 19 mulcld ⊢ ( 𝑘 ∈ ℤ → ( 2 · 𝑘 ) ∈ ℂ )
74 73 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( 2 · 𝑘 ) ∈ ℂ )
75 1cnd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → 1 ∈ ℂ )
76 17 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → π ∈ ℂ )
77 74 75 76 adddird ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( ( 2 · 𝑘 ) + 1 ) · π ) = ( ( ( 2 · 𝑘 ) · π ) + ( 1 · π ) ) )
78 16 19 mulcomd ⊢ ( 𝑘 ∈ ℤ → ( 2 · 𝑘 ) = ( 𝑘 · 2 ) )
79 78 oveq1d ⊢ ( 𝑘 ∈ ℤ → ( ( 2 · 𝑘 ) · π ) = ( ( 𝑘 · 2 ) · π ) )
80 19 16 18 mulassd ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 · 2 ) · π ) = ( 𝑘 · ( 2 · π ) ) )
81 1 eqcomi ⊢ ( 2 · π ) = 𝑇
82 81 a1i ⊢ ( 𝑘 ∈ ℤ → ( 2 · π ) = 𝑇 )
83 82 oveq2d ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 · ( 2 · π ) ) = ( 𝑘 · 𝑇 ) )
84 79 80 83 3eqtrd ⊢ ( 𝑘 ∈ ℤ → ( ( 2 · 𝑘 ) · π ) = ( 𝑘 · 𝑇 ) )
85 17 mullidi ⊢ ( 1 · π ) = π
86 85 a1i ⊢ ( 𝑘 ∈ ℤ → ( 1 · π ) = π )
87 84 86 oveq12d ⊢ ( 𝑘 ∈ ℤ → ( ( ( 2 · 𝑘 ) · π ) + ( 1 · π ) ) = ( ( 𝑘 · 𝑇 ) + π ) )
88 87 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( ( 2 · 𝑘 ) · π ) + ( 1 · π ) ) = ( ( 𝑘 · 𝑇 ) + π ) )
89 1 45 eqeltrid ⊢ ( 𝑘 ∈ ℤ → 𝑇 ∈ ℂ )
90 19 89 mulcld ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 · 𝑇 ) ∈ ℂ )
91 90 18 addcomd ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 · 𝑇 ) + π ) = ( π + ( 𝑘 · 𝑇 ) ) )
92 91 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( 𝑘 · 𝑇 ) + π ) = ( π + ( 𝑘 · 𝑇 ) ) )
93 77 88 92 3eqtrrd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( π + ( 𝑘 · 𝑇 ) ) = ( ( ( 2 · 𝑘 ) + 1 ) · π ) )
94 peano2cn ⊢ ( ( 2 · 𝑘 ) ∈ ℂ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
95 73 94 syl ⊢ ( 𝑘 ∈ ℤ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
96 95 18 mulcomd ⊢ ( 𝑘 ∈ ℤ → ( ( ( 2 · 𝑘 ) + 1 ) · π ) = ( π · ( ( 2 · 𝑘 ) + 1 ) ) )
97 96 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( ( 2 · 𝑘 ) + 1 ) · π ) = ( π · ( ( 2 · 𝑘 ) + 1 ) ) )
98 id ⊢ ( ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) → ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) )
99 98 eqcomd ⊢ ( ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) → ( 𝑋 / π ) = ( ( 2 · 𝑘 ) + 1 ) )
100 99 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( 𝑋 / π ) = ( ( 2 · 𝑘 ) + 1 ) )
101 30 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → 𝑋 ∈ ℂ )
102 95 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
103 38 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → π ≠ 0 )
104 101 76 102 103 divmuld ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( 𝑋 / π ) = ( ( 2 · 𝑘 ) + 1 ) ↔ ( π · ( ( 2 · 𝑘 ) + 1 ) ) = 𝑋 ) )
105 100 104 mpbid ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( π · ( ( 2 · 𝑘 ) + 1 ) ) = 𝑋 )
106 93 97 105 3eqtrrd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → 𝑋 = ( π + ( 𝑘 · 𝑇 ) ) )
107 106 oveq1d ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( 𝑋 mod 𝑇 ) = ( ( π + ( 𝑘 · 𝑇 ) ) mod 𝑇 ) )
108 modcyc ⊢ ( ( π ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( ( π + ( 𝑘 · 𝑇 ) ) mod 𝑇 ) = ( π mod 𝑇 ) )
109 36 65 108 mp3an12 ⊢ ( 𝑘 ∈ ℤ → ( ( π + ( 𝑘 · 𝑇 ) ) mod 𝑇 ) = ( π mod 𝑇 ) )
110 109 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( ( π + ( 𝑘 · 𝑇 ) ) mod 𝑇 ) = ( π mod 𝑇 ) )
111 36 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → π ∈ ℝ )
112 65 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → 𝑇 ∈ ℝ+ )
113 0re ⊢ 0 ∈ ℝ
114 113 36 37 ltleii ⊢ 0 ≤ π
115 114 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → 0 ≤ π )
116 2timesgt ⊢ ( π ∈ ℝ+ → π < ( 2 · π ) )
117 8 116 ax-mp ⊢ π < ( 2 · π )
118 117 1 breqtrri ⊢ π < 𝑇
119 118 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → π < 𝑇 )
120 modid ⊢ ( ( ( π ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) ∧ ( 0 ≤ π ∧ π < 𝑇 ) ) → ( π mod 𝑇 ) = π )
121 111 112 115 119 120 syl22anc ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( π mod 𝑇 ) = π )
122 107 110 121 3eqtrd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) ) → ( 𝑋 mod 𝑇 ) = π )
123 122 ex ⊢ ( 𝑘 ∈ ℤ → ( ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) → ( 𝑋 mod 𝑇 ) = π ) )
124 123 a1i ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ 2 ∥ ( 𝑋 / π ) ) → ( 𝑘 ∈ ℤ → ( ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) → ( 𝑋 mod 𝑇 ) = π ) ) )
125 124 rexlimdv ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ 2 ∥ ( 𝑋 / π ) ) → ( ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( 𝑋 / π ) → ( 𝑋 mod 𝑇 ) = π ) )
126 72 125 mpd ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ 2 ∥ ( 𝑋 / π ) ) → ( 𝑋 mod 𝑇 ) = π )
127 126 olcd ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ 2 ∥ ( 𝑋 / π ) ) → ( ( 𝑋 mod 𝑇 ) = 0 ∨ ( 𝑋 mod 𝑇 ) = π ) )
128 69 127 pm2.61dan ⊢ ( ( 𝑋 mod π ) = 0 → ( ( 𝑋 mod 𝑇 ) = 0 ∨ ( 𝑋 mod 𝑇 ) = π ) )
129 0xr ⊢ 0 ∈ ℝ*
130 36 rexri ⊢ π ∈ ℝ*
131 iocgtlb ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ) → 0 < ( 𝑋 mod 𝑇 ) )
132 129 130 131 mp3an12 ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → 0 < ( 𝑋 mod 𝑇 ) )
133 132 gt0ne0d ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → ( 𝑋 mod 𝑇 ) ≠ 0 )
134 133 neneqd ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → ¬ ( 𝑋 mod 𝑇 ) = 0 )
135 pm2.53 ⊢ ( ( ( 𝑋 mod 𝑇 ) = 0 ∨ ( 𝑋 mod 𝑇 ) = π ) → ( ¬ ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod 𝑇 ) = π ) )
136 135 imp ⊢ ( ( ( ( 𝑋 mod 𝑇 ) = 0 ∨ ( 𝑋 mod 𝑇 ) = π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) = π )
137 128 134 136 syl2anr ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod π ) = 0 ) → ( 𝑋 mod 𝑇 ) = π )
138 129 a1i ⊢ ( ( 𝑋 mod 𝑇 ) = π → 0 ∈ ℝ* )
139 130 a1i ⊢ ( ( 𝑋 mod 𝑇 ) = π → π ∈ ℝ* )
140 modcl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) → ( 𝑋 mod 𝑇 ) ∈ ℝ )
141 3 65 140 mp2an ⊢ ( 𝑋 mod 𝑇 ) ∈ ℝ
142 141 rexri ⊢ ( 𝑋 mod 𝑇 ) ∈ ℝ*
143 142 a1i ⊢ ( ( 𝑋 mod 𝑇 ) = π → ( 𝑋 mod 𝑇 ) ∈ ℝ* )
144 id ⊢ ( ( 𝑋 mod 𝑇 ) = π → ( 𝑋 mod 𝑇 ) = π )
145 37 144 breqtrrid ⊢ ( ( 𝑋 mod 𝑇 ) = π → 0 < ( 𝑋 mod 𝑇 ) )
146 36 eqlei2 ⊢ ( ( 𝑋 mod 𝑇 ) = π → ( 𝑋 mod 𝑇 ) ≤ π )
147 138 139 143 145 146 eliocd ⊢ ( ( 𝑋 mod 𝑇 ) = π → ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) )
148 147 iftrued ⊢ ( ( 𝑋 mod 𝑇 ) = π → if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) = 1 )
149 148 adantl ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ( 𝑋 mod 𝑇 ) = π ) → if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) = 1 )
150 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 mod 𝑇 ) = ( 𝑋 mod 𝑇 ) )
151 150 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 mod 𝑇 ) < π ↔ ( 𝑋 mod 𝑇 ) < π ) )
152 151 ifbid ⊢ ( 𝑥 = 𝑋 → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) = if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) )
153 1ex ⊢ 1 ∈ V
154 negex ⊢ - 1 ∈ V
155 153 154 ifex ⊢ if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) ∈ V
156 152 2 155 fvmpt ⊢ ( 𝑋 ∈ ℝ → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) )
157 3 156 ax-mp ⊢ ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 )
158 141 a1i ⊢ ( ( 𝑋 mod 𝑇 ) < π → ( 𝑋 mod 𝑇 ) ∈ ℝ )
159 id ⊢ ( ( 𝑋 mod 𝑇 ) < π → ( 𝑋 mod 𝑇 ) < π )
160 158 159 ltned ⊢ ( ( 𝑋 mod 𝑇 ) < π → ( 𝑋 mod 𝑇 ) ≠ π )
161 160 necon2bi ⊢ ( ( 𝑋 mod 𝑇 ) = π → ¬ ( 𝑋 mod 𝑇 ) < π )
162 161 iffalsed ⊢ ( ( 𝑋 mod 𝑇 ) = π → if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) = - 1 )
163 157 162 eqtrid ⊢ ( ( 𝑋 mod 𝑇 ) = π → ( 𝐹 ‘ 𝑋 ) = - 1 )
164 163 adantl ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ( 𝑋 mod 𝑇 ) = π ) → ( 𝐹 ‘ 𝑋 ) = - 1 )
165 149 164 oveq12d ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ( 𝑋 mod 𝑇 ) = π ) → ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) = ( 1 + - 1 ) )
166 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
167 165 166 eqtrdi ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ( 𝑋 mod 𝑇 ) = π ) → ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) = 0 )
168 167 oveq1d ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ( 𝑋 mod 𝑇 ) = π ) → ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( 0 / 2 ) )
169 168 adantll ⊢ ( ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod π ) = 0 ) ∧ ( 𝑋 mod 𝑇 ) = π ) → ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( 0 / 2 ) )
170 2cn ⊢ 2 ∈ ℂ
171 170 46 div0i ⊢ ( 0 / 2 ) = 0
172 171 a1i ⊢ ( ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod π ) = 0 ) ∧ ( 𝑋 mod 𝑇 ) = π ) → ( 0 / 2 ) = 0 )
173 iftrue ⊢ ( ( 𝑋 mod π ) = 0 → if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) ) = 0 )
174 4 173 eqtr2id ⊢ ( ( 𝑋 mod π ) = 0 → 0 = 𝑌 )
175 174 ad2antlr ⊢ ( ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod π ) = 0 ) ∧ ( 𝑋 mod 𝑇 ) = π ) → 0 = 𝑌 )
176 169 172 175 3eqtrrd ⊢ ( ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod π ) = 0 ) ∧ ( 𝑋 mod 𝑇 ) = π ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
177 137 176 mpdan ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod π ) = 0 ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
178 iftrue ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) = 1 )
179 178 adantr ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) = 1 )
180 141 a1i ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( 𝑋 mod 𝑇 ) ∈ ℝ )
181 36 a1i ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → π ∈ ℝ )
182 iocleub ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ) → ( 𝑋 mod 𝑇 ) ≤ π )
183 129 130 182 mp3an12 ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → ( 𝑋 mod 𝑇 ) ≤ π )
184 183 adantr ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( 𝑋 mod 𝑇 ) ≤ π )
185 ax-1cn ⊢ 1 ∈ ℂ
186 185 17 mulcomi ⊢ ( 1 · π ) = ( π · 1 )
187 85 186 eqtr3i ⊢ π = ( π · 1 )
188 187 oveq1i ⊢ ( π + ( π · ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) = ( ( π · 1 ) + ( π · ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
189 170 17 mulcomi ⊢ ( 2 · π ) = ( π · 2 )
190 1 189 eqtri ⊢ 𝑇 = ( π · 2 )
191 190 oveq1i ⊢ ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) = ( ( π · 2 ) · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) )
192 113 64 gtneii ⊢ 𝑇 ≠ 0
193 3 61 192 redivcli ⊢ ( 𝑋 / 𝑇 ) ∈ ℝ
194 flcl ⊢ ( ( 𝑋 / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ∈ ℤ )
195 193 194 ax-mp ⊢ ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ∈ ℤ
196 zcn ⊢ ( ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ∈ ℤ → ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ∈ ℂ )
197 195 196 ax-mp ⊢ ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ∈ ℂ
198 17 170 197 mulassi ⊢ ( ( π · 2 ) · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) = ( π · ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) )
199 191 198 eqtri ⊢ ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) = ( π · ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) )
200 199 oveq2i ⊢ ( π + ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) = ( π + ( π · ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
201 170 197 mulcli ⊢ ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ∈ ℂ
202 17 185 201 adddii ⊢ ( π · ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) = ( ( π · 1 ) + ( π · ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
203 188 200 202 3eqtr4ri ⊢ ( π · ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) = ( π + ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) )
204 203 a1i ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( π · ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) = ( π + ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
205 id ⊢ ( π = ( 𝑋 mod 𝑇 ) → π = ( 𝑋 mod 𝑇 ) )
206 modval ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) → ( 𝑋 mod 𝑇 ) = ( 𝑋 − ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
207 3 65 206 mp2an ⊢ ( 𝑋 mod 𝑇 ) = ( 𝑋 − ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) )
208 205 207 eqtrdi ⊢ ( π = ( 𝑋 mod 𝑇 ) → π = ( 𝑋 − ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
209 208 oveq1d ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( π + ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) = ( ( 𝑋 − ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) + ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
210 30 a1i ⊢ ( π = ( 𝑋 mod 𝑇 ) → 𝑋 ∈ ℂ )
211 61 recni ⊢ 𝑇 ∈ ℂ
212 211 197 mulcli ⊢ ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ∈ ℂ
213 212 a1i ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ∈ ℂ )
214 210 213 npcand ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( ( 𝑋 − ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) + ( 𝑇 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) = 𝑋 )
215 204 209 214 3eqtrrd ⊢ ( π = ( 𝑋 mod 𝑇 ) → 𝑋 = ( π · ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) )
216 215 oveq1d ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( 𝑋 / π ) = ( ( π · ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) / π ) )
217 185 201 addcli ⊢ ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ∈ ℂ
218 217 17 38 divcan3i ⊢ ( ( π · ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ) / π ) = ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) )
219 216 218 eqtrdi ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( 𝑋 / π ) = ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) )
220 1z ⊢ 1 ∈ ℤ
221 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ∈ ℤ ) → ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ∈ ℤ )
222 6 195 221 mp2an ⊢ ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ∈ ℤ
223 zaddcl ⊢ ( ( 1 ∈ ℤ ∧ ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ∈ ℤ ) → ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ∈ ℤ )
224 220 222 223 mp2an ⊢ ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ∈ ℤ
225 224 a1i ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( 1 + ( 2 · ( ⌊ ‘ ( 𝑋 / 𝑇 ) ) ) ) ∈ ℤ )
226 219 225 eqeltrd ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( 𝑋 / π ) ∈ ℤ )
227 226 10 sylibr ⊢ ( π = ( 𝑋 mod 𝑇 ) → ( 𝑋 mod π ) = 0 )
228 227 necon3bi ⊢ ( ¬ ( 𝑋 mod π ) = 0 → π ≠ ( 𝑋 mod 𝑇 ) )
229 228 adantl ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → π ≠ ( 𝑋 mod 𝑇 ) )
230 180 181 184 229 leneltd ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( 𝑋 mod 𝑇 ) < π )
231 iftrue ⊢ ( ( 𝑋 mod 𝑇 ) < π → if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) = 1 )
232 157 231 eqtrid ⊢ ( ( 𝑋 mod 𝑇 ) < π → ( 𝐹 ‘ 𝑋 ) = 1 )
233 230 232 syl ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( 𝐹 ‘ 𝑋 ) = 1 )
234 179 233 oveq12d ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) = ( 1 + 1 ) )
235 234 oveq1d ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( ( 1 + 1 ) / 2 ) )
236 1p1e2 ⊢ ( 1 + 1 ) = 2
237 236 oveq1i ⊢ ( ( 1 + 1 ) / 2 ) = ( 2 / 2 )
238 2div2e1 ⊢ ( 2 / 2 ) = 1
239 237 238 eqtr2i ⊢ 1 = ( ( 1 + 1 ) / 2 )
240 233 239 eqtr2di ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( ( 1 + 1 ) / 2 ) = ( 𝐹 ‘ 𝑋 ) )
241 iffalse ⊢ ( ¬ ( 𝑋 mod π ) = 0 → if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
242 4 241 eqtr2id ⊢ ( ¬ ( 𝑋 mod π ) = 0 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
243 242 adantl ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
244 235 240 243 3eqtrrd ⊢ ( ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod π ) = 0 ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
245 177 244 pm2.61dan ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
246 133 necon2bi ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) )
247 246 iffalsed ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) = - 1 )
248 id ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod 𝑇 ) = 0 )
249 248 37 eqbrtrdi ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod 𝑇 ) < π )
250 249 iftrued ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) = 1 )
251 157 250 eqtrid ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( 𝐹 ‘ 𝑋 ) = 1 )
252 247 251 oveq12d ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) = ( - 1 + 1 ) )
253 252 oveq1d ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( ( - 1 + 1 ) / 2 ) )
254 neg1cn ⊢ - 1 ∈ ℂ
255 185 254 166 addcomli ⊢ ( - 1 + 1 ) = 0
256 255 oveq1i ⊢ ( ( - 1 + 1 ) / 2 ) = ( 0 / 2 )
257 256 171 eqtri ⊢ ( ( - 1 + 1 ) / 2 ) = 0
258 257 a1i ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( ( - 1 + 1 ) / 2 ) = 0 )
259 1 oveq2i ⊢ ( 𝑋 / 𝑇 ) = ( 𝑋 / ( 2 · π ) )
260 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
261 17 38 pm3.2i ⊢ ( π ∈ ℂ ∧ π ≠ 0 )
262 divdiv1 ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( π ∈ ℂ ∧ π ≠ 0 ) ) → ( ( 𝑋 / 2 ) / π ) = ( 𝑋 / ( 2 · π ) ) )
263 30 260 261 262 mp3an ⊢ ( ( 𝑋 / 2 ) / π ) = ( 𝑋 / ( 2 · π ) )
264 30 170 17 46 38 divdiv32i ⊢ ( ( 𝑋 / 2 ) / π ) = ( ( 𝑋 / π ) / 2 )
265 259 263 264 3eqtr2i ⊢ ( 𝑋 / 𝑇 ) = ( ( 𝑋 / π ) / 2 )
266 265 oveq2i ⊢ ( 2 · ( 𝑋 / 𝑇 ) ) = ( 2 · ( ( 𝑋 / π ) / 2 ) )
267 30 17 38 divcli ⊢ ( 𝑋 / π ) ∈ ℂ
268 267 170 46 divcan2i ⊢ ( 2 · ( ( 𝑋 / π ) / 2 ) ) = ( 𝑋 / π )
269 266 268 eqtr2i ⊢ ( 𝑋 / π ) = ( 2 · ( 𝑋 / 𝑇 ) )
270 6 a1i ⊢ ( ( 𝑋 / 𝑇 ) ∈ ℤ → 2 ∈ ℤ )
271 id ⊢ ( ( 𝑋 / 𝑇 ) ∈ ℤ → ( 𝑋 / 𝑇 ) ∈ ℤ )
272 270 271 zmulcld ⊢ ( ( 𝑋 / 𝑇 ) ∈ ℤ → ( 2 · ( 𝑋 / 𝑇 ) ) ∈ ℤ )
273 269 272 eqeltrid ⊢ ( ( 𝑋 / 𝑇 ) ∈ ℤ → ( 𝑋 / π ) ∈ ℤ )
274 67 273 sylbi ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 / π ) ∈ ℤ )
275 274 10 sylibr ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod π ) = 0 )
276 275 iftrued ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) ) = 0 )
277 4 276 eqtr2id ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → 0 = 𝑌 )
278 253 258 277 3eqtrrd ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
279 278 adantl ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ( 𝑋 mod 𝑇 ) = 0 ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
280 130 a1i ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → π ∈ ℝ* )
281 61 rexri ⊢ 𝑇 ∈ ℝ*
282 281 a1i ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → 𝑇 ∈ ℝ* )
283 141 a1i ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ∈ ℝ )
284 pm4.56 ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) ↔ ¬ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∨ ( 𝑋 mod 𝑇 ) = 0 ) )
285 284 biimpi ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ¬ ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∨ ( 𝑋 mod 𝑇 ) = 0 ) )
286 olc ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∨ ( 𝑋 mod 𝑇 ) = 0 ) )
287 286 adantl ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ( 𝑋 mod 𝑇 ) = 0 ) → ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∨ ( 𝑋 mod 𝑇 ) = 0 ) )
288 129 a1i ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → 0 ∈ ℝ* )
289 130 a1i ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → π ∈ ℝ* )
290 142 a1i ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ∈ ℝ* )
291 0red ⊢ ( ¬ ( 𝑋 mod 𝑇 ) = 0 → 0 ∈ ℝ )
292 141 a1i ⊢ ( ¬ ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod 𝑇 ) ∈ ℝ )
293 modge0 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) → 0 ≤ ( 𝑋 mod 𝑇 ) )
294 3 65 293 mp2an ⊢ 0 ≤ ( 𝑋 mod 𝑇 )
295 294 a1i ⊢ ( ¬ ( 𝑋 mod 𝑇 ) = 0 → 0 ≤ ( 𝑋 mod 𝑇 ) )
296 neqne ⊢ ( ¬ ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod 𝑇 ) ≠ 0 )
297 291 292 295 296 leneltd ⊢ ( ¬ ( 𝑋 mod 𝑇 ) = 0 → 0 < ( 𝑋 mod 𝑇 ) )
298 297 adantl ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → 0 < ( 𝑋 mod 𝑇 ) )
299 simpl ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ≤ π )
300 288 289 290 298 299 eliocd ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) )
301 300 orcd ⊢ ( ( ( 𝑋 mod 𝑇 ) ≤ π ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∨ ( 𝑋 mod 𝑇 ) = 0 ) )
302 287 301 pm2.61dan ⊢ ( ( 𝑋 mod 𝑇 ) ≤ π → ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∨ ( 𝑋 mod 𝑇 ) = 0 ) )
303 285 302 nsyl ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ¬ ( 𝑋 mod 𝑇 ) ≤ π )
304 36 a1i ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → π ∈ ℝ )
305 304 283 ltnled ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( π < ( 𝑋 mod 𝑇 ) ↔ ¬ ( 𝑋 mod 𝑇 ) ≤ π ) )
306 303 305 mpbird ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → π < ( 𝑋 mod 𝑇 ) )
307 modlt ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) → ( 𝑋 mod 𝑇 ) < 𝑇 )
308 3 65 307 mp2an ⊢ ( 𝑋 mod 𝑇 ) < 𝑇
309 308 a1i ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) < 𝑇 )
310 280 282 283 306 309 eliood ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) )
311 129 a1i ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → 0 ∈ ℝ* )
312 36 a1i ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → π ∈ ℝ )
313 142 a1i ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( 𝑋 mod 𝑇 ) ∈ ℝ* )
314 ioogtlb ⊢ ( ( π ∈ ℝ* ∧ 𝑇 ∈ ℝ* ∧ ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) ) → π < ( 𝑋 mod 𝑇 ) )
315 130 281 314 mp3an12 ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → π < ( 𝑋 mod 𝑇 ) )
316 311 312 313 315 gtnelioc ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) )
317 316 iffalsed ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) = - 1 )
318 141 a1i ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( 𝑋 mod 𝑇 ) ∈ ℝ )
319 312 318 315 ltnsymd ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ¬ ( 𝑋 mod 𝑇 ) < π )
320 319 iffalsed ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → if ( ( 𝑋 mod 𝑇 ) < π , 1 , - 1 ) = - 1 )
321 157 320 eqtrid ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( 𝐹 ‘ 𝑋 ) = - 1 )
322 317 321 oveq12d ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) = ( - 1 + - 1 ) )
323 322 oveq1d ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( ( - 1 + - 1 ) / 2 ) )
324 df-2 ⊢ 2 = ( 1 + 1 )
325 324 negeqi ⊢ - 2 = - ( 1 + 1 )
326 185 185 negdii ⊢ - ( 1 + 1 ) = ( - 1 + - 1 )
327 325 326 eqtr2i ⊢ ( - 1 + - 1 ) = - 2
328 327 oveq1i ⊢ ( ( - 1 + - 1 ) / 2 ) = ( - 2 / 2 )
329 divneg ⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 2 / 2 ) = ( - 2 / 2 ) )
330 170 170 46 329 mp3an ⊢ - ( 2 / 2 ) = ( - 2 / 2 )
331 238 negeqi ⊢ - ( 2 / 2 ) = - 1
332 328 330 331 3eqtr2i ⊢ ( ( - 1 + - 1 ) / 2 ) = - 1
333 332 a1i ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( ( - 1 + - 1 ) / 2 ) = - 1 )
334 4 a1i ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → 𝑌 = if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) ) )
335 312 318 ltnled ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ( π < ( 𝑋 mod 𝑇 ) ↔ ¬ ( 𝑋 mod 𝑇 ) ≤ π ) )
336 315 335 mpbid ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ¬ ( 𝑋 mod 𝑇 ) ≤ π )
337 248 114 eqbrtrdi ⊢ ( ( 𝑋 mod 𝑇 ) = 0 → ( 𝑋 mod 𝑇 ) ≤ π )
338 337 adantl ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ≤ π )
339 128 orcanai ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) = π )
340 339 146 syl ⊢ ( ( ( 𝑋 mod π ) = 0 ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → ( 𝑋 mod 𝑇 ) ≤ π )
341 338 340 pm2.61dan ⊢ ( ( 𝑋 mod π ) = 0 → ( 𝑋 mod 𝑇 ) ≤ π )
342 336 341 nsyl ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → ¬ ( 𝑋 mod π ) = 0 )
343 342 iffalsed ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → if ( ( 𝑋 mod π ) = 0 , 0 , ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
344 334 343 321 3eqtrrd ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → - 1 = 𝑌 )
345 323 333 344 3eqtrrd ⊢ ( ( 𝑋 mod 𝑇 ) ∈ ( π (,) 𝑇 ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
346 310 345 syl ⊢ ( ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) ∧ ¬ ( 𝑋 mod 𝑇 ) = 0 ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
347 279 346 pm2.61dan ⊢ ( ¬ ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) → 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
348 245 347 pm2.61i ⊢ 𝑌 = ( ( if ( ( 𝑋 mod 𝑇 ) ∈ ( 0 (,] π ) , 1 , - 1 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 )