Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem63 Structured version   Visualization version   GIF version

Theorem fourierdlem63 45616
Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem63.t 𝑇 = (𝐡 βˆ’ 𝐴)
fourierdlem63.p 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐴 ∧ (π‘β€˜π‘š) = 𝐡) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem63.m (πœ‘ β†’ 𝑀 ∈ β„•)
fourierdlem63.q (πœ‘ β†’ 𝑄 ∈ (π‘ƒβ€˜π‘€))
fourierdlem63.c (πœ‘ β†’ 𝐢 ∈ ℝ)
fourierdlem63.d (πœ‘ β†’ 𝐷 ∈ ℝ)
fourierdlem63.cltd (πœ‘ β†’ 𝐢 < 𝐷)
fourierdlem63.o 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐢 ∧ (π‘β€˜π‘š) = 𝐷) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem63.h 𝐻 = ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
fourierdlem63.n 𝑁 = ((β™―β€˜π») βˆ’ 1)
fourierdlem63.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem63.e 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)))
fourierdlem63.k (πœ‘ β†’ 𝐾 ∈ (0...𝑀))
fourierdlem63.j (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
fourierdlem63.y (πœ‘ β†’ π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))))
fourierdlem63.eyltqk (πœ‘ β†’ (πΈβ€˜π‘Œ) < (π‘„β€˜πΎ))
fourierdlem63.x 𝑋 = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
Assertion
Ref Expression
fourierdlem63 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜πΎ))
Distinct variable groups:   𝐴,𝑖,π‘š,𝑝   π‘₯,𝐴,𝑖   𝐡,𝑖,π‘š,𝑝   π‘₯,𝐡   𝐢,𝑖,π‘š,𝑝   π‘₯,𝐢   𝐷,𝑖,π‘š,𝑝   π‘₯,𝐷   π‘˜,𝐸,π‘₯   𝑓,𝐻   π‘₯,𝐻   π‘˜,𝐽,π‘₯   π‘˜,𝐾,π‘₯   𝑖,𝑀,π‘š,𝑝   𝑓,𝑁   𝑖,𝑁,π‘š,𝑝   π‘₯,𝑁   𝑄,𝑖,π‘˜,π‘₯   𝑄,𝑝   𝑆,𝑓   𝑆,𝑖,π‘˜,π‘₯   𝑆,𝑝   𝑇,𝑖,π‘˜,π‘₯   π‘˜,π‘Œ,π‘₯   πœ‘,𝑓   πœ‘,𝑖,π‘˜,π‘₯
Allowed substitution hints:   πœ‘(π‘š,𝑝)   𝐴(𝑓,π‘˜)   𝐡(𝑓,π‘˜)   𝐢(𝑓,π‘˜)   𝐷(𝑓,π‘˜)   𝑃(π‘₯,𝑓,𝑖,π‘˜,π‘š,𝑝)   𝑄(𝑓,π‘š)   𝑆(π‘š)   𝑇(𝑓,π‘š,𝑝)   𝐸(𝑓,𝑖,π‘š,𝑝)   𝐻(𝑖,π‘˜,π‘š,𝑝)   𝐽(𝑓,𝑖,π‘š,𝑝)   𝐾(𝑓,𝑖,π‘š,𝑝)   𝑀(π‘₯,𝑓,π‘˜)   𝑁(π‘˜)   𝑂(π‘₯,𝑓,𝑖,π‘˜,π‘š,𝑝)   𝑋(π‘₯,𝑓,𝑖,π‘˜,π‘š,𝑝)   π‘Œ(𝑓,𝑖,π‘š,𝑝)

