This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fperiodmul

Description: A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fperiodmul.f 
|- ( ph -> F : RR --> CC )
fperiodmul.t 
|- ( ph -> T e. RR )
fperiodmul.n 
|- ( ph -> N e. ZZ )
fperiodmul.x 
|- ( ph -> X e. RR )
fperiodmul.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
Assertion fperiodmul 
|- ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 fperiodmul.f 
 |-  ( ph -> F : RR --> CC )
2 fperiodmul.t 
 |-  ( ph -> T e. RR )
3 fperiodmul.n 
 |-  ( ph -> N e. ZZ )
4 fperiodmul.x 
 |-  ( ph -> X e. RR )
5 fperiodmul.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
6 1 adantr 
 |-  ( ( ph /\ N e. NN0 ) -> F : RR --> CC )
7 2 adantr 
 |-  ( ( ph /\ N e. NN0 ) -> T e. RR )
8 simpr 
 |-  ( ( ph /\ N e. NN0 ) -> N e. NN0 )
9 4 adantr 
 |-  ( ( ph /\ N e. NN0 ) -> X e. RR )
10 5 adantlr 
 |-  ( ( ( ph /\ N e. NN0 ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
11 6 7 8 9 10 fperiodmullem 
 |-  ( ( ph /\ N e. NN0 ) -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )
12 4 recnd 
 |-  ( ph -> X e. CC )
13 3 zcnd 
 |-  ( ph -> N e. CC )
14 2 recnd 
 |-  ( ph -> T e. CC )
15 13 14 mulcld 
 |-  ( ph -> ( N x. T ) e. CC )
16 12 15 subnegd 
 |-  ( ph -> ( X - -u ( N x. T ) ) = ( X + ( N x. T ) ) )
17 13 14 mulneg1d 
 |-  ( ph -> ( -u N x. T ) = -u ( N x. T ) )
18 17 eqcomd 
 |-  ( ph -> -u ( N x. T ) = ( -u N x. T ) )
19 18 oveq2d 
 |-  ( ph -> ( X - -u ( N x. T ) ) = ( X - ( -u N x. T ) ) )
20 16 19 eqtr3d 
 |-  ( ph -> ( X + ( N x. T ) ) = ( X - ( -u N x. T ) ) )
21 20 fveq2d 
 |-  ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` ( X - ( -u N x. T ) ) ) )
22 21 adantr 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( F ` ( X + ( N x. T ) ) ) = ( F ` ( X - ( -u N x. T ) ) ) )
23 1 adantr 
 |-  ( ( ph /\ -. N e. NN0 ) -> F : RR --> CC )
24 2 adantr 
 |-  ( ( ph /\ -. N e. NN0 ) -> T e. RR )
25 znnn0nn 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> -u N e. NN )
26 3 25 sylan 
 |-  ( ( ph /\ -. N e. NN0 ) -> -u N e. NN )
27 26 nnnn0d 
 |-  ( ( ph /\ -. N e. NN0 ) -> -u N e. NN0 )
28 4 adantr 
 |-  ( ( ph /\ -. N e. NN0 ) -> X e. RR )
29 3 adantr 
 |-  ( ( ph /\ -. N e. NN0 ) -> N e. ZZ )
30 29 zred 
 |-  ( ( ph /\ -. N e. NN0 ) -> N e. RR )
31 30 renegcld 
 |-  ( ( ph /\ -. N e. NN0 ) -> -u N e. RR )
32 31 24 remulcld 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( -u N x. T ) e. RR )
33 28 32 resubcld 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( X - ( -u N x. T ) ) e. RR )
34 5 adantlr 
 |-  ( ( ( ph /\ -. N e. NN0 ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
35 23 24 27 33 34 fperiodmullem 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( F ` ( ( X - ( -u N x. T ) ) + ( -u N x. T ) ) ) = ( F ` ( X - ( -u N x. T ) ) ) )
36 28 recnd 
 |-  ( ( ph /\ -. N e. NN0 ) -> X e. CC )
37 30 recnd 
 |-  ( ( ph /\ -. N e. NN0 ) -> N e. CC )
38 37 negcld 
 |-  ( ( ph /\ -. N e. NN0 ) -> -u N e. CC )
39 24 recnd 
 |-  ( ( ph /\ -. N e. NN0 ) -> T e. CC )
40 38 39 mulcld 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( -u N x. T ) e. CC )
41 36 40 npcand 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( ( X - ( -u N x. T ) ) + ( -u N x. T ) ) = X )
42 41 fveq2d 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( F ` ( ( X - ( -u N x. T ) ) + ( -u N x. T ) ) ) = ( F ` X ) )
43 22 35 42 3eqtr2d 
 |-  ( ( ph /\ -. N e. NN0 ) -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )
44 11 43 pm2.61dan 
 |-  ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )