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 45480
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 7422 . . . . . . . . 9 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))))
54oveq1d 7429 . . . . . . . 8 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
65fveq2d 6895 . . . . . . 7 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
76oveq1d 7429 . . . . . 6 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
83, 7oveq12d 7432 . . . . 5 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
98adantl 481 . . . 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 45471 . . . . . . . . . 10 (πœ‘ β†’ ((𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 494 . . . . . . . . 9 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)))
2322simprd 495 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ (π‘‚β€˜π‘))
2422simpld 494 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•)
2517fourierdlem2 45420 . . . . . . . . 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 494 . . . . . 6 (πœ‘ β†’ 𝑆 ∈ (ℝ ↑m (0...𝑁)))
29 elmapi 8859 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) β†’ 𝑆:(0...𝑁)βŸΆβ„)
3028, 29syl 17 . . . . 5 (πœ‘ β†’ 𝑆:(0...𝑁)βŸΆβ„)
31 fourierdlem63.j . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
32 fzofzp1 13753 . . . . . 6 (𝐽 ∈ (0..^𝑁) β†’ (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (πœ‘ β†’ (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7089 . . . 4 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 45429 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡))
3635simp2d 1141 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ℝ)
3736, 34resubcld 11664 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
3835simp1d 1140 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
3936, 38resubcld 11664 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
4010, 39eqeltrid 2832 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ ℝ)
4135simp3d 1142 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
4238, 36posdifd 11823 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
4341, 42mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
4443, 10breqtrrdi 5184 . . . . . . . . . 10 (πœ‘ β†’ 0 < 𝑇)
4544gt0ne0d 11800 . . . . . . . . 9 (πœ‘ β†’ 𝑇 β‰  0)
4637, 40, 45redivcld 12064 . . . . . . . 8 (πœ‘ β†’ ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13787 . . . . . . 7 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ β„€)
4847zred 12688 . . . . . 6 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11266 . . . . 5 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) ∈ ℝ)
5034, 49readdcld 11265 . . . 4 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 7006 . . 3 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
5251, 50eqeltrd 2828 . 2 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 45420 . . . . . . 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 494 . . . 4 (πœ‘ β†’ 𝑄 ∈ (ℝ ↑m (0...𝑀)))
57 elmapi 8859 . . . 4 (𝑄 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑄:(0...𝑀)βŸΆβ„)
5856, 57syl 17 . . 3 (πœ‘ β†’ 𝑄:(0...𝑀)βŸΆβ„)
59 fourierdlem63.k . . 3 (πœ‘ β†’ 𝐾 ∈ (0...𝑀))
6058, 59ffvelcdmd 7089 . 2 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ℝ)
6114adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ∈ ℝ)
6215adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐷 ∈ ℝ)
6338rexrd 11286 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ*)
64 iocssre 13428 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ) β†’ (𝐴(,]𝐡) βŠ† ℝ)
6563, 36, 64syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(,]𝐡) βŠ† ℝ)
6638, 36, 41, 10, 1fourierdlem4 45422 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸:β„βŸΆ(𝐴(,]𝐡))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))))
68 elfzofz 13672 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7089 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜π½) ∈ ℝ)
7134rexrd 11286 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*)
72 elico2 13412 . . . . . . . . . . . . . . 15 (((π‘†β€˜π½) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ*) β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7370, 71, 72syl2anc 583 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ ∈ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) ↔ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1)))))
7467, 73mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ (π‘†β€˜π½) ≀ π‘Œ ∧ π‘Œ < (π‘†β€˜(𝐽 + 1))))
7574simp1d 1140 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ ℝ)
7666, 75ffvelcdmd 7089 . . . . . . . . . . 11 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ (𝐴(,]𝐡))
7765, 76sseldd 3979 . . . . . . . . . 10 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ ℝ)
7877, 75resubcld 11664 . . . . . . . . 9 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ ℝ)
7960, 78resubcld 11664 . . . . . . . 8 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
8079adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ℝ)
81 icossicc 13437 . . . . . . . . . . . . . 14 ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1)))
8214rexrd 11286 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐢 ∈ ℝ*)
8315rexrd 11286 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 45433 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆:(0...𝑁)⟢(𝐢[,]𝐷))
8582, 83, 84, 31fourierdlem8 45426 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘†β€˜π½)[,](π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8681, 85sstrid 3989 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘†β€˜π½)[,)(π‘†β€˜(𝐽 + 1))) βŠ† (𝐢[,]𝐷))
8786, 67sseldd 3979 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ (𝐢[,]𝐷))
88 elicc2 13413 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
8914, 15, 88syl2anc 583 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘Œ ∈ (𝐢[,]𝐷) ↔ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷)))
9087, 89mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ ∈ ℝ ∧ 𝐢 ≀ π‘Œ ∧ π‘Œ ≀ 𝐷))
9190simp2d 1141 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ≀ π‘Œ)
9260, 77resubcld 11664 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜π‘Œ) < (π‘„β€˜πΎ))
9477, 60posdifd 11823 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((πΈβ€˜π‘Œ) < (π‘„β€˜πΎ) ↔ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9593, 94mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)))
9692, 95elrpd 13037 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ)) ∈ ℝ+)
9775, 96ltaddrpd 13073 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ < (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
9860recnd 11264 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ β„‚)
9977recnd 11264 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΈβ€˜π‘Œ) ∈ β„‚)
10075recnd 11264 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ∈ β„‚)
10198, 99, 100subsub3d 11623 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)))
10298, 100addcomd 11438 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘„β€˜πΎ) + π‘Œ) = (π‘Œ + (π‘„β€˜πΎ)))
103102oveq1d 7429 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘„β€˜πΎ) + π‘Œ) βˆ’ (πΈβ€˜π‘Œ)) = ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)))
104100, 98, 99addsubassd 11613 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘Œ + (π‘„β€˜πΎ)) βˆ’ (πΈβ€˜π‘Œ)) = (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))))
105101, 103, 1043eqtrrd 2772 . . . . . . . . . . 11 (πœ‘ β†’ (π‘Œ + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜π‘Œ))) = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10697, 105breqtrd 5168 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10714, 75, 79, 91, 106lelttrd 11394 . . . . . . . . 9 (πœ‘ β†’ 𝐢 < ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
10814, 79, 107ltled 11384 . . . . . . . 8 (πœ‘ β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
109108adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝐢 ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
11034adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
11160adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ ℝ)
11252, 34resubcld 11664 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
113112adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11664 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1142 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ < (π‘†β€˜(𝐽 + 1)))
11675, 34, 115ltled 11384 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ≀ (π‘†β€˜(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 45425 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ≀ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
118112, 78, 60, 117lesub2dd 11853 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
119118adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))))
12098adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) ∈ β„‚)
12152recnd 11264 . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
122121adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
123110recnd 11264 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
124120, 122, 123subsubd 11621 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))))
12598, 121subcld 11593 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ β„‚)
12634recnd 11264 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
127125, 126addcomd 11438 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
128127adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) + (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
129124, 128eqtrd 2767 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
130 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
13152adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11862 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
133130, 132mpbird 257 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0)
134111, 131resubcld 11664 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11451 . . . . . . . . . . . . 13 ((((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ ∧ (π‘†β€˜(𝐽 + 1)) ∈ ℝ) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
136134, 110, 135syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) < 0 ↔ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1))))
137133, 136mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘†β€˜(𝐽 + 1)) + ((π‘„β€˜πΎ) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) < (π‘†β€˜(𝐽 + 1)))
138129, 137eqbrtrd 5164 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1)))) < (π‘†β€˜(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11394 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < (π‘†β€˜(𝐽 + 1)))
14084, 33ffvelcdmd 7089 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷))
141 elicc2 13413 . . . . . . . . . . . . 13 ((𝐢 ∈ ℝ ∧ 𝐷 ∈ ℝ) β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
14214, 15, 141syl2anc 583 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ (𝐢[,]𝐷) ↔ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)))
143140, 142mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) ∈ ℝ ∧ 𝐢 ≀ (π‘†β€˜(𝐽 + 1)) ∧ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷))
144143simp3d 1142 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
145144adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ (π‘†β€˜(𝐽 + 1)) ≀ 𝐷)
14680, 110, 62, 139, 145ltletrd 11396 . . . . . . . 8 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) < 𝐷)
14780, 62, 146ltled 11384 . . . . . . 7 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ≀ 𝐷)
14861, 62, 80, 109, 147eliccd 44812 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ π‘₯ = π‘Œ)
150 oveq2 7422 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Œ β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ π‘Œ))
151150oveq1d 7429 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Œ β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ π‘Œ) / 𝑇))
152151fveq2d 6895 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Œ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
153152oveq1d 7429 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Œ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
154149, 153oveq12d 7432 . . . . . . . . . . . . . 14 (π‘₯ = π‘Œ β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
155154adantl 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ = π‘Œ) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
15636, 75resubcld 11664 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 βˆ’ π‘Œ) ∈ ℝ)
157156, 40, 45redivcld 12064 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝐡 βˆ’ π‘Œ) / 𝑇) ∈ ℝ)
158157flcld 13787 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„€)
159158zred 12688 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11266 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ ℝ)
16175, 160readdcld 11265 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 7006 . . . . . . . . . . . 12 (πœ‘ β†’ (πΈβ€˜π‘Œ) = (π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)))
163162oveq1d 7429 . . . . . . . . . . 11 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) = ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ))
164163oveq1d 7429 . . . . . . . . . 10 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇))
165160recnd 11264 . . . . . . . . . . . 12 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) ∈ β„‚)
166100, 165pncan2d 11595 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) = ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇))
167166oveq1d 7429 . . . . . . . . . 10 (πœ‘ β†’ (((π‘Œ + ((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇)) βˆ’ π‘Œ) / 𝑇) = (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇))
168159recnd 11264 . . . . . . . . . . 11 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) ∈ β„‚)
16940recnd 11264 . . . . . . . . . . 11 (πœ‘ β†’ 𝑇 ∈ β„‚)
170168, 169, 45divcan4d 12018 . . . . . . . . . 10 (πœ‘ β†’ (((βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)) Β· 𝑇) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
171164, 167, 1703eqtrd 2771 . . . . . . . . 9 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ π‘Œ) / 𝑇)))
172171, 158eqeltrd 2828 . . . . . . . 8 (πœ‘ β†’ (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€)
17378recnd 11264 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ) ∈ β„‚)
174173, 169, 45divcan1d 12013 . . . . . . . . . . 11 (πœ‘ β†’ ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇) = ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
175174oveq2d 7430 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)))
17698, 173npcand 11597 . . . . . . . . . 10 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) = (π‘„β€˜πΎ))
177175, 176eqtrd 2767 . . . . . . . . 9 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) = (π‘„β€˜πΎ))
178 ffun 6719 . . . . . . . . . . 11 (𝑄:(0...𝑀)βŸΆβ„ β†’ Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (πœ‘ β†’ Fun 𝑄)
18058fdmd 6727 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2831 . . . . . . . . . 10 (πœ‘ β†’ 𝐾 ∈ dom 𝑄)
182 fvelrn 7080 . . . . . . . . . 10 ((Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄) β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
183179, 181, 182syl2anc 583 . . . . . . . . 9 (πœ‘ β†’ (π‘„β€˜πΎ) ∈ ran 𝑄)
184177, 183eqeltrd 2828 . . . . . . . 8 (πœ‘ β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄)
185 oveq1 7421 . . . . . . . . . . 11 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (π‘˜ Β· 𝑇) = ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇))
186185oveq2d 7430 . . . . . . . . . 10 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)))
187186eleq1d 2813 . . . . . . . . 9 (π‘˜ = (((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) β†’ ((((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄))
188187rspcev 3607 . . . . . . . 8 (((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) ∈ β„€ ∧ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + ((((πΈβ€˜π‘Œ) βˆ’ π‘Œ) / 𝑇) Β· 𝑇)) ∈ ran 𝑄) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 583 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
190189adantr 480 . . . . . 6 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄)
191 oveq1 7421 . . . . . . . . 9 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (π‘₯ + (π‘˜ Β· 𝑇)) = (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)))
192191eleq1d 2813 . . . . . . . 8 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ ((π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
193192rexbidv 3173 . . . . . . 7 (π‘₯ = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) β†’ (βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
194193elrab 3680 . . . . . 6 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} ↔ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ (𝐢[,]𝐷) ∧ βˆƒπ‘˜ ∈ β„€ (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 582 . . . . 5 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
196 elun2 4173 . . . . 5 (((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ)) ∈ ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((π‘„β€˜πΎ) βˆ’ ((πΈβ€˜π‘Œ) βˆ’ π‘Œ))
199197, 198, 183eltr4g 2845 . . 3 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 ∈ 𝐻)
200 elfzelz 13525 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ β„€)
201200ad2antlr 726 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝑗 ∈ β„€)
202 elfzoelz 13656 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ β„€)
20331, 202syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐽 ∈ β„€)
204203ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 ∈ β„€)
205 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
20621simprd 495 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 ∈ (0...𝑁))
209 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑁))
210 isorel 7328 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
211207, 208, 209, 210syl12anc 836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ (𝐽 < 𝑗 ↔ (π‘†β€˜π½) < (π‘†β€˜π‘—)))
212205, 211mpbird 257 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π½) < (π‘†β€˜π‘—)) β†’ 𝐽 < 𝑗)
213212adantrr 716 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))) β†’ 𝐽 < 𝑗)
214 simpr 484 . . . . . . . . . . 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 7328 . . . . . . . . . . . 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 12660 . . . . . . . . 9 ((𝐽 ∈ β„€ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) β†’ Β¬ 𝑗 ∈ β„€)
223204, 213, 221, 222syl3anc 1369 . . . . . . . 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 7088 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π‘†β€˜π‘—) ∈ ℝ)
229228adantr 480 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) ∈ ℝ)
23074simp2d 1141 . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜π½) ≀ π‘Œ)
231230ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) ≀ π‘Œ)
232106, 198breqtrrdi 5184 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ < 𝑋)
233232adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < 𝑋)
234 eqcom 2734 . . . . . . . . . . . . 13 (𝑋 = (π‘†β€˜π‘—) ↔ (π‘†β€˜π‘—) = 𝑋)
235234biimpri 227 . . . . . . . . . . . 12 ((π‘†β€˜π‘—) = 𝑋 β†’ 𝑋 = (π‘†β€˜π‘—))
236235adantl 481 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 = (π‘†β€˜π‘—))
237233, 236breqtrd 5168 . . . . . . . . . 10 ((πœ‘ ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
238237adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ π‘Œ < (π‘†β€˜π‘—))
239226, 227, 229, 231, 238lelttrd 11394 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
240239adantllr 718 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π½) < (π‘†β€˜π‘—))
241 simpr 484 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) = 𝑋)
242198, 139eqbrtrid 5177 . . . . . . . . . 10 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
243242adantr 480 . . . . . . . . 9 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ 𝑋 < (π‘†β€˜(𝐽 + 1)))
244241, 243eqbrtrd 5164 . . . . . . . 8 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
245244adantlr 714 . . . . . . 7 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1)))
246240, 245jca 511 . . . . . 6 ((((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘†β€˜π‘—) = 𝑋) β†’ ((π‘†β€˜π½) < (π‘†β€˜π‘—) ∧ (π‘†β€˜π‘—) < (π‘†β€˜(𝐽 + 1))))
247225, 246mtand 815 . . . . 5 (((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Β¬ (π‘†β€˜π‘—) = 𝑋)
248247nrexdv 3144 . . . 4 ((πœ‘ ∧ (π‘„β€˜πΎ) < (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ Β¬ βˆƒπ‘— ∈ (0...𝑁)(π‘†β€˜π‘—) = 𝑋)
249 isof1o 7325 . . . . . . . . 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 7111 . . . . . . 7 ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
254252, 253sylan 579 . . . . . 6 ((πœ‘ ∧ 𝑋 ∈ 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑋 = (π‘†β€˜π‘—))
255234rexbii 3089 . . . . . 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 11386 1 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜πΎ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427   βˆͺ cun 3942   βŠ† wss 3944  {cpr 4626   class class class wbr 5142   ↦ cmpt 5225  dom cdm 5672  ran crn 5673  β„©cio 6492  Fun wfun 6536  βŸΆwf 6538  β€“ontoβ†’wfo 6540  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542   Isom wiso 6543  (class class class)co 7414   ↑m cmap 8836  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135  β„*cxr 11269   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466   / cdiv 11893  β„•cn 12234  β„€cz 12580  (,]cioc 13349  [,)cico 13350  [,]cicc 13351  ...cfz 13508  ..^cfzo 13651  βŒŠcfl 13779  β™―chash 14313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  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 8838  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-dju 9916  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-xnn0 12567  df-z 12581  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-rest 17395  df-topgen 17416  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-top 22783  df-topon 22800  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-cmp 23278
This theorem is referenced by:  fourierdlem79  45496
  Copyright terms: Public domain W3C validator