This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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