Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. 2
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β π β Word π) |
2 | | elfz2 13438 |
. . . . . 6
β’ (πΏ β (πΎ...(π β π)) β ((πΎ β β€ β§ (π β π) β β€ β§ πΏ β β€) β§ (πΎ β€ πΏ β§ πΏ β€ (π β π)))) |
3 | | elfz2nn0 13539 |
. . . . . . . . . . . 12
β’ (πΎ β (0...(π β π)) β (πΎ β β0 β§ (π β π) β β0 β§ πΎ β€ (π β π))) |
4 | | elfz2nn0 13539 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β (π β β0 β§ π β β0
β§ π β€ π)) |
5 | | nn0addcl 12455 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β0
β§ πΎ β
β0) β (π + πΎ) β
β0) |
6 | 5 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β (π
+ πΎ) β
β0) |
7 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ πΎ
β€ πΏ) β (π + πΎ) β
β0) |
8 | | elnn0z 12519 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΎ β β0
β (πΎ β β€
β§ 0 β€ πΎ)) |
9 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΎ β β€ β§ πΏ β β€) β 0 β
β) |
10 | | zre 12510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (πΎ β β€ β πΎ β
β) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΎ β β€ β§ πΏ β β€) β πΎ β
β) |
12 | | zre 12510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (πΏ β β€ β πΏ β
β) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΎ β β€ β§ πΏ β β€) β πΏ β
β) |
14 | | letr 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((0
β β β§ πΎ
β β β§ πΏ
β β) β ((0 β€ πΎ β§ πΎ β€ πΏ) β 0 β€ πΏ)) |
15 | 9, 11, 13, 14 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΎ β β€ β§ πΏ β β€) β ((0 β€
πΎ β§ πΎ β€ πΏ) β 0 β€ πΏ)) |
16 | | elnn0z 12519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (πΏ β β0
β (πΏ β β€
β§ 0 β€ πΏ)) |
17 | | nn0addcl 12455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β β0
β§ πΏ β
β0) β (π + πΏ) β
β0) |
18 | 17 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (πΏ β β0
β (π β
β0 β (π + πΏ) β
β0)) |
19 | 16, 18 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΏ β β€ β§ 0 β€
πΏ) β (π β β0
β (π + πΏ) β
β0)) |
20 | 19 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΏ β β€ β (0 β€
πΏ β (π β β0 β (π + πΏ) β
β0))) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΏ β (π β β0 β (π + πΏ) β
β0))) |
22 | 15, 21 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΎ β β€ β§ πΏ β β€) β ((0 β€
πΎ β§ πΎ β€ πΏ) β (π β β0 β (π + πΏ) β
β0))) |
23 | 22 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΎ β (πΎ β€ πΏ β (π β β0 β (π + πΏ) β
β0)))) |
24 | 23 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΎ β (π β β0 β (πΎ β€ πΏ β (π + πΏ) β
β0)))) |
25 | 24 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΎ β β€ β§ 0 β€
πΎ) β (πΏ β β€ β (π β β0
β (πΎ β€ πΏ β (π + πΏ) β
β0)))) |
26 | 8, 25 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΎ β β0
β (πΏ β β€
β (π β
β0 β (πΎ β€ πΏ β (π + πΏ) β
β0)))) |
27 | 26 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΎ β β0
β§ πΏ β β€)
β (π β
β0 β (πΎ β€ πΏ β (π + πΏ) β
β0))) |
28 | 27 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β (πΎ
β€ πΏ β (π + πΏ) β
β0)) |
29 | 28 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ πΎ
β€ πΏ) β (π + πΏ) β
β0) |
30 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΎ β β0
β πΎ β
β) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΎ β β0
β§ πΏ β β€)
β πΎ β
β) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β πΎ
β β) |
33 | 12 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΎ β β0
β§ πΏ β β€)
β πΏ β
β) |
34 | 33 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β πΏ
β β) |
35 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β π β
β) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β π
β β) |
37 | 32, 34, 36 | leadd2d 11757 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β (πΎ
β€ πΏ β (π + πΎ) β€ (π + πΏ))) |
38 | 37 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ πΎ
β€ πΏ) β (π + πΎ) β€ (π + πΏ)) |
39 | 7, 29, 38 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ πΎ
β€ πΏ) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))) |
40 | 39 | exp31 421 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β ((πΎ β
β0 β§ πΏ
β β€) β (πΎ
β€ πΏ β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
41 | 40 | com23 86 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (πΎ β€ πΏ β ((πΎ β β0 β§ πΏ β β€) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β (πΎ β€ πΏ β ((πΎ β β0 β§ πΏ β β€) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
43 | 4, 42 | sylbi 216 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β (πΎ β€ πΏ β ((πΎ β β0 β§ πΏ β β€) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
44 | 43 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β (πΎ β€ πΏ β ((πΎ β β0 β§ πΏ β β€) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
45 | 44 | com13 88 |
. . . . . . . . . . . . . 14
β’ ((πΎ β β0
β§ πΏ β β€)
β (πΎ β€ πΏ β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
46 | 45 | ex 414 |
. . . . . . . . . . . . 13
β’ (πΎ β β0
β (πΏ β β€
β (πΎ β€ πΏ β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
47 | 46 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((πΎ β β0
β§ (π β π) β β0
β§ πΎ β€ (π β π)) β (πΏ β β€ β (πΎ β€ πΏ β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
48 | 3, 47 | sylbi 216 |
. . . . . . . . . . 11
β’ (πΎ β (0...(π β π)) β (πΏ β β€ β (πΎ β€ πΏ β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
49 | 48 | com13 88 |
. . . . . . . . . 10
β’ (πΎ β€ πΏ β (πΏ β β€ β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
50 | 49 | adantr 482 |
. . . . . . . . 9
β’ ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β (πΏ β β€ β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
51 | 50 | com12 32 |
. . . . . . . 8
β’ (πΏ β β€ β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
52 | 51 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((πΎ β β€ β§ (π β π) β β€ β§ πΏ β β€) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))))) |
53 | 52 | imp 408 |
. . . . . 6
β’ (((πΎ β β€ β§ (π β π) β β€ β§ πΏ β β€) β§ (πΎ β€ πΏ β§ πΏ β€ (π β π))) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
54 | 2, 53 | sylbi 216 |
. . . . 5
β’ (πΏ β (πΎ...(π β π)) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))))) |
55 | 54 | impcom 409 |
. . . 4
β’ ((πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π))) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ)))) |
56 | 55 | impcom 409 |
. . 3
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))) |
57 | | elfz2nn0 13539 |
. . 3
β’ ((π + πΎ) β (0...(π + πΏ)) β ((π + πΎ) β β0 β§ (π + πΏ) β β0 β§ (π + πΎ) β€ (π + πΏ))) |
58 | 56, 57 | sylibr 233 |
. 2
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β (π + πΎ) β (0...(π + πΏ))) |
59 | | elfz2nn0 13539 |
. . . . . . . . . . . . . . . 16
β’ (π β
(0...(β―βπ))
β (π β
β0 β§ (β―βπ) β β0 β§ π β€ (β―βπ))) |
60 | 28 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΎ β€ πΏ β ((π β β0 β§ (πΎ β β0
β§ πΏ β β€))
β (π + πΏ) β
β0)) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§ (πΎ β β0
β§ πΏ β β€))
β (π + πΏ) β
β0)) |
62 | 61 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ (πΎ
β€ πΏ β§ πΏ β€ (π β π))) β (π + πΏ) β
β0) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ (πΎ
β€ πΏ β§ πΏ β€ (π β π))) β§ (π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ)))
β (π + πΏ) β
β0) |
64 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ (πΎ
β€ πΏ β§ πΏ β€ (π β π))) β§ (π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ)))
β (β―βπ)
β β0) |
65 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ (π β β0
β π β
β) |
66 | 65, 35 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π β β0
β§ π β
β0) β (π β β β§ π β β)) |
67 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((β―βπ)
β β0 β (β―βπ) β β) |
68 | 66, 67 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π β β0
β§ π β
β0) β§ (β―βπ) β β0) β ((π β β β§ π β β) β§
(β―βπ) β
β)) |
69 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β π β
β) |
70 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β πΏ β
β) |
71 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β π β
β) |
72 | 69, 70, 71 | leaddsub2d 11764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β ((π + πΏ) β€ π β πΏ β€ (π β π))) |
73 | | readdcl 11141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ ((π β β β§ πΏ β β) β (π + πΏ) β β) |
74 | 73 | ad4ant24 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β (π + πΏ) β
β) |
75 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ (((π β β β§ π β β) β§
(β―βπ) β
β) β (β―βπ) β β) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β (β―βπ) β β) |
77 | | letr 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ (((π + πΏ) β β β§ π β β β§ (β―βπ) β β) β
(((π + πΏ) β€ π β§ π β€ (β―βπ)) β (π + πΏ) β€ (β―βπ))) |
78 | 77 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’ (((π + πΏ) β β β§ π β β β§ (β―βπ) β β) β ((π + πΏ) β€ π β (π β€ (β―βπ) β (π + πΏ) β€ (β―βπ)))) |
79 | 74, 71, 76, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β ((π + πΏ) β€ π β (π β€ (β―βπ) β (π + πΏ) β€ (β―βπ)))) |
80 | 79 | a1ddd 80 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β ((π + πΏ) β€ π β (π β€ (β―βπ) β (0 β€ πΏ β (π + πΏ) β€ (β―βπ))))) |
81 | 72, 80 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β (πΏ β€
(π β π) β (π β€ (β―βπ) β (0 β€ πΏ β (π + πΏ) β€ (β―βπ))))) |
82 | 81 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((((π β β β§ π β β) β§
(β―βπ) β
β) β§ πΏ β
β) β (π β€
(β―βπ) β
(πΏ β€ (π β π) β (0 β€ πΏ β (π + πΏ) β€ (β―βπ))))) |
83 | 68, 12, 82 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((((π β β0
β§ π β
β0) β§ (β―βπ) β β0) β§ πΏ β β€) β (π β€ (β―βπ) β (πΏ β€ (π β π) β (0 β€ πΏ β (π + πΏ) β€ (β―βπ))))) |
84 | 83 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((π β β0
β§ π β
β0) β§ (β―βπ) β β0) β (πΏ β β€ β (π β€ (β―βπ) β (πΏ β€ (π β π) β (0 β€ πΏ β (π + πΏ) β€ (β―βπ)))))) |
85 | 84 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((π β β0
β§ π β
β0) β§ (β―βπ) β β0) β (0 β€
πΏ β (π β€ (β―βπ) β (πΏ β€ (π β π) β (πΏ β β€ β (π + πΏ) β€ (β―βπ)))))) |
86 | 85 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β β0
β§ π β
β0) β ((β―βπ) β β0 β (0 β€
πΏ β (π β€ (β―βπ) β (πΏ β€ (π β π) β (πΏ β β€ β (π + πΏ) β€ (β―βπ))))))) |
87 | 86 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β β0
β§ π β
β0) β (π β€ (β―βπ) β (0 β€ πΏ β ((β―βπ) β β0 β (πΏ β€ (π β π) β (πΏ β β€ β (π + πΏ) β€ (β―βπ))))))) |
88 | 87 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β β0
β (π β
β0 β (π β€ (β―βπ) β (0 β€ πΏ β ((β―βπ) β β0 β (πΏ β€ (π β π) β (πΏ β β€ β (π + πΏ) β€ (β―βπ)))))))) |
89 | 88 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β β0
β ((β―βπ)
β β0 β (π β€ (β―βπ) β (0 β€ πΏ β (π β β0 β (πΏ β€ (π β π) β (πΏ β β€ β (π + πΏ) β€ (β―βπ)))))))) |
90 | 89 | 3imp 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β β0
β§ (β―βπ)
β β0 β§ π β€ (β―βπ)) β (0 β€ πΏ β (π β β0 β (πΏ β€ (π β π) β (πΏ β β€ β (π + πΏ) β€ (β―βπ)))))) |
91 | 90 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (πΏ β β€ β (0 β€
πΏ β (π β β0 β (πΏ β€ (π β π) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))))) |
92 | 91 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΏ β (π β β0 β (πΏ β€ (π β π) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))))) |
93 | 15, 92 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((πΎ β β€ β§ πΏ β β€) β ((0 β€
πΎ β§ πΎ β€ πΏ) β (π β β0 β (πΏ β€ (π β π) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))))) |
94 | 93 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΎ β (πΎ β€ πΏ β (π β β0 β (πΏ β€ (π β π) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ))))))) |
95 | 94 | com35 98 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΎ β (πΏ β€ (π β π) β (π β β0 β (πΎ β€ πΏ β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ))))))) |
96 | 95 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΎ β β€ β§ πΏ β β€) β (πΎ β€ πΏ β (πΏ β€ (π β π) β (π β β0 β (0 β€
πΎ β ((π β β0
β§ (β―βπ)
β β0 β§ π β€ (β―βπ)) β (π + πΏ) β€ (β―βπ))))))) |
97 | 96 | impd 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΎ β β€ β§ πΏ β β€) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β (π β β0 β (0 β€
πΎ β ((π β β0
β§ (β―βπ)
β β0 β§ π β€ (β―βπ)) β (π + πΏ) β€ (β―βπ)))))) |
98 | 97 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΎ β β€ β§ πΏ β β€) β (0 β€
πΎ β (π β β0 β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))))) |
99 | 98 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΎ β β€ β§ 0 β€
πΎ) β (πΏ β β€ β (π β β0
β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))))) |
100 | 8, 99 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΎ β β0
β (πΏ β β€
β (π β
β0 β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))))) |
101 | 100 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΎ β β0
β§ πΏ β β€)
β (π β
β0 β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ))))) |
102 | 101 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β ((πΎ
β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ)))) |
103 | 102 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ (πΎ
β€ πΏ β§ πΏ β€ (π β π))) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β (π + πΏ) β€ (β―βπ))) |
104 | 103 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ (πΎ
β€ πΏ β§ πΏ β€ (π β π))) β§ (π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ)))
β (π + πΏ) β€ (β―βπ)) |
105 | 63, 64, 104 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β β0
β§ (πΎ β
β0 β§ πΏ
β β€)) β§ (πΎ
β€ πΏ β§ πΏ β€ (π β π))) β§ (π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ)))
β ((π + πΏ) β β0
β§ (β―βπ)
β β0 β§ (π + πΏ) β€ (β―βπ))) |
106 | 105 | exp41 436 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β ((πΎ β
β0 β§ πΏ
β β€) β ((πΎ
β€ πΏ β§ πΏ β€ (π β π)) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β ((π + πΏ) β β0
β§ (β―βπ)
β β0 β§ (π + πΏ) β€ (β―βπ)))))) |
107 | 106 | com24 95 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β ((π β
β0 β§ (β―βπ) β β0 β§ π β€ (β―βπ)) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
108 | 107 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β ((π β β0
β§ (β―βπ)
β β0 β§ π β€ (β―βπ)) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
109 | 4, 108 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β ((π β β0 β§
(β―βπ) β
β0 β§ π
β€ (β―βπ))
β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
110 | 109 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ (β―βπ)
β β0 β§ π β€ (β―βπ)) β (π β (0...π) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
111 | 59, 110 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π β
(0...(β―βπ))
β (π β (0...π) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
112 | 111 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((π β
(0...(β―βπ))
β§ π β (0...π)) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))))) |
113 | 112 | 3adant1 1131 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((πΎ β β0 β§ πΏ β β€) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))))) |
114 | 113 | com13 88 |
. . . . . . . . . . . 12
β’ ((πΎ β β0
β§ πΏ β β€)
β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))))) |
115 | 114 | ex 414 |
. . . . . . . . . . 11
β’ (πΎ β β0
β (πΏ β β€
β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
116 | 115 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((πΎ β β0
β§ (π β π) β β0
β§ πΎ β€ (π β π)) β (πΏ β β€ β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
117 | 3, 116 | sylbi 216 |
. . . . . . . . 9
β’ (πΎ β (0...(π β π)) β (πΏ β β€ β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
118 | 117 | com3l 89 |
. . . . . . . 8
β’ (πΏ β β€ β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
119 | 118 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((πΎ β β€ β§ (π β π) β β€ β§ πΏ β β€) β ((πΎ β€ πΏ β§ πΏ β€ (π β π)) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))))) |
120 | 119 | imp 408 |
. . . . . 6
β’ (((πΎ β β€ β§ (π β π) β β€ β§ πΏ β β€) β§ (πΎ β€ πΏ β§ πΏ β€ (π β π))) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))))) |
121 | 2, 120 | sylbi 216 |
. . . . 5
β’ (πΏ β (πΎ...(π β π)) β (πΎ β (0...(π β π)) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))))) |
122 | 121 | impcom 409 |
. . . 4
β’ ((πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π))) β ((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ)))) |
123 | 122 | impcom 409 |
. . 3
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))) |
124 | | elfz2nn0 13539 |
. . 3
β’ ((π + πΏ) β (0...(β―βπ)) β ((π + πΏ) β β0 β§
(β―βπ) β
β0 β§ (π + πΏ) β€ (β―βπ))) |
125 | 123, 124 | sylibr 233 |
. 2
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β (π + πΏ) β (0...(β―βπ))) |
126 | 1, 58, 125 | 3jca 1129 |
1
β’ (((π β Word π β§ π β (0...(β―βπ)) β§ π β (0...π)) β§ (πΎ β (0...(π β π)) β§ πΏ β (πΎ...(π β π)))) β (π β Word π β§ (π + πΎ) β (0...(π + πΏ)) β§ (π + πΏ) β (0...(β―βπ)))) |