Proof of Theorem fourierdlem63
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem63.e . . . . 5 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)))
21a1i 11 . . . 4 (πœ‘ β†’ 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇))))
3 id 22 . . . . . 6 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ π‘₯ = (π‘†β€˜(𝐽 + 1)))
4 oveq2 7421 . . . . . . . . 9 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))))
54oveq1d 7428 . . . . . . . 8 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
65fveq2d 6894 . . . . . . 7 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
76oveq1d 7428 . . . . . 6 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
83, 7oveq12d 7431 . . . . 5 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
98adantl 480 . . . 4 ((πœ‘ ∧ π‘₯ = (π‘†β€˜(𝐽 + 1))) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
10 fourierdlem63.t . . . . . . . . . . 11 𝑇 = (𝐡 βˆ’ 𝐴)
11 fourierdlem63.p . . . . . . . . . . 11 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐴 ∧ (π‘β€˜π‘š) = 𝐡) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
12 fourierdlem63.m . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ β„•)
13 fourierdlem63.q . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ (π‘ƒβ€˜π‘€))
14 fourierdlem63.c . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 ∈ ℝ)
15 fourierdlem63.d . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 ∈ ℝ)
16 fourierdlem63.cltd . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 < 𝐷)
17 fourierdlem63.o . . . . . . . . . . 11 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐢 ∧ (π‘β€˜π‘š) = 𝐷) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
18 fourierdlem63.h . . . . . . . . . . 11 𝐻 = ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
19 fourierdlem63.n . . . . . . . . . . 11 𝑁 = ((β™―β€˜π») βˆ’ 1)
20 fourierdlem63.s . . . . . . . . . . 11 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
2110, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20fourierdlem54 45607 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 493 . . . . . . . . 9 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)))
2322simprd 494 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ (π‘‚β€˜π‘))
2422simpld 493 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•)
2517fourierdlem2 45556 . . . . . . . . 9 (𝑁 ∈ β„• β†’ (𝑆 ∈ (π‘‚β€˜π‘) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((π‘†β€˜0) = 𝐢 ∧ (π‘†β€˜π‘) = 𝐷) ∧ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1))))))
2624, 25syl 17 . . . . . . . 8 (πœ‘ β†’ (𝑆 ∈ (π‘‚β€˜π‘) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((π‘†β€˜0) = 𝐢 ∧ (π‘†β€˜π‘) = 𝐷) ∧ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1))))))
2723, 26mpbid 231 . . . . . . 7 (πœ‘ β†’ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((π‘†β€˜0) = 𝐢 ∧ (π‘†β€˜π‘) = 𝐷) ∧ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1)))))
2827simpld 493 . . . . . 6 (πœ‘ β†’ 𝑆 ∈ (ℝ ↑m (0...𝑁)))
29 elmapi 8861 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) β†’ 𝑆:(0...𝑁)βŸΆβ„)
3028, 29syl 17 . . . . 5 (πœ‘ β†’ 𝑆:(0...𝑁)βŸΆβ„)
31 fourierdlem63.j . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
32 fzofzp1 13756 . . . . . 6 (𝐽 ∈ (0..^𝑁) β†’ (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (πœ‘ β†’ (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7088 . . . 4 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 45565 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡))
3635simp2d 1140 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ℝ)
3736, 34resubcld 11667 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
3835simp1d 1139 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
3936, 38resubcld 11667 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
4010, 39eqeltrid 2829 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ ℝ)
4135simp3d 1141 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
4238, 36posdifd 11826 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
4341, 42mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
4443, 10breqtrrdi 5186 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝑇)
4544gt0ne0d 11803 . . . . . . . . 9 (πœ‘ β†’ 𝑇 β‰  0)
4637, 40, 45redivcld 12067 . . . . . . . 8 (πœ‘ β†’ ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13790 . . . . . . 7 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ β„€)
4847zred 12691 . . . . . 6 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11269 . . . . 5 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) ∈ ℝ)
5034, 49readdcld 11268 . . . 4 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 7005 . . 3 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
5251, 50eqeltrd 2825 . 2 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 45556 . . . . . . 7 (𝑀 ∈ β„• β†’ (𝑄 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘„β€˜0) = 𝐴 ∧ (π‘„β€˜π‘€) = 𝐡) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1))))))
5412, 53syl 17 . . . . . 6 (πœ‘ β†’ (𝑄 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘„β€˜0) = 𝐴 ∧ (π‘„β€˜π‘€) = 𝐡) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1))))))
5513, 54mpbid 231 . . . . 5 (πœ‘ β†’ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘„β€˜0) = 𝐴 ∧ (π‘„β€˜π‘€) = 𝐡) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))))
5655simpld 493 . . . 4 (πœ‘ β†’ 𝑄 ∈ (ℝ ↑m (0...𝑀)))
57 elmapi 8861 . . . 4 (𝑄 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑄:(0...𝑀)βŸΆβ„)
5856, 57syl 17 . . 3 (πœ‘ β†’ 𝑄:(0...𝑀)βŸΆβ„)
59 fourierdlem63.k . . 3 (πœ‘ β†’ 𝐾 ∈ (0...𝑀))
6058, 59ffvelcdmd 7088 . 2 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ℝ)
6114adantr 479 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ∈ ℝ)
6215adantr 479 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐷 ∈ ℝ)
6338rexrd 11289 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ*)
64 iocssre 13431 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ) β†’ (𝐴(,]𝐡) βŠ† ℝ)
6563, 36, 64syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(,]𝐡) βŠ† ℝ)
6638, 36, 41, 10, 1fourierdlem4 45558 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸:β„βŸΆ(𝐴(,]𝐡))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))))
68 elfzofz 13675 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7088 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜π½) ∈ ℝ)
7134rexrd 11289 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*)
72 elico2 13415 . . . . . . . . . . . . . . 15 (((π‘†β€˜π½) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*) β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7370, 71, 72syl2anc 582 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7467, 73mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1))))
7574simp1d 1139 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ ℝ)
7666, 75ffvelcdmd 7088 . . . . . . . . . . 11 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ (𝐴(,]𝐡))
7765, 76sseldd 3974 . . . . . . . . . 10 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ ℝ)
7877, 75resubcld 11667 . . . . . . . . 9 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ ℝ)
7960, 78resubcld 11667 . . . . . . . 8 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
8079adantr 479 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
81 icossicc 13440 . . . . . . . . . . . . . 14 ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1)))
8214rexrd 11289 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 ∈ ℝ*)
8315rexrd 11289 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 45569 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆:(0...𝑁)⟢(𝐢[,]𝐷))
8582, 83, 84, 31fourierdlem8 45562 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8681, 85sstrid 3985 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8786, 67sseldd 3974 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ (𝐢[,]𝐷))
88 elicc2 13416 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
8914, 15, 88syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
9087, 89mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷))
9190simp2d 1140 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ≀ π‘Œ)
9260, 77resubcld 11667 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜π‘Œ) < (π‘„β€˜πΎ))
9477, 60posdifd 11826 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((πΈβ€˜π‘Œ) < (π‘„β€˜πΎ) ↔ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9593, 94mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)))
9692, 95elrpd 13040 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ+)
9775, 96ltaddrpd 13076 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ < (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9860recnd 11267 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ β„‚)
9977recnd 11267 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ β„‚)
10075recnd 11267 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ∈ β„‚)
10198, 99, 100subsub3d 11626 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)))
10298, 100addcomd 11441 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) + π‘Œ) = (π‘Œ + (π‘„β€˜πΎ)))
103102oveq1d 7428 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)) = ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)))
104100, 98, 99addsubassd 11616 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)) = (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
105101, 103, 1043eqtrrd 2770 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))) = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10697, 105breqtrd 5170 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10714, 75, 79, 91, 106lelttrd 11397 . . . . . . . . 9 (πœ‘ β†’ 𝐢 < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10814, 79, 107ltled 11387 . . . . . . . 8 (πœ‘ β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
109108adantr 479 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
11034adantr 479 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
11160adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ ℝ)
11252, 34resubcld 11667 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
113112adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11667 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1141 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ < (π‘†β€˜(𝐽 + 1)))
11675, 34, 115ltled 11387 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ≀ (π‘†β€˜(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 45561 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ≀ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
118112, 78, 60, 117lesub2dd 11856 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
119118adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
12098adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ β„‚)
12152recnd 11267 . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
122121adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
123110recnd 11267 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
124120, 122, 123subsubd 11624 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))))
12598, 121subcld 11596 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ β„‚)
12634recnd 11267 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
127125, 126addcomd 11441 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
128127adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
129124, 128eqtrd 2765 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
130 simpr 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
13152adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11865 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
133130, 132mpbird 256 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0)
134111, 131resubcld 11667 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11454 . . . . . . . . . . . . 13 ((((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
136134, 110, 135syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
137133, 136mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1)))
138129, 137eqbrtrd 5166 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) < (π‘†β€˜(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11397 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < (π‘†β€˜(𝐽 + 1)))
14084, 33ffvelcdmd 7088 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷))
141 elicc2 13416 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
14214, 15, 141syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
143140, 142mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷))
144143simp3d 1141 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
145144adantr 479 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
14680, 110, 62, 139, 145ltletrd 11399 . . . . . . . 8 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < 𝐷)
14780, 62, 146ltled 11387 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ 𝐷)
14861, 62, 80, 109, 147eliccd 44948 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ π‘₯ = π‘Œ)
150 oveq2 7421 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Œ β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ π‘Œ))
151150oveq1d 7428 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Œ β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ π‘Œ) / 𝑇))
152151fveq2d 6894 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Œ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
153152oveq1d 7428 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
154149, 153oveq12d 7431 . . . . . . . . . . . . . 14 (π‘₯ = π‘Œ β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
155154adantl 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ = π‘Œ) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
15636, 75resubcld 11667 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 βˆ’ π‘Œ) ∈ ℝ)
157156, 40, 45redivcld 12067 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝐡 βˆ’ π‘Œ) / 𝑇) ∈ ℝ)
158157flcld 13790 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„€)
159158zred 12691 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11269 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ ℝ)
16175, 160readdcld 11268 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 7005 . . . . . . . . . . . 12 (πœ‘ β†’ (πΈβ€˜π‘Œ) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
163162oveq1d 7428 . . . . . . . . . . 11 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) = ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ))
164163oveq1d 7428 . . . . . . . . . 10 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇))
165160recnd 11267 . . . . . . . . . . . 12 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ β„‚)
166100, 165pncan2d 11598 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
167166oveq1d 7428 . . . . . . . . . 10 (πœ‘ β†’ (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇) = (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇))
168159recnd 11267 . . . . . . . . . . 11 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„‚)
16940recnd 11267 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ β„‚)
170168, 169, 45divcan4d 12021 . . . . . . . . . 10 (πœ‘ β†’ (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
171164, 167, 1703eqtrd 2769 . . . . . . . . 9 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
172171, 158eqeltrd 2825 . . . . . . . 8 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€)
17378recnd 11267 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ β„‚)
174173, 169, 45divcan1d 12016 . . . . . . . . . . 11 (πœ‘ β†’ ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇) = ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
175174oveq2d 7429 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
17698, 173npcand 11600 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (π‘„β€˜πΎ))
177175, 176eqtrd 2765 . . . . . . . . 9 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (π‘„β€˜πΎ))
178 ffun 6720 . . . . . . . . . . 11 (𝑄:(0...𝑀)βŸΆβ„ β†’ Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (πœ‘ β†’ Fun 𝑄)
18058fdmd 6727 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2828 . . . . . . . . . 10 (πœ‘ β†’ 𝐾 ∈ dom 𝑄)
182 fvelrn 7079 . . . . . . . . . 10 ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
183179, 181, 182syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
184177, 183eqeltrd 2825 . . . . . . . 8 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄)
185 oveq1 7420 . . . . . . . . . . 11 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (π‘˜ Β· 𝑇) = ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇))
186185oveq2d 7429 . . . . . . . . . 10 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)))
187186eleq1d 2810 . . . . . . . . 9 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ ((((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄))
188187rspcev 3603 . . . . . . . 8 (((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€ ∧ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 582 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
190189adantr 479 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
191 oveq1 7420 . . . . . . . . 9 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (π‘₯ + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)))
192191eleq1d 2810 . . . . . . . 8 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ ((π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
193192rexbidv 3169 . . . . . . 7 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
194193elrab 3676 . . . . . 6 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷) ∧ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 581 . . . . 5 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
196 elun2 4172 . . . . 5 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
199197, 198, 183eltr4g 2842 . . 3 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 ∈ 𝐻)
200 elfzelz 13528 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ β„€)
201200ad2antlr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝑗 ∈ β„€)
202 elfzoelz 13659 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ β„€)
20331, 202syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐽 ∈ β„€)
204203ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 ∈ β„€)
205 simpr 483 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
20621simprd 494 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 ∈ (0...𝑁))
209 simplr 767 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑁))
210 isorel 7327 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
211207, 208, 209, 210syl12anc 835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
212205, 211mpbird 256 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 < 𝑗)
213212adantrr 715 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 < 𝑗)
214 simpr 483 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
215206ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
216 simplr 767 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ 𝑗 ∈ (0...𝑁))
21733ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ (𝐽 + 1) ∈ (0...𝑁))
218 isorel 7327 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) β†’ (𝑗 < (𝐽 + 1) ↔ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
219215, 216, 217, 218syl12anc 835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ (𝑗 < (𝐽 + 1) ↔ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
220214, 219mpbird 256 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ 𝑗 < (𝐽 + 1))
221220adantrl 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝑗 < (𝐽 + 1))
222 btwnnz 12663 . . . . . . . . 9 ((𝐽 ∈ β„€ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) β†’ Β¬ 𝑗 ∈ β„€)
223204, 213, 221, 222syl3anc 1368 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ Β¬ 𝑗 ∈ β„€)
224201, 223pm2.65da 815 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
225224adantlr 713 . . . . . 6 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
22670ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) ∈ ℝ)
22775ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ ∈ ℝ)
22830ffvelcdmda 7087 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π‘†β€˜π‘—) ∈ ℝ)
229228adantr 479 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) ∈ ℝ)
23074simp2d 1140 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜π½) ≀ π‘Œ)
231230ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) ≀ π‘Œ)
232106, 198breqtrrdi 5186 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ < 𝑋)
233232adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < 𝑋)
234 eqcom 2732 . . . . . . . . . . . . 13 (𝑋 = (π‘†β€˜π‘—) ↔ (π‘†β€˜π‘—) = 𝑋)
235234biimpri 227 . . . . . . . . . . . 12 ((π‘†β€˜π‘—) = 𝑋 β†’ 𝑋 = (π‘†β€˜π‘—))
236235adantl 480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 = (π‘†β€˜π‘—))
237233, 236breqtrd 5170 . . . . . . . . . 10 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
238237adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
239226, 227, 229, 231, 238lelttrd 11397 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
240239adantllr 717 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
241 simpr 483 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) = 𝑋)
242198, 139eqbrtrid 5179 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
243242adantr 479 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
244241, 243eqbrtrd 5166 . . . . . . . 8 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
245244adantlr 713 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
246240, 245jca 510 . . . . . 6 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
247225, 246mtand 814 . . . . 5 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ (π‘†β€˜π‘—) = 𝑋)
248247nrexdv 3139 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ Β¬ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
249 isof1o 7324 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) β†’ 𝑆:(0...𝑁)–1-1-onto→𝐻)
250206, 249syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑆:(0...𝑁)–1-1-onto→𝐻)
251 f1ofo 6839 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto→𝐻 β†’ 𝑆:(0...𝑁)–onto→𝐻)
252250, 251syl 17 . . . . . . 7 (πœ‘ β†’ 𝑆:(0...𝑁)–onto→𝐻)
253 foelrn 7110 . . . . . . 7 ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
254252, 253sylan 578 . . . . . 6 ((πœ‘ ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
255234rexbii 3084 . . . . . 6 (βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—) ↔ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
256254, 255sylib 217 . . . . 5 ((πœ‘ ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
257256adantlr 713 . . . 4 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
258248, 257mtand 814 . . 3 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ Β¬ 𝑋 ∈ 𝐻)
259199, 258pm2.65da 815 . 2 (πœ‘ β†’ Β¬ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
26052, 60, 259nltled 11389 1 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜πΎ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  βˆƒwrex 3060  {crab 3419   βˆͺ cun 3939   βŠ† wss 3941  {cpr 4627   class class class wbr 5144   ↦ cmpt 5227  dom cdm 5673  ran crn 5674  β„©cio 6493  Fun wfun 6537  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7413   ↑m cmap 8838  β„‚cc 11131  β„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   Β· cmul 11138  β„*cxr 11272   < clt 11273   ≀ cle 11274   βˆ’ cmin 11469   / cdiv 11896  β„•cn 12237  β„€cz 12583  (,]cioc 13352  [,)cico 13353  [,]cicc 13354  ...cfz 13511  ..^cfzo 13654  βŒŠcfl 13782  β™―chash 14316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-er 8718  df-map 8840  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fi 9429  df-sup 9460  df-inf 9461  df-oi 9528  df-dju 9919  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-n0 12498  df-xnn0 12570  df-z 12584  df-uz 12848  df-q 12958  df-rp 13002  df-xneg 13119  df-xadd 13120  df-xmul 13121  df-ioo 13355  df-ioc 13356  df-ico 13357  df-icc 13358  df-fz 13512  df-fzo 13655  df-fl 13784  df-seq 13994  df-exp 14054  df-hash 14317  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-rest 17398  df-topgen 17419  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-top 22809  df-topon 22826  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-cmp 23304
This theorem is referenced by:  fourierdlem79  45632
  Copyright terms: Public domain W3C validator