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 44970
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 7419 . . . . . . . . 9 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))))
54oveq1d 7426 . . . . . . . 8 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
65fveq2d 6895 . . . . . . 7 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
76oveq1d 7426 . . . . . 6 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
83, 7oveq12d 7429 . . . . 5 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
98adantl 482 . . . 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 44961 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 495 . . . . . . . . 9 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)))
2322simprd 496 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ (π‘‚β€˜π‘))
2422simpld 495 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•)
2517fourierdlem2 44910 . . . . . . . . 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 495 . . . . . 6 (πœ‘ β†’ 𝑆 ∈ (ℝ ↑m (0...𝑁)))
29 elmapi 8845 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) β†’ 𝑆:(0...𝑁)βŸΆβ„)
3028, 29syl 17 . . . . 5 (πœ‘ β†’ 𝑆:(0...𝑁)βŸΆβ„)
31 fourierdlem63.j . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
32 fzofzp1 13731 . . . . . 6 (𝐽 ∈ (0..^𝑁) β†’ (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (πœ‘ β†’ (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7087 . . . 4 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 44919 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡))
3635simp2d 1143 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ℝ)
3736, 34resubcld 11644 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
3835simp1d 1142 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
3936, 38resubcld 11644 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
4010, 39eqeltrid 2837 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ ℝ)
4135simp3d 1144 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
4238, 36posdifd 11803 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
4341, 42mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
4443, 10breqtrrdi 5190 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝑇)
4544gt0ne0d 11780 . . . . . . . . 9 (πœ‘ β†’ 𝑇 β‰  0)
4637, 40, 45redivcld 12044 . . . . . . . 8 (πœ‘ β†’ ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13765 . . . . . . 7 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ β„€)
4847zred 12668 . . . . . 6 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11246 . . . . 5 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) ∈ ℝ)
5034, 49readdcld 11245 . . . 4 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 7005 . . 3 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
5251, 50eqeltrd 2833 . 2 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 44910 . . . . . . 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 495 . . . 4 (πœ‘ β†’ 𝑄 ∈ (ℝ ↑m (0...𝑀)))
57 elmapi 8845 . . . 4 (𝑄 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑄:(0...𝑀)βŸΆβ„)
5856, 57syl 17 . . 3 (πœ‘ β†’ 𝑄:(0...𝑀)βŸΆβ„)
59 fourierdlem63.k . . 3 (πœ‘ β†’ 𝐾 ∈ (0...𝑀))
6058, 59ffvelcdmd 7087 . 2 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ℝ)
6114adantr 481 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ∈ ℝ)
6215adantr 481 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐷 ∈ ℝ)
6338rexrd 11266 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ*)
64 iocssre 13406 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ) β†’ (𝐴(,]𝐡) βŠ† ℝ)
6563, 36, 64syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(,]𝐡) βŠ† ℝ)
6638, 36, 41, 10, 1fourierdlem4 44912 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸:β„βŸΆ(𝐴(,]𝐡))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))))
68 elfzofz 13650 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7087 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜π½) ∈ ℝ)
7134rexrd 11266 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*)
72 elico2 13390 . . . . . . . . . . . . . . 15 (((π‘†β€˜π½) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*) β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7370, 71, 72syl2anc 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7467, 73mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1))))
7574simp1d 1142 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ ℝ)
7666, 75ffvelcdmd 7087 . . . . . . . . . . 11 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ (𝐴(,]𝐡))
7765, 76sseldd 3983 . . . . . . . . . 10 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ ℝ)
7877, 75resubcld 11644 . . . . . . . . 9 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ ℝ)
7960, 78resubcld 11644 . . . . . . . 8 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
8079adantr 481 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
81 icossicc 13415 . . . . . . . . . . . . . 14 ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1)))
8214rexrd 11266 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 ∈ ℝ*)
8315rexrd 11266 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 44923 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆:(0...𝑁)⟢(𝐢[,]𝐷))
8582, 83, 84, 31fourierdlem8 44916 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8681, 85sstrid 3993 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8786, 67sseldd 3983 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ (𝐢[,]𝐷))
88 elicc2 13391 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
8914, 15, 88syl2anc 584 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
9087, 89mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷))
9190simp2d 1143 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ≀ π‘Œ)
9260, 77resubcld 11644 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜π‘Œ) < (π‘„β€˜πΎ))
9477, 60posdifd 11803 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((πΈβ€˜π‘Œ) < (π‘„β€˜πΎ) ↔ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9593, 94mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)))
9692, 95elrpd 13015 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ+)
9775, 96ltaddrpd 13051 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ < (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9860recnd 11244 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ β„‚)
9977recnd 11244 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ β„‚)
10075recnd 11244 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ∈ β„‚)
10198, 99, 100subsub3d 11603 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)))
10298, 100addcomd 11418 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) + π‘Œ) = (π‘Œ + (π‘„β€˜πΎ)))
103102oveq1d 7426 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)) = ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)))
104100, 98, 99addsubassd 11593 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)) = (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
105101, 103, 1043eqtrrd 2777 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))) = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10697, 105breqtrd 5174 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10714, 75, 79, 91, 106lelttrd 11374 . . . . . . . . 9 (πœ‘ β†’ 𝐢 < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10814, 79, 107ltled 11364 . . . . . . . 8 (πœ‘ β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
109108adantr 481 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
11034adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
11160adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ ℝ)
11252, 34resubcld 11644 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
113112adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11644 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1144 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ < (π‘†β€˜(𝐽 + 1)))
11675, 34, 115ltled 11364 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ≀ (π‘†β€˜(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 44915 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ≀ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
118112, 78, 60, 117lesub2dd 11833 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
119118adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
12098adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ β„‚)
12152recnd 11244 . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
122121adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
123110recnd 11244 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
124120, 122, 123subsubd 11601 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))))
12598, 121subcld 11573 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ β„‚)
12634recnd 11244 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
127125, 126addcomd 11418 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
128127adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
129124, 128eqtrd 2772 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
130 simpr 485 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
13152adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11842 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
133130, 132mpbird 256 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0)
134111, 131resubcld 11644 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11431 . . . . . . . . . . . . 13 ((((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
136134, 110, 135syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
137133, 136mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1)))
138129, 137eqbrtrd 5170 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) < (π‘†β€˜(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11374 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < (π‘†β€˜(𝐽 + 1)))
14084, 33ffvelcdmd 7087 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷))
141 elicc2 13391 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
14214, 15, 141syl2anc 584 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
143140, 142mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷))
144143simp3d 1144 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
145144adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
14680, 110, 62, 139, 145ltletrd 11376 . . . . . . . 8 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < 𝐷)
14780, 62, 146ltled 11364 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ 𝐷)
14861, 62, 80, 109, 147eliccd 44302 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ π‘₯ = π‘Œ)
150 oveq2 7419 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Œ β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ π‘Œ))
151150oveq1d 7426 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Œ β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ π‘Œ) / 𝑇))
152151fveq2d 6895 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Œ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
153152oveq1d 7426 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
154149, 153oveq12d 7429 . . . . . . . . . . . . . 14 (π‘₯ = π‘Œ β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
155154adantl 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ = π‘Œ) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
15636, 75resubcld 11644 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 βˆ’ π‘Œ) ∈ ℝ)
157156, 40, 45redivcld 12044 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝐡 βˆ’ π‘Œ) / 𝑇) ∈ ℝ)
158157flcld 13765 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„€)
159158zred 12668 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11246 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ ℝ)
16175, 160readdcld 11245 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 7005 . . . . . . . . . . . 12 (πœ‘ β†’ (πΈβ€˜π‘Œ) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
163162oveq1d 7426 . . . . . . . . . . 11 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) = ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ))
164163oveq1d 7426 . . . . . . . . . 10 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇))
165160recnd 11244 . . . . . . . . . . . 12 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ β„‚)
166100, 165pncan2d 11575 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
167166oveq1d 7426 . . . . . . . . . 10 (πœ‘ β†’ (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇) = (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇))
168159recnd 11244 . . . . . . . . . . 11 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„‚)
16940recnd 11244 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ β„‚)
170168, 169, 45divcan4d 11998 . . . . . . . . . 10 (πœ‘ β†’ (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
171164, 167, 1703eqtrd 2776 . . . . . . . . 9 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
172171, 158eqeltrd 2833 . . . . . . . 8 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€)
17378recnd 11244 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ β„‚)
174173, 169, 45divcan1d 11993 . . . . . . . . . . 11 (πœ‘ β†’ ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇) = ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
175174oveq2d 7427 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
17698, 173npcand 11577 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (π‘„β€˜πΎ))
177175, 176eqtrd 2772 . . . . . . . . 9 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (π‘„β€˜πΎ))
178 ffun 6720 . . . . . . . . . . 11 (𝑄:(0...𝑀)βŸΆβ„ β†’ Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (πœ‘ β†’ Fun 𝑄)
18058fdmd 6728 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2836 . . . . . . . . . 10 (πœ‘ β†’ 𝐾 ∈ dom 𝑄)
182 fvelrn 7078 . . . . . . . . . 10 ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
183179, 181, 182syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
184177, 183eqeltrd 2833 . . . . . . . 8 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄)
185 oveq1 7418 . . . . . . . . . . 11 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (π‘˜ Β· 𝑇) = ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇))
186185oveq2d 7427 . . . . . . . . . 10 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)))
187186eleq1d 2818 . . . . . . . . 9 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ ((((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄))
188187rspcev 3612 . . . . . . . 8 (((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€ ∧ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 584 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
190189adantr 481 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
191 oveq1 7418 . . . . . . . . 9 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (π‘₯ + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)))
192191eleq1d 2818 . . . . . . . 8 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ ((π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
193192rexbidv 3178 . . . . . . 7 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
194193elrab 3683 . . . . . 6 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷) ∧ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 583 . . . . 5 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
196 elun2 4177 . . . . 5 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
199197, 198, 183eltr4g 2850 . . 3 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 ∈ 𝐻)
200 elfzelz 13503 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ β„€)
201200ad2antlr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝑗 ∈ β„€)
202 elfzoelz 13634 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ β„€)
20331, 202syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐽 ∈ β„€)
204203ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 ∈ β„€)
205 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
20621simprd 496 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 ∈ (0...𝑁))
209 simplr 767 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑁))
210 isorel 7325 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
211207, 208, 209, 210syl12anc 835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
212205, 211mpbird 256 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 < 𝑗)
213212adantrr 715 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 < 𝑗)
214 simpr 485 . . . . . . . . . . 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 7325 . . . . . . . . . . . 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 12640 . . . . . . . . 9 ((𝐽 ∈ β„€ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) β†’ Β¬ 𝑗 ∈ β„€)
223204, 213, 221, 222syl3anc 1371 . . . . . . . 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 7086 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π‘†β€˜π‘—) ∈ ℝ)
229228adantr 481 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) ∈ ℝ)
23074simp2d 1143 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜π½) ≀ π‘Œ)
231230ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) ≀ π‘Œ)
232106, 198breqtrrdi 5190 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ < 𝑋)
233232adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < 𝑋)
234 eqcom 2739 . . . . . . . . . . . . 13 (𝑋 = (π‘†β€˜π‘—) ↔ (π‘†β€˜π‘—) = 𝑋)
235234biimpri 227 . . . . . . . . . . . 12 ((π‘†β€˜π‘—) = 𝑋 β†’ 𝑋 = (π‘†β€˜π‘—))
236235adantl 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 = (π‘†β€˜π‘—))
237233, 236breqtrd 5174 . . . . . . . . . 10 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
238237adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
239226, 227, 229, 231, 238lelttrd 11374 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
240239adantllr 717 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
241 simpr 485 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) = 𝑋)
242198, 139eqbrtrid 5183 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
243242adantr 481 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
244241, 243eqbrtrd 5170 . . . . . . . 8 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
245244adantlr 713 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
246240, 245jca 512 . . . . . 6 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
247225, 246mtand 814 . . . . 5 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ (π‘†β€˜π‘—) = 𝑋)
248247nrexdv 3149 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ Β¬ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
249 isof1o 7322 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) β†’ 𝑆:(0...𝑁)–1-1-onto→𝐻)
250206, 249syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑆:(0...𝑁)–1-1-onto→𝐻)
251 f1ofo 6840 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto→𝐻 β†’ 𝑆:(0...𝑁)–onto→𝐻)
252250, 251syl 17 . . . . . . 7 (πœ‘ β†’ 𝑆:(0...𝑁)–onto→𝐻)
253 foelrn 7108 . . . . . . 7 ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
254252, 253sylan 580 . . . . . 6 ((πœ‘ ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
255234rexbii 3094 . . . . . 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 11366 1 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜πΎ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   βˆͺ cun 3946   βŠ† wss 3948  {cpr 4630   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  ran crn 5677  β„©cio 6493  Fun wfun 6537  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7411   ↑m cmap 8822  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  β„*cxr 11249   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446   / cdiv 11873  β„•cn 12214  β„€cz 12560  (,]cioc 13327  [,)cico 13328  [,]cicc 13329  ...cfz 13486  ..^cfzo 13629  βŒŠcfl 13757  β™―chash 14292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-xnn0 12547  df-z 12561  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-ioo 13330  df-ioc 13331  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-rest 17370  df-topgen 17391  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-top 22403  df-topon 22420  df-bases 22456  df-cld 22530  df-ntr 22531  df-cls 22532  df-nei 22609  df-lp 22647  df-cmp 22898
This theorem is referenced by:  fourierdlem79  44986
  Copyright terms: Public domain W3C validator