Step | Hyp | Ref
| Expression |
1 | | ral0 4513 |
. . . 4
β’
βπ β
β
(πβ0) <
(πβπ) |
2 | | oveq2 7420 |
. . . . . 6
β’ (π = 1 β (1..^π) = (1..^1)) |
3 | | fzo0 13661 |
. . . . . 6
β’ (1..^1) =
β
|
4 | 2, 3 | eqtrdi 2787 |
. . . . 5
β’ (π = 1 β (1..^π) = β
) |
5 | 4 | raleqdv 3324 |
. . . 4
β’ (π = 1 β (βπ β (1..^π)(πβ0) < (πβπ) β βπ β β
(πβ0) < (πβπ))) |
6 | 1, 5 | mpbiri 257 |
. . 3
β’ (π = 1 β βπ β (1..^π)(πβ0) < (πβπ)) |
7 | 6 | a1d 25 |
. 2
β’ (π = 1 β (π β βπ β (1..^π)(πβ0) < (πβπ))) |
8 | | iccpartgtprec.m |
. . . . . 6
β’ (π β π β β) |
9 | | iccpartgtprec.p |
. . . . . 6
β’ (π β π β (RePartβπ)) |
10 | 8 | nnnn0d 12537 |
. . . . . . 7
β’ (π β π β
β0) |
11 | | 0elfz 13603 |
. . . . . . 7
β’ (π β β0
β 0 β (0...π)) |
12 | 10, 11 | syl 17 |
. . . . . 6
β’ (π β 0 β (0...π)) |
13 | 8, 9, 12 | iccpartxr 46387 |
. . . . 5
β’ (π β (πβ0) β
β*) |
14 | 13 | adantr 480 |
. . . 4
β’ ((π β§ Β¬ π = 1) β (πβ0) β
β*) |
15 | | elxr 13101 |
. . . . 5
β’ ((πβ0) β
β* β ((πβ0) β β β¨ (πβ0) = +β β¨ (πβ0) =
-β)) |
16 | | 0zd 12575 |
. . . . . . . . 9
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β 0 β β€) |
17 | | elfzouz 13641 |
. . . . . . . . . . 11
β’ (π β (1..^π) β π β
(β€β₯β1)) |
18 | | 0p1e1 12339 |
. . . . . . . . . . . 12
β’ (0 + 1) =
1 |
19 | 18 | fveq2i 6895 |
. . . . . . . . . . 11
β’
(β€β₯β(0 + 1)) =
(β€β₯β1) |
20 | 17, 19 | eleqtrrdi 2843 |
. . . . . . . . . 10
β’ (π β (1..^π) β π β (β€β₯β(0 +
1))) |
21 | 20 | adantl 481 |
. . . . . . . . 9
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β π β (β€β₯β(0 +
1))) |
22 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (πβπ) = (πβ0)) |
23 | 22 | eqcomd 2737 |
. . . . . . . . . . . . 13
β’ (π = 0 β (πβ0) = (πβπ)) |
24 | 23 | eleq1d 2817 |
. . . . . . . . . . . 12
β’ (π = 0 β ((πβ0) β β β (πβπ) β β)) |
25 | 24 | biimpcd 248 |
. . . . . . . . . . 11
β’ ((πβ0) β β β
(π = 0 β (πβπ) β β)) |
26 | 25 | ad3antrrr 727 |
. . . . . . . . . 10
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...π)) β (π = 0 β (πβπ) β β)) |
27 | 8 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (1..^π) β§ (π β (0...π) β§ π β 0))) β π β β) |
28 | 9 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (1..^π) β§ (π β (0...π) β§ π β 0))) β π β (RePartβπ)) |
29 | | elfz2nn0 13597 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0...π) β (π β β0 β§ π β β0
β§ π β€ π)) |
30 | | elfzo2 13640 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1..^π) β (π β (β€β₯β1)
β§ π β β€
β§ π < π)) |
31 | | simpl1 1190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ π β
β0 β§ π
β€ π) β§ (π β
(β€β₯β1) β§ π β β€ β§ π < π)) β π β β0) |
32 | | simpr2 1194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β0
β§ π β
β0 β§ π
β€ π) β§ (π β
(β€β₯β1) β§ π β β€ β§ π < π)) β π β β€) |
33 | | nn0ge0 12502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β0
β 0 β€ π) |
34 | | 0red 11222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β
(β€β₯β1) β§ π β β€) β 0 β
β) |
35 | | eluzelre 12838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β1) β π β β) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β
(β€β₯β1) β§ π β β€) β π β β) |
37 | | zre 12567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β β€ β π β
β) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β
(β€β₯β1) β§ π β β€) β π β β) |
39 | | lelttr 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((0
β β β§ π
β β β§ π
β β) β ((0 β€ π β§ π < π) β 0 < π)) |
40 | 34, 36, 38, 39 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β
(β€β₯β1) β§ π β β€) β ((0 β€ π β§ π < π) β 0 < π)) |
41 | 40 | expcomd 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β
(β€β₯β1) β§ π β β€) β (π < π β (0 β€ π β 0 < π))) |
42 | 41 | 3impia 1116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(β€β₯β1) β§ π β β€ β§ π < π) β (0 β€ π β 0 < π)) |
43 | 33, 42 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β0
β ((π β
(β€β₯β1) β§ π β β€ β§ π < π) β 0 < π)) |
44 | 43 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β ((π β
(β€β₯β1) β§ π β β€ β§ π < π) β 0 < π)) |
45 | 44 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β0
β§ π β
β0 β§ π
β€ π) β§ (π β
(β€β₯β1) β§ π β β€ β§ π < π)) β 0 < π) |
46 | | elnnz 12573 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (π β β€ β§ 0 <
π)) |
47 | 32, 45, 46 | sylanbrc 582 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ π β
β0 β§ π
β€ π) β§ (π β
(β€β₯β1) β§ π β β€ β§ π < π)) β π β β) |
48 | | nn0re 12486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β β0
β π β
β) |
49 | 48 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β
(β€β₯β1) β§ π β β€) β§ (π β β0 β§ π β β0))
β π β
β) |
50 | | nn0re 12486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β β0
β π β
β) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β β0
β§ π β
β0) β π β β) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β
(β€β₯β1) β§ π β β€) β§ (π β β0 β§ π β β0))
β π β
β) |
53 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β
(β€β₯β1) β§ π β β€) β§ (π β β0 β§ π β β0))
β π β
β) |
54 | | lelttr 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β β β§ π β β β§ π β β) β ((π β€ π β§ π < π) β π < π)) |
55 | 54 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β β β§ π β β β§ π β β) β (π β€ π β (π < π β π < π))) |
56 | 49, 52, 53, 55 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β
(β€β₯β1) β§ π β β€) β§ (π β β0 β§ π β β0))
β (π β€ π β (π < π β π < π))) |
57 | 56 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β
(β€β₯β1) β (π β β€ β ((π β β0 β§ π β β0)
β (π β€ π β (π < π β π < π))))) |
58 | 57 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β
(β€β₯β1) β (π β β€ β (π β€ π β ((π β β0 β§ π β β0)
β (π < π β π < π))))) |
59 | 58 | com35 98 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β
(β€β₯β1) β (π β β€ β (π < π β ((π β β0 β§ π β β0)
β (π β€ π β π < π))))) |
60 | 59 | 3imp 1110 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β
(β€β₯β1) β§ π β β€ β§ π < π) β ((π β β0 β§ π β β0)
β (π β€ π β π < π))) |
61 | 60 | expdcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β (π β
β0 β ((π β (β€β₯β1)
β§ π β β€
β§ π < π) β (π β€ π β π < π)))) |
62 | 61 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β (π β
β0 β (π β€ π β ((π β (β€β₯β1)
β§ π β β€
β§ π < π) β π < π)))) |
63 | 62 | 3imp1 1346 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ π β
β0 β§ π
β€ π) β§ (π β
(β€β₯β1) β§ π β β€ β§ π < π)) β π < π) |
64 | | elfzo0 13678 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β (π β β0 β§ π β β β§ π < π)) |
65 | 31, 47, 63, 64 | syl3anbrc 1342 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β0
β§ π β
β0 β§ π
β€ π) β§ (π β
(β€β₯β1) β§ π β β€ β§ π < π)) β π β (0..^π)) |
66 | 65 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β ((π β
(β€β₯β1) β§ π β β€ β§ π < π) β π β (0..^π))) |
67 | 30, 66 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β (π β (1..^π) β π β (0..^π))) |
68 | 29, 67 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...π) β (π β (1..^π) β π β (0..^π))) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...π) β§ π β 0) β (π β (1..^π) β π β (0..^π))) |
70 | 69 | impcom 407 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1..^π) β§ (π β (0...π) β§ π β 0)) β π β (0..^π)) |
71 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...π) β§ π β 0) β π β 0) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1..^π) β§ (π β (0...π) β§ π β 0)) β π β 0) |
73 | | fzo1fzo0n0 13688 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1..^π) β (π β (0..^π) β§ π β 0)) |
74 | 70, 72, 73 | sylanbrc 582 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1..^π) β§ (π β (0...π) β§ π β 0)) β π β (1..^π)) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (1..^π) β§ (π β (0...π) β§ π β 0))) β π β (1..^π)) |
76 | 27, 28, 75 | iccpartipre 46389 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (1..^π) β§ (π β (0...π) β§ π β 0))) β (πβπ) β β) |
77 | 76 | exp32 420 |
. . . . . . . . . . . . 13
β’ (π β (π β (1..^π) β ((π β (0...π) β§ π β 0) β (πβπ) β β))) |
78 | 77 | ad2antrl 725 |
. . . . . . . . . . . 12
β’ (((πβ0) β β β§
(π β§ Β¬ π = 1)) β (π β (1..^π) β ((π β (0...π) β§ π β 0) β (πβπ) β β))) |
79 | 78 | imp 406 |
. . . . . . . . . . 11
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β ((π β (0...π) β§ π β 0) β (πβπ) β β)) |
80 | 79 | expdimp 452 |
. . . . . . . . . 10
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...π)) β (π β 0 β (πβπ) β β)) |
81 | 26, 80 | pm2.61dne 3027 |
. . . . . . . . 9
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...π)) β (πβπ) β β) |
82 | 8 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π = 1) β π β β) |
83 | 82 | ad3antlr 728 |
. . . . . . . . . . 11
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...(π β 1))) β π β β) |
84 | 9 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π = 1) β π β (RePartβπ)) |
85 | 84 | ad3antlr 728 |
. . . . . . . . . . 11
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...(π β 1))) β π β (RePartβπ)) |
86 | | elfzoelz 13637 |
. . . . . . . . . . . . . . . 16
β’ (π β (1..^π) β π β β€) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β π β β€) |
88 | | fzoval 13638 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β
(0..^π) = (0...(π β 1))) |
89 | 88 | eqcomd 2737 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β
(0...(π β 1)) =
(0..^π)) |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (0...(π β 1)) = (0..^π)) |
91 | 90 | eleq2d 2818 |
. . . . . . . . . . . . 13
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (π β (0...(π β 1)) β π β (0..^π))) |
92 | | elfzouz2 13652 |
. . . . . . . . . . . . . . . 16
β’ (π β (1..^π) β π β (β€β₯βπ)) |
93 | 92 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β π β (β€β₯βπ)) |
94 | | fzoss2 13665 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (0..^π) β (0..^π)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (0..^π) β (0..^π)) |
96 | 95 | sseld 3982 |
. . . . . . . . . . . . 13
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (π β (0..^π) β π β (0..^π))) |
97 | 91, 96 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (π β (0...(π β 1)) β π β (0..^π))) |
98 | 97 | imp 406 |
. . . . . . . . . . 11
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...(π β 1))) β π β (0..^π)) |
99 | | iccpartimp 46385 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (RePartβπ) β§ π β (0..^π)) β (π β (β*
βm (0...π))
β§ (πβπ) < (πβ(π + 1)))) |
100 | 83, 85, 98, 99 | syl3anc 1370 |
. . . . . . . . . 10
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...(π β 1))) β (π β (β*
βm (0...π))
β§ (πβπ) < (πβ(π + 1)))) |
101 | 100 | simprd 495 |
. . . . . . . . 9
β’
(((((πβ0)
β β β§ (π β§
Β¬ π = 1)) β§ π β (1..^π)) β§ π β (0...(π β 1))) β (πβπ) < (πβ(π + 1))) |
102 | 16, 21, 81, 101 | smonoord 46339 |
. . . . . . . 8
β’ ((((πβ0) β β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (πβ0) < (πβπ)) |
103 | 102 | ralrimiva 3145 |
. . . . . . 7
β’ (((πβ0) β β β§
(π β§ Β¬ π = 1)) β βπ β (1..^π)(πβ0) < (πβπ)) |
104 | 103 | ex 412 |
. . . . . 6
β’ ((πβ0) β β β
((π β§ Β¬ π = 1) β βπ β (1..^π)(πβ0) < (πβπ))) |
105 | | lbfzo0 13677 |
. . . . . . . . . . . . . . . 16
β’ (0 β
(0..^π) β π β
β) |
106 | 8, 105 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β (0..^π)) |
107 | 8, 9, 106 | 3jca 1127 |
. . . . . . . . . . . . . 14
β’ (π β (π β β β§ π β (RePartβπ) β§ 0 β (0..^π))) |
108 | 107 | ad2antrl 725 |
. . . . . . . . . . . . 13
β’ (((πβ0) = +β β§
(π β§ Β¬ π = 1)) β (π β β β§ π β (RePartβπ) β§ 0 β (0..^π))) |
109 | 108 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (π β β β§ π β (RePartβπ) β§ 0 β (0..^π))) |
110 | | iccpartimp 46385 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (RePartβπ) β§ 0 β (0..^π)) β (π β (β*
βm (0...π))
β§ (πβ0) <
(πβ(0 +
1)))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . 11
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (π β (β*
βm (0...π))
β§ (πβ0) <
(πβ(0 +
1)))) |
112 | 111 | simprd 495 |
. . . . . . . . . 10
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (πβ0) < (πβ(0 + 1))) |
113 | | breq1 5152 |
. . . . . . . . . . . 12
β’ ((πβ0) = +β β
((πβ0) < (πβ(0 + 1)) β +β
< (πβ(0 +
1)))) |
114 | 113 | adantr 480 |
. . . . . . . . . . 11
β’ (((πβ0) = +β β§
(π β§ Β¬ π = 1)) β ((πβ0) < (πβ(0 + 1)) β +β
< (πβ(0 +
1)))) |
115 | 114 | adantr 480 |
. . . . . . . . . 10
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β ((πβ0) < (πβ(0 + 1)) β +β < (πβ(0 +
1)))) |
116 | 112, 115 | mpbid 231 |
. . . . . . . . 9
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β +β < (πβ(0 + 1))) |
117 | 8 | ad2antrl 725 |
. . . . . . . . . . . 12
β’ (((πβ0) = +β β§
(π β§ Β¬ π = 1)) β π β β) |
118 | 117 | adantr 480 |
. . . . . . . . . . 11
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β π β β) |
119 | 9 | ad2antrl 725 |
. . . . . . . . . . . 12
β’ (((πβ0) = +β β§
(π β§ Β¬ π = 1)) β π β (RePartβπ)) |
120 | 119 | adantr 480 |
. . . . . . . . . . 11
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β π β (RePartβπ)) |
121 | | 1nn0 12493 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β0 |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β 1 β
β0) |
123 | | nnnn0 12484 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β0) |
124 | | nnge1 12245 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β 1 β€
π) |
125 | 122, 123,
124 | 3jca 1127 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (1 β
β0 β§ π
β β0 β§ 1 β€ π)) |
126 | 8, 125 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (1 β
β0 β§ π
β β0 β§ 1 β€ π)) |
127 | | elfz2nn0 13597 |
. . . . . . . . . . . . . . 15
β’ (1 β
(0...π) β (1 β
β0 β§ π
β β0 β§ 1 β€ π)) |
128 | 126, 127 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π β 1 β (0...π)) |
129 | 18, 128 | eqeltrid 2836 |
. . . . . . . . . . . . 13
β’ (π β (0 + 1) β (0...π)) |
130 | 129 | ad2antrl 725 |
. . . . . . . . . . . 12
β’ (((πβ0) = +β β§
(π β§ Β¬ π = 1)) β (0 + 1) β
(0...π)) |
131 | 130 | adantr 480 |
. . . . . . . . . . 11
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (0 + 1) β (0...π)) |
132 | 118, 120,
131 | iccpartxr 46387 |
. . . . . . . . . 10
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (πβ(0 + 1)) β
β*) |
133 | | pnfnlt 13113 |
. . . . . . . . . 10
β’ ((πβ(0 + 1)) β
β* β Β¬ +β < (πβ(0 + 1))) |
134 | 132, 133 | syl 17 |
. . . . . . . . 9
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β Β¬ +β < (πβ(0 +
1))) |
135 | 116, 134 | pm2.21dd 194 |
. . . . . . . 8
β’ ((((πβ0) = +β β§
(π β§ Β¬ π = 1)) β§ π β (1..^π)) β (πβ0) < (πβπ)) |
136 | 135 | ralrimiva 3145 |
. . . . . . 7
β’ (((πβ0) = +β β§
(π β§ Β¬ π = 1)) β βπ β (1..^π)(πβ0) < (πβπ)) |
137 | 136 | ex 412 |
. . . . . 6
β’ ((πβ0) = +β β
((π β§ Β¬ π = 1) β βπ β (1..^π)(πβ0) < (πβπ))) |
138 | 8 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1..^π)) β π β β) |
139 | 9 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1..^π)) β π β (RePartβπ)) |
140 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1..^π)) β π β (1..^π)) |
141 | 138, 139,
140 | iccpartipre 46389 |
. . . . . . . . . . 11
β’ ((π β§ π β (1..^π)) β (πβπ) β β) |
142 | | mnflt 13108 |
. . . . . . . . . . 11
β’ ((πβπ) β β β -β < (πβπ)) |
143 | 141, 142 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (1..^π)) β -β < (πβπ)) |
144 | 143 | ralrimiva 3145 |
. . . . . . . . 9
β’ (π β βπ β (1..^π)-β < (πβπ)) |
145 | 144 | ad2antrl 725 |
. . . . . . . 8
β’ (((πβ0) = -β β§
(π β§ Β¬ π = 1)) β βπ β (1..^π)-β < (πβπ)) |
146 | | breq1 5152 |
. . . . . . . . . 10
β’ ((πβ0) = -β β
((πβ0) < (πβπ) β -β < (πβπ))) |
147 | 146 | adantr 480 |
. . . . . . . . 9
β’ (((πβ0) = -β β§
(π β§ Β¬ π = 1)) β ((πβ0) < (πβπ) β -β < (πβπ))) |
148 | 147 | ralbidv 3176 |
. . . . . . . 8
β’ (((πβ0) = -β β§
(π β§ Β¬ π = 1)) β (βπ β (1..^π)(πβ0) < (πβπ) β βπ β (1..^π)-β < (πβπ))) |
149 | 145, 148 | mpbird 256 |
. . . . . . 7
β’ (((πβ0) = -β β§
(π β§ Β¬ π = 1)) β βπ β (1..^π)(πβ0) < (πβπ)) |
150 | 149 | ex 412 |
. . . . . 6
β’ ((πβ0) = -β β
((π β§ Β¬ π = 1) β βπ β (1..^π)(πβ0) < (πβπ))) |
151 | 104, 137,
150 | 3jaoi 1426 |
. . . . 5
β’ (((πβ0) β β β¨
(πβ0) = +β β¨
(πβ0) = -β)
β ((π β§ Β¬ π = 1) β βπ β (1..^π)(πβ0) < (πβπ))) |
152 | 15, 151 | sylbi 216 |
. . . 4
β’ ((πβ0) β
β* β ((π β§ Β¬ π = 1) β βπ β (1..^π)(πβ0) < (πβπ))) |
153 | 14, 152 | mpcom 38 |
. . 3
β’ ((π β§ Β¬ π = 1) β βπ β (1..^π)(πβ0) < (πβπ)) |
154 | 153 | expcom 413 |
. 2
β’ (Β¬
π = 1 β (π β βπ β (1..^π)(πβ0) < (πβπ))) |
155 | 7, 154 | pm2.61i 182 |
1
β’ (π β βπ β (1..^π)(πβ0) < (πβπ)) |