Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . 6
β’ ((πΌ + 1) = π½ β (πβ(πΌ + 1)) = (πβπ½)) |
2 | 1 | olcd 873 |
. . . . 5
β’ ((πΌ + 1) = π½ β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½))) |
3 | 2 | a1d 25 |
. . . 4
β’ ((πΌ + 1) = π½ β (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½)))) |
4 | | elfzoelz 13581 |
. . . . . . . . . . 11
β’ (πΌ β (0..^π) β πΌ β β€) |
5 | | elfzoelz 13581 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β π½ β β€) |
6 | | zltp1le 12561 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β β€ β§ π½ β β€) β (πΌ < π½ β (πΌ + 1) β€ π½)) |
7 | 6 | biimpcd 249 |
. . . . . . . . . . . . . . . 16
β’ (πΌ < π½ β ((πΌ β β€ β§ π½ β β€) β (πΌ + 1) β€ π½)) |
8 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((πΌ < π½ β§ Β¬ (πΌ + 1) = π½) β ((πΌ β β€ β§ π½ β β€) β (πΌ + 1) β€ π½)) |
9 | 8 | impcom 409 |
. . . . . . . . . . . . . 14
β’ (((πΌ β β€ β§ π½ β β€) β§ (πΌ < π½ β§ Β¬ (πΌ + 1) = π½)) β (πΌ + 1) β€ π½) |
10 | | df-ne 2941 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ + 1) β π½ β Β¬ (πΌ + 1) = π½) |
11 | | necom 2994 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ + 1) β π½ β π½ β (πΌ + 1)) |
12 | 10, 11 | sylbb1 236 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(πΌ + 1) = π½ β π½ β (πΌ + 1)) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((πΌ < π½ β§ Β¬ (πΌ + 1) = π½) β π½ β (πΌ + 1)) |
14 | 13 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((πΌ β β€ β§ π½ β β€) β§ (πΌ < π½ β§ Β¬ (πΌ + 1) = π½)) β π½ β (πΌ + 1)) |
15 | 9, 14 | jca 513 |
. . . . . . . . . . . . 13
β’ (((πΌ β β€ β§ π½ β β€) β§ (πΌ < π½ β§ Β¬ (πΌ + 1) = π½)) β ((πΌ + 1) β€ π½ β§ π½ β (πΌ + 1))) |
16 | | peano2z 12552 |
. . . . . . . . . . . . . . . . 17
β’ (πΌ β β€ β (πΌ + 1) β
β€) |
17 | 16 | zred 12615 |
. . . . . . . . . . . . . . . 16
β’ (πΌ β β€ β (πΌ + 1) β
β) |
18 | | zre 12511 |
. . . . . . . . . . . . . . . 16
β’ (π½ β β€ β π½ β
β) |
19 | 17, 18 | anim12i 614 |
. . . . . . . . . . . . . . 15
β’ ((πΌ β β€ β§ π½ β β€) β ((πΌ + 1) β β β§ π½ β
β)) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((πΌ β β€ β§ π½ β β€) β§ (πΌ < π½ β§ Β¬ (πΌ + 1) = π½)) β ((πΌ + 1) β β β§ π½ β β)) |
21 | | ltlen 11264 |
. . . . . . . . . . . . . 14
β’ (((πΌ + 1) β β β§ π½ β β) β ((πΌ + 1) < π½ β ((πΌ + 1) β€ π½ β§ π½ β (πΌ + 1)))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
β’ (((πΌ β β€ β§ π½ β β€) β§ (πΌ < π½ β§ Β¬ (πΌ + 1) = π½)) β ((πΌ + 1) < π½ β ((πΌ + 1) β€ π½ β§ π½ β (πΌ + 1)))) |
23 | 15, 22 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((πΌ β β€ β§ π½ β β€) β§ (πΌ < π½ β§ Β¬ (πΌ + 1) = π½)) β (πΌ + 1) < π½) |
24 | 23 | ex 414 |
. . . . . . . . . . 11
β’ ((πΌ β β€ β§ π½ β β€) β ((πΌ < π½ β§ Β¬ (πΌ + 1) = π½) β (πΌ + 1) < π½)) |
25 | 4, 5, 24 | syl2an 597 |
. . . . . . . . . 10
β’ ((πΌ β (0..^π) β§ π½ β (0..^π)) β ((πΌ < π½ β§ Β¬ (πΌ + 1) = π½) β (πΌ + 1) < π½)) |
26 | 25 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β ((πΌ < π½ β§ Β¬ (πΌ + 1) = π½) β (πΌ + 1) < π½)) |
27 | | iccpartiun.m |
. . . . . . . . . . 11
β’ (π β π β β) |
28 | | iccpartiun.p |
. . . . . . . . . . 11
β’ (π β π β (RePartβπ)) |
29 | 27, 28 | iccpartgt 45709 |
. . . . . . . . . 10
β’ (π β βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ))) |
30 | | fzofzp1 13678 |
. . . . . . . . . . 11
β’ (πΌ β (0..^π) β (πΌ + 1) β (0...π)) |
31 | | elfzofz 13597 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β π½ β (0...π)) |
32 | | breq1 5112 |
. . . . . . . . . . . . 13
β’ (π = (πΌ + 1) β (π < π β (πΌ + 1) < π)) |
33 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = (πΌ + 1) β (πβπ) = (πβ(πΌ + 1))) |
34 | 33 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (π = (πΌ + 1) β ((πβπ) < (πβπ) β (πβ(πΌ + 1)) < (πβπ))) |
35 | 32, 34 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (πΌ + 1) β ((π < π β (πβπ) < (πβπ)) β ((πΌ + 1) < π β (πβ(πΌ + 1)) < (πβπ)))) |
36 | | breq2 5113 |
. . . . . . . . . . . . 13
β’ (π = π½ β ((πΌ + 1) < π β (πΌ + 1) < π½)) |
37 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π½ β (πβπ) = (πβπ½)) |
38 | 37 | breq2d 5121 |
. . . . . . . . . . . . 13
β’ (π = π½ β ((πβ(πΌ + 1)) < (πβπ) β (πβ(πΌ + 1)) < (πβπ½))) |
39 | 36, 38 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π½ β (((πΌ + 1) < π β (πβ(πΌ + 1)) < (πβπ)) β ((πΌ + 1) < π½ β (πβ(πΌ + 1)) < (πβπ½)))) |
40 | 35, 39 | rspc2v 3592 |
. . . . . . . . . . 11
β’ (((πΌ + 1) β (0...π) β§ π½ β (0...π)) β (βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ)) β ((πΌ + 1) < π½ β (πβ(πΌ + 1)) < (πβπ½)))) |
41 | 30, 31, 40 | syl2an 597 |
. . . . . . . . . 10
β’ ((πΌ β (0..^π) β§ π½ β (0..^π)) β (βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ)) β ((πΌ + 1) < π½ β (πβ(πΌ + 1)) < (πβπ½)))) |
42 | 29, 41 | mpan9 508 |
. . . . . . . . 9
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β ((πΌ + 1) < π½ β (πβ(πΌ + 1)) < (πβπ½))) |
43 | 26, 42 | syld 47 |
. . . . . . . 8
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β ((πΌ < π½ β§ Β¬ (πΌ + 1) = π½) β (πβ(πΌ + 1)) < (πβπ½))) |
44 | 43 | expdimp 454 |
. . . . . . 7
β’ (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β (Β¬ (πΌ + 1) = π½ β (πβ(πΌ + 1)) < (πβπ½))) |
45 | 44 | impcom 409 |
. . . . . 6
β’ ((Β¬
(πΌ + 1) = π½ β§ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½)) β (πβ(πΌ + 1)) < (πβπ½)) |
46 | 45 | orcd 872 |
. . . . 5
β’ ((Β¬
(πΌ + 1) = π½ β§ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½)) β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½))) |
47 | 46 | ex 414 |
. . . 4
β’ (Β¬
(πΌ + 1) = π½ β (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½)))) |
48 | 3, 47 | pm2.61i 182 |
. . 3
β’ (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½))) |
49 | 27 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β π β β) |
50 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β π β (RePartβπ)) |
51 | 30 | adantr 482 |
. . . . . . . 8
β’ ((πΌ β (0..^π) β§ π½ β (0..^π)) β (πΌ + 1) β (0...π)) |
52 | 51 | adantl 483 |
. . . . . . 7
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β (πΌ + 1) β (0...π)) |
53 | 49, 50, 52 | iccpartxr 45701 |
. . . . . 6
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β (πβ(πΌ + 1)) β
β*) |
54 | 31 | adantl 483 |
. . . . . . . 8
β’ ((πΌ β (0..^π) β§ π½ β (0..^π)) β π½ β (0...π)) |
55 | 54 | adantl 483 |
. . . . . . 7
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β π½ β (0...π)) |
56 | 49, 50, 55 | iccpartxr 45701 |
. . . . . 6
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β (πβπ½) β
β*) |
57 | 53, 56 | jca 513 |
. . . . 5
β’ ((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β ((πβ(πΌ + 1)) β β* β§
(πβπ½) β
β*)) |
58 | 57 | adantr 482 |
. . . 4
β’ (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β ((πβ(πΌ + 1)) β β* β§
(πβπ½) β
β*)) |
59 | | xrleloe 13072 |
. . . 4
β’ (((πβ(πΌ + 1)) β β* β§
(πβπ½) β β*) β ((πβ(πΌ + 1)) β€ (πβπ½) β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½)))) |
60 | 58, 59 | syl 17 |
. . 3
β’ (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β ((πβ(πΌ + 1)) β€ (πβπ½) β ((πβ(πΌ + 1)) < (πβπ½) β¨ (πβ(πΌ + 1)) = (πβπ½)))) |
61 | 48, 60 | mpbird 257 |
. 2
β’ (((π β§ (πΌ β (0..^π) β§ π½ β (0..^π))) β§ πΌ < π½) β (πβ(πΌ + 1)) β€ (πβπ½)) |
62 | 61 | exp31 421 |
1
β’ (π β ((πΌ β (0..^π) β§ π½ β (0..^π)) β (πΌ < π½ β (πβ(πΌ + 1)) β€ (πβπ½)))) |