Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . 7
β’ (π β π β β) |
2 | | iccpartgtprec.p |
. . . . . . 7
β’ (π β π β (RePartβπ)) |
3 | | lbfzo0 13621 |
. . . . . . . 8
β’ (0 β
(0..^π) β π β
β) |
4 | 1, 3 | sylibr 233 |
. . . . . . 7
β’ (π β 0 β (0..^π)) |
5 | | iccpartimp 45699 |
. . . . . . 7
β’ ((π β β β§ π β (RePartβπ) β§ 0 β (0..^π)) β (π β (β*
βm (0...π))
β§ (πβ0) <
(πβ(0 +
1)))) |
6 | 1, 2, 4, 5 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β (β*
βm (0...π))
β§ (πβ0) <
(πβ(0 +
1)))) |
7 | 6 | simprd 497 |
. . . . 5
β’ (π β (πβ0) < (πβ(0 + 1))) |
8 | 7 | adantl 483 |
. . . 4
β’ ((π = 1 β§ π) β (πβ0) < (πβ(0 + 1))) |
9 | | fveq2 6846 |
. . . . . 6
β’ (π = 1 β (πβπ) = (πβ1)) |
10 | | 1e0p1 12668 |
. . . . . . 7
β’ 1 = (0 +
1) |
11 | 10 | fveq2i 6849 |
. . . . . 6
β’ (πβ1) = (πβ(0 + 1)) |
12 | 9, 11 | eqtrdi 2789 |
. . . . 5
β’ (π = 1 β (πβπ) = (πβ(0 + 1))) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π = 1 β§ π) β (πβπ) = (πβ(0 + 1))) |
14 | 8, 13 | breqtrrd 5137 |
. . 3
β’ ((π = 1 β§ π) β (πβ0) < (πβπ)) |
15 | 14 | ex 414 |
. 2
β’ (π = 1 β (π β (πβ0) < (πβπ))) |
16 | 1, 2 | iccpartiltu 45704 |
. . . 4
β’ (π β βπ β (1..^π)(πβπ) < (πβπ)) |
17 | 1, 2 | iccpartigtl 45705 |
. . . 4
β’ (π β βπ β (1..^π)(πβ0) < (πβπ)) |
18 | | 1nn 12172 |
. . . . . . . . . 10
β’ 1 β
β |
19 | 18 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ Β¬ π = 1) β 1 β
β) |
20 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ Β¬ π = 1) β π β β) |
21 | | df-ne 2941 |
. . . . . . . . . . 11
β’ (π β 1 β Β¬ π = 1) |
22 | 1 | nnge1d 12209 |
. . . . . . . . . . . 12
β’ (π β 1 β€ π) |
23 | | 1red 11164 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
24 | 1 | nnred 12176 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
25 | 23, 24 | ltlend 11308 |
. . . . . . . . . . . . 13
β’ (π β (1 < π β (1 β€ π β§ π β 1))) |
26 | 25 | biimprd 248 |
. . . . . . . . . . . 12
β’ (π β ((1 β€ π β§ π β 1) β 1 < π)) |
27 | 22, 26 | mpand 694 |
. . . . . . . . . . 11
β’ (π β (π β 1 β 1 < π)) |
28 | 21, 27 | biimtrrid 242 |
. . . . . . . . . 10
β’ (π β (Β¬ π = 1 β 1 < π)) |
29 | 28 | imp 408 |
. . . . . . . . 9
β’ ((π β§ Β¬ π = 1) β 1 < π) |
30 | | elfzo1 13631 |
. . . . . . . . 9
β’ (1 β
(1..^π) β (1 β
β β§ π β
β β§ 1 < π)) |
31 | 19, 20, 29, 30 | syl3anbrc 1344 |
. . . . . . . 8
β’ ((π β§ Β¬ π = 1) β 1 β (1..^π)) |
32 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = 1 β (πβπ) = (πβ1)) |
33 | 32 | breq2d 5121 |
. . . . . . . . 9
β’ (π = 1 β ((πβ0) < (πβπ) β (πβ0) < (πβ1))) |
34 | 33 | rspcv 3579 |
. . . . . . . 8
β’ (1 β
(1..^π) β
(βπ β
(1..^π)(πβ0) < (πβπ) β (πβ0) < (πβ1))) |
35 | 31, 34 | syl 17 |
. . . . . . 7
β’ ((π β§ Β¬ π = 1) β (βπ β (1..^π)(πβ0) < (πβπ) β (πβ0) < (πβ1))) |
36 | 32 | breq1d 5119 |
. . . . . . . . . . 11
β’ (π = 1 β ((πβπ) < (πβπ) β (πβ1) < (πβπ))) |
37 | 36 | rspcv 3579 |
. . . . . . . . . 10
β’ (1 β
(1..^π) β
(βπ β
(1..^π)(πβπ) < (πβπ) β (πβ1) < (πβπ))) |
38 | 31, 37 | syl 17 |
. . . . . . . . 9
β’ ((π β§ Β¬ π = 1) β (βπ β (1..^π)(πβπ) < (πβπ) β (πβ1) < (πβπ))) |
39 | | nnnn0 12428 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β0) |
40 | | 0elfz 13547 |
. . . . . . . . . . . . . 14
β’ (π β β0
β 0 β (0...π)) |
41 | 1, 39, 40 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β 0 β (0...π)) |
42 | 1, 2, 41 | iccpartxr 45701 |
. . . . . . . . . . . 12
β’ (π β (πβ0) β
β*) |
43 | 42 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π = 1) β (πβ0) β
β*) |
44 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π = 1) β π β (RePartβπ)) |
45 | | 1nn0 12437 |
. . . . . . . . . . . . . 14
β’ 1 β
β0 |
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ π = 1) β 1 β
β0) |
47 | 1, 39 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β
β0) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ π = 1) β π β
β0) |
49 | 22 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ π = 1) β 1 β€ π) |
50 | | elfz2nn0 13541 |
. . . . . . . . . . . . 13
β’ (1 β
(0...π) β (1 β
β0 β§ π
β β0 β§ 1 β€ π)) |
51 | 46, 48, 49, 50 | syl3anbrc 1344 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π = 1) β 1 β (0...π)) |
52 | 20, 44, 51 | iccpartxr 45701 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π = 1) β (πβ1) β
β*) |
53 | | nn0fz0 13548 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β (0...π)) |
54 | 39, 53 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β β β π β (0...π)) |
55 | 1, 54 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β (0...π)) |
56 | 1, 2, 55 | iccpartxr 45701 |
. . . . . . . . . . . 12
β’ (π β (πβπ) β
β*) |
57 | 56 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π = 1) β (πβπ) β
β*) |
58 | | xrlttr 13068 |
. . . . . . . . . . 11
β’ (((πβ0) β
β* β§ (πβ1) β β* β§
(πβπ) β β*) β
(((πβ0) < (πβ1) β§ (πβ1) < (πβπ)) β (πβ0) < (πβπ))) |
59 | 43, 52, 57, 58 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π = 1) β (((πβ0) < (πβ1) β§ (πβ1) < (πβπ)) β (πβ0) < (πβπ))) |
60 | 59 | expcomd 418 |
. . . . . . . . 9
β’ ((π β§ Β¬ π = 1) β ((πβ1) < (πβπ) β ((πβ0) < (πβ1) β (πβ0) < (πβπ)))) |
61 | 38, 60 | syld 47 |
. . . . . . . 8
β’ ((π β§ Β¬ π = 1) β (βπ β (1..^π)(πβπ) < (πβπ) β ((πβ0) < (πβ1) β (πβ0) < (πβπ)))) |
62 | 61 | com23 86 |
. . . . . . 7
β’ ((π β§ Β¬ π = 1) β ((πβ0) < (πβ1) β (βπ β (1..^π)(πβπ) < (πβπ) β (πβ0) < (πβπ)))) |
63 | 35, 62 | syld 47 |
. . . . . 6
β’ ((π β§ Β¬ π = 1) β (βπ β (1..^π)(πβ0) < (πβπ) β (βπ β (1..^π)(πβπ) < (πβπ) β (πβ0) < (πβπ)))) |
64 | 63 | ex 414 |
. . . . 5
β’ (π β (Β¬ π = 1 β (βπ β (1..^π)(πβ0) < (πβπ) β (βπ β (1..^π)(πβπ) < (πβπ) β (πβ0) < (πβπ))))) |
65 | 64 | com24 95 |
. . . 4
β’ (π β (βπ β (1..^π)(πβπ) < (πβπ) β (βπ β (1..^π)(πβ0) < (πβπ) β (Β¬ π = 1 β (πβ0) < (πβπ))))) |
66 | 16, 17, 65 | mp2d 49 |
. . 3
β’ (π β (Β¬ π = 1 β (πβ0) < (πβπ))) |
67 | 66 | com12 32 |
. 2
β’ (Β¬
π = 1 β (π β (πβ0) < (πβπ))) |
68 | 15, 67 | pm2.61i 182 |
1
β’ (π β (πβ0) < (πβπ)) |