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 mulid2i ( 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 syl5eq ( ( 𝑋 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 syl5eq ( ( 𝑋 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 syl5eq ( ( 𝑋 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 syl5eq ( ( 𝑋 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 )