Step | Hyp | Ref
| Expression |
1 | | 1zzd 12535 |
. . . 4
β’ ((π β§ π‘ β π) β 1 β β€) |
2 | | fmuldfeq.8 |
. . . . . 6
β’ (π β π β β) |
3 | 2 | nnzd 12527 |
. . . . 5
β’ (π β π β β€) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β π β β€) |
5 | 2 | nnge1d 12202 |
. . . . 5
β’ (π β 1 β€ π) |
6 | 5 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β 1 β€ π) |
7 | | nnre 12161 |
. . . . . 6
β’ (π β β β π β
β) |
8 | | leid 11252 |
. . . . . 6
β’ (π β β β π β€ π) |
9 | 2, 7, 8 | 3syl 18 |
. . . . 5
β’ (π β π β€ π) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β π β€ π) |
11 | 1, 4, 4, 6, 10 | elfzd 13433 |
. . 3
β’ ((π β§ π‘ β π) β π β (1...π)) |
12 | 2 | 3ad2ant1 1134 |
. . . 4
β’ ((π β§ π‘ β π β§ π β (1...π)) β π β β) |
13 | | eleq1 2826 |
. . . . . . 7
β’ (π = 1 β (π β (1...π) β 1 β (1...π))) |
14 | 13 | 3anbi3d 1443 |
. . . . . 6
β’ (π = 1 β ((π β§ π‘ β π β§ π β (1...π)) β (π β§ π‘ β π β§ 1 β (1...π)))) |
15 | | fveq2 6843 |
. . . . . . . 8
β’ (π = 1 β (seq1(π, π)βπ) = (seq1(π, π)β1)) |
16 | 15 | fveq1d 6845 |
. . . . . . 7
β’ (π = 1 β ((seq1(π, π)βπ)βπ‘) = ((seq1(π, π)β1)βπ‘)) |
17 | | fveq2 6843 |
. . . . . . 7
β’ (π = 1 β (seq1( Β· ,
(πΉβπ‘))βπ) = (seq1( Β· , (πΉβπ‘))β1)) |
18 | 16, 17 | eqeq12d 2753 |
. . . . . 6
β’ (π = 1 β (((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ) β ((seq1(π, π)β1)βπ‘) = (seq1( Β· , (πΉβπ‘))β1))) |
19 | 14, 18 | imbi12d 345 |
. . . . 5
β’ (π = 1 β (((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β ((π β§ π‘ β π β§ 1 β (1...π)) β ((seq1(π, π)β1)βπ‘) = (seq1( Β· , (πΉβπ‘))β1)))) |
20 | | eleq1 2826 |
. . . . . . 7
β’ (π = π β (π β (1...π) β π β (1...π))) |
21 | 20 | 3anbi3d 1443 |
. . . . . 6
β’ (π = π β ((π β§ π‘ β π β§ π β (1...π)) β (π β§ π‘ β π β§ π β (1...π)))) |
22 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (seq1(π, π)βπ) = (seq1(π, π)βπ)) |
23 | 22 | fveq1d 6845 |
. . . . . . 7
β’ (π = π β ((seq1(π, π)βπ)βπ‘) = ((seq1(π, π)βπ)βπ‘)) |
24 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (seq1( Β· , (πΉβπ‘))βπ) = (seq1( Β· , (πΉβπ‘))βπ)) |
25 | 23, 24 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β (((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
26 | 21, 25 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)))) |
27 | | eleq1 2826 |
. . . . . . 7
β’ (π = (π + 1) β (π β (1...π) β (π + 1) β (1...π))) |
28 | 27 | 3anbi3d 1443 |
. . . . . 6
β’ (π = (π + 1) β ((π β§ π‘ β π β§ π β (1...π)) β (π β§ π‘ β π β§ (π + 1) β (1...π)))) |
29 | | fveq2 6843 |
. . . . . . . 8
β’ (π = (π + 1) β (seq1(π, π)βπ) = (seq1(π, π)β(π + 1))) |
30 | 29 | fveq1d 6845 |
. . . . . . 7
β’ (π = (π + 1) β ((seq1(π, π)βπ)βπ‘) = ((seq1(π, π)β(π + 1))βπ‘)) |
31 | | fveq2 6843 |
. . . . . . 7
β’ (π = (π + 1) β (seq1( Β· , (πΉβπ‘))βπ) = (seq1( Β· , (πΉβπ‘))β(π + 1))) |
32 | 30, 31 | eqeq12d 2753 |
. . . . . 6
β’ (π = (π + 1) β (((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1)))) |
33 | 28, 32 | imbi12d 345 |
. . . . 5
β’ (π = (π + 1) β (((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β ((π β§ π‘ β π β§ (π + 1) β (1...π)) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))))) |
34 | | eleq1 2826 |
. . . . . . 7
β’ (π = π β (π β (1...π) β π β (1...π))) |
35 | 34 | 3anbi3d 1443 |
. . . . . 6
β’ (π = π β ((π β§ π‘ β π β§ π β (1...π)) β (π β§ π‘ β π β§ π β (1...π)))) |
36 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (seq1(π, π)βπ) = (seq1(π, π)βπ)) |
37 | 36 | fveq1d 6845 |
. . . . . . 7
β’ (π = π β ((seq1(π, π)βπ)βπ‘) = ((seq1(π, π)βπ)βπ‘)) |
38 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (seq1( Β· , (πΉβπ‘))βπ) = (seq1( Β· , (πΉβπ‘))βπ)) |
39 | 37, 38 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β (((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
40 | 35, 39 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)))) |
41 | | 1z 12534 |
. . . . . . . 8
β’ 1 β
β€ |
42 | | seq1 13920 |
. . . . . . . 8
β’ (1 β
β€ β (seq1( Β· , (πΉβπ‘))β1) = ((πΉβπ‘)β1)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
β’ (seq1(
Β· , (πΉβπ‘))β1) = ((πΉβπ‘)β1) |
44 | | 1zzd 12535 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
45 | | 1le1 11784 |
. . . . . . . . . . . . 13
β’ 1 β€
1 |
46 | 45 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 1 β€ 1) |
47 | 44, 3, 44, 46, 5 | elfzd 13433 |
. . . . . . . . . . 11
β’ (π β 1 β (1...π)) |
48 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π π‘ β π |
49 | | fmuldfeq.5 |
. . . . . . . . . . . . . . . . 17
β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
50 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ |
51 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π β (1...π) β¦ ((πβπ)βπ‘)) |
52 | 50, 51 | nfmpt 5213 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
53 | 49, 52 | nfcxfr 2906 |
. . . . . . . . . . . . . . . 16
β’
β²ππΉ |
54 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²ππ‘ |
55 | 53, 54 | nffv 6853 |
. . . . . . . . . . . . . . 15
β’
β²π(πΉβπ‘) |
56 | | nfcv 2908 |
. . . . . . . . . . . . . . 15
β’
β²π1 |
57 | 55, 56 | nffv 6853 |
. . . . . . . . . . . . . 14
β’
β²π((πΉβπ‘)β1) |
58 | | nffvmpt1 6854 |
. . . . . . . . . . . . . 14
β’
β²π((π β (1...π) β¦ ((πβπ)βπ‘))β1) |
59 | 57, 58 | nfeq 2921 |
. . . . . . . . . . . . 13
β’
β²π((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1) |
60 | 48, 59 | nfim 1900 |
. . . . . . . . . . . 12
β’
β²π(π‘ β π β ((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1)) |
61 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ((πΉβπ‘)βπ) = ((πΉβπ‘)β1)) |
62 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1)) |
63 | 61, 62 | eqeq12d 2753 |
. . . . . . . . . . . . 13
β’ (π = 1 β (((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) β ((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1))) |
64 | 63 | imbi2d 341 |
. . . . . . . . . . . 12
β’ (π = 1 β ((π‘ β π β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) β (π‘ β π β ((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1)))) |
65 | | ovex 7391 |
. . . . . . . . . . . . . . 15
β’
(1...π) β
V |
66 | 65 | mptex 7174 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) β V |
67 | 49 | fvmpt2 6960 |
. . . . . . . . . . . . . 14
β’ ((π‘ β π β§ (π β (1...π) β¦ ((πβπ)βπ‘)) β V) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
68 | 66, 67 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (π‘ β π β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
69 | 68 | fveq1d 6845 |
. . . . . . . . . . . 12
β’ (π‘ β π β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) |
70 | 60, 64, 69 | vtoclg1f 3525 |
. . . . . . . . . . 11
β’ (1 β
(1...π) β (π‘ β π β ((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1))) |
71 | 47, 70 | syl 17 |
. . . . . . . . . 10
β’ (π β (π‘ β π β ((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1))) |
72 | 71 | imp 408 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((πΉβπ‘)β1) = ((π β (1...π) β¦ ((πβπ)βπ‘))β1)) |
73 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) = (π β (1...π) β¦ ((πβπ)βπ‘)) |
74 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = 1 β (πβπ) = (πβ1)) |
75 | 74 | fveq1d 6845 |
. . . . . . . . . 10
β’ (π = 1 β ((πβπ)βπ‘) = ((πβ1)βπ‘)) |
76 | 47 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β 1 β (1...π)) |
77 | | fmuldfeq.9 |
. . . . . . . . . . . . 13
β’ (π β π:(1...π)βΆπ) |
78 | 77, 47 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ (π β (πβ1) β π) |
79 | 78 | ancli 550 |
. . . . . . . . . . . 12
β’ (π β (π β§ (πβ1) β π)) |
80 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ1) β (π β π β (πβ1) β π)) |
81 | 80 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π = (πβ1) β ((π β§ π β π) β (π β§ (πβ1) β π))) |
82 | | feq1 6650 |
. . . . . . . . . . . . . 14
β’ (π = (πβ1) β (π:πβΆβ β (πβ1):πβΆβ)) |
83 | 81, 82 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = (πβ1) β (((π β§ π β π) β π:πβΆβ) β ((π β§ (πβ1) β π) β (πβ1):πβΆβ))) |
84 | | fmuldfeq.10 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π:πβΆβ) |
85 | 84 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β§ π β π) β π:πβΆβ)) |
86 | 83, 85 | vtoclga 3535 |
. . . . . . . . . . . 12
β’ ((πβ1) β π β ((π β§ (πβ1) β π) β (πβ1):πβΆβ)) |
87 | 78, 79, 86 | sylc 65 |
. . . . . . . . . . 11
β’ (π β (πβ1):πβΆβ) |
88 | 87 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β ((πβ1)βπ‘) β β) |
89 | 73, 75, 76, 88 | fvmptd3 6972 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((π β (1...π) β¦ ((πβπ)βπ‘))β1) = ((πβ1)βπ‘)) |
90 | 72, 89 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β ((πΉβπ‘)β1) = ((πβ1)βπ‘)) |
91 | | seq1 13920 |
. . . . . . . . . 10
β’ (1 β
β€ β (seq1(π,
π)β1) = (πβ1)) |
92 | 41, 91 | ax-mp 5 |
. . . . . . . . 9
β’
(seq1(π, π)β1) = (πβ1) |
93 | 92 | fveq1i 6844 |
. . . . . . . 8
β’
((seq1(π, π)β1)βπ‘) = ((πβ1)βπ‘) |
94 | 90, 93 | eqtr4di 2795 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((πΉβπ‘)β1) = ((seq1(π, π)β1)βπ‘)) |
95 | 43, 94 | eqtr2id 2790 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((seq1(π, π)β1)βπ‘) = (seq1( Β· , (πΉβπ‘))β1)) |
96 | 95 | 3adant3 1133 |
. . . . 5
β’ ((π β§ π‘ β π β§ 1 β (1...π)) β ((seq1(π, π)β1)βπ‘) = (seq1( Β· , (πΉβπ‘))β1)) |
97 | | simp31 1210 |
. . . . . . 7
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β π) |
98 | | simp1 1137 |
. . . . . . . . . 10
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β π β β) |
99 | | simp33 1212 |
. . . . . . . . . 10
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β (π + 1) β (1...π)) |
100 | 98, 99 | jca 513 |
. . . . . . . . 9
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β (π β β β§ (π + 1) β (1...π))) |
101 | | elnnuz 12808 |
. . . . . . . . . . 11
β’ (π β β β π β
(β€β₯β1)) |
102 | 101 | biimpi 215 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β1)) |
103 | 102 | anim1i 616 |
. . . . . . . . 9
β’ ((π β β β§ (π + 1) β (1...π)) β (π β (β€β₯β1)
β§ (π + 1) β
(1...π))) |
104 | | peano2fzr 13455 |
. . . . . . . . 9
β’ ((π β
(β€β₯β1) β§ (π + 1) β (1...π)) β π β (1...π)) |
105 | 100, 103,
104 | 3syl 18 |
. . . . . . . 8
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β π β (1...π)) |
106 | | simp32 1211 |
. . . . . . . . 9
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β π‘ β π) |
107 | | simp2 1138 |
. . . . . . . . 9
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
108 | 97, 106, 105, 107 | mp3and 1465 |
. . . . . . . 8
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
109 | 105, 99, 108 | 3jca 1129 |
. . . . . . 7
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
110 | | nfv 1918 |
. . . . . . . . 9
β’
β²ππ |
111 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π β (1...π) |
112 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π + 1) β (1...π) |
113 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π1 |
114 | | fmuldfeq.3 |
. . . . . . . . . . . . . . 15
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
115 | | nfmpo1 7438 |
. . . . . . . . . . . . . . 15
β’
β²π(π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
116 | 114, 115 | nfcxfr 2906 |
. . . . . . . . . . . . . 14
β’
β²ππ |
117 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²ππ |
118 | 113, 116,
117 | nfseq 13917 |
. . . . . . . . . . . . 13
β’
β²πseq1(π, π) |
119 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²ππ |
120 | 118, 119 | nffv 6853 |
. . . . . . . . . . . 12
β’
β²π(seq1(π, π)βπ) |
121 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²ππ‘ |
122 | 120, 121 | nffv 6853 |
. . . . . . . . . . 11
β’
β²π((seq1(π, π)βπ)βπ‘) |
123 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π(seq1( Β· , (πΉβπ‘))βπ) |
124 | 122, 123 | nfeq 2921 |
. . . . . . . . . 10
β’
β²π((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ) |
125 | 111, 112,
124 | nf3an 1905 |
. . . . . . . . 9
β’
β²π(π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
126 | 110, 125 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
127 | | nfv 1918 |
. . . . . . . . 9
β’
β²ππ |
128 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π β (1...π) |
129 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π + 1) β (1...π) |
130 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π1 |
131 | | nfmpo2 7439 |
. . . . . . . . . . . . . . 15
β’
β²π(π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
132 | 114, 131 | nfcxfr 2906 |
. . . . . . . . . . . . . 14
β’
β²ππ |
133 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²ππ |
134 | 130, 132,
133 | nfseq 13917 |
. . . . . . . . . . . . 13
β’
β²πseq1(π, π) |
135 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²ππ |
136 | 134, 135 | nffv 6853 |
. . . . . . . . . . . 12
β’
β²π(seq1(π, π)βπ) |
137 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²ππ‘ |
138 | 136, 137 | nffv 6853 |
. . . . . . . . . . 11
β’
β²π((seq1(π, π)βπ)βπ‘) |
139 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π(seq1( Β· , (πΉβπ‘))βπ) |
140 | 138, 139 | nfeq 2921 |
. . . . . . . . . 10
β’
β²π((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ) |
141 | 128, 129,
140 | nf3an 1905 |
. . . . . . . . 9
β’
β²π(π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
142 | 127, 141 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
143 | | fmuldfeq.2 |
. . . . . . . 8
β’
β²π‘π |
144 | | fmuldfeq.7 |
. . . . . . . . 9
β’ (π β π β V) |
145 | 144 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β π β V) |
146 | 77 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β π:(1...π)βΆπ) |
147 | | fmuldfeq.11 |
. . . . . . . . 9
β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
148 | 147 | 3adant1r 1178 |
. . . . . . . 8
β’ (((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
149 | | simpr1 1195 |
. . . . . . . 8
β’ ((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β π β (1...π)) |
150 | | simpr2 1196 |
. . . . . . . 8
β’ ((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β (π + 1) β (1...π)) |
151 | | simpr3 1197 |
. . . . . . . 8
β’ ((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
152 | 84 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β§ π β π) β π:πβΆβ) |
153 | 126, 142,
143, 114, 49, 145, 146, 148, 149, 150, 151, 152 | fmuldfeqlem1 43830 |
. . . . . . 7
β’ (((π β§ (π β (1...π) β§ (π + 1) β (1...π) β§ ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) |
154 | 97, 109, 106, 153 | syl21anc 837 |
. . . . . 6
β’ ((π β β β§ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β§ (π β§ π‘ β π β§ (π + 1) β (1...π))) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) |
155 | 154 | 3exp 1120 |
. . . . 5
β’ (π β β β (((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) β ((π β§ π‘ β π β§ (π + 1) β (1...π)) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))))) |
156 | 19, 26, 33, 40, 96, 155 | nnind 12172 |
. . . 4
β’ (π β β β ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ))) |
157 | 12, 156 | mpcom 38 |
. . 3
β’ ((π β§ π‘ β π β§ π β (1...π)) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
158 | 11, 157 | mpd3an3 1463 |
. 2
β’ ((π β§ π‘ β π) β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
159 | | fmuldfeq.4 |
. . . 4
β’ π = (seq1(π, π)βπ) |
160 | 159 | fveq1i 6844 |
. . 3
β’ (πβπ‘) = ((seq1(π, π)βπ)βπ‘) |
161 | 160 | a1i 11 |
. 2
β’ ((π β§ π‘ β π) β (πβπ‘) = ((seq1(π, π)βπ)βπ‘)) |
162 | | simpr 486 |
. . 3
β’ ((π β§ π‘ β π) β π‘ β π) |
163 | | elnnuz 12808 |
. . . . . 6
β’ (π β β β π β
(β€β₯β1)) |
164 | 2, 163 | sylib 217 |
. . . . 5
β’ (π β π β
(β€β₯β1)) |
165 | 164 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β π β
(β€β₯β1)) |
166 | | fmuldfeq.1 |
. . . . . . . 8
β’
β²ππ |
167 | 166, 48 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π‘ β π) |
168 | | nfv 1918 |
. . . . . . 7
β’
β²π π β (1...π) |
169 | 167, 168 | nfan 1903 |
. . . . . 6
β’
β²π((π β§ π‘ β π) β§ π β (1...π)) |
170 | | nfcv 2908 |
. . . . . . . 8
β’
β²ππ |
171 | 55, 170 | nffv 6853 |
. . . . . . 7
β’
β²π((πΉβπ‘)βπ) |
172 | 171 | nfel1 2924 |
. . . . . 6
β’
β²π((πΉβπ‘)βπ) β β |
173 | 169, 172 | nfim 1900 |
. . . . 5
β’
β²π(((π β§ π‘ β π) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
174 | | eleq1 2826 |
. . . . . . 7
β’ (π = π β (π β (1...π) β π β (1...π))) |
175 | 174 | anbi2d 630 |
. . . . . 6
β’ (π = π β (((π β§ π‘ β π) β§ π β (1...π)) β ((π β§ π‘ β π) β§ π β (1...π)))) |
176 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
177 | 176 | eleq1d 2823 |
. . . . . 6
β’ (π = π β (((πΉβπ‘)βπ) β β β ((πΉβπ‘)βπ) β β)) |
178 | 175, 177 | imbi12d 345 |
. . . . 5
β’ (π = π β ((((π β§ π‘ β π) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) β (((π β§ π‘ β π) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β))) |
179 | 69 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πΉβπ‘)βπ) = ((π β (1...π) β¦ ((πβπ)βπ‘))βπ)) |
180 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π‘ β π) β§ π β (1...π)) β π β (1...π)) |
181 | 77 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πβπ) β π) |
182 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β π) |
183 | 182, 181 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (π β§ (πβπ) β π)) |
184 | | eleq1 2826 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (π β π β (πβπ) β π)) |
185 | 184 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β§ π β π) β (π β§ (πβπ) β π))) |
186 | | feq1 6650 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β (π:πβΆβ β (πβπ):πβΆβ)) |
187 | 185, 186 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (((π β§ π β π) β π:πβΆβ) β ((π β§ (πβπ) β π) β (πβπ):πβΆβ))) |
188 | 187, 85 | vtoclga 3535 |
. . . . . . . . . . 11
β’ ((πβπ) β π β ((π β§ (πβπ) β π) β (πβπ):πβΆβ)) |
189 | 181, 183,
188 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πβπ):πβΆβ) |
190 | 189 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ π β (1...π)) β (πβπ):πβΆβ) |
191 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ π β (1...π)) β π‘ β π) |
192 | 190, 191 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πβπ)βπ‘) β β) |
193 | 73 | fvmpt2 6960 |
. . . . . . . 8
β’ ((π β (1...π) β§ ((πβπ)βπ‘) β β) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((πβπ)βπ‘)) |
194 | 180, 192,
193 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) = ((πβπ)βπ‘)) |
195 | 194, 192 | eqeltrd 2838 |
. . . . . 6
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((π β (1...π) β¦ ((πβπ)βπ‘))βπ) β β) |
196 | 179, 195 | eqeltrd 2838 |
. . . . 5
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
197 | 173, 178,
196 | chvarfv 2234 |
. . . 4
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πΉβπ‘)βπ) β β) |
198 | | remulcl 11137 |
. . . . 5
β’ ((π β β β§ π β β) β (π Β· π) β β) |
199 | 198 | adantl 483 |
. . . 4
β’ (((π β§ π‘ β π) β§ (π β β β§ π β β)) β (π Β· π) β β) |
200 | 165, 197,
199 | seqcl 13929 |
. . 3
β’ ((π β§ π‘ β π) β (seq1( Β· , (πΉβπ‘))βπ) β β) |
201 | | fmuldfeq.6 |
. . . 4
β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) |
202 | 201 | fvmpt2 6960 |
. . 3
β’ ((π‘ β π β§ (seq1( Β· , (πΉβπ‘))βπ) β β) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
203 | 162, 200,
202 | syl2anc 585 |
. 2
β’ ((π β§ π‘ β π) β (πβπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
204 | 158, 161,
203 | 3eqtr4d 2787 |
1
β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) |