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 44885
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 7417 . . . . . . . . 9 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))))
54oveq1d 7424 . . . . . . . 8 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
65fveq2d 6896 . . . . . . 7 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
76oveq1d 7424 . . . . . 6 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
83, 7oveq12d 7427 . . . . 5 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
98adantl 483 . . . 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 44876 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 496 . . . . . . . . 9 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)))
2322simprd 497 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ (π‘‚β€˜π‘))
2422simpld 496 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•)
2517fourierdlem2 44825 . . . . . . . . 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 496 . . . . . 6 (πœ‘ β†’ 𝑆 ∈ (ℝ ↑m (0...𝑁)))
29 elmapi 8843 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) β†’ 𝑆:(0...𝑁)βŸΆβ„)
3028, 29syl 17 . . . . 5 (πœ‘ β†’ 𝑆:(0...𝑁)βŸΆβ„)
31 fourierdlem63.j . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
32 fzofzp1 13729 . . . . . 6 (𝐽 ∈ (0..^𝑁) β†’ (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (πœ‘ β†’ (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7088 . . . 4 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 44834 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡))
3635simp2d 1144 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ℝ)
3736, 34resubcld 11642 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
3835simp1d 1143 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
3936, 38resubcld 11642 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
4010, 39eqeltrid 2838 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ ℝ)
4135simp3d 1145 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
4238, 36posdifd 11801 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
4341, 42mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
4443, 10breqtrrdi 5191 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝑇)
4544gt0ne0d 11778 . . . . . . . . 9 (πœ‘ β†’ 𝑇 β‰  0)
4637, 40, 45redivcld 12042 . . . . . . . 8 (πœ‘ β†’ ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13763 . . . . . . 7 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ β„€)
4847zred 12666 . . . . . 6 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11244 . . . . 5 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) ∈ ℝ)
5034, 49readdcld 11243 . . . 4 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 7006 . . 3 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
5251, 50eqeltrd 2834 . 2 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 44825 . . . . . . 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 496 . . . 4 (πœ‘ β†’ 𝑄 ∈ (ℝ ↑m (0...𝑀)))
57 elmapi 8843 . . . 4 (𝑄 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑄:(0...𝑀)βŸΆβ„)
5856, 57syl 17 . . 3 (πœ‘ β†’ 𝑄:(0...𝑀)βŸΆβ„)
59 fourierdlem63.k . . 3 (πœ‘ β†’ 𝐾 ∈ (0...𝑀))
6058, 59ffvelcdmd 7088 . 2 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ℝ)
6114adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ∈ ℝ)
6215adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐷 ∈ ℝ)
6338rexrd 11264 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ*)
64 iocssre 13404 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ) β†’ (𝐴(,]𝐡) βŠ† ℝ)
6563, 36, 64syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(,]𝐡) βŠ† ℝ)
6638, 36, 41, 10, 1fourierdlem4 44827 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸:β„βŸΆ(𝐴(,]𝐡))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))))
68 elfzofz 13648 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7088 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜π½) ∈ ℝ)
7134rexrd 11264 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*)
72 elico2 13388 . . . . . . . . . . . . . . 15 (((π‘†β€˜π½) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*) β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7370, 71, 72syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7467, 73mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1))))
7574simp1d 1143 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ ℝ)
7666, 75ffvelcdmd 7088 . . . . . . . . . . 11 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ (𝐴(,]𝐡))
7765, 76sseldd 3984 . . . . . . . . . 10 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ ℝ)
7877, 75resubcld 11642 . . . . . . . . 9 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ ℝ)
7960, 78resubcld 11642 . . . . . . . 8 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
8079adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
81 icossicc 13413 . . . . . . . . . . . . . 14 ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1)))
8214rexrd 11264 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 ∈ ℝ*)
8315rexrd 11264 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 44838 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆:(0...𝑁)⟢(𝐢[,]𝐷))
8582, 83, 84, 31fourierdlem8 44831 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8681, 85sstrid 3994 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8786, 67sseldd 3984 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ (𝐢[,]𝐷))
88 elicc2 13389 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
8914, 15, 88syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
9087, 89mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷))
9190simp2d 1144 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ≀ π‘Œ)
9260, 77resubcld 11642 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜π‘Œ) < (π‘„β€˜πΎ))
9477, 60posdifd 11801 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((πΈβ€˜π‘Œ) < (π‘„β€˜πΎ) ↔ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9593, 94mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)))
9692, 95elrpd 13013 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ+)
9775, 96ltaddrpd 13049 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ < (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9860recnd 11242 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ β„‚)
9977recnd 11242 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ β„‚)
10075recnd 11242 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ∈ β„‚)
10198, 99, 100subsub3d 11601 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)))
10298, 100addcomd 11416 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) + π‘Œ) = (π‘Œ + (π‘„β€˜πΎ)))
103102oveq1d 7424 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)) = ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)))
104100, 98, 99addsubassd 11591 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)) = (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
105101, 103, 1043eqtrrd 2778 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))) = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10697, 105breqtrd 5175 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10714, 75, 79, 91, 106lelttrd 11372 . . . . . . . . 9 (πœ‘ β†’ 𝐢 < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10814, 79, 107ltled 11362 . . . . . . . 8 (πœ‘ β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
109108adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
11034adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
11160adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ ℝ)
11252, 34resubcld 11642 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
113112adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11642 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1145 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ < (π‘†β€˜(𝐽 + 1)))
11675, 34, 115ltled 11362 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ≀ (π‘†β€˜(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 44830 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ≀ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
118112, 78, 60, 117lesub2dd 11831 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
119118adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
12098adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ β„‚)
12152recnd 11242 . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
122121adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
123110recnd 11242 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
124120, 122, 123subsubd 11599 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))))
12598, 121subcld 11571 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ β„‚)
12634recnd 11242 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
127125, 126addcomd 11416 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
128127adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
129124, 128eqtrd 2773 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
130 simpr 486 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
13152adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11840 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
133130, 132mpbird 257 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0)
134111, 131resubcld 11642 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11429 . . . . . . . . . . . . 13 ((((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
136134, 110, 135syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
137133, 136mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1)))
138129, 137eqbrtrd 5171 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) < (π‘†β€˜(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11372 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < (π‘†β€˜(𝐽 + 1)))
14084, 33ffvelcdmd 7088 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷))
141 elicc2 13389 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
14214, 15, 141syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
143140, 142mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷))
144143simp3d 1145 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
145144adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
14680, 110, 62, 139, 145ltletrd 11374 . . . . . . . 8 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < 𝐷)
14780, 62, 146ltled 11362 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ 𝐷)
14861, 62, 80, 109, 147eliccd 44217 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ π‘₯ = π‘Œ)
150 oveq2 7417 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Œ β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ π‘Œ))
151150oveq1d 7424 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Œ β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ π‘Œ) / 𝑇))
152151fveq2d 6896 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Œ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
153152oveq1d 7424 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
154149, 153oveq12d 7427 . . . . . . . . . . . . . 14 (π‘₯ = π‘Œ β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
155154adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ = π‘Œ) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
15636, 75resubcld 11642 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 βˆ’ π‘Œ) ∈ ℝ)
157156, 40, 45redivcld 12042 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝐡 βˆ’ π‘Œ) / 𝑇) ∈ ℝ)
158157flcld 13763 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„€)
159158zred 12666 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11244 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ ℝ)
16175, 160readdcld 11243 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 7006 . . . . . . . . . . . 12 (πœ‘ β†’ (πΈβ€˜π‘Œ) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
163162oveq1d 7424 . . . . . . . . . . 11 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) = ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ))
164163oveq1d 7424 . . . . . . . . . 10 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇))
165160recnd 11242 . . . . . . . . . . . 12 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ β„‚)
166100, 165pncan2d 11573 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
167166oveq1d 7424 . . . . . . . . . 10 (πœ‘ β†’ (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇) = (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇))
168159recnd 11242 . . . . . . . . . . 11 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„‚)
16940recnd 11242 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ β„‚)
170168, 169, 45divcan4d 11996 . . . . . . . . . 10 (πœ‘ β†’ (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
171164, 167, 1703eqtrd 2777 . . . . . . . . 9 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
172171, 158eqeltrd 2834 . . . . . . . 8 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€)
17378recnd 11242 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ β„‚)
174173, 169, 45divcan1d 11991 . . . . . . . . . . 11 (πœ‘ β†’ ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇) = ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
175174oveq2d 7425 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
17698, 173npcand 11575 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (π‘„β€˜πΎ))
177175, 176eqtrd 2773 . . . . . . . . 9 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (π‘„β€˜πΎ))
178 ffun 6721 . . . . . . . . . . 11 (𝑄:(0...𝑀)βŸΆβ„ β†’ Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (πœ‘ β†’ Fun 𝑄)
18058fdmd 6729 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2837 . . . . . . . . . 10 (πœ‘ β†’ 𝐾 ∈ dom 𝑄)
182 fvelrn 7079 . . . . . . . . . 10 ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
183179, 181, 182syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
184177, 183eqeltrd 2834 . . . . . . . 8 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄)
185 oveq1 7416 . . . . . . . . . . 11 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (π‘˜ Β· 𝑇) = ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇))
186185oveq2d 7425 . . . . . . . . . 10 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)))
187186eleq1d 2819 . . . . . . . . 9 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ ((((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄))
188187rspcev 3613 . . . . . . . 8 (((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€ ∧ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 585 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
190189adantr 482 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
191 oveq1 7416 . . . . . . . . 9 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (π‘₯ + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)))
192191eleq1d 2819 . . . . . . . 8 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ ((π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
193192rexbidv 3179 . . . . . . 7 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
194193elrab 3684 . . . . . 6 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷) ∧ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 584 . . . . 5 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
196 elun2 4178 . . . . 5 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
199197, 198, 183eltr4g 2851 . . 3 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 ∈ 𝐻)
200 elfzelz 13501 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ β„€)
201200ad2antlr 726 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝑗 ∈ β„€)
202 elfzoelz 13632 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ β„€)
20331, 202syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐽 ∈ β„€)
204203ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 ∈ β„€)
205 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
20621simprd 497 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 ∈ (0...𝑁))
209 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑁))
210 isorel 7323 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
211207, 208, 209, 210syl12anc 836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
212205, 211mpbird 257 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 < 𝑗)
213212adantrr 716 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 < 𝑗)
214 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
215206ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
216 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ 𝑗 ∈ (0...𝑁))
21733ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ (𝐽 + 1) ∈ (0...𝑁))
218 isorel 7323 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) β†’ (𝑗 < (𝐽 + 1) ↔ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
219215, 216, 217, 218syl12anc 836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ (𝑗 < (𝐽 + 1) ↔ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
220214, 219mpbird 257 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))) β†’ 𝑗 < (𝐽 + 1))
221220adantrl 715 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝑗 < (𝐽 + 1))
222 btwnnz 12638 . . . . . . . . 9 ((𝐽 ∈ β„€ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) β†’ Β¬ 𝑗 ∈ β„€)
223204, 213, 221, 222syl3anc 1372 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ Β¬ 𝑗 ∈ β„€)
224201, 223pm2.65da 816 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
225224adantlr 714 . . . . . 6 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
22670ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) ∈ ℝ)
22775ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ ∈ ℝ)
22830ffvelcdmda 7087 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π‘†β€˜π‘—) ∈ ℝ)
229228adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) ∈ ℝ)
23074simp2d 1144 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜π½) ≀ π‘Œ)
231230ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) ≀ π‘Œ)
232106, 198breqtrrdi 5191 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ < 𝑋)
233232adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < 𝑋)
234 eqcom 2740 . . . . . . . . . . . . 13 (𝑋 = (π‘†β€˜π‘—) ↔ (π‘†β€˜π‘—) = 𝑋)
235234biimpri 227 . . . . . . . . . . . 12 ((π‘†β€˜π‘—) = 𝑋 β†’ 𝑋 = (π‘†β€˜π‘—))
236235adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 = (π‘†β€˜π‘—))
237233, 236breqtrd 5175 . . . . . . . . . 10 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
238237adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
239226, 227, 229, 231, 238lelttrd 11372 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
240239adantllr 718 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
241 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) = 𝑋)
242198, 139eqbrtrid 5184 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
243242adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
244241, 243eqbrtrd 5171 . . . . . . . 8 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
245244adantlr 714 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
246240, 245jca 513 . . . . . 6 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
247225, 246mtand 815 . . . . 5 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ (π‘†β€˜π‘—) = 𝑋)
248247nrexdv 3150 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ Β¬ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
249 isof1o 7320 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) β†’ 𝑆:(0...𝑁)–1-1-onto→𝐻)
250206, 249syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑆:(0...𝑁)–1-1-onto→𝐻)
251 f1ofo 6841 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto→𝐻 β†’ 𝑆:(0...𝑁)–onto→𝐻)
252250, 251syl 17 . . . . . . 7 (πœ‘ β†’ 𝑆:(0...𝑁)–onto→𝐻)
253 foelrn 7108 . . . . . . 7 ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
254252, 253sylan 581 . . . . . 6 ((πœ‘ ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
255234rexbii 3095 . . . . . 6 (βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—) ↔ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
256254, 255sylib 217 . . . . 5 ((πœ‘ ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
257256adantlr 714 . . . 4 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
258248, 257mtand 815 . . 3 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ Β¬ 𝑋 ∈ 𝐻)
259199, 258pm2.65da 816 . 2 (πœ‘ β†’ Β¬ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
26052, 60, 259nltled 11364 1 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜πΎ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433   βˆͺ cun 3947   βŠ† wss 3949  {cpr 4631   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ran crn 5678  β„©cio 6494  Fun wfun 6538  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544   Isom wiso 6545  (class class class)co 7409   ↑m cmap 8820  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115  β„*cxr 11247   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444   / cdiv 11871  β„•cn 12212  β„€cz 12558  (,]cioc 13325  [,)cico 13326  [,]cicc 13327  ...cfz 13484  ..^cfzo 13627  βŒŠcfl 13755  β™―chash 14290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fi 9406  df-sup 9437  df-inf 9438  df-oi 9505  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-ioo 13328  df-ioc 13329  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-fl 13757  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-rest 17368  df-topgen 17389  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-top 22396  df-topon 22413  df-bases 22449  df-cld 22523  df-ntr 22524  df-cls 22525  df-nei 22602  df-lp 22640  df-cmp 22891
This theorem is referenced by:  fourierdlem79  44901
  Copyright terms: Public domain W3C validator