Step | Hyp | Ref
| Expression |
1 | | fltltc.c |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
2 | 1 | nnred 12175 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
3 | | fltltc.n |
. . . . . . 7
โข (๐ โ ๐ โ
(โคโฅโ3)) |
4 | | eluzge3nn 12822 |
. . . . . . 7
โข (๐ โ
(โคโฅโ3) โ ๐ โ โ) |
5 | | nnm1nn0 12461 |
. . . . . . 7
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ
โ0) |
7 | 2, 6 | reexpcld 14075 |
. . . . 5
โข (๐ โ (๐ถโ(๐ โ 1)) โ
โ) |
8 | 6 | nn0red 12481 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ โ) |
9 | | fltltc.b |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
10 | 9 | nnred 12175 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
11 | 10, 6 | reexpcld 14075 |
. . . . . 6
โข (๐ โ (๐ตโ(๐ โ 1)) โ
โ) |
12 | 8, 11 | remulcld 11192 |
. . . . 5
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) โ
โ) |
13 | 7, 12 | readdcld 11191 |
. . . 4
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) โ
โ) |
14 | | fzofi 13886 |
. . . . . 6
โข
(0..^๐) โ
Fin |
15 | 14 | a1i 11 |
. . . . 5
โข (๐ โ (0..^๐) โ Fin) |
16 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0..^๐)) โ ๐ถ โ โ) |
17 | | elfzonn0 13624 |
. . . . . . . 8
โข (๐ โ (0..^๐) โ ๐ โ โ0) |
18 | 17 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ (0..^๐)) โ ๐ โ โ0) |
19 | 16, 18 | reexpcld 14075 |
. . . . . 6
โข ((๐ โง ๐ โ (0..^๐)) โ (๐ถโ๐) โ โ) |
20 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0..^๐)) โ ๐ต โ โ) |
21 | | fzonnsub 13604 |
. . . . . . . . 9
โข (๐ โ (0..^๐) โ (๐ โ ๐) โ โ) |
22 | 21 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0..^๐)) โ (๐ โ ๐) โ โ) |
23 | | nnm1nn0 12461 |
. . . . . . . 8
โข ((๐ โ ๐) โ โ โ ((๐ โ ๐) โ 1) โ
โ0) |
24 | 22, 23 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ โ (0..^๐)) โ ((๐ โ ๐) โ 1) โ
โ0) |
25 | 20, 24 | reexpcld 14075 |
. . . . . 6
โข ((๐ โง ๐ โ (0..^๐)) โ (๐ตโ((๐ โ ๐) โ 1)) โ
โ) |
26 | 19, 25 | remulcld 11192 |
. . . . 5
โข ((๐ โง ๐ โ (0..^๐)) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) โ
โ) |
27 | 15, 26 | fsumrecl 15626 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0..^๐)((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) โ
โ) |
28 | | fltltc.a |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
29 | | fltltc.1 |
. . . . . 6
โข (๐ โ ((๐ดโ๐) + (๐ตโ๐)) = (๐ถโ๐)) |
30 | 28, 9, 1, 3, 29 | fltltc 41028 |
. . . . 5
โข (๐ โ ๐ต < ๐ถ) |
31 | | difrp 12960 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต < ๐ถ โ (๐ถ โ ๐ต) โ
โ+)) |
32 | 10, 2, 31 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ต < ๐ถ โ (๐ถ โ ๐ต) โ
โ+)) |
33 | 30, 32 | mpbid 231 |
. . . 4
โข (๐ โ (๐ถ โ ๐ต) โ
โ+) |
34 | | fzofi 13886 |
. . . . . . . . . 10
โข
(0..^(๐ โ 1))
โ Fin |
35 | 34 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (0..^(๐ โ 1)) โ Fin) |
36 | 2 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ถ โ โ) |
37 | | elfzonn0 13624 |
. . . . . . . . . . . 12
โข (๐ โ (0..^(๐ โ 1)) โ ๐ โ โ0) |
38 | 37 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ โ โ0) |
39 | 36, 38 | reexpcld 14075 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ (๐ถโ๐) โ โ) |
40 | 10 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ต โ โ) |
41 | | fzonnsub 13604 |
. . . . . . . . . . . . 13
โข (๐ โ (0..^(๐ โ 1)) โ ((๐ โ 1) โ ๐) โ โ) |
42 | 41 | nnnn0d 12480 |
. . . . . . . . . . . 12
โข (๐ โ (0..^(๐ โ 1)) โ ((๐ โ 1) โ ๐) โ
โ0) |
43 | 42 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ((๐ โ 1) โ ๐) โ
โ0) |
44 | 40, 43 | reexpcld 14075 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ (๐ตโ((๐ โ 1) โ ๐)) โ โ) |
45 | 39, 44 | remulcld 11192 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
46 | 35, 45 | fsumrecl 15626 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
47 | | fzofi 13886 |
. . . . . . . . . . . . . 14
โข
(0..^((๐ โ 1)
โ 1)) โ Fin |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (0..^((๐ โ 1) โ 1)) โ
Fin) |
49 | 10 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ต โ
โ) |
50 | | elfzonn0 13624 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0..^((๐ โ 1) โ 1)) โ ๐ โ
โ0) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ โ
โ0) |
52 | 49, 51 | reexpcld 14075 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ตโ๐) โ โ) |
53 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ โ (0..^((๐ โ 1) โ 1))) |
54 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ0 |
55 | | elfzoext 13636 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (0..^((๐ โ 1) โ 1)) โง 1 โ
โ0) โ ๐ โ (0..^(((๐ โ 1) โ 1) +
1))) |
56 | 53, 54, 55 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ โ (0..^(((๐ โ 1) โ 1) +
1))) |
57 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ0) |
58 | 3, 4, 57 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ โ
โ0) |
59 | 58 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ โ โ) |
60 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 1 โ
โ) |
61 | 59, 60 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ โ 1) โ โ) |
62 | 61, 60 | npcand 11523 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((๐ โ 1) โ 1) + 1) = (๐ โ 1)) |
63 | 62 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0..^(((๐ โ 1) โ 1) + 1)) = (0..^(๐ โ 1))) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ
(0..^(((๐ โ 1)
โ 1) + 1)) = (0..^(๐
โ 1))) |
65 | 56, 64 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ โ (0..^(๐ โ 1))) |
66 | 65, 42 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ((๐ โ 1) โ ๐) โ
โ0) |
67 | 49, 66 | reexpcld 14075 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ตโ((๐ โ 1) โ ๐)) โ โ) |
68 | 52, 67 | remulcld 11192 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
69 | 48, 68 | fsumrecl 15626 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
70 | | sub1m1 12412 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ((๐ โ 1) โ 1) = (๐ โ 2)) |
71 | 59, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ โ 1) โ 1) = (๐ โ 2)) |
72 | | uz3m2nn 12823 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ3) โ (๐ โ 2) โ โ) |
73 | 3, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ 2) โ โ) |
74 | 71, 73 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ โ 1) โ 1) โ
โ) |
75 | 74 | nnnn0d 12480 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ โ 1) โ 1) โ
โ0) |
76 | 10, 75 | reexpcld 14075 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ตโ((๐ โ 1) โ 1)) โ
โ) |
77 | 76, 10 | remulcld 11192 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต) โ
โ) |
78 | 69, 77 | readdcld 11191 |
. . . . . . . . . . 11
โข (๐ โ (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต)) โ
โ) |
79 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ถ โ
โ) |
80 | 79, 51 | reexpcld 14075 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ถโ๐) โ โ) |
81 | 80, 67 | remulcld 11192 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
82 | 48, 81 | fsumrecl 15626 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
83 | 2, 75 | reexpcld 14075 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ถโ((๐ โ 1) โ 1)) โ
โ) |
84 | 83, 10 | remulcld 11192 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต) โ
โ) |
85 | 82, 84 | readdcld 11191 |
. . . . . . . . . . 11
โข (๐ โ (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต)) โ
โ) |
86 | 9 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ โ) |
87 | | uzuzle23 12821 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ
(โคโฅโ3) โ ๐ โ
(โคโฅโ2)) |
88 | 3, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ
(โคโฅโ2)) |
89 | | uz2m1nn 12855 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ โ 1) โ โ) |
91 | | expm1t 14003 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ โ โง (๐ โ 1) โ โ)
โ (๐ตโ(๐ โ 1)) = ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต)) |
92 | 86, 90, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ตโ(๐ โ 1)) = ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต)) |
93 | 92 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต) = (๐ตโ(๐ โ 1))) |
94 | 93 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต)) = ((((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1))) + (๐ตโ(๐ โ 1)))) |
95 | 61, 60 | subcld 11519 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ โ 1) โ 1) โ
โ) |
96 | 86, 6 | expcld 14058 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ตโ(๐ โ 1)) โ
โ) |
97 | 95, 96 | adddirp1d 11188 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ โ 1) โ 1) + 1) ยท (๐ตโ(๐ โ 1))) = ((((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1))) + (๐ตโ(๐ โ 1)))) |
98 | 62 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ โ 1) โ 1) + 1) ยท (๐ตโ(๐ โ 1))) = ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) |
99 | 94, 97, 98 | 3eqtr2rd 2784 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) = ((((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต))) |
100 | 12, 99 | eqled 11265 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) โค ((((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต))) |
101 | 37 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0..^(๐ โ 1)) โ ๐ โ โ) |
102 | 65, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ โ
โ) |
103 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ โ 1) โ
โ) |
104 | 102, 103 | pncan3d 11522 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ + ((๐ โ 1) โ ๐)) = (๐ โ 1)) |
105 | 104 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ตโ(๐ + ((๐ โ 1) โ ๐))) = (๐ตโ(๐ โ 1))) |
106 | 105 | sumeq2dv 15595 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))(๐ตโ(๐ + ((๐ โ 1) โ ๐))) = ฮฃ๐ โ (0..^((๐ โ 1) โ 1))(๐ตโ(๐ โ 1))) |
107 | 86 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ต โ
โ) |
108 | 107, 66, 51 | expaddd 14060 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ตโ(๐ + ((๐ โ 1) โ ๐))) = ((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
109 | 108 | sumeq2dv 15595 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))(๐ตโ(๐ + ((๐ โ 1) โ ๐))) = ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
110 | | fsumconst 15682 |
. . . . . . . . . . . . . . . 16
โข
(((0..^((๐ โ
1) โ 1)) โ Fin โง (๐ตโ(๐ โ 1)) โ โ) โ
ฮฃ๐ โ
(0..^((๐ โ 1) โ
1))(๐ตโ(๐ โ 1)) =
((โฏโ(0..^((๐
โ 1) โ 1))) ยท (๐ตโ(๐ โ 1)))) |
111 | 48, 96, 110 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))(๐ตโ(๐ โ 1)) = ((โฏโ(0..^((๐ โ 1) โ 1)))
ยท (๐ตโ(๐ โ 1)))) |
112 | | hashfzo0 14337 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ 1) โ 1) โ
โ0 โ (โฏโ(0..^((๐ โ 1) โ 1))) = ((๐ โ 1) โ
1)) |
113 | 75, 112 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โฏโ(0..^((๐
โ 1) โ 1))) = ((๐ โ 1) โ 1)) |
114 | 113 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ
((โฏโ(0..^((๐
โ 1) โ 1))) ยท (๐ตโ(๐ โ 1))) = (((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1)))) |
115 | 111, 114 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))(๐ตโ(๐ โ 1)) = (((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1)))) |
116 | 106, 109,
115 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) = (((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1)))) |
117 | 116 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต)) = ((((๐ โ 1) โ 1) ยท (๐ตโ(๐ โ 1))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต))) |
118 | 100, 117 | breqtrrd 5138 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) โค (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต))) |
119 | 9 | nnrpd 12962 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ
โ+) |
120 | 119 | rpge0d 12968 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 โค ๐ต) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ 0 โค ๐ต) |
122 | 49, 66, 121 | expge0d 14076 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ 0 โค
(๐ตโ((๐ โ 1) โ ๐))) |
123 | 10, 2, 30 | ltled 11310 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โค ๐ถ) |
124 | 123 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ๐ต โค ๐ถ) |
125 | | leexp1a 14087 |
. . . . . . . . . . . . . . 15
โข (((๐ต โ โ โง ๐ถ โ โ โง ๐ โ โ0)
โง (0 โค ๐ต โง ๐ต โค ๐ถ)) โ (๐ตโ๐) โค (๐ถโ๐)) |
126 | 49, 79, 51, 121, 124, 125 | syl32anc 1379 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ (๐ตโ๐) โค (๐ถโ๐)) |
127 | 52, 80, 67, 122, 126 | lemul1ad 12101 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0..^((๐ โ 1) โ 1))) โ ((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โค ((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
128 | 48, 68, 81, 127 | fsumle 15691 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โค ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
129 | 1 | nnrpd 12962 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ถ โ
โ+) |
130 | 119, 129,
74, 30 | ltexp1dd 40838 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ตโ((๐ โ 1) โ 1)) < (๐ถโ((๐ โ 1) โ 1))) |
131 | 76, 83, 119, 130 | ltmul1dd 13019 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต) < ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต)) |
132 | 69, 77, 82, 84, 128, 131 | leltaddd 11784 |
. . . . . . . . . . 11
โข (๐ โ (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ตโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ตโ((๐ โ 1) โ 1)) ยท ๐ต)) < (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต))) |
133 | 12, 78, 85, 118, 132 | lelttrd 11320 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) < (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต))) |
134 | 61, 60 | nncand 11524 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ โ 1) โ ((๐ โ 1) โ 1)) =
1) |
135 | 134 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1))) = (๐ตโ1)) |
136 | 86 | exp1d 14053 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ตโ1) = ๐ต) |
137 | 135, 136 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1))) = ๐ต) |
138 | 137 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถโ((๐ โ 1) โ 1)) ยท (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1)))) = ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต)) |
139 | 138 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1))))) = (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท ๐ต))) |
140 | 133, 139 | breqtrrd 5138 |
. . . . . . . . 9
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) < (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1)))))) |
141 | | 0zd 12518 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โค) |
142 | 141 | peano2zd 12617 |
. . . . . . . . . . . 12
โข (๐ โ (0 + 1) โ
โค) |
143 | | 0cn 11154 |
. . . . . . . . . . . . . . . . 17
โข 0 โ
โ |
144 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
โ |
145 | 143, 144,
144 | addassi 11172 |
. . . . . . . . . . . . . . . 16
โข ((0 + 1)
+ 1) = (0 + (1 + 1)) |
146 | 144, 144 | addcli 11168 |
. . . . . . . . . . . . . . . . 17
โข (1 + 1)
โ โ |
147 | 146 | addid2i 11350 |
. . . . . . . . . . . . . . . 16
โข (0 + (1 +
1)) = (1 + 1) |
148 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . 16
โข (1 + 1) =
2 |
149 | 145, 147,
148 | 3eqtri 2769 |
. . . . . . . . . . . . . . 15
โข ((0 + 1)
+ 1) = 2 |
150 | 149 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ ((0 + 1) + 1) =
2) |
151 | 150 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ((0 + 1) + 1)) =
(โคโฅโ2)) |
152 | 88, 151 | eleqtrrd 2841 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (โคโฅโ((0 +
1) + 1))) |
153 | | eluzp1m1 12796 |
. . . . . . . . . . . 12
โข (((0 + 1)
โ โค โง ๐
โ (โคโฅโ((0 + 1) + 1))) โ (๐ โ 1) โ
(โคโฅโ(0 + 1))) |
154 | 142, 152,
153 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ 1) โ
(โคโฅโ(0 + 1))) |
155 | | eluzp1m1 12796 |
. . . . . . . . . . 11
โข ((0
โ โค โง (๐
โ 1) โ (โคโฅโ(0 + 1))) โ ((๐ โ 1) โ 1) โ
(โคโฅโ0)) |
156 | 141, 154,
155 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ 1) โ 1) โ
(โคโฅโ0)) |
157 | 1 | nncnd 12176 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ถ โ โ) |
158 | 157 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ถ โ โ) |
159 | 158, 38 | expcld 14058 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ (๐ถโ๐) โ โ) |
160 | 86 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ต โ โ) |
161 | 160, 43 | expcld 14058 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ (๐ตโ((๐ โ 1) โ ๐)) โ โ) |
162 | 159, 161 | mulcld 11182 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
163 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ = ((๐ โ 1) โ 1) โ (๐ถโ๐) = (๐ถโ((๐ โ 1) โ 1))) |
164 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ = ((๐ โ 1) โ 1) โ ((๐ โ 1) โ ๐) = ((๐ โ 1) โ ((๐ โ 1) โ 1))) |
165 | 164 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ = ((๐ โ 1) โ 1) โ (๐ตโ((๐ โ 1) โ ๐)) = (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1)))) |
166 | 163, 165 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ = ((๐ โ 1) โ 1) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) = ((๐ถโ((๐ โ 1) โ 1)) ยท (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1))))) |
167 | 6 | nn0zd 12532 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โค) |
168 | 156, 162,
166, 167 | fzosumm1 40696 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) = (ฮฃ๐ โ (0..^((๐ โ 1) โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + ((๐ถโ((๐ โ 1) โ 1)) ยท (๐ตโ((๐ โ 1) โ ((๐ โ 1) โ 1)))))) |
169 | 140, 168 | breqtrrd 5138 |
. . . . . . . 8
โข (๐ โ ((๐ โ 1) ยท (๐ตโ(๐ โ 1))) < ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
170 | 12, 46, 7, 169 | ltadd2dd 11321 |
. . . . . . 7
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) < ((๐ถโ(๐ โ 1)) + ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))))) |
171 | 35, 162 | fsumcl 15625 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) โ โ) |
172 | 157, 6 | expcld 14058 |
. . . . . . . 8
โข (๐ โ (๐ถโ(๐ โ 1)) โ
โ) |
173 | 171, 172 | addcomd 11364 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + (๐ถโ(๐ โ 1))) = ((๐ถโ(๐ โ 1)) + ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))))) |
174 | 170, 173 | breqtrrd 5138 |
. . . . . 6
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) < (ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + (๐ถโ(๐ โ 1)))) |
175 | 59 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ โ โ) |
176 | 101 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ๐ โ โ) |
177 | | 1cnd 11157 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ 1 โ
โ) |
178 | 175, 176,
177 | sub32d 11551 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ((๐ โ ๐) โ 1) = ((๐ โ 1) โ ๐)) |
179 | 178 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ (๐ตโ((๐ โ ๐) โ 1)) = (๐ตโ((๐ โ 1) โ ๐))) |
180 | 179 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0..^(๐ โ 1))) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) = ((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
181 | 180 | sumeq2dv 15595 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) = ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐)))) |
182 | 59, 59, 60 | nnncand 11552 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ (๐ โ 1)) โ 1) = (๐ โ ๐)) |
183 | 59 | subidd 11507 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ ๐) = 0) |
184 | 182, 183 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ (๐ โ 1)) โ 1) =
0) |
185 | 184 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ((๐ โ (๐ โ 1)) โ 1)) = (๐ตโ0)) |
186 | 86 | exp0d 14052 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ0) = 1) |
187 | 185, 186 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ (๐ตโ((๐ โ (๐ โ 1)) โ 1)) =
1) |
188 | 187 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((๐ถโ(๐ โ 1)) ยท (๐ตโ((๐ โ (๐ โ 1)) โ 1))) = ((๐ถโ(๐ โ 1)) ยท 1)) |
189 | 7 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ (๐ถโ(๐ โ 1)) โ
โ) |
190 | 189 | mulid1d 11179 |
. . . . . . . 8
โข (๐ โ ((๐ถโ(๐ โ 1)) ยท 1) = (๐ถโ(๐ โ 1))) |
191 | 188, 190 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ ((๐ถโ(๐ โ 1)) ยท (๐ตโ((๐ โ (๐ โ 1)) โ 1))) = (๐ถโ(๐ โ 1))) |
192 | 181, 191 | oveq12d 7380 |
. . . . . 6
โข (๐ โ (ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) + ((๐ถโ(๐ โ 1)) ยท (๐ตโ((๐ โ (๐ โ 1)) โ 1)))) = (ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ 1) โ ๐))) + (๐ถโ(๐ โ 1)))) |
193 | 174, 192 | breqtrrd 5138 |
. . . . 5
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) < (ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) + ((๐ถโ(๐ โ 1)) ยท (๐ตโ((๐ โ (๐ โ 1)) โ 1))))) |
194 | | elnn0uz 12815 |
. . . . . . 7
โข ((๐ โ 1) โ
โ0 โ (๐ โ 1) โ
(โคโฅโ0)) |
195 | 6, 194 | sylib 217 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ
(โคโฅโ0)) |
196 | 157 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0..^๐)) โ ๐ถ โ โ) |
197 | 196, 18 | expcld 14058 |
. . . . . . 7
โข ((๐ โง ๐ โ (0..^๐)) โ (๐ถโ๐) โ โ) |
198 | 86 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0..^๐)) โ ๐ต โ โ) |
199 | 198, 24 | expcld 14058 |
. . . . . . 7
โข ((๐ โง ๐ โ (0..^๐)) โ (๐ตโ((๐ โ ๐) โ 1)) โ
โ) |
200 | 197, 199 | mulcld 11182 |
. . . . . 6
โข ((๐ โง ๐ โ (0..^๐)) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) โ
โ) |
201 | | oveq2 7370 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ (๐ถโ๐) = (๐ถโ(๐ โ 1))) |
202 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = (๐ โ 1) โ (๐ โ ๐) = (๐ โ (๐ โ 1))) |
203 | 202 | oveq1d 7377 |
. . . . . . . 8
โข (๐ = (๐ โ 1) โ ((๐ โ ๐) โ 1) = ((๐ โ (๐ โ 1)) โ 1)) |
204 | 203 | oveq2d 7378 |
. . . . . . 7
โข (๐ = (๐ โ 1) โ (๐ตโ((๐ โ ๐) โ 1)) = (๐ตโ((๐ โ (๐ โ 1)) โ 1))) |
205 | 201, 204 | oveq12d 7380 |
. . . . . 6
โข (๐ = (๐ โ 1) โ ((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) = ((๐ถโ(๐ โ 1)) ยท (๐ตโ((๐ โ (๐ โ 1)) โ 1)))) |
206 | 58 | nn0zd 12532 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
207 | 195, 200,
205, 206 | fzosumm1 40696 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0..^๐)((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) = (ฮฃ๐ โ (0..^(๐ โ 1))((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))) + ((๐ถโ(๐ โ 1)) ยท (๐ตโ((๐ โ (๐ โ 1)) โ 1))))) |
208 | 193, 207 | breqtrrd 5138 |
. . . 4
โข (๐ โ ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1)))) < ฮฃ๐ โ (0..^๐)((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1)))) |
209 | 13, 27, 33, 208 | ltmul2dd 13020 |
. . 3
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < ((๐ถ โ ๐ต) ยท ฮฃ๐ โ (0..^๐)((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))))) |
210 | | pwdif 15760 |
. . . 4
โข ((๐ โ โ0
โง ๐ถ โ โ
โง ๐ต โ โ)
โ ((๐ถโ๐) โ (๐ตโ๐)) = ((๐ถ โ ๐ต) ยท ฮฃ๐ โ (0..^๐)((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))))) |
211 | 58, 157, 86, 210 | syl3anc 1372 |
. . 3
โข (๐ โ ((๐ถโ๐) โ (๐ตโ๐)) = ((๐ถ โ ๐ต) ยท ฮฃ๐ โ (0..^๐)((๐ถโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))))) |
212 | 209, 211 | breqtrrd 5138 |
. 2
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < ((๐ถโ๐) โ (๐ตโ๐))) |
213 | 28 | nncnd 12176 |
. . . 4
โข (๐ โ ๐ด โ โ) |
214 | 213, 58 | expcld 14058 |
. . 3
โข (๐ โ (๐ดโ๐) โ โ) |
215 | 86, 58 | expcld 14058 |
. . 3
โข (๐ โ (๐ตโ๐) โ โ) |
216 | 214, 215,
29 | mvlraddd 11572 |
. 2
โข (๐ โ (๐ดโ๐) = ((๐ถโ๐) โ (๐ตโ๐))) |
217 | 212, 216 | breqtrrd 5138 |
1
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐ถโ(๐ โ 1)) + ((๐ โ 1) ยท (๐ตโ(๐ โ 1))))) < (๐ดโ๐)) |