Step | Hyp | Ref
| Expression |
1 | | simpl2l 1226 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ ๐ด โ (๐ผโ๐)) |
2 | | fveecn 28025 |
. . . . 5
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
3 | 1, 2 | sylancom 588 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
4 | | simpl2r 1227 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ ๐ถ โ (๐ผโ๐)) |
5 | | fveecn 28025 |
. . . . 5
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
6 | 4, 5 | sylancom 588 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
7 | | elicc01 13425 |
. . . . . . . . 9
โข (๐ โ (0[,]1) โ (๐ โ โ โง 0 โค
๐ โง ๐ โค 1)) |
8 | 7 | simp1bi 1145 |
. . . . . . . 8
โข (๐ โ (0[,]1) โ ๐ โ
โ) |
9 | 8 | adantr 481 |
. . . . . . 7
โข ((๐ โ (0[,]1) โง
โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) โ ๐ โ โ) |
10 | 9 | 3ad2ant3 1135 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ๐ โ โ) |
11 | 10 | recnd 11224 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ๐ โ โ) |
12 | 11 | adantr 481 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ ๐ โ โ) |
13 | | fveq2 6878 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
14 | | fveq2 6878 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
15 | 14 | oveq2d 7409 |
. . . . . . . . 9
โข (๐ = ๐ โ ((1 โ ๐) ยท (๐ดโ๐)) = ((1 โ ๐) ยท (๐ดโ๐))) |
16 | | fveq2 6878 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ถโ๐) = (๐ถโ๐)) |
17 | 16 | oveq2d 7409 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท (๐ถโ๐)) = (๐ ยท (๐ถโ๐))) |
18 | 15, 17 | oveq12d 7411 |
. . . . . . . 8
โข (๐ = ๐ โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) |
19 | 13, 18 | eqeq12d 2747 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โ (๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) |
20 | 19 | rspccva 3608 |
. . . . . 6
โข
((โ๐ โ
(1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง ๐ โ (1...๐)) โ (๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) |
21 | 20 | adantll 712 |
. . . . 5
โข (((๐ โ (0[,]1) โง
โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) โง ๐ โ (1...๐)) โ (๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) |
22 | 21 | 3ad2antl3 1187 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ (๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) |
23 | | oveq2 7401 |
. . . . . 6
โข ((๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โ ((๐ดโ๐) โ (๐ตโ๐)) = ((๐ดโ๐) โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) |
24 | 23 | oveq1d 7408 |
. . . . 5
โข ((๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โ (((๐ดโ๐) โ (๐ตโ๐))โ2) = (((๐ดโ๐) โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))โ2)) |
25 | | subdi 11629 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ ยท ((๐ดโ๐) โ (๐ถโ๐))) = ((๐ ยท (๐ดโ๐)) โ (๐ ยท (๐ถโ๐)))) |
26 | 25 | 3coml 1127 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (๐ ยท ((๐ดโ๐) โ (๐ถโ๐))) = ((๐ ยท (๐ดโ๐)) โ (๐ ยท (๐ถโ๐)))) |
27 | | ax-1cn 11150 |
. . . . . . . . . . . 12
โข 1 โ
โ |
28 | | subcl 11441 |
. . . . . . . . . . . . . 14
โข ((1
โ โ โง ๐
โ โ) โ (1 โ ๐) โ โ) |
29 | 27, 28 | mpan 688 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (1
โ ๐) โ
โ) |
30 | 29 | adantl 482 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ (1 โ ๐) โ
โ) |
31 | | simpl 483 |
. . . . . . . . . . . 12
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
32 | | subdir 11630 |
. . . . . . . . . . . 12
โข ((1
โ โ โง (1 โ ๐) โ โ โง (๐ดโ๐) โ โ) โ ((1 โ (1
โ ๐)) ยท (๐ดโ๐)) = ((1 ยท (๐ดโ๐)) โ ((1 โ ๐) ยท (๐ดโ๐)))) |
33 | 27, 30, 31, 32 | mp3an2i 1466 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ ((1 โ (1
โ ๐)) ยท (๐ดโ๐)) = ((1 ยท (๐ดโ๐)) โ ((1 โ ๐) ยท (๐ดโ๐)))) |
34 | | nncan 11471 |
. . . . . . . . . . . . . 14
โข ((1
โ โ โง ๐
โ โ) โ (1 โ (1 โ ๐)) = ๐) |
35 | 27, 34 | mpan 688 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (1
โ (1 โ ๐)) =
๐) |
36 | 35 | oveq1d 7408 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1
โ (1 โ ๐))
ยท (๐ดโ๐)) = (๐ ยท (๐ดโ๐))) |
37 | 36 | adantl 482 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ ((1 โ (1
โ ๐)) ยท (๐ดโ๐)) = (๐ ยท (๐ดโ๐))) |
38 | | mullid 11195 |
. . . . . . . . . . . . 13
โข ((๐ดโ๐) โ โ โ (1 ยท (๐ดโ๐)) = (๐ดโ๐)) |
39 | 38 | oveq1d 7408 |
. . . . . . . . . . . 12
โข ((๐ดโ๐) โ โ โ ((1 ยท (๐ดโ๐)) โ ((1 โ ๐) ยท (๐ดโ๐))) = ((๐ดโ๐) โ ((1 โ ๐) ยท (๐ดโ๐)))) |
40 | 39 | adantr 481 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ ((1 ยท (๐ดโ๐)) โ ((1 โ ๐) ยท (๐ดโ๐))) = ((๐ดโ๐) โ ((1 โ ๐) ยท (๐ดโ๐)))) |
41 | 33, 37, 40 | 3eqtr3rd 2780 |
. . . . . . . . . 10
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ ((๐ดโ๐) โ ((1 โ ๐) ยท (๐ดโ๐))) = (๐ ยท (๐ดโ๐))) |
42 | 41 | oveq1d 7408 |
. . . . . . . . 9
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ (((๐ดโ๐) โ ((1 โ ๐) ยท (๐ดโ๐))) โ (๐ ยท (๐ถโ๐))) = ((๐ ยท (๐ดโ๐)) โ (๐ ยท (๐ถโ๐)))) |
43 | 42 | 3adant2 1131 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (((๐ดโ๐) โ ((1 โ ๐) ยท (๐ดโ๐))) โ (๐ ยท (๐ถโ๐))) = ((๐ ยท (๐ดโ๐)) โ (๐ ยท (๐ถโ๐)))) |
44 | | simp1 1136 |
. . . . . . . . 9
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
45 | | mulcl 11176 |
. . . . . . . . . . . 12
โข (((1
โ ๐) โ โ
โง (๐ดโ๐) โ โ) โ ((1
โ ๐) ยท (๐ดโ๐)) โ โ) |
46 | 29, 45 | sylan 580 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ดโ๐) โ โ) โ ((1 โ ๐) ยท (๐ดโ๐)) โ โ) |
47 | 46 | ancoms 459 |
. . . . . . . . . 10
โข (((๐ดโ๐) โ โ โง ๐ โ โ) โ ((1 โ ๐) ยท (๐ดโ๐)) โ โ) |
48 | 47 | 3adant2 1131 |
. . . . . . . . 9
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ ((1 โ ๐) ยท (๐ดโ๐)) โ โ) |
49 | | mulcl 11176 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ถโ๐) โ โ) โ (๐ ยท (๐ถโ๐)) โ โ) |
50 | 49 | ancoms 459 |
. . . . . . . . . 10
โข (((๐ถโ๐) โ โ โง ๐ โ โ) โ (๐ ยท (๐ถโ๐)) โ โ) |
51 | 50 | 3adant1 1130 |
. . . . . . . . 9
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (๐ ยท (๐ถโ๐)) โ โ) |
52 | 44, 48, 51 | subsub4d 11584 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (((๐ดโ๐) โ ((1 โ ๐) ยท (๐ดโ๐))) โ (๐ ยท (๐ถโ๐))) = ((๐ดโ๐) โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) |
53 | 26, 43, 52 | 3eqtr2rd 2778 |
. . . . . . 7
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ ((๐ดโ๐) โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) = (๐ ยท ((๐ดโ๐) โ (๐ถโ๐)))) |
54 | 53 | oveq1d 7408 |
. . . . . 6
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (((๐ดโ๐) โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))โ2) = ((๐ ยท ((๐ดโ๐) โ (๐ถโ๐)))โ2)) |
55 | | simp3 1138 |
. . . . . . 7
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ ๐ โ โ) |
56 | | subcl 11441 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ดโ๐) โ (๐ถโ๐)) โ โ) |
57 | 56 | 3adant3 1132 |
. . . . . . 7
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ ((๐ดโ๐) โ (๐ถโ๐)) โ โ) |
58 | 55, 57 | sqmuld 14105 |
. . . . . 6
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ ((๐ ยท ((๐ดโ๐) โ (๐ถโ๐)))โ2) = ((๐โ2) ยท (((๐ดโ๐) โ (๐ถโ๐))โ2))) |
59 | 54, 58 | eqtrd 2771 |
. . . . 5
โข (((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โ (((๐ดโ๐) โ (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))โ2) = ((๐โ2) ยท (((๐ดโ๐) โ (๐ถโ๐))โ2))) |
60 | 24, 59 | sylan9eqr 2793 |
. . . 4
โข ((((๐ดโ๐) โ โ โง (๐ถโ๐) โ โ โง ๐ โ โ) โง (๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) โ (((๐ดโ๐) โ (๐ตโ๐))โ2) = ((๐โ2) ยท (((๐ดโ๐) โ (๐ถโ๐))โ2))) |
61 | 3, 6, 12, 22, 60 | syl31anc 1373 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ (((๐ดโ๐) โ (๐ตโ๐))โ2) = ((๐โ2) ยท (((๐ดโ๐) โ (๐ถโ๐))โ2))) |
62 | 61 | sumeq2dv 15631 |
. 2
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) = ฮฃ๐ โ (1...๐)((๐โ2) ยท (((๐ดโ๐) โ (๐ถโ๐))โ2))) |
63 | | fzfid 13920 |
. . 3
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ (1...๐) โ Fin) |
64 | 8 | resqcld 14072 |
. . . . . 6
โข (๐ โ (0[,]1) โ (๐โ2) โ
โ) |
65 | 64 | recnd 11224 |
. . . . 5
โข (๐ โ (0[,]1) โ (๐โ2) โ
โ) |
66 | 65 | adantr 481 |
. . . 4
โข ((๐ โ (0[,]1) โง
โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐)))) โ (๐โ2) โ โ) |
67 | 66 | 3ad2ant3 1135 |
. . 3
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ (๐โ2) โ โ) |
68 | 2 | 3adant1 1130 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
69 | 68 | 3adant2r 1179 |
. . . . . . 7
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
70 | 5 | 3adant1 1130 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
71 | 70 | 3adant2l 1178 |
. . . . . . 7
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
72 | 69, 71 | subcld 11553 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ ((๐ดโ๐) โ (๐ถโ๐)) โ โ) |
73 | 72 | sqcld 14091 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (((๐ดโ๐) โ (๐ถโ๐))โ2) โ โ) |
74 | 73 | 3expa 1118 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((๐ดโ๐) โ (๐ถโ๐))โ2) โ โ) |
75 | 74 | 3adantl3 1168 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โง ๐ โ (1...๐)) โ (((๐ดโ๐) โ (๐ถโ๐))โ2) โ โ) |
76 | 63, 67, 75 | fsummulc2 15712 |
. 2
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ((๐โ2) ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) = ฮฃ๐ โ (1...๐)((๐โ2) ยท (((๐ดโ๐) โ (๐ถโ๐))โ2))) |
77 | 62, 76 | eqtr4d 2774 |
1
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) = ((๐โ2) ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2))) |