Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ = ๐ฟ) โ ๐ = ๐ฟ) |
2 | 1 | fveq2d 6847 |
. . . 4
โข ((๐ โง ๐ = ๐ฟ) โ (๐ดโ๐) = (๐ดโ๐ฟ)) |
3 | | fmul01lt1lem1.3 |
. . . . . 6
โข ๐ด = seq๐ฟ( ยท , ๐ต) |
4 | 3 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ = ๐ฟ) โ ๐ด = seq๐ฟ( ยท , ๐ต)) |
5 | 4 | fveq1d 6845 |
. . . 4
โข ((๐ โง ๐ = ๐ฟ) โ (๐ดโ๐ฟ) = (seq๐ฟ( ยท , ๐ต)โ๐ฟ)) |
6 | | fmul01lt1lem1.4 |
. . . . . 6
โข (๐ โ ๐ฟ โ โค) |
7 | | seq1 13920 |
. . . . . 6
โข (๐ฟ โ โค โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) = (๐ตโ๐ฟ)) |
8 | 6, 7 | syl 17 |
. . . . 5
โข (๐ โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) = (๐ตโ๐ฟ)) |
9 | 8 | adantr 482 |
. . . 4
โข ((๐ โง ๐ = ๐ฟ) โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) = (๐ตโ๐ฟ)) |
10 | 2, 5, 9 | 3eqtrd 2781 |
. . 3
โข ((๐ โง ๐ = ๐ฟ) โ (๐ดโ๐) = (๐ตโ๐ฟ)) |
11 | | fmul01lt1lem1.10 |
. . . 4
โข (๐ โ (๐ตโ๐ฟ) < ๐ธ) |
12 | 11 | adantr 482 |
. . 3
โข ((๐ โง ๐ = ๐ฟ) โ (๐ตโ๐ฟ) < ๐ธ) |
13 | 10, 12 | eqbrtrd 5128 |
. 2
โข ((๐ โง ๐ = ๐ฟ) โ (๐ดโ๐) < ๐ธ) |
14 | | simpr 486 |
. . . . 5
โข ((๐ โง ยฌ ๐ = ๐ฟ) โ ยฌ ๐ = ๐ฟ) |
15 | 14 | neqned 2951 |
. . . 4
โข ((๐ โง ยฌ ๐ = ๐ฟ) โ ๐ โ ๐ฟ) |
16 | 6 | zred 12608 |
. . . . . . 7
โข (๐ โ ๐ฟ โ โ) |
17 | | fmul01lt1lem1.5 |
. . . . . . . . 9
โข (๐ โ ๐ โ (โคโฅโ๐ฟ)) |
18 | | eluzelz 12774 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐ฟ) โ ๐ โ โค) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
20 | 19 | zred 12608 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
21 | | eluzle 12777 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐ฟ) โ ๐ฟ โค ๐) |
22 | 17, 21 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ฟ โค ๐) |
23 | 16, 20, 22 | 3jca 1129 |
. . . . . 6
โข (๐ โ (๐ฟ โ โ โง ๐ โ โ โง ๐ฟ โค ๐)) |
24 | 23 | adantr 482 |
. . . . 5
โข ((๐ โง ยฌ ๐ = ๐ฟ) โ (๐ฟ โ โ โง ๐ โ โ โง ๐ฟ โค ๐)) |
25 | | leltne 11245 |
. . . . 5
โข ((๐ฟ โ โ โง ๐ โ โ โง ๐ฟ โค ๐) โ (๐ฟ < ๐ โ ๐ โ ๐ฟ)) |
26 | 24, 25 | syl 17 |
. . . 4
โข ((๐ โง ยฌ ๐ = ๐ฟ) โ (๐ฟ < ๐ โ ๐ โ ๐ฟ)) |
27 | 15, 26 | mpbird 257 |
. . 3
โข ((๐ โง ยฌ ๐ = ๐ฟ) โ ๐ฟ < ๐) |
28 | 3 | fveq1i 6844 |
. . . 4
โข (๐ดโ๐) = (seq๐ฟ( ยท , ๐ต)โ๐) |
29 | | remulcl 11137 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
30 | 29 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ฟ < ๐) โง (๐ โ โ โง ๐ โ โ)) โ (๐ ยท ๐) โ โ) |
31 | | recn 11142 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
32 | 31 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
33 | | recn 11142 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
34 | 33 | 3ad2ant2 1135 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
35 | | recn 11142 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
36 | 35 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
37 | 32, 34, 36 | mulassd 11179 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
38 | 37 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ฟ < ๐) โง (๐ โ โ โง ๐ โ โ โง ๐ โ โ)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
39 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โง ๐ฟ < ๐) โ ๐ฟ < ๐) |
40 | 39 | olcd 873 |
. . . . . . . . 9
โข ((๐ โง ๐ฟ < ๐) โ (๐ < ๐ฟ โจ ๐ฟ < ๐)) |
41 | 20, 16 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ โง ๐ฟ โ โ)) |
42 | 41 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฟ < ๐) โ (๐ โ โ โง ๐ฟ โ โ)) |
43 | | lttri2 11238 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฟ โ โ) โ (๐ โ ๐ฟ โ (๐ < ๐ฟ โจ ๐ฟ < ๐))) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ฟ < ๐) โ (๐ โ ๐ฟ โ (๐ < ๐ฟ โจ ๐ฟ < ๐))) |
45 | 40, 44 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ ๐ฟ) |
46 | 45 | neneqd 2949 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ ยฌ ๐ = ๐ฟ) |
47 | | uzp1 12805 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ๐ฟ) โ (๐ = ๐ฟ โจ ๐ โ (โคโฅโ(๐ฟ + 1)))) |
48 | 17, 47 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ = ๐ฟ โจ ๐ โ (โคโฅโ(๐ฟ + 1)))) |
49 | 48 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฟ < ๐) โ (๐ = ๐ฟ โจ ๐ โ (โคโฅโ(๐ฟ + 1)))) |
50 | 49 | ord 863 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ (ยฌ ๐ = ๐ฟ โ ๐ โ (โคโฅโ(๐ฟ + 1)))) |
51 | 46, 50 | mpd 15 |
. . . . . 6
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ (โคโฅโ(๐ฟ + 1))) |
52 | 6 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ ๐ฟ โ โค) |
53 | | uzid 12779 |
. . . . . . 7
โข (๐ฟ โ โค โ ๐ฟ โ
(โคโฅโ๐ฟ)) |
54 | 52, 53 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ฟ < ๐) โ ๐ฟ โ (โคโฅโ๐ฟ)) |
55 | | fmul01lt1lem1.2 |
. . . . . . . . . 10
โข
โฒ๐๐ |
56 | | nfv 1918 |
. . . . . . . . . 10
โข
โฒ๐ ๐ โ (๐ฟ...๐) |
57 | 55, 56 | nfan 1903 |
. . . . . . . . 9
โข
โฒ๐(๐ โง ๐ โ (๐ฟ...๐)) |
58 | | fmul01lt1lem1.1 |
. . . . . . . . . . 11
โข
โฒ๐๐ต |
59 | | nfcv 2908 |
. . . . . . . . . . 11
โข
โฒ๐๐ |
60 | 58, 59 | nffv 6853 |
. . . . . . . . . 10
โข
โฒ๐(๐ตโ๐) |
61 | 60 | nfel1 2924 |
. . . . . . . . 9
โข
โฒ๐(๐ตโ๐) โ โ |
62 | 57, 61 | nfim 1900 |
. . . . . . . 8
โข
โฒ๐((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ) |
63 | | eleq1 2826 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ (๐ฟ...๐) โ ๐ โ (๐ฟ...๐))) |
64 | 63 | anbi2d 630 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ โง ๐ โ (๐ฟ...๐)))) |
65 | | fveq2 6843 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
66 | 65 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ตโ๐) โ โ โ (๐ตโ๐) โ โ)) |
67 | 64, 66 | imbi12d 345 |
. . . . . . . 8
โข (๐ = ๐ โ (((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ) โ ((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ))) |
68 | | fmul01lt1lem1.6 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ) |
69 | 62, 67, 68 | chvarfv 2234 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ) |
70 | 69 | adantlr 714 |
. . . . . 6
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ) |
71 | 30, 38, 51, 54, 70 | seqsplit 13942 |
. . . . 5
โข ((๐ โง ๐ฟ < ๐) โ (seq๐ฟ( ยท , ๐ต)โ๐) = ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท (seq(๐ฟ + 1)( ยท , ๐ต)โ๐))) |
72 | | eluzfz1 13449 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐ฟ) โ ๐ฟ โ (๐ฟ...๐)) |
73 | 17, 72 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ฟ โ (๐ฟ...๐)) |
74 | 73 | ancli 550 |
. . . . . . . . . 10
โข (๐ โ (๐ โง ๐ฟ โ (๐ฟ...๐))) |
75 | | nfv 1918 |
. . . . . . . . . . . . 13
โข
โฒ๐ ๐ฟ โ (๐ฟ...๐) |
76 | 55, 75 | nfan 1903 |
. . . . . . . . . . . 12
โข
โฒ๐(๐ โง ๐ฟ โ (๐ฟ...๐)) |
77 | | nfcv 2908 |
. . . . . . . . . . . . . 14
โข
โฒ๐๐ฟ |
78 | 58, 77 | nffv 6853 |
. . . . . . . . . . . . 13
โข
โฒ๐(๐ตโ๐ฟ) |
79 | 78 | nfel1 2924 |
. . . . . . . . . . . 12
โข
โฒ๐(๐ตโ๐ฟ) โ โ |
80 | 76, 79 | nfim 1900 |
. . . . . . . . . . 11
โข
โฒ๐((๐ โง ๐ฟ โ (๐ฟ...๐)) โ (๐ตโ๐ฟ) โ โ) |
81 | | eleq1 2826 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฟ โ (๐ โ (๐ฟ...๐) โ ๐ฟ โ (๐ฟ...๐))) |
82 | 81 | anbi2d 630 |
. . . . . . . . . . . 12
โข (๐ = ๐ฟ โ ((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ โง ๐ฟ โ (๐ฟ...๐)))) |
83 | | fveq2 6843 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฟ โ (๐ตโ๐) = (๐ตโ๐ฟ)) |
84 | 83 | eleq1d 2823 |
. . . . . . . . . . . 12
โข (๐ = ๐ฟ โ ((๐ตโ๐) โ โ โ (๐ตโ๐ฟ) โ โ)) |
85 | 82, 84 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ = ๐ฟ โ (((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โ โ) โ ((๐ โง ๐ฟ โ (๐ฟ...๐)) โ (๐ตโ๐ฟ) โ โ))) |
86 | 80, 85, 68 | vtoclg1f 3525 |
. . . . . . . . . 10
โข (๐ฟ โ (๐ฟ...๐) โ ((๐ โง ๐ฟ โ (๐ฟ...๐)) โ (๐ตโ๐ฟ) โ โ)) |
87 | 73, 74, 86 | sylc 65 |
. . . . . . . . 9
โข (๐ โ (๐ตโ๐ฟ) โ โ) |
88 | 8, 87 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) โ โ) |
89 | 88 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) โ โ) |
90 | 6 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โ โค) |
91 | 19 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โค) |
92 | | elfzelz 13442 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ฟ + 1)...๐) โ ๐ โ โค) |
93 | 92 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โค) |
94 | 16 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โ โ) |
95 | | peano2re 11329 |
. . . . . . . . . . . . . 14
โข (๐ฟ โ โ โ (๐ฟ + 1) โ
โ) |
96 | 16, 95 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฟ + 1) โ โ) |
97 | 96 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ฟ + 1) โ โ) |
98 | 92 | zred 12608 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ฟ + 1)...๐) โ ๐ โ โ) |
99 | 98 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โ) |
100 | 16 | lep1d 12087 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ฟ โค (๐ฟ + 1)) |
101 | 100 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โค (๐ฟ + 1)) |
102 | | elfzle1 13445 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ฟ + 1)...๐) โ (๐ฟ + 1) โค ๐) |
103 | 102 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ฟ + 1) โค ๐) |
104 | 94, 97, 99, 101, 103 | letrd 11313 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โค ๐) |
105 | | elfzle2 13446 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ฟ + 1)...๐) โ ๐ โค ๐) |
106 | 105 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โค ๐) |
107 | 90, 91, 93, 104, 106 | elfzd 13433 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ (๐ฟ...๐)) |
108 | 107, 69 | syldan 592 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ตโ๐) โ โ) |
109 | 108 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ตโ๐) โ โ) |
110 | 51, 109, 30 | seqcl 13929 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ (seq(๐ฟ + 1)( ยท , ๐ต)โ๐) โ โ) |
111 | 89, 110 | remulcld 11186 |
. . . . . 6
โข ((๐ โง ๐ฟ < ๐) โ ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท (seq(๐ฟ + 1)( ยท , ๐ต)โ๐)) โ โ) |
112 | | fmul01lt1lem1.9 |
. . . . . . . 8
โข (๐ โ ๐ธ โ
โ+) |
113 | 112 | rpred 12958 |
. . . . . . 7
โข (๐ โ ๐ธ โ โ) |
114 | 113 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฟ < ๐) โ ๐ธ โ โ) |
115 | | 1red 11157 |
. . . . . . . 8
โข ((๐ โง ๐ฟ < ๐) โ 1 โ โ) |
116 | | nfcv 2908 |
. . . . . . . . . . . . . 14
โข
โฒ๐0 |
117 | | nfcv 2908 |
. . . . . . . . . . . . . 14
โข
โฒ๐
โค |
118 | 116, 117,
78 | nfbr 5153 |
. . . . . . . . . . . . 13
โข
โฒ๐0 โค
(๐ตโ๐ฟ) |
119 | 76, 118 | nfim 1900 |
. . . . . . . . . . . 12
โข
โฒ๐((๐ โง ๐ฟ โ (๐ฟ...๐)) โ 0 โค (๐ตโ๐ฟ)) |
120 | 83 | breq2d 5118 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฟ โ (0 โค (๐ตโ๐) โ 0 โค (๐ตโ๐ฟ))) |
121 | 82, 120 | imbi12d 345 |
. . . . . . . . . . . 12
โข (๐ = ๐ฟ โ (((๐ โง ๐ โ (๐ฟ...๐)) โ 0 โค (๐ตโ๐)) โ ((๐ โง ๐ฟ โ (๐ฟ...๐)) โ 0 โค (๐ตโ๐ฟ)))) |
122 | | fmul01lt1lem1.7 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐ฟ...๐)) โ 0 โค (๐ตโ๐)) |
123 | 119, 121,
122 | vtoclg1f 3525 |
. . . . . . . . . . 11
โข (๐ฟ โ (๐ฟ...๐) โ ((๐ โง ๐ฟ โ (๐ฟ...๐)) โ 0 โค (๐ตโ๐ฟ))) |
124 | 73, 74, 123 | sylc 65 |
. . . . . . . . . 10
โข (๐ โ 0 โค (๐ตโ๐ฟ)) |
125 | 124, 8 | breqtrrd 5134 |
. . . . . . . . 9
โข (๐ โ 0 โค (seq๐ฟ( ยท , ๐ต)โ๐ฟ)) |
126 | 125 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฟ < ๐) โ 0 โค (seq๐ฟ( ยท , ๐ต)โ๐ฟ)) |
127 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ ๐ฟ < ๐ |
128 | 55, 127 | nfan 1903 |
. . . . . . . . . 10
โข
โฒ๐(๐ โง ๐ฟ < ๐) |
129 | | eqid 2737 |
. . . . . . . . . 10
โข seq(๐ฟ + 1)( ยท , ๐ต) = seq(๐ฟ + 1)( ยท , ๐ต) |
130 | 6 | peano2zd 12611 |
. . . . . . . . . . 11
โข (๐ โ (๐ฟ + 1) โ โค) |
131 | 130 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฟ < ๐) โ (๐ฟ + 1) โ โค) |
132 | 16 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฟ < ๐) โ ๐ฟ โ โ) |
133 | 132, 39 | gtned 11291 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ ๐ฟ) |
134 | 133 | neneqd 2949 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฟ < ๐) โ ยฌ ๐ = ๐ฟ) |
135 | 17 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ (โคโฅโ๐ฟ)) |
136 | 135, 47 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฟ < ๐) โ (๐ = ๐ฟ โจ ๐ โ (โคโฅโ(๐ฟ + 1)))) |
137 | | orel1 888 |
. . . . . . . . . . 11
โข (ยฌ
๐ = ๐ฟ โ ((๐ = ๐ฟ โจ ๐ โ (โคโฅโ(๐ฟ + 1))) โ ๐ โ (โคโฅโ(๐ฟ + 1)))) |
138 | 134, 136,
137 | sylc 65 |
. . . . . . . . . 10
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ (โคโฅโ(๐ฟ + 1))) |
139 | 19 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ โค) |
140 | | zltp1le 12554 |
. . . . . . . . . . . . 13
โข ((๐ฟ โ โค โง ๐ โ โค) โ (๐ฟ < ๐ โ (๐ฟ + 1) โค ๐)) |
141 | 52, 139, 140 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฟ < ๐) โ (๐ฟ < ๐ โ (๐ฟ + 1) โค ๐)) |
142 | 39, 141 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฟ < ๐) โ (๐ฟ + 1) โค ๐) |
143 | 20 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ โ) |
144 | 143 | leidd 11722 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฟ < ๐) โ ๐ โค ๐) |
145 | 131, 139,
139, 142, 144 | elfzd 13433 |
. . . . . . . . . 10
โข ((๐ โง ๐ฟ < ๐) โ ๐ โ ((๐ฟ + 1)...๐)) |
146 | 6 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โ โค) |
147 | 19 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โค) |
148 | | elfzelz 13442 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ฟ + 1)...๐) โ ๐ โ โค) |
149 | 148 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โค) |
150 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โ โ) |
151 | 150, 95 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ฟ + 1) โ โ) |
152 | 148 | zred 12608 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ฟ + 1)...๐) โ ๐ โ โ) |
153 | 152 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โ) |
154 | 100 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โค (๐ฟ + 1)) |
155 | | elfzle1 13445 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ฟ + 1)...๐) โ (๐ฟ + 1) โค ๐) |
156 | 155 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ฟ + 1) โค ๐) |
157 | 150, 151,
153, 154, 156 | letrd 11313 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โค ๐) |
158 | | elfzle2 13446 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ฟ + 1)...๐) โ ๐ โค ๐) |
159 | 158 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โค ๐) |
160 | 146, 147,
149, 157, 159 | elfzd 13433 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ (๐ฟ...๐)) |
161 | 160, 68 | syldan 592 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ตโ๐) โ โ) |
162 | 161 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ตโ๐) โ โ) |
163 | | simpll 766 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐) |
164 | 6 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โ โค) |
165 | 19 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โค) |
166 | 148 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โค) |
167 | 16 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โ โ) |
168 | 96 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ฟ + 1) โ โ) |
169 | 152 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ โ) |
170 | 100 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โค (๐ฟ + 1)) |
171 | 155 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ฟ + 1) โค ๐) |
172 | 167, 168,
169, 170, 171 | letrd 11313 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ฟ โค ๐) |
173 | 158 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โค ๐) |
174 | 164, 165,
166, 172, 173 | elfzd 13433 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ ๐ โ (๐ฟ...๐)) |
175 | 163, 174,
122 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ 0 โค (๐ตโ๐)) |
176 | | fmul01lt1lem1.8 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (๐ฟ...๐)) โ (๐ตโ๐) โค 1) |
177 | 163, 174,
176 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ โง ๐ฟ < ๐) โง ๐ โ ((๐ฟ + 1)...๐)) โ (๐ตโ๐) โค 1) |
178 | 58, 128, 129, 131, 138, 145, 162, 175, 177 | fmul01 43828 |
. . . . . . . . 9
โข ((๐ โง ๐ฟ < ๐) โ (0 โค (seq(๐ฟ + 1)( ยท , ๐ต)โ๐) โง (seq(๐ฟ + 1)( ยท , ๐ต)โ๐) โค 1)) |
179 | 178 | simprd 497 |
. . . . . . . 8
โข ((๐ โง ๐ฟ < ๐) โ (seq(๐ฟ + 1)( ยท , ๐ต)โ๐) โค 1) |
180 | 110, 115,
89, 126, 179 | lemul2ad 12096 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท (seq(๐ฟ + 1)( ยท , ๐ต)โ๐)) โค ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท 1)) |
181 | 88 | recnd 11184 |
. . . . . . . . 9
โข (๐ โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) โ โ) |
182 | 181 | mulid1d 11173 |
. . . . . . . 8
โข (๐ โ ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท 1) = (seq๐ฟ( ยท , ๐ต)โ๐ฟ)) |
183 | 182 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฟ < ๐) โ ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท 1) = (seq๐ฟ( ยท , ๐ต)โ๐ฟ)) |
184 | 180, 183 | breqtrd 5132 |
. . . . . 6
โข ((๐ โง ๐ฟ < ๐) โ ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท (seq(๐ฟ + 1)( ยท , ๐ต)โ๐)) โค (seq๐ฟ( ยท , ๐ต)โ๐ฟ)) |
185 | 8, 11 | eqbrtrd 5128 |
. . . . . . 7
โข (๐ โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) < ๐ธ) |
186 | 185 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฟ < ๐) โ (seq๐ฟ( ยท , ๐ต)โ๐ฟ) < ๐ธ) |
187 | 111, 89, 114, 184, 186 | lelttrd 11314 |
. . . . 5
โข ((๐ โง ๐ฟ < ๐) โ ((seq๐ฟ( ยท , ๐ต)โ๐ฟ) ยท (seq(๐ฟ + 1)( ยท , ๐ต)โ๐)) < ๐ธ) |
188 | 71, 187 | eqbrtrd 5128 |
. . . 4
โข ((๐ โง ๐ฟ < ๐) โ (seq๐ฟ( ยท , ๐ต)โ๐) < ๐ธ) |
189 | 28, 188 | eqbrtrid 5141 |
. . 3
โข ((๐ โง ๐ฟ < ๐) โ (๐ดโ๐) < ๐ธ) |
190 | 27, 189 | syldan 592 |
. 2
โข ((๐ โง ยฌ ๐ = ๐ฟ) โ (๐ดโ๐) < ๐ธ) |
191 | 13, 190 | pm2.61dan 812 |
1
โข (๐ โ (๐ดโ๐) < ๐ธ) |