Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . 3
β’ (π β π β β) |
2 | | iccpartgtprec.p |
. . 3
β’ (π β π β (RePartβπ)) |
3 | | nnz 12528 |
. . . . . . . 8
β’ (π β β β π β
β€) |
4 | | peano2zm 12554 |
. . . . . . . . 9
β’ (π β β€ β (π β 1) β
β€) |
5 | | id 22 |
. . . . . . . . 9
β’ (π β β€ β π β
β€) |
6 | | zre 12511 |
. . . . . . . . . 10
β’ (π β β€ β π β
β) |
7 | 6 | lem1d 12096 |
. . . . . . . . 9
β’ (π β β€ β (π β 1) β€ π) |
8 | 4, 5, 7 | 3jca 1129 |
. . . . . . . 8
β’ (π β β€ β ((π β 1) β β€ β§
π β β€ β§
(π β 1) β€ π)) |
9 | 3, 8 | syl 17 |
. . . . . . 7
β’ (π β β β ((π β 1) β β€ β§
π β β€ β§
(π β 1) β€ π)) |
10 | | eluz2 12777 |
. . . . . . 7
β’ (π β
(β€β₯β(π β 1)) β ((π β 1) β β€ β§ π β β€ β§ (π β 1) β€ π)) |
11 | 9, 10 | sylibr 233 |
. . . . . 6
β’ (π β β β π β
(β€β₯β(π β 1))) |
12 | 1, 11 | syl 17 |
. . . . 5
β’ (π β π β (β€β₯β(π β 1))) |
13 | | fzss2 13490 |
. . . . 5
β’ (π β
(β€β₯β(π β 1)) β (0...(π β 1)) β (0...π)) |
14 | 12, 13 | syl 17 |
. . . 4
β’ (π β (0...(π β 1)) β (0...π)) |
15 | | fzossfz 13600 |
. . . . . 6
β’
(1..^π) β
(1...π) |
16 | | iccpartipre.i |
. . . . . 6
β’ (π β πΌ β (1..^π)) |
17 | 15, 16 | sselid 3946 |
. . . . 5
β’ (π β πΌ β (1...π)) |
18 | | elfzoelz 13581 |
. . . . . . 7
β’ (πΌ β (1..^π) β πΌ β β€) |
19 | 16, 18 | syl 17 |
. . . . . 6
β’ (π β πΌ β β€) |
20 | 1 | nnzd 12534 |
. . . . . 6
β’ (π β π β β€) |
21 | | elfzm1b 13528 |
. . . . . 6
β’ ((πΌ β β€ β§ π β β€) β (πΌ β (1...π) β (πΌ β 1) β (0...(π β 1)))) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . 5
β’ (π β (πΌ β (1...π) β (πΌ β 1) β (0...(π β 1)))) |
23 | 17, 22 | mpbid 231 |
. . . 4
β’ (π β (πΌ β 1) β (0...(π β 1))) |
24 | 14, 23 | sseldd 3949 |
. . 3
β’ (π β (πΌ β 1) β (0...π)) |
25 | 1, 2, 24 | iccpartxr 45701 |
. 2
β’ (π β (πβ(πΌ β 1)) β
β*) |
26 | | 1eluzge0 12825 |
. . . . . 6
β’ 1 β
(β€β₯β0) |
27 | | fzoss1 13608 |
. . . . . 6
β’ (1 β
(β€β₯β0) β (1..^π) β (0..^π)) |
28 | 26, 27 | mp1i 13 |
. . . . 5
β’ (π β (1..^π) β (0..^π)) |
29 | | fzossfz 13600 |
. . . . 5
β’
(0..^π) β
(0...π) |
30 | 28, 29 | sstrdi 3960 |
. . . 4
β’ (π β (1..^π) β (0...π)) |
31 | 30, 16 | sseldd 3949 |
. . 3
β’ (π β πΌ β (0...π)) |
32 | 1, 2, 31 | iccpartxr 45701 |
. 2
β’ (π β (πβπΌ) β
β*) |
33 | 28, 16 | sseldd 3949 |
. . . 4
β’ (π β πΌ β (0..^π)) |
34 | | fzofzp1 13678 |
. . . 4
β’ (πΌ β (0..^π) β (πΌ + 1) β (0...π)) |
35 | 33, 34 | syl 17 |
. . 3
β’ (π β (πΌ + 1) β (0...π)) |
36 | 1, 2, 35 | iccpartxr 45701 |
. 2
β’ (π β (πβ(πΌ + 1)) β
β*) |
37 | 1, 2, 17 | iccpartgtprec 45702 |
. 2
β’ (π β (πβ(πΌ β 1)) < (πβπΌ)) |
38 | | iccpartimp 45699 |
. . . 4
β’ ((π β β β§ π β (RePartβπ) β§ πΌ β (0..^π)) β (π β (β*
βm (0...π))
β§ (πβπΌ) < (πβ(πΌ + 1)))) |
39 | 1, 2, 33, 38 | syl3anc 1372 |
. . 3
β’ (π β (π β (β*
βm (0...π))
β§ (πβπΌ) < (πβ(πΌ + 1)))) |
40 | 39 | simprd 497 |
. 2
β’ (π β (πβπΌ) < (πβ(πΌ + 1))) |
41 | | xrre2 13098 |
. 2
β’ ((((πβ(πΌ β 1)) β β*
β§ (πβπΌ) β β*
β§ (πβ(πΌ + 1)) β
β*) β§ ((πβ(πΌ β 1)) < (πβπΌ) β§ (πβπΌ) < (πβ(πΌ + 1)))) β (πβπΌ) β β) |
42 | 25, 32, 36, 37, 40, 41 | syl32anc 1379 |
1
β’ (π β (πβπΌ) β β) |