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

Theorem fourierdlem77 44577
Description: If 𝐻 is bounded, then π‘ˆ is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem77.f (πœ‘ β†’ 𝐹:β„βŸΆβ„)
fourierdlem77.x (πœ‘ β†’ 𝑋 ∈ ℝ)
fourierdlem77.y (πœ‘ β†’ π‘Œ ∈ ℝ)
fourierdlem77.w (πœ‘ β†’ π‘Š ∈ ℝ)
fourierdlem77.h 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
fourierdlem77.k 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
fourierdlem77.u π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
fourierdlem77.bd (πœ‘ β†’ βˆƒπ‘Ž ∈ ℝ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
Assertion
Ref Expression
fourierdlem77 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏)
Distinct variable groups:   𝐾,𝑏,𝑠   π‘ˆ,π‘Ž,𝑏   πœ‘,π‘Ž,𝑠
Allowed substitution hints:   πœ‘(𝑏)   π‘ˆ(𝑠)   𝐹(𝑠,π‘Ž,𝑏)   𝐻(𝑠,π‘Ž,𝑏)   𝐾(π‘Ž)   π‘Š(𝑠,π‘Ž,𝑏)   𝑋(𝑠,π‘Ž,𝑏)   π‘Œ(𝑠,π‘Ž,𝑏)

