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

Metamath Proof Explorer

Theorem fourierdlem51

Description: X is in the periodic partition, when the considered interval is centered at X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem51.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem51.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem51.alt0 ⊢ ( 𝜑 → 𝐴 < 0 )
fourierdlem51.bgt0 ⊢ ( 𝜑 → 0 < 𝐵 )
fourierdlem51.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem51.cfi ⊢ ( 𝜑 → 𝐶 ∈ Fin )
fourierdlem51.css ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐴 [,] 𝐵 ) )
fourierdlem51.bc ⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
fourierdlem51.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem51.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem51.exc ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ 𝐶 )
fourierdlem51.d ⊢ 𝐷 = ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
fourierdlem51.f ⊢ 𝐹 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) )
fourierdlem51.h ⊢ 𝐻 = { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
Assertion fourierdlem51 ( 𝜑 → 𝑋 ∈ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 fourierdlem51.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem51.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem51.alt0 ⊢ ( 𝜑 → 𝐴 < 0 )
4 fourierdlem51.bgt0 ⊢ ( 𝜑 → 0 < 𝐵 )
5 fourierdlem51.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
6 fourierdlem51.cfi ⊢ ( 𝜑 → 𝐶 ∈ Fin )
7 fourierdlem51.css ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐴 [,] 𝐵 ) )
8 fourierdlem51.bc ⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
9 fourierdlem51.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
10 fourierdlem51.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
11 fourierdlem51.exc ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ 𝐶 )
12 fourierdlem51.d ⊢ 𝐷 = ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
13 fourierdlem51.f ⊢ 𝐹 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) )
14 fourierdlem51.h ⊢ 𝐻 = { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
15 1 10 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ )
16 2 10 readdcld ⊢ ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ )
17 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
18 1 17 10 3 ltadd1dd ⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) < ( 0 + 𝑋 ) )
19 10 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
20 19 addlidd ⊢ ( 𝜑 → ( 0 + 𝑋 ) = 𝑋 )
21 18 20 breqtrd ⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) < 𝑋 )
22 15 10 21 ltled ⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ≤ 𝑋 )
23 17 2 10 4 ltadd1dd ⊢ ( 𝜑 → ( 0 + 𝑋 ) < ( 𝐵 + 𝑋 ) )
24 20 23 eqbrtrrd ⊢ ( 𝜑 → 𝑋 < ( 𝐵 + 𝑋 ) )
25 10 16 24 ltled ⊢ ( 𝜑 → 𝑋 ≤ ( 𝐵 + 𝑋 ) )
26 15 16 10 22 25 eliccd ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
27 2 10 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
28 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
29 5 28 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
30 1 17 2 3 4 lttrd ⊢ ( 𝜑 → 𝐴 < 𝐵 )
31 1 2 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
32 30 31 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
33 5 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
34 33 a1i ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = 𝑇 )
35 32 34 breqtrd ⊢ ( 𝜑 → 0 < 𝑇 )
36 35 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
37 27 29 36 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℝ )
38 37 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℤ )
39 9 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
40 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
41 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑋 ) )
42 41 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
43 42 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
44 43 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
45 40 44 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
47 38 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℝ )
48 47 29 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
49 10 48 readdcld ⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
50 39 46 10 49 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
51 50 11 eqeltrrd ⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐶 )
52 oveq1 ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
53 52 oveq2d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( 𝑋 + ( 𝑘 · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
54 53 eleq1d ⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐶 ) )
55 54 rspcev ⊢ ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℤ ∧ ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐶 ) → ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
56 38 51 55 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
57 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
58 57 eleq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
59 58 rexbidv ⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
60 59 elrab ⊢ ( 𝑋 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↔ ( 𝑋 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
61 26 56 60 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
62 elun2 ⊢ ( 𝑋 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑋 ∈ ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
63 61 62 syl ⊢ ( 𝜑 → 𝑋 ∈ ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
64 63 12 eleqtrrdi ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
65 prfi ⊢ { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∈ Fin
66 snfi ⊢ { ( 𝐴 + 𝑋 ) } ∈ Fin
67 fvres ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
69 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
70 69 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
71 70 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
72 71 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↔ ( 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
73 72 simprbi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
75 nfv ⊢ Ⅎ 𝑘 𝜑
76 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶
77 nfcv ⊢ Ⅎ 𝑘 ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) )
78 76 77 nfrabw ⊢ Ⅎ 𝑘 { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
79 78 nfcri ⊢ Ⅎ 𝑘 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
80 75 79 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
81 nfv ⊢ Ⅎ 𝑘 ( 𝐸 ‘ 𝑥 ) ∈ 𝐶
82 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝜑 )
83 15 rexrd ⊢ ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ* )
84 iocssre ⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
85 83 16 84 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
87 elrabi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
88 87 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
89 86 88 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ℝ )
90 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
91 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
92 91 90 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐵 − 𝑥 ) ∈ ℝ )
93 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
94 36 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ≠ 0 )
95 92 93 94 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) ∈ ℝ )
96 95 flcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
97 96 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
98 97 93 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
99 90 98 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
100 9 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
101 90 99 100 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
102 101 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
103 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) )
104 96 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
105 simpr ⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 )
106 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
107 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
108 1 2 30 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
109 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
110 106 107 108 109 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
112 105 111 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
113 112 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
114 103 104 113 jca31 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
115 iocssicc ⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
116 1 2 30 5 9 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
117 116 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
118 115 117 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) )
119 101 118 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
120 119 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
121 106 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ* )
122 91 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ* )
123 iocgtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
124 121 122 117 123 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
125 124 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
126 id ⊢ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 )
127 126 eqcomd ⊢ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → 𝐴 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
128 127 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
129 125 128 102 3brtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
130 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
131 130 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
132 29 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℝ )
133 131 132 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
134 133 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
135 134 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
136 98 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
137 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑥 ∈ ℝ )
138 135 136 137 ltadd2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑘 · 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
139 129 138 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑘 · 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
140 130 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑘 ∈ ℝ )
141 97 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
142 29 35 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
143 142 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑇 ∈ ℝ+ )
144 140 141 143 ltmul1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ↔ ( 𝑘 · 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
145 139 144 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) )
146 fvex ⊢ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ V
147 eleq1 ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑗 ∈ ℤ ↔ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) )
148 147 anbi2d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ) )
149 148 anbi1d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
150 oveq1 ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑗 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
151 150 oveq2d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
152 151 eleq1d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
153 149 152 anbi12d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
154 breq2 ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑘 < 𝑗 ↔ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) )
155 153 154 anbi12d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) ) )
156 eqeq1 ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑗 = ( 𝑘 + 1 ) ↔ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) ) )
157 155 156 imbi12d ⊢ ( 𝑗 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) → 𝑗 = ( 𝑘 + 1 ) ) ↔ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) ) ) )
158 eleq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ℤ ↔ 𝑘 ∈ ℤ ) )
159 158 anbi2d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ) )
160 159 anbi1d ⊢ ( 𝑖 = 𝑘 → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ) )
161 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 · 𝑇 ) = ( 𝑘 · 𝑇 ) )
162 161 oveq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑥 + ( 𝑖 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
163 162 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
164 160 163 anbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
165 164 anbi1d ⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
166 breq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 < 𝑗 ↔ 𝑘 < 𝑗 ) )
167 165 166 anbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) ) )
168 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 + 1 ) = ( 𝑘 + 1 ) )
169 168 eqeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑗 = ( 𝑖 + 1 ) ↔ 𝑗 = ( 𝑘 + 1 ) ) )
170 167 169 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 = ( 𝑖 + 1 ) ) ↔ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) → 𝑗 = ( 𝑘 + 1 ) ) ) )
171 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝜑 )
172 171 1 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝐴 ∈ ℝ )
173 171 2 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝐵 ∈ ℝ )
174 171 30 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝐴 < 𝐵 )
175 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑥 ∈ ℝ )
176 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ ℤ )
177 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ℤ )
178 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 )
179 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
180 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
181 172 173 174 5 175 176 177 178 179 180 fourierdlem6 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑖 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 = ( 𝑖 + 1 ) )
182 170 181 chvarvv ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < 𝑗 ) → 𝑗 = ( 𝑘 + 1 ) )
183 146 157 182 vtocl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑘 < ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) )
184 114 120 145 183 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( 𝑘 + 1 ) )
185 184 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( 𝑘 + 1 ) · 𝑇 ) )
186 185 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) )
187 131 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
188 29 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
189 188 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℂ )
190 187 189 adddirp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 + 1 ) · 𝑇 ) = ( ( 𝑘 · 𝑇 ) + 𝑇 ) )
191 190 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
192 191 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
193 192 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
194 90 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
195 194 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → 𝑥 ∈ ℂ )
196 134 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℂ )
197 188 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℂ )
198 195 196 197 addassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) )
199 198 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) = ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) )
200 199 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( 𝑘 · 𝑇 ) + 𝑇 ) ) = ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) )
201 oveq1 ⊢ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = ( 𝐴 + 𝑇 ) )
202 201 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = ( 𝐴 + 𝑇 ) )
203 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
204 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
205 203 204 188 subaddd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) = 𝑇 ↔ ( 𝐴 + 𝑇 ) = 𝐵 ) )
206 34 205 mpbid ⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) = 𝐵 )
207 206 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐴 + 𝑇 ) = 𝐵 )
208 202 207 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) + 𝑇 ) = 𝐵 )
209 193 200 208 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( ( 𝑘 + 1 ) · 𝑇 ) ) = 𝐵 )
210 102 186 209 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) = 𝐵 )
211 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐵 ∈ 𝐶 )
212 210 211 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
213 212 3adantl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
214 simpl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝜑 ∧ 𝑥 ∈ ℝ ) )
215 simpl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝑘 ∈ ℤ )
216 7 sselda ⊢ ( ( 𝜑 ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
217 216 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
218 217 3adant2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
219 218 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
220 neqne ⊢ ( ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ≠ 𝐴 )
221 220 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ≠ 𝐴 )
222 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
223 214 222 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐴 ∈ ℝ )
224 214 91 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → 𝐵 ∈ ℝ )
225 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → 𝑥 ∈ ℝ )
226 225 134 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
227 226 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
228 214 215 227 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
229 223 224 228 eliccelioc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ≠ 𝐴 ) ) )
230 219 221 229 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
231 101 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
232 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 ∈ ℝ )
233 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐵 ∈ ℝ )
234 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < 𝐵 )
235 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝑥 ∈ ℝ )
236 96 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
237 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝑘 ∈ ℤ )
238 101 117 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
239 238 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
240 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
241 232 233 234 5 235 236 237 239 240 fourierdlem35 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = 𝑘 )
242 241 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( 𝑘 · 𝑇 ) )
243 242 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
244 231 243 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
245 214 215 230 244 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
246 simpl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
247 245 246 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ ( 𝑥 + ( 𝑘 · 𝑇 ) ) = 𝐴 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
248 213 247 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℤ ∧ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
249 248 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑘 ∈ ℤ → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 ) ) )
250 82 89 249 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( 𝑘 ∈ ℤ → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 ) ) )
251 80 81 250 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 ) )
252 74 251 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝐶 )
253 68 252 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ∈ 𝐶 )
254 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) )
255 253 254 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 )
256 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
257 106 2 256 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
258 116 257 fssd ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ℝ )
259 ssrab2 ⊢ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) )
260 259 85 sstrid ⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ℝ )
261 258 260 fssresd ⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ ℝ )
262 261 feqmptd ⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) = ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) )
263 262 feq1d ⊢ ( 𝜑 → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 ↔ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↦ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑥 ) ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 ) )
264 255 263 mpbird ⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 )
265 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝜑 )
266 id ⊢ ( 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
267 266 14 eleqtrrdi ⊢ ( 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑤 ∈ 𝐻 )
268 267 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝑤 ∈ 𝐻 )
269 265 268 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) )
270 id ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
271 270 14 eleqtrrdi ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑧 ∈ 𝐻 )
272 271 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝑧 ∈ 𝐻 )
273 fvres ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) = ( 𝐸 ‘ 𝑧 ) )
274 273 eqcomd ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( 𝐸 ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) )
275 274 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( 𝐸 ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) )
276 id ⊢ ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) )
277 276 eqcomd ⊢ ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) )
278 277 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) )
279 fvres ⊢ ( 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( 𝐸 ‘ 𝑤 ) )
280 279 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( 𝐸 ‘ 𝑤 ) )
281 275 278 280 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) )
282 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝐴 ∈ ℝ )
283 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝐵 ∈ ℝ )
284 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝐴 < 𝐵 )
285 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑋 ∈ ℝ )
286 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑤 ∈ 𝐻 )
287 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑧 ∈ 𝐻 )
288 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) )
289 282 283 284 285 14 5 9 286 287 288 fourierdlem19 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ¬ 𝑤 < 𝑧 )
290 288 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑧 ) )
291 282 283 284 285 14 5 9 287 286 290 fourierdlem19 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ¬ 𝑧 < 𝑤 )
292 14 260 eqsstrid ⊢ ( 𝜑 → 𝐻 ⊆ ℝ )
293 292 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) → 𝑤 ∈ ℝ )
294 293 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑤 ∈ ℝ )
295 292 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) → 𝐻 ⊆ ℝ )
296 295 sselda ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) → 𝑧 ∈ ℝ )
297 296 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑧 ∈ ℝ )
298 294 297 lttri3d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → ( 𝑤 = 𝑧 ↔ ( ¬ 𝑤 < 𝑧 ∧ ¬ 𝑧 < 𝑤 ) ) )
299 289 291 298 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝐻 ) ∧ ( 𝐸 ‘ 𝑧 ) = ( 𝐸 ‘ 𝑤 ) ) → 𝑤 = 𝑧 )
300 269 272 281 299 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) ) → 𝑤 = 𝑧 )
301 300 ex ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∧ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
302 301 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ∀ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
303 302 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∀ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
304 dff13 ⊢ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } –1-1→ 𝐶 ↔ ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⟶ 𝐶 ∧ ∀ 𝑤 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∀ 𝑧 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ( ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑤 ) = ( ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ‘ 𝑧 ) → 𝑤 = 𝑧 ) ) )
305 264 303 304 sylanbrc ⊢ ( 𝜑 → ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } –1-1→ 𝐶 )
306 f1fi ⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝐸 ↾ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) : { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } –1-1→ 𝐶 ) → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
307 6 305 306 syl2anc ⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
308 unfi ⊢ ( ( { ( 𝐴 + 𝑋 ) } ∈ Fin ∧ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin ) → ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
309 66 307 308 sylancr ⊢ ( 𝜑 → ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
310 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝜑 )
311 elrabi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
312 311 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
313 71 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ↔ ( 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) )
314 313 simprbi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
315 314 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
316 velsn ⊢ ( 𝑥 ∈ { ( 𝐴 + 𝑋 ) } ↔ 𝑥 = ( 𝐴 + 𝑋 ) )
317 elun1 ⊢ ( 𝑥 ∈ { ( 𝐴 + 𝑋 ) } → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
318 316 317 sylbir ⊢ ( 𝑥 = ( 𝐴 + 𝑋 ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
319 318 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
320 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ* )
321 16 rexrd ⊢ ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ* )
322 321 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐵 + 𝑋 ) ∈ ℝ* )
323 15 16 iccssred ⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
324 323 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ∈ ℝ )
325 324 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ∈ ℝ* )
326 325 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ℝ* )
327 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ )
328 324 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ℝ )
329 83 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) ∈ ℝ* )
330 321 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐵 + 𝑋 ) ∈ ℝ* )
331 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) )
332 iccgelb ⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) ≤ 𝑥 )
333 329 330 331 332 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) ≤ 𝑥 )
334 333 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) ≤ 𝑥 )
335 neqne ⊢ ( ¬ 𝑥 = ( 𝐴 + 𝑋 ) → 𝑥 ≠ ( 𝐴 + 𝑋 ) )
336 335 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ≠ ( 𝐴 + 𝑋 ) )
337 327 328 334 336 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ( 𝐴 + 𝑋 ) < 𝑥 )
338 iccleub ⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑋 ) )
339 329 330 331 338 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑋 ) )
340 339 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ≤ ( 𝐵 + 𝑋 ) )
341 320 322 326 337 340 eliocd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
342 341 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
343 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 )
344 342 343 72 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } )
345 elun2 ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
346 344 345 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) ∧ ¬ 𝑥 = ( 𝐴 + 𝑋 ) ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
347 319 346 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
348 310 312 315 347 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) → 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
349 348 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
350 dfss3 ⊢ ( { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ↔ ∀ 𝑥 ∈ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } 𝑥 ∈ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
351 349 350 sylibr ⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) )
352 ssfi ⊢ ( ( ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin ∧ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( { ( 𝐴 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ) → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
353 309 351 352 syl2anc ⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin )
354 unfi ⊢ ( ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∈ Fin ∧ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ∈ Fin ) → ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
355 65 353 354 sylancr ⊢ ( 𝜑 → ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ∈ Fin )
356 12 355 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ Fin )
357 prssi ⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ ∧ ( 𝐵 + 𝑋 ) ∈ ℝ ) → { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ⊆ ℝ )
358 15 16 357 syl2anc ⊢ ( 𝜑 → { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ⊆ ℝ )
359 ssrab2 ⊢ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) )
360 359 323 sstrid ⊢ ( 𝜑 → { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ℝ )
361 358 360 unssd ⊢ ( 𝜑 → ( { ( 𝐴 + 𝑋 ) , ( 𝐵 + 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) [,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ) ⊆ ℝ )
362 12 361 eqsstrid ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
363 eqid ⊢ ( ( ♯ ‘ 𝐷 ) − 1 ) = ( ( ♯ ‘ 𝐷 ) − 1 )
364 356 362 13 363 fourierdlem36 ⊢ ( 𝜑 → 𝐹 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) )
365 isof1o ⊢ ( 𝐹 Isom < , < ( ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) , 𝐷 ) → 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –1-1-onto→ 𝐷 )
366 f1ofo ⊢ ( 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –1-1-onto→ 𝐷 → 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –onto→ 𝐷 )
367 forn ⊢ ( 𝐹 : ( 0 ... ( ( ♯ ‘ 𝐷 ) − 1 ) ) –onto→ 𝐷 → ran 𝐹 = 𝐷 )
368 364 365 366 367 4syl ⊢ ( 𝜑 → ran 𝐹 = 𝐷 )
369 64 368 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐹 )