Step | Hyp | Ref
| Expression |
1 | | elioo3g 13302 |
. . 3
β’ (π β ((πβπΌ)(,)(πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1))))) |
2 | | iccpartnel.x |
. . . . . . 7
β’ (π β π β ran π) |
3 | | iccpartnel.p |
. . . . . . . . 9
β’ (π β π β (RePartβπ)) |
4 | | iccpartnel.m |
. . . . . . . . . . 11
β’ (π β π β β) |
5 | | iccpart 45698 |
. . . . . . . . . . 11
β’ (π β β β (π β (RePartβπ) β (π β (β*
βm (0...π))
β§ βπ β
(0..^π)(πβπ) < (πβ(π + 1))))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (RePartβπ) β (π β (β*
βm (0...π))
β§ βπ β
(0..^π)(πβπ) < (πβ(π + 1))))) |
7 | | elmapfn 8809 |
. . . . . . . . . . 11
β’ (π β (β*
βm (0...π))
β π Fn (0...π)) |
8 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β (β*
βm (0...π))
β§ βπ β
(0..^π)(πβπ) < (πβ(π + 1))) β π Fn (0...π)) |
9 | 6, 8 | syl6bi 253 |
. . . . . . . . 9
β’ (π β (π β (RePartβπ) β π Fn (0...π))) |
10 | 3, 9 | mpd 15 |
. . . . . . . 8
β’ (π β π Fn (0...π)) |
11 | | fvelrnb 6907 |
. . . . . . . 8
β’ (π Fn (0...π) β (π β ran π β βπ₯ β (0...π)(πβπ₯) = π)) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ (π β (π β ran π β βπ₯ β (0...π)(πβπ₯) = π)) |
13 | 2, 12 | mpbid 231 |
. . . . . 6
β’ (π β βπ₯ β (0...π)(πβπ₯) = π) |
14 | | elfzelz 13450 |
. . . . . . . . . . . . 13
β’ (π₯ β (0...π) β π₯ β β€) |
15 | 14 | zred 12615 |
. . . . . . . . . . . 12
β’ (π₯ β (0...π) β π₯ β β) |
16 | 15 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (0...π)) β π₯ β β) |
17 | | elfzoelz 13581 |
. . . . . . . . . . . 12
β’ (πΌ β (0..^π) β πΌ β β€) |
18 | 17 | zred 12615 |
. . . . . . . . . . 11
β’ (πΌ β (0..^π) β πΌ β β) |
19 | | lelttric 11270 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ πΌ β β) β (π₯ β€ πΌ β¨ πΌ < π₯)) |
20 | 16, 18, 19 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (π₯ β€ πΌ β¨ πΌ < π₯)) |
21 | | breq2 5113 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ₯) = π β ((πβπΌ) < (πβπ₯) β (πβπΌ) < π)) |
22 | | breq1 5112 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ₯) = π β ((πβπ₯) < (πβ(πΌ + 1)) β π < (πβ(πΌ + 1)))) |
23 | 21, 22 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ₯) = π β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β ((πβπΌ) < π β§ π < (πβ(πΌ + 1))))) |
24 | | leloe 11249 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β β β§ πΌ β β) β (π₯ β€ πΌ β (π₯ < πΌ β¨ π₯ = πΌ))) |
25 | 16, 18, 24 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (π₯ β€ πΌ β (π₯ < πΌ β¨ π₯ = πΌ))) |
26 | 4, 3 | iccpartgt 45709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β (0...π)) β βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ))) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ))) |
29 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β (0...π)) β π₯ β (0...π)) |
30 | | elfzofz 13597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΌ β (0..^π) β πΌ β (0...π)) |
31 | | breq1 5112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π₯ β (π < π β π₯ < π)) |
32 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
33 | 32 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π₯ β ((πβπ) < (πβπ) β (πβπ₯) < (πβπ))) |
34 | 31, 33 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π₯ β ((π < π β (πβπ) < (πβπ)) β (π₯ < π β (πβπ₯) < (πβπ)))) |
35 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = πΌ β (π₯ < π β π₯ < πΌ)) |
36 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = πΌ β (πβπ) = (πβπΌ)) |
37 | 36 | breq2d 5121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = πΌ β ((πβπ₯) < (πβπ) β (πβπ₯) < (πβπΌ))) |
38 | 35, 37 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = πΌ β ((π₯ < π β (πβπ₯) < (πβπ)) β (π₯ < πΌ β (πβπ₯) < (πβπΌ)))) |
39 | 34, 38 | rspc2v 3592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ β (0...π) β§ πΌ β (0...π)) β (βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ)) β (π₯ < πΌ β (πβπ₯) < (πβπΌ)))) |
40 | 29, 30, 39 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ)) β (π₯ < πΌ β (πβπ₯) < (πβπΌ)))) |
41 | 28, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (π₯ < πΌ β (πβπ₯) < (πβπΌ))) |
42 | | pm3.35 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π₯ < πΌ β§ (π₯ < πΌ β (πβπ₯) < (πβπΌ))) β (πβπ₯) < (πβπΌ)) |
43 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ π₯ β (0...π)) β π β β) |
44 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ π₯ β (0...π)) β π β (RePartβπ)) |
45 | 43, 44, 29 | iccpartxr 45701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π₯ β (0...π)) β (πβπ₯) β
β*) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (πβπ₯) β
β*) |
47 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (πβπΌ) β
β*) |
48 | | xrltle 13077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((πβπ₯) β β* β§ (πβπΌ) β β*) β ((πβπ₯) < (πβπΌ) β (πβπ₯) β€ (πβπΌ))) |
49 | 46, 47, 48 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β ((πβπ₯) < (πβπΌ) β (πβπ₯) β€ (πβπΌ))) |
50 | | xrlenlt 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((πβπ₯) β β* β§ (πβπΌ) β β*) β ((πβπ₯) β€ (πβπΌ) β Β¬ (πβπΌ) < (πβπ₯))) |
51 | 46, 47, 50 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β ((πβπ₯) β€ (πβπΌ) β Β¬ (πβπΌ) < (πβπ₯))) |
52 | 49, 51 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β ((πβπ₯) < (πβπΌ) β Β¬ (πβπΌ) < (πβπ₯))) |
53 | 52 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πβπ₯) < (πβπΌ) β Β¬ (πβπΌ) < (πβπ₯)))) |
54 | 53 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((πβπ₯) < (πβπΌ) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ (πβπΌ) < (πβπ₯)))) |
55 | 54 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((πβπ₯) < (πβπΌ) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ (πβπΌ) < (πβπ₯))) |
56 | 55 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((πβπ₯) < (πβπΌ) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β Β¬ (πβπΌ) < (πβπ₯)) |
57 | 56 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((πβπ₯) < (πβπΌ) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
58 | 57 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((πβπ₯) < (πβπΌ) β§ ((π β§ π₯ β (0...π)) β§ πΌ β (0..^π))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
59 | 58 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ₯) < (πβπΌ) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
60 | 42, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ < πΌ β§ (π₯ < πΌ β (πβπ₯) < (πβπΌ))) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
61 | 60 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ < πΌ β ((π₯ < πΌ β (πβπ₯) < (πβπΌ)) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
62 | 61 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((π₯ < πΌ β (πβπ₯) < (πβπΌ)) β (π₯ < πΌ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
63 | 41, 62 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (π₯ < πΌ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
64 | 63 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ < πΌ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
65 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ = πΌ β (πβπ₯) = (πβπΌ)) |
66 | 65 | breq2d 5121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = πΌ β ((πβπΌ) < (πβπ₯) β (πβπΌ) < (πβπΌ))) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ = πΌ β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β ((πβπΌ) < (πβπ₯) β (πβπΌ) < (πβπΌ))) |
68 | | xrltnr 13048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πβπΌ) β β* β Β¬
(πβπΌ) < (πβπΌ)) |
69 | 68 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ (πβπΌ) < (πβπΌ)) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ = πΌ β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β Β¬ (πβπΌ) < (πβπΌ)) |
71 | 70 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ = πΌ β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β ((πβπΌ) < (πβπΌ) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
72 | 67, 71 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ = πΌ β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
73 | 72 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = πΌ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
74 | 73 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = πΌ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
75 | 64, 74 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ < πΌ β¨ π₯ = πΌ) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((π₯ < πΌ β¨ π₯ = πΌ) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
77 | 25, 76 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (π₯ β€ πΌ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
78 | 77 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (π₯ β€ πΌ β ((πβπΌ) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
79 | 78 | com14 96 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπΌ) < (πβπ₯) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (π₯ β€ πΌ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (π₯ β€ πΌ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
81 | 23, 80 | syl6bir 254 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ₯) = π β (((πβπΌ) < π β§ π < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (π₯ β€ πΌ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
82 | 81 | com14 96 |
. . . . . . . . . . . . . . 15
β’ (π₯ β€ πΌ β (((πβπΌ) < π β§ π < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπ₯) = π β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
83 | 82 | com23 86 |
. . . . . . . . . . . . . 14
β’ (π₯ β€ πΌ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < π β§ π < (πβ(πΌ + 1))) β ((πβπ₯) = π β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
84 | 83 | impd 412 |
. . . . . . . . . . . . 13
β’ (π₯ β€ πΌ β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β ((πβπ₯) = π β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
85 | 84 | com24 95 |
. . . . . . . . . . . 12
β’ (π₯ β€ πΌ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πβπ₯) = π β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
86 | 14 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (0...π)) β π₯ β β€) |
87 | | zltp1le 12561 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ β β€ β§ π₯ β β€) β (πΌ < π₯ β (πΌ + 1) β€ π₯)) |
88 | 17, 86, 87 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (πΌ < π₯ β (πΌ + 1) β€ π₯)) |
89 | 17 | peano2zd 12618 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΌ β (0..^π) β (πΌ + 1) β β€) |
90 | 89 | zred 12615 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΌ β (0..^π) β (πΌ + 1) β β) |
91 | | leloe 11249 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΌ + 1) β β β§ π₯ β β) β ((πΌ + 1) β€ π₯ β ((πΌ + 1) < π₯ β¨ (πΌ + 1) = π₯))) |
92 | 90, 16, 91 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πΌ + 1) β€ π₯ β ((πΌ + 1) < π₯ β¨ (πΌ + 1) = π₯))) |
93 | 88, 92 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (πΌ < π₯ β ((πΌ + 1) < π₯ β¨ (πΌ + 1) = π₯))) |
94 | | fzofzp1 13678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΌ β (0..^π) β (πΌ + 1) β (0...π)) |
95 | | breq1 5112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (πΌ + 1) β (π < π β (πΌ + 1) < π)) |
96 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = (πΌ + 1) β (πβπ) = (πβ(πΌ + 1))) |
97 | 96 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (πΌ + 1) β ((πβπ) < (πβπ) β (πβ(πΌ + 1)) < (πβπ))) |
98 | 95, 97 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = (πΌ + 1) β ((π < π β (πβπ) < (πβπ)) β ((πΌ + 1) < π β (πβ(πΌ + 1)) < (πβπ)))) |
99 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π₯ β ((πΌ + 1) < π β (πΌ + 1) < π₯)) |
100 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
101 | 100 | breq2d 5121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π₯ β ((πβ(πΌ + 1)) < (πβπ) β (πβ(πΌ + 1)) < (πβπ₯))) |
102 | 99, 101 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π₯ β (((πΌ + 1) < π β (πβ(πΌ + 1)) < (πβπ)) β ((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯)))) |
103 | 98, 102 | rspc2v 3592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πΌ + 1) β (0...π) β§ π₯ β (0...π)) β (βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ)) β ((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯)))) |
104 | 94, 29, 103 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (βπ β (0...π)βπ β (0...π)(π < π β (πβπ) < (πβπ)) β ((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯)))) |
105 | 28, 104 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯))) |
106 | | pm3.35 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΌ + 1) < π₯ β§ ((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯))) β (πβ(πΌ + 1)) < (πβπ₯)) |
107 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (πβ(πΌ + 1)) β
β*) |
108 | | xrltnsym 13065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πβπ₯) β β* β§ (πβ(πΌ + 1)) β β*) β
((πβπ₯) < (πβ(πΌ + 1)) β Β¬ (πβ(πΌ + 1)) < (πβπ₯))) |
109 | 46, 107, 108 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β ((πβπ₯) < (πβ(πΌ + 1)) β Β¬ (πβ(πΌ + 1)) < (πβπ₯))) |
110 | 109 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ (πβ(πΌ + 1)) < (πβπ₯)) |
111 | 110 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β§ (πβπ₯) < (πβ(πΌ + 1))) β ((πβ(πΌ + 1)) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
112 | 111 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πβπ₯) < (πβ(πΌ + 1)) β ((((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β§ ((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*)) β ((πβ(πΌ + 1)) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
113 | 112 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πβπ₯) < (πβ(πΌ + 1)) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβ(πΌ + 1)) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
114 | 113 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβ(πΌ + 1)) < (πβπ₯) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
115 | 114 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβ(πΌ + 1)) < (πβπ₯) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
116 | 106, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πΌ + 1) < π₯ β§ ((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯))) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
117 | 116 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΌ + 1) < π₯ β (((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯)) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
118 | 117 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πΌ + 1) < π₯ β (πβ(πΌ + 1)) < (πβπ₯)) β ((πΌ + 1) < π₯ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
119 | 105, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πΌ + 1) < π₯ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
120 | 119 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ + 1) < π₯ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
121 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΌ + 1) = π₯ β (πβ(πΌ + 1)) = (πβπ₯)) |
122 | 121 | breq2d 5121 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΌ + 1) = π₯ β ((πβπΌ) < (πβ(πΌ + 1)) β (πβπΌ) < (πβπ₯))) |
123 | 121 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΌ + 1) = π₯ β ((πβ(πΌ + 1)) < (πβ(πΌ + 1)) β (πβπ₯) < (πβ(πΌ + 1)))) |
124 | 122, 123 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΌ + 1) = π₯ β (((πβπΌ) < (πβ(πΌ + 1)) β§ (πβ(πΌ + 1)) < (πβ(πΌ + 1))) β ((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))))) |
125 | | xrltnr 13048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πβ(πΌ + 1)) β β* β
Β¬ (πβ(πΌ + 1)) < (πβ(πΌ + 1))) |
126 | 125 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ (πβ(πΌ + 1)) < (πβ(πΌ + 1))) |
127 | 126 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβ(πΌ + 1)) < (πβ(πΌ + 1)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβ(πΌ + 1)) < (πβ(πΌ + 1)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
129 | 128 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πβπΌ) < (πβ(πΌ + 1)) β§ (πβ(πΌ + 1)) < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
130 | 124, 129 | syl6bir 254 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΌ + 1) = π₯ β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
131 | 130 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΌ + 1) = π₯ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
132 | 131 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ + 1) = π₯ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
133 | 120, 132 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΌ + 1) < π₯ β¨ (πΌ + 1) = π₯) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
134 | 133 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πΌ + 1) < π₯ β¨ (πΌ + 1) = π₯) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
135 | 93, 134 | sylbid 239 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (πΌ < π₯ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
136 | 135 | com23 86 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (πΌ < π₯ β (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
137 | 136 | com14 96 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπΌ) < (πβπ₯) β§ (πβπ₯) < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (πΌ < π₯ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
138 | 23, 137 | syl6bir 254 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ₯) = π β (((πβπΌ) < π β§ π < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (πΌ < π₯ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
139 | 138 | com14 96 |
. . . . . . . . . . . . . . 15
β’ (πΌ < π₯ β (((πβπΌ) < π β§ π < (πβ(πΌ + 1))) β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β ((πβπ₯) = π β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
140 | 139 | com23 86 |
. . . . . . . . . . . . . 14
β’ (πΌ < π₯ β (((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β (((πβπΌ) < π β§ π < (πβ(πΌ + 1))) β ((πβπ₯) = π β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))))) |
141 | 140 | impd 412 |
. . . . . . . . . . . . 13
β’ (πΌ < π₯ β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β ((πβπ₯) = π β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
142 | 141 | com24 95 |
. . . . . . . . . . . 12
β’ (πΌ < π₯ β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πβπ₯) = π β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
143 | 85, 142 | jaoi 856 |
. . . . . . . . . . 11
β’ ((π₯ β€ πΌ β¨ πΌ < π₯) β (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πβπ₯) = π β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
144 | 143 | com12 32 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((π₯ β€ πΌ β¨ πΌ < π₯) β ((πβπ₯) = π β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
145 | 20, 144 | mpd 15 |
. . . . . . . . 9
β’ (((π β§ π₯ β (0...π)) β§ πΌ β (0..^π)) β ((πβπ₯) = π β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
146 | 145 | ex 414 |
. . . . . . . 8
β’ ((π β§ π₯ β (0...π)) β (πΌ β (0..^π) β ((πβπ₯) = π β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
147 | 146 | com23 86 |
. . . . . . 7
β’ ((π β§ π₯ β (0...π)) β ((πβπ₯) = π β (πΌ β (0..^π) β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
148 | 147 | rexlimdva 3149 |
. . . . . 6
β’ (π β (βπ₯ β (0...π)(πβπ₯) = π β (πΌ β (0..^π) β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))))) |
149 | 13, 148 | mpd 15 |
. . . . 5
β’ (π β (πΌ β (0..^π) β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))))) |
150 | 149 | imp 408 |
. . . 4
β’ ((π β§ πΌ β (0..^π)) β ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
151 | 150 | com12 32 |
. . 3
β’ ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β* β§
π β
β*) β§ ((πβπΌ) < π β§ π < (πβ(πΌ + 1)))) β ((π β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
152 | 1, 151 | sylbi 216 |
. 2
β’ (π β ((πβπΌ)(,)(πβ(πΌ + 1))) β ((π β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
153 | | ax-1 6 |
. 2
β’ (Β¬
π β ((πβπΌ)(,)(πβ(πΌ + 1))) β ((π β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
154 | 152, 153 | pm2.61i 182 |
1
β’ ((π β§ πΌ β (0..^π)) β Β¬ π β ((πβπΌ)(,)(πβ(πΌ + 1)))) |