Step | Hyp | Ref
| Expression |
1 | | prodfn0.1 |
. . 3
|
2 | | eluzfz2 12349 |
. . 3
|
3 | 1, 2 | syl 17 |
. 2
|
4 | | fveq2 6191 |
. . . . 5
|
5 | | fveq2 6191 |
. . . . . 6
|
6 | 5 | oveq2d 6666 |
. . . . 5
|
7 | 4, 6 | eqeq12d 2637 |
. . . 4
|
8 | 7 | imbi2d 330 |
. . 3
|
9 | | fveq2 6191 |
. . . . 5
|
10 | | fveq2 6191 |
. . . . . 6
|
11 | 10 | oveq2d 6666 |
. . . . 5
|
12 | 9, 11 | eqeq12d 2637 |
. . . 4
|
13 | 12 | imbi2d 330 |
. . 3
|
14 | | fveq2 6191 |
. . . . 5
|
15 | | fveq2 6191 |
. . . . . 6
|
16 | 15 | oveq2d 6666 |
. . . . 5
|
17 | 14, 16 | eqeq12d 2637 |
. . . 4
|
18 | 17 | imbi2d 330 |
. . 3
|
19 | | fveq2 6191 |
. . . . 5
|
20 | | fveq2 6191 |
. . . . . 6
|
21 | 20 | oveq2d 6666 |
. . . . 5
|
22 | 19, 21 | eqeq12d 2637 |
. . . 4
|
23 | 22 | imbi2d 330 |
. . 3
|
24 | | eluzfz1 12348 |
. . . . . . 7
|
25 | 1, 24 | syl 17 |
. . . . . 6
|
26 | | fveq2 6191 |
. . . . . . . . 9
|
27 | | fveq2 6191 |
. . . . . . . . . 10
|
28 | 27 | oveq2d 6666 |
. . . . . . . . 9
|
29 | 26, 28 | eqeq12d 2637 |
. . . . . . . 8
|
30 | 29 | imbi2d 330 |
. . . . . . 7
|
31 | | prodfrec.4 |
. . . . . . . 8
|
32 | 31 | expcom 451 |
. . . . . . 7
|
33 | 30, 32 | vtoclga 3272 |
. . . . . 6
|
34 | 25, 33 | mpcom 38 |
. . . . 5
|
35 | | eluzel2 11692 |
. . . . . . 7
|
36 | 1, 35 | syl 17 |
. . . . . 6
|
37 | | seq1 12814 |
. . . . . 6
|
38 | 36, 37 | syl 17 |
. . . . 5
|
39 | | seq1 12814 |
. . . . . . 7
|
40 | 36, 39 | syl 17 |
. . . . . 6
|
41 | 40 | oveq2d 6666 |
. . . . 5
|
42 | 34, 38, 41 | 3eqtr4d 2666 |
. . . 4
|
43 | 42 | a1i 11 |
. . 3
|
44 | | oveq1 6657 |
. . . . . . . . 9
|
45 | 44 | 3ad2ant3 1084 |
. . . . . . . 8
..^ |
46 | | fzofzp1 12565 |
. . . . . . . . . . . . 13
..^
|
47 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
49 | 48 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
50 | 47, 49 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
|
51 | 50 | imbi2d 330 |
. . . . . . . . . . . . . 14
|
52 | 51, 32 | vtoclga 3272 |
. . . . . . . . . . . . 13
|
53 | 46, 52 | syl 17 |
. . . . . . . . . . . 12
..^
|
54 | 53 | impcom 446 |
. . . . . . . . . . 11
..^
|
55 | 54 | oveq2d 6666 |
. . . . . . . . . 10
..^
|
56 | | 1cnd 10056 |
. . . . . . . . . . . 12
..^ |
57 | | elfzouz 12474 |
. . . . . . . . . . . . . 14
..^
|
58 | 57 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
59 | | elfzouz2 12484 |
. . . . . . . . . . . . . . . . 17
..^
|
60 | | fzss2 12381 |
. . . . . . . . . . . . . . . . 17
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
..^
|
62 | 61 | sselda 3603 |
. . . . . . . . . . . . . . 15
..^ |
63 | | prodfn0.2 |
. . . . . . . . . . . . . . 15
|
64 | 62, 63 | sylan2 491 |
. . . . . . . . . . . . . 14
..^ |
65 | 64 | anassrs 680 |
. . . . . . . . . . . . 13
..^ |
66 | | mulcl 10020 |
. . . . . . . . . . . . . 14
|
67 | 66 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
68 | 58, 65, 67 | seqcl 12821 |
. . . . . . . . . . . 12
..^ |
69 | 48 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | imbi2d 330 |
. . . . . . . . . . . . . . 15
|
71 | 63 | expcom 451 |
. . . . . . . . . . . . . . 15
|
72 | 70, 71 | vtoclga 3272 |
. . . . . . . . . . . . . 14
|
73 | 46, 72 | syl 17 |
. . . . . . . . . . . . 13
..^
|
74 | 73 | impcom 446 |
. . . . . . . . . . . 12
..^
|
75 | | prodfn0.3 |
. . . . . . . . . . . . . . 15
|
76 | 62, 75 | sylan2 491 |
. . . . . . . . . . . . . 14
..^ |
77 | 76 | anassrs 680 |
. . . . . . . . . . . . 13
..^ |
78 | 58, 65, 77 | prodfn0 14626 |
. . . . . . . . . . . 12
..^ |
79 | 48 | neeq1d 2853 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | imbi2d 330 |
. . . . . . . . . . . . . . 15
|
81 | 75 | expcom 451 |
. . . . . . . . . . . . . . 15
|
82 | 80, 81 | vtoclga 3272 |
. . . . . . . . . . . . . 14
|
83 | 46, 82 | syl 17 |
. . . . . . . . . . . . 13
..^
|
84 | 83 | impcom 446 |
. . . . . . . . . . . 12
..^
|
85 | 56, 68, 56, 74, 78, 84 | divmuldivd 10842 |
. . . . . . . . . . 11
..^
|
86 | | 1t1e1 11175 |
. . . . . . . . . . . 12
|
87 | 86 | oveq1i 6660 |
. . . . . . . . . . 11
|
88 | 85, 87 | syl6eq 2672 |
. . . . . . . . . 10
..^
|
89 | 55, 88 | eqtrd 2656 |
. . . . . . . . 9
..^ |
90 | 89 | 3adant3 1081 |
. . . . . . . 8
..^ |
91 | 45, 90 | eqtrd 2656 |
. . . . . . 7
..^ |
92 | | seqp1 12816 |
. . . . . . . . 9
|
93 | 57, 92 | syl 17 |
. . . . . . . 8
..^
|
94 | 93 | 3ad2ant2 1083 |
. . . . . . 7
..^
|
95 | | seqp1 12816 |
. . . . . . . . . 10
|
96 | 57, 95 | syl 17 |
. . . . . . . . 9
..^
|
97 | 96 | oveq2d 6666 |
. . . . . . . 8
..^
|
98 | 97 | 3ad2ant2 1083 |
. . . . . . 7
..^ |
99 | 91, 94, 98 | 3eqtr4d 2666 |
. . . . . 6
..^
|
100 | 99 | 3exp 1264 |
. . . . 5
..^
|
101 | 100 | com12 32 |
. . . 4
..^
|
102 | 101 | a2d 29 |
. . 3
..^
|
103 | 8, 13, 18, 23, 43, 102 | fzind2 12586 |
. 2
|
104 | 3, 103 | mpcom 38 |
1
|