Step | Hyp | Ref
| Expression |
1 | | iprodefisumlem.1 |
. . . 4
β’ π =
(β€β₯βπ) |
2 | | iprodefisumlem.2 |
. . . 4
β’ (π β π β β€) |
3 | | iprodefisumlem.3 |
. . . . . 6
β’ (π β πΉ:πβΆβ) |
4 | | fvco3 6960 |
. . . . . 6
β’ ((πΉ:πβΆβ β§ π β π) β ((exp β πΉ)βπ) = (expβ(πΉβπ))) |
5 | 3, 4 | sylan 580 |
. . . . 5
β’ ((π β§ π β π) β ((exp β πΉ)βπ) = (expβ(πΉβπ))) |
6 | 3 | ffvelcdmda 7055 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
7 | | efcl 15991 |
. . . . . 6
β’ ((πΉβπ) β β β (expβ(πΉβπ)) β β) |
8 | 6, 7 | syl 17 |
. . . . 5
β’ ((π β§ π β π) β (expβ(πΉβπ)) β β) |
9 | 5, 8 | eqeltrd 2832 |
. . . 4
β’ ((π β§ π β π) β ((exp β πΉ)βπ) β β) |
10 | 1, 2, 9 | prodf 15798 |
. . 3
β’ (π β seqπ( Β· , (exp β πΉ)):πβΆβ) |
11 | 10 | ffnd 6689 |
. 2
β’ (π β seqπ( Β· , (exp β πΉ)) Fn π) |
12 | | eff 15990 |
. . . 4
β’
exp:ββΆβ |
13 | | ffn 6688 |
. . . 4
β’
(exp:ββΆβ β exp Fn β) |
14 | 12, 13 | ax-mp 5 |
. . 3
β’ exp Fn
β |
15 | 1, 2, 6 | serf 13961 |
. . 3
β’ (π β seqπ( + , πΉ):πβΆβ) |
16 | | fnfco 6727 |
. . 3
β’ ((exp Fn
β β§ seqπ( + ,
πΉ):πβΆβ) β (exp β
seqπ( + , πΉ)) Fn π) |
17 | 14, 15, 16 | sylancr 587 |
. 2
β’ (π β (exp β seqπ( + , πΉ)) Fn π) |
18 | | fveq2 6862 |
. . . . . . . 8
β’ (π = π β (seqπ( Β· , (exp β πΉ))βπ) = (seqπ( Β· , (exp β πΉ))βπ)) |
19 | | 2fveq3 6867 |
. . . . . . . 8
β’ (π = π β (expβ(seqπ( + , πΉ)βπ)) = (expβ(seqπ( + , πΉ)βπ))) |
20 | 18, 19 | eqeq12d 2747 |
. . . . . . 7
β’ (π = π β ((seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)) β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)))) |
21 | 20 | imbi2d 340 |
. . . . . 6
β’ (π = π β ((π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))))) |
22 | | fveq2 6862 |
. . . . . . . 8
β’ (π = π β (seqπ( Β· , (exp β πΉ))βπ) = (seqπ( Β· , (exp β πΉ))βπ)) |
23 | | 2fveq3 6867 |
. . . . . . . 8
β’ (π = π β (expβ(seqπ( + , πΉ)βπ)) = (expβ(seqπ( + , πΉ)βπ))) |
24 | 22, 23 | eqeq12d 2747 |
. . . . . . 7
β’ (π = π β ((seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)) β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)))) |
25 | 24 | imbi2d 340 |
. . . . . 6
β’ (π = π β ((π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))))) |
26 | | fveq2 6862 |
. . . . . . . 8
β’ (π = (π + 1) β (seqπ( Β· , (exp β πΉ))βπ) = (seqπ( Β· , (exp β πΉ))β(π + 1))) |
27 | | 2fveq3 6867 |
. . . . . . . 8
β’ (π = (π + 1) β (expβ(seqπ( + , πΉ)βπ)) = (expβ(seqπ( + , πΉ)β(π + 1)))) |
28 | 26, 27 | eqeq12d 2747 |
. . . . . . 7
β’ (π = (π + 1) β ((seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)) β (seqπ( Β· , (exp β πΉ))β(π + 1)) = (expβ(seqπ( + , πΉ)β(π + 1))))) |
29 | 28 | imbi2d 340 |
. . . . . 6
β’ (π = (π + 1) β ((π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (π β (seqπ( Β· , (exp β πΉ))β(π + 1)) = (expβ(seqπ( + , πΉ)β(π + 1)))))) |
30 | | fveq2 6862 |
. . . . . . . 8
β’ (π = π β (seqπ( Β· , (exp β πΉ))βπ) = (seqπ( Β· , (exp β πΉ))βπ)) |
31 | | 2fveq3 6867 |
. . . . . . . 8
β’ (π = π β (expβ(seqπ( + , πΉ)βπ)) = (expβ(seqπ( + , πΉ)βπ))) |
32 | 30, 31 | eqeq12d 2747 |
. . . . . . 7
β’ (π = π β ((seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)) β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)))) |
33 | 32 | imbi2d 340 |
. . . . . 6
β’ (π = π β ((π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))))) |
34 | | uzid 12802 |
. . . . . . . . . . 11
β’ (π β β€ β π β
(β€β₯βπ)) |
35 | 2, 34 | syl 17 |
. . . . . . . . . 10
β’ (π β π β (β€β₯βπ)) |
36 | 35, 1 | eleqtrrdi 2843 |
. . . . . . . . 9
β’ (π β π β π) |
37 | | fvco3 6960 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β π) β ((exp β πΉ)βπ) = (expβ(πΉβπ))) |
38 | 3, 36, 37 | syl2anc 584 |
. . . . . . . 8
β’ (π β ((exp β πΉ)βπ) = (expβ(πΉβπ))) |
39 | | seq1 13944 |
. . . . . . . . 9
β’ (π β β€ β (seqπ( Β· , (exp β πΉ))βπ) = ((exp β πΉ)βπ)) |
40 | 2, 39 | syl 17 |
. . . . . . . 8
β’ (π β (seqπ( Β· , (exp β πΉ))βπ) = ((exp β πΉ)βπ)) |
41 | | seq1 13944 |
. . . . . . . . . 10
β’ (π β β€ β (seqπ( + , πΉ)βπ) = (πΉβπ)) |
42 | 2, 41 | syl 17 |
. . . . . . . . 9
β’ (π β (seqπ( + , πΉ)βπ) = (πΉβπ)) |
43 | 42 | fveq2d 6866 |
. . . . . . . 8
β’ (π β (expβ(seqπ( + , πΉ)βπ)) = (expβ(πΉβπ))) |
44 | 38, 40, 43 | 3eqtr4d 2781 |
. . . . . . 7
β’ (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) |
45 | 44 | a1i 11 |
. . . . . 6
β’ (π β β€ β (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)))) |
46 | | oveq1 7384 |
. . . . . . . . . . 11
β’
((seqπ( Β· ,
(exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)) β ((seqπ( Β· , (exp β πΉ))βπ) Β· ((exp β πΉ)β(π + 1))) = ((expβ(seqπ( + , πΉ)βπ)) Β· ((exp β πΉ)β(π + 1)))) |
47 | 46 | 3ad2ant3 1135 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π β§ (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β ((seqπ( Β· , (exp β πΉ))βπ) Β· ((exp β πΉ)β(π + 1))) = ((expβ(seqπ( + , πΉ)βπ)) Β· ((exp β πΉ)β(π + 1)))) |
48 | 3 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯βπ) β§ π) β πΉ:πβΆβ) |
49 | | peano2uz 12850 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
50 | 49, 1 | eleqtrrdi 2843 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (π + 1) β π) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯βπ) β§ π) β (π + 1) β π) |
52 | | fvco3 6960 |
. . . . . . . . . . . . . 14
β’ ((πΉ:πβΆβ β§ (π + 1) β π) β ((exp β πΉ)β(π + 1)) = (expβ(πΉβ(π + 1)))) |
53 | 48, 51, 52 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯βπ) β§ π) β ((exp β πΉ)β(π + 1)) = (expβ(πΉβ(π + 1)))) |
54 | 53 | oveq2d 7393 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯βπ) β§ π) β ((expβ(seqπ( + , πΉ)βπ)) Β· ((exp β πΉ)β(π + 1))) = ((expβ(seqπ( + , πΉ)βπ)) Β· (expβ(πΉβ(π + 1))))) |
55 | 15 | ffvelcdmda 7055 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
56 | 55 | expcom 414 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π β (seqπ( + , πΉ)βπ) β β)) |
57 | 1 | eqcomi 2740 |
. . . . . . . . . . . . . . 15
β’
(β€β₯βπ) = π |
58 | 56, 57 | eleq2s 2850 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β (π β (seqπ( + , πΉ)βπ) β β)) |
59 | 58 | imp 407 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯βπ) β§ π) β (seqπ( + , πΉ)βπ) β β) |
60 | 48, 51 | ffvelcdmd 7056 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯βπ) β§ π) β (πΉβ(π + 1)) β β) |
61 | | efadd 16002 |
. . . . . . . . . . . . 13
β’
(((seqπ( + , πΉ)βπ) β β β§ (πΉβ(π + 1)) β β) β
(expβ((seqπ( + ,
πΉ)βπ) + (πΉβ(π + 1)))) = ((expβ(seqπ( + , πΉ)βπ)) Β· (expβ(πΉβ(π + 1))))) |
62 | 59, 60, 61 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯βπ) β§ π) β (expβ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))) = ((expβ(seqπ( + , πΉ)βπ)) Β· (expβ(πΉβ(π + 1))))) |
63 | 54, 62 | eqtr4d 2774 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π) β ((expβ(seqπ( + , πΉ)βπ)) Β· ((exp β πΉ)β(π + 1))) = (expβ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1))))) |
64 | 63 | 3adant3 1132 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π β§ (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β ((expβ(seqπ( + , πΉ)βπ)) Β· ((exp β πΉ)β(π + 1))) = (expβ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1))))) |
65 | 47, 64 | eqtrd 2771 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β§ (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β ((seqπ( Β· , (exp β πΉ))βπ) Β· ((exp β πΉ)β(π + 1))) = (expβ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1))))) |
66 | | seqp1 13946 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β (seqπ( Β· , (exp β πΉ))β(π + 1)) = ((seqπ( Β· , (exp β πΉ))βπ) Β· ((exp β πΉ)β(π + 1)))) |
67 | 66 | adantr 481 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π) β (seqπ( Β· , (exp β πΉ))β(π + 1)) = ((seqπ( Β· , (exp β πΉ))βπ) Β· ((exp β πΉ)β(π + 1)))) |
68 | 67 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β§ (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (seqπ( Β· , (exp β πΉ))β(π + 1)) = ((seqπ( Β· , (exp β πΉ))βπ) Β· ((exp β πΉ)β(π + 1)))) |
69 | | seqp1 13946 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β (seqπ( + , πΉ)β(π + 1)) = ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))) |
70 | 69 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π) β (seqπ( + , πΉ)β(π + 1)) = ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))) |
71 | 70 | fveq2d 6866 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π) β (expβ(seqπ( + , πΉ)β(π + 1))) = (expβ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1))))) |
72 | 71 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β§ (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (expβ(seqπ( + , πΉ)β(π + 1))) = (expβ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1))))) |
73 | 65, 68, 72 | 3eqtr4d 2781 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ π β§ (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (seqπ( Β· , (exp β πΉ))β(π + 1)) = (expβ(seqπ( + , πΉ)β(π + 1)))) |
74 | 73 | 3exp 1119 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (π β ((seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)) β (seqπ( Β· , (exp β πΉ))β(π + 1)) = (expβ(seqπ( + , πΉ)β(π + 1)))))) |
75 | 74 | a2d 29 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) β (π β (seqπ( Β· , (exp β πΉ))β(π + 1)) = (expβ(seqπ( + , πΉ)β(π + 1)))))) |
76 | 21, 25, 29, 33, 45, 75 | uzind4 12855 |
. . . . 5
β’ (π β
(β€β₯βπ) β (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)))) |
77 | 76, 1 | eleq2s 2850 |
. . . 4
β’ (π β π β (π β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ)))) |
78 | 77 | impcom 408 |
. . 3
β’ ((π β§ π β π) β (seqπ( Β· , (exp β πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) |
79 | | fvco3 6960 |
. . . 4
β’
((seqπ( + , πΉ):πβΆβ β§ π β π) β ((exp β seqπ( + , πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) |
80 | 15, 79 | sylan 580 |
. . 3
β’ ((π β§ π β π) β ((exp β seqπ( + , πΉ))βπ) = (expβ(seqπ( + , πΉ)βπ))) |
81 | 78, 80 | eqtr4d 2774 |
. 2
β’ ((π β§ π β π) β (seqπ( Β· , (exp β πΉ))βπ) = ((exp β seqπ( + , πΉ))βπ)) |
82 | 11, 17, 81 | eqfnfvd 7005 |
1
β’ (π β seqπ( Β· , (exp β πΉ)) = (exp β seqπ( + , πΉ))) |