Proof of Theorem fourierdlem77
Dummy variables 𝑐 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem77.bd . 2 (πœ‘ β†’ βˆƒπ‘Ž ∈ ℝ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
2 pire 25867 . . . . . . . . . 10 Ο€ ∈ ℝ
32renegcli 11486 . . . . . . . . 9 -Ο€ ∈ ℝ
43a1i 11 . . . . . . . 8 (⊀ β†’ -Ο€ ∈ ℝ)
52a1i 11 . . . . . . . 8 (⊀ β†’ Ο€ ∈ ℝ)
6 pirp 25870 . . . . . . . . . . 11 Ο€ ∈ ℝ+
7 neglt 43672 . . . . . . . . . . 11 (Ο€ ∈ ℝ+ β†’ -Ο€ < Ο€)
86, 7ax-mp 5 . . . . . . . . . 10 -Ο€ < Ο€
93, 2, 8ltleii 11302 . . . . . . . . 9 -Ο€ ≀ Ο€
109a1i 11 . . . . . . . 8 (⊀ β†’ -Ο€ ≀ Ο€)
11 fourierdlem77.k . . . . . . . . . 10 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
1211fourierdlem62 44562 . . . . . . . . 9 𝐾 ∈ ((-Ο€[,]Ο€)–cn→ℝ)
1312a1i 11 . . . . . . . 8 (⊀ β†’ 𝐾 ∈ ((-Ο€[,]Ο€)–cn→ℝ))
144, 5, 10, 13evthiccabs 43887 . . . . . . 7 (⊀ β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)) ∧ βˆƒπ‘₯ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘₯)) ≀ (absβ€˜(πΎβ€˜π‘¦))))
1514mptru 1548 . . . . . 6 (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)) ∧ βˆƒπ‘₯ ∈ (-Ο€[,]Ο€)βˆ€π‘¦ ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘₯)) ≀ (absβ€˜(πΎβ€˜π‘¦)))
1615simpli 484 . . . . 5 βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))
1716a1i 11 . . . 4 ((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) β†’ βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)))
18 simpl 483 . . . . . . . . . . . 12 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ π‘Ž ∈ ℝ)
1911fourierdlem43 44544 . . . . . . . . . . . . . 14 𝐾:(-Ο€[,]Ο€)βŸΆβ„
2019ffvelcdmi 7054 . . . . . . . . . . . . 13 (𝑐 ∈ (-Ο€[,]Ο€) β†’ (πΎβ€˜π‘) ∈ ℝ)
2120adantl 482 . . . . . . . . . . . 12 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (πΎβ€˜π‘) ∈ ℝ)
2218, 21remulcld 11209 . . . . . . . . . . 11 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (π‘Ž Β· (πΎβ€˜π‘)) ∈ ℝ)
2322recnd 11207 . . . . . . . . . 10 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (π‘Ž Β· (πΎβ€˜π‘)) ∈ β„‚)
2423abscld 15348 . . . . . . . . 9 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) ∈ ℝ)
2523absge0d 15356 . . . . . . . . 9 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ 0 ≀ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))))
2624, 25ge0p1rpd 13011 . . . . . . . 8 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) ∈ ℝ+)
27263ad2antl2 1186 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) ∈ ℝ+)
28273adant3 1132 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) β†’ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) ∈ ℝ+)
29 nfv 1917 . . . . . . . . 9 β„²π‘ πœ‘
30 nfv 1917 . . . . . . . . 9 Ⅎ𝑠 π‘Ž ∈ ℝ
31 nfra1 3278 . . . . . . . . 9 β„²π‘ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž
3229, 30, 31nf3an 1904 . . . . . . . 8 Ⅎ𝑠(πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
33 nfv 1917 . . . . . . . 8 Ⅎ𝑠 𝑐 ∈ (-Ο€[,]Ο€)
34 nfra1 3278 . . . . . . . 8 β„²π‘ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))
3532, 33, 34nf3an 1904 . . . . . . 7 Ⅎ𝑠((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)))
36 simpl11 1248 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ πœ‘)
37 simpl12 1249 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ π‘Ž ∈ ℝ)
3836, 37jca 512 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (πœ‘ ∧ π‘Ž ∈ ℝ))
39 simpl13 1250 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
40 rspa 3242 . . . . . . . . . . 11 ((βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
4139, 40sylancom 588 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
42 simpl2 1192 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 𝑐 ∈ (-Ο€[,]Ο€))
4338, 41, 42jca31 515 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)))
44 rspa 3242 . . . . . . . . . 10 ((βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)))
45443ad2antl3 1187 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)))
46 simpr 485 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
47 simp-5l 783 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ πœ‘)
48 simpr 485 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
49 fourierdlem77.f . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
50 fourierdlem77.x . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑋 ∈ ℝ)
51 fourierdlem77.y . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘Œ ∈ ℝ)
52 fourierdlem77.w . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘Š ∈ ℝ)
53 fourierdlem77.h . . . . . . . . . . . . . . . . . 18 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
5449, 50, 51, 52, 53fourierdlem9 44510 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„)
5554ffvelcdmda 7055 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (π»β€˜π‘ ) ∈ ℝ)
5619ffvelcdmi 7054 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-Ο€[,]Ο€) β†’ (πΎβ€˜π‘ ) ∈ ℝ)
5756adantl 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (πΎβ€˜π‘ ) ∈ ℝ)
5855, 57remulcld 11209 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ)
59 fourierdlem77.u . . . . . . . . . . . . . . . 16 π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
6059fvmpt2 6979 . . . . . . . . . . . . . . 15 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
6148, 58, 60syl2anc 584 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
6261, 58eqeltrd 2832 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (π‘ˆβ€˜π‘ ) ∈ ℝ)
6362recnd 11207 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (π‘ˆβ€˜π‘ ) ∈ β„‚)
6463abscld 15348 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) ∈ ℝ)
6547, 64sylancom 588 . . . . . . . . . 10 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) ∈ ℝ)
66 simp-5r 784 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ π‘Ž ∈ ℝ)
67 simpllr 774 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 𝑐 ∈ (-Ο€[,]Ο€))
6866, 67, 24syl2anc 584 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) ∈ ℝ)
69 peano2re 11352 . . . . . . . . . . 11 ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) ∈ ℝ β†’ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) ∈ ℝ)
7068, 69syl 17 . . . . . . . . . 10 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) ∈ ℝ)
7161fveq2d 6866 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) = (absβ€˜((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))))
7247, 71sylancom 588 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) = (absβ€˜((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))))
7355recnd 11207 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (π»β€˜π‘ ) ∈ β„‚)
7473abscld 15348 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ∈ ℝ)
7547, 74sylancom 588 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ∈ ℝ)
76 recn 11165 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ ℝ β†’ π‘Ž ∈ β„‚)
7776abscld 15348 . . . . . . . . . . . . . . 15 (π‘Ž ∈ ℝ β†’ (absβ€˜π‘Ž) ∈ ℝ)
7866, 77syl 17 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜π‘Ž) ∈ ℝ)
7956recnd 11207 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (-Ο€[,]Ο€) β†’ (πΎβ€˜π‘ ) ∈ β„‚)
8079abscld 15348 . . . . . . . . . . . . . . 15 (𝑠 ∈ (-Ο€[,]Ο€) β†’ (absβ€˜(πΎβ€˜π‘ )) ∈ ℝ)
8180adantl 482 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(πΎβ€˜π‘ )) ∈ ℝ)
8220recnd 11207 . . . . . . . . . . . . . . . 16 (𝑐 ∈ (-Ο€[,]Ο€) β†’ (πΎβ€˜π‘) ∈ β„‚)
8382abscld 15348 . . . . . . . . . . . . . . 15 (𝑐 ∈ (-Ο€[,]Ο€) β†’ (absβ€˜(πΎβ€˜π‘)) ∈ ℝ)
8467, 83syl 17 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(πΎβ€˜π‘)) ∈ ℝ)
8573absge0d 15356 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 0 ≀ (absβ€˜(π»β€˜π‘ )))
8647, 85sylancom 588 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 0 ≀ (absβ€˜(π»β€˜π‘ )))
8782absge0d 15356 . . . . . . . . . . . . . . 15 (𝑐 ∈ (-Ο€[,]Ο€) β†’ 0 ≀ (absβ€˜(πΎβ€˜π‘)))
8867, 87syl 17 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ 0 ≀ (absβ€˜(πΎβ€˜π‘)))
8974ad4ant14 750 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ∈ ℝ)
90 simpllr 774 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ π‘Ž ∈ ℝ)
9177ad3antlr 729 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜π‘Ž) ∈ ℝ)
92 simplr 767 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž)
9390leabsd 15326 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ π‘Ž ≀ (absβ€˜π‘Ž))
9489, 90, 91, 92, 93letrd 11336 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ≀ (absβ€˜π‘Ž))
9594ad4ant14 750 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π»β€˜π‘ )) ≀ (absβ€˜π‘Ž))
96 simplr 767 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)))
9775, 78, 81, 84, 86, 88, 95, 96lemul12bd 12122 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ ((absβ€˜(π»β€˜π‘ )) Β· (absβ€˜(πΎβ€˜π‘ ))) ≀ ((absβ€˜π‘Ž) Β· (absβ€˜(πΎβ€˜π‘))))
9857recnd 11207 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (πΎβ€˜π‘ ) ∈ β„‚)
9973, 98absmuld 15366 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) = ((absβ€˜(π»β€˜π‘ )) Β· (absβ€˜(πΎβ€˜π‘ ))))
10047, 99sylancom 588 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) = ((absβ€˜(π»β€˜π‘ )) Β· (absβ€˜(πΎβ€˜π‘ ))))
10176adantr 481 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ π‘Ž ∈ β„‚)
10221recnd 11207 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (πΎβ€˜π‘) ∈ β„‚)
103101, 102absmuld 15366 . . . . . . . . . . . . . 14 ((π‘Ž ∈ ℝ ∧ 𝑐 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) = ((absβ€˜π‘Ž) Β· (absβ€˜(πΎβ€˜π‘))))
10466, 67, 103syl2anc 584 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) = ((absβ€˜π‘Ž) Β· (absβ€˜(πΎβ€˜π‘))))
10597, 100, 1043brtr4d 5157 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) ≀ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))))
10672, 105eqbrtrd 5147 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) ≀ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))))
10768ltp1d 12109 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) < ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1))
10865, 68, 70, 106, 107lelttrd 11337 . . . . . . . . . 10 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) < ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1))
10965, 70, 108ltled 11327 . . . . . . . . 9 ((((((πœ‘ ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€)) ∧ (absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1))
11043, 45, 46, 109syl21anc 836 . . . . . . . 8 ((((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) ∧ 𝑠 ∈ (-Ο€[,]Ο€)) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1))
111110ex 413 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) β†’ (𝑠 ∈ (-Ο€[,]Ο€) β†’ (absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1)))
11235, 111ralrimi 3251 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) β†’ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1))
113 breq2 5129 . . . . . . . 8 (𝑏 = ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) β†’ ((absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏 ↔ (absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1)))
114113ralbidv 3176 . . . . . . 7 (𝑏 = ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) β†’ (βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏 ↔ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1)))
115114rspcev 3595 . . . . . 6 ((((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1) ∈ ℝ+ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ ((absβ€˜(π‘Ž Β· (πΎβ€˜π‘))) + 1)) β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏)
11628, 112, 115syl2anc 584 . . . . 5 (((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) ∧ 𝑐 ∈ (-Ο€[,]Ο€) ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘))) β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏)
117116rexlimdv3a 3158 . . . 4 ((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) β†’ (βˆƒπ‘ ∈ (-Ο€[,]Ο€)βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(πΎβ€˜π‘ )) ≀ (absβ€˜(πΎβ€˜π‘)) β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏))
11817, 117mpd 15 . . 3 ((πœ‘ ∧ π‘Ž ∈ ℝ ∧ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž) β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏)
119118rexlimdv3a 3158 . 2 (πœ‘ β†’ (βˆƒπ‘Ž ∈ ℝ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π»β€˜π‘ )) ≀ π‘Ž β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏))
1201, 119mpd 15 1 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ+ βˆ€π‘  ∈ (-Ο€[,]Ο€)(absβ€˜(π‘ˆβ€˜π‘ )) ≀ 𝑏)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106  βˆ€wral 3060  βˆƒwrex 3069  ifcif 4506   class class class wbr 5125   ↦ cmpt 5208  βŸΆwf 6512  β€˜cfv 6516  (class class class)co 7377  β„‚cc 11073  β„cr 11074  0cc0 11075  1c1 11076   + caddc 11078   Β· cmul 11080   < clt 11213   ≀ cle 11214   βˆ’ cmin 11409  -cneg 11410   / cdiv 11836  2c2 12232  β„+crp 12939  [,]cicc 13292  abscabs 15146  sincsin 15972  Ο€cpi 15975  β€“cnβ†’ccncf 24291
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 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-inf2 9601  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154  ax-mulf 11155
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-pss 3947  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4886  df-int 4928  df-iun 4976  df-iin 4977  df-br 5126  df-opab 5188  df-mpt 5209  df-tr 5243  df-id 5551  df-eprel 5557  df-po 5565  df-so 5566  df-fr 5608  df-se 5609  df-we 5610  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-pred 6273  df-ord 6340  df-on 6341  df-lim 6342  df-suc 6343  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-of 7637  df-om 7823  df-1st 7941  df-2nd 7942  df-supp 8113  df-frecs 8232  df-wrecs 8263  df-recs 8337  df-rdg 8376  df-1o 8432  df-2o 8433  df-er 8670  df-map 8789  df-pm 8790  df-ixp 8858  df-en 8906  df-dom 8907  df-sdom 8908  df-fin 8909  df-fsupp 9328  df-fi 9371  df-sup 9402  df-inf 9403  df-oi 9470  df-card 9899  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11411  df-neg 11412  df-div 11837  df-nn 12178  df-2 12240  df-3 12241  df-4 12242  df-5 12243  df-6 12244  df-7 12245  df-8 12246  df-9 12247  df-n0 12438  df-z 12524  df-dec 12643  df-uz 12788  df-q 12898  df-rp 12940  df-xneg 13057  df-xadd 13058  df-xmul 13059  df-ioo 13293  df-ioc 13294  df-ico 13295  df-icc 13296  df-fz 13450  df-fzo 13593  df-fl 13722  df-mod 13800  df-seq 13932  df-exp 13993  df-fac 14199  df-bc 14228  df-hash 14256  df-shft 14979  df-cj 15011  df-re 15012  df-im 15013  df-sqrt 15147  df-abs 15148  df-limsup 15380  df-clim 15397  df-rlim 15398  df-sum 15598  df-ef 15976  df-sin 15978  df-cos 15979  df-pi 15981  df-struct 17045  df-sets 17062  df-slot 17080  df-ndx 17092  df-base 17110  df-ress 17139  df-plusg 17175  df-mulr 17176  df-starv 17177  df-sca 17178  df-vsca 17179  df-ip 17180  df-tset 17181  df-ple 17182  df-ds 17184  df-unif 17185  df-hom 17186  df-cco 17187  df-rest 17333  df-topn 17334  df-0g 17352  df-gsum 17353  df-topgen 17354  df-pt 17355  df-prds 17358  df-xrs 17413  df-qtop 17418  df-imas 17419  df-xps 17421  df-mre 17495  df-mrc 17496  df-acs 17498  df-mgm 18526  df-sgrp 18575  df-mnd 18586  df-submnd 18631  df-mulg 18902  df-cntz 19126  df-cmn 19593  df-psmet 20840  df-xmet 20841  df-met 20842  df-bl 20843  df-mopn 20844  df-fbas 20845  df-fg 20846  df-cnfld 20849  df-top 22295  df-topon 22312  df-topsp 22334  df-bases 22348  df-cld 22422  df-ntr 22423  df-cls 22424  df-nei 22501  df-lp 22539  df-perf 22540  df-cn 22630  df-cnp 22631  df-t1 22717  df-haus 22718  df-cmp 22790  df-tx 22965  df-hmeo 23158  df-fil 23249  df-fm 23341  df-flim 23342  df-flf 23343  df-xms 23725  df-ms 23726  df-tms 23727  df-cncf 24293  df-limc 25282  df-dv 25283
This theorem is referenced by:  fourierdlem87  44587
  Copyright terms: Public domain W3C validator