Step | Hyp | Ref
| Expression |
1 | | elfzo0l 13724 |
. . 3
β’ (πΌ β
(0..^(β―βπΉ))
β (πΌ = 0 β¨ πΌ β
(1..^(β―βπΉ)))) |
2 | | simpr 485 |
. . . . . . . . 9
β’ ((1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β πΉ(PathsβπΊ)π) |
3 | | pthiswlk 29022 |
. . . . . . . . . . 11
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) |
4 | | wlkcl 28910 |
. . . . . . . . . . 11
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
5 | | 1zzd 12595 |
. . . . . . . . . . . . . 14
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β 1 β β€) |
6 | | nn0z 12585 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β€) |
7 | 6 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β (β―βπΉ) β β€) |
8 | | simpr 485 |
. . . . . . . . . . . . . 14
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β 1 < (β―βπΉ)) |
9 | | fzolb 13640 |
. . . . . . . . . . . . . 14
β’ (1 β
(1..^(β―βπΉ))
β (1 β β€ β§ (β―βπΉ) β β€ β§ 1 <
(β―βπΉ))) |
10 | 5, 7, 8, 9 | syl3anbrc 1343 |
. . . . . . . . . . . . 13
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β 1 β (1..^(β―βπΉ))) |
11 | | 0elfz 13600 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ)
β β0 β 0 β (0...(β―βπΉ))) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . 13
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β 0 β (0...(β―βπΉ))) |
13 | | ax-1ne0 11181 |
. . . . . . . . . . . . . 14
β’ 1 β
0 |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β 1 β 0) |
15 | 10, 12, 14 | 3jca 1128 |
. . . . . . . . . . . 12
β’
(((β―βπΉ)
β β0 β§ 1 < (β―βπΉ)) β (1 β
(1..^(β―βπΉ))
β§ 0 β (0...(β―βπΉ)) β§ 1 β 0)) |
16 | 15 | ex 413 |
. . . . . . . . . . 11
β’
((β―βπΉ)
β β0 β (1 < (β―βπΉ) β (1 β (1..^(β―βπΉ)) β§ 0 β
(0...(β―βπΉ))
β§ 1 β 0))) |
17 | 3, 4, 16 | 3syl 18 |
. . . . . . . . . 10
β’ (πΉ(PathsβπΊ)π β (1 < (β―βπΉ) β (1 β
(1..^(β―βπΉ))
β§ 0 β (0...(β―βπΉ)) β§ 1 β 0))) |
18 | 17 | impcom 408 |
. . . . . . . . 9
β’ ((1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β (1 β (1..^(β―βπΉ)) β§ 0 β
(0...(β―βπΉ))
β§ 1 β 0)) |
19 | | pthdivtx 29024 |
. . . . . . . . 9
β’ ((πΉ(PathsβπΊ)π β§ (1 β (1..^(β―βπΉ)) β§ 0 β
(0...(β―βπΉ))
β§ 1 β 0)) β (πβ1) β (πβ0)) |
20 | 2, 18, 19 | syl2anc 584 |
. . . . . . . 8
β’ ((1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β (πβ1) β (πβ0)) |
21 | 20 | necomd 2996 |
. . . . . . 7
β’ ((1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β (πβ0) β (πβ1)) |
22 | 21 | 3adant1 1130 |
. . . . . 6
β’ ((πΌ = 0 β§ 1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β (πβ0) β (πβ1)) |
23 | | fveq2 6891 |
. . . . . . . 8
β’ (πΌ = 0 β (πβπΌ) = (πβ0)) |
24 | | fv0p1e1 12337 |
. . . . . . . 8
β’ (πΌ = 0 β (πβ(πΌ + 1)) = (πβ1)) |
25 | 23, 24 | neeq12d 3002 |
. . . . . . 7
β’ (πΌ = 0 β ((πβπΌ) β (πβ(πΌ + 1)) β (πβ0) β (πβ1))) |
26 | 25 | 3ad2ant1 1133 |
. . . . . 6
β’ ((πΌ = 0 β§ 1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β ((πβπΌ) β (πβ(πΌ + 1)) β (πβ0) β (πβ1))) |
27 | 22, 26 | mpbird 256 |
. . . . 5
β’ ((πΌ = 0 β§ 1 <
(β―βπΉ) β§
πΉ(PathsβπΊ)π) β (πβπΌ) β (πβ(πΌ + 1))) |
28 | 27 | 3exp 1119 |
. . . 4
β’ (πΌ = 0 β (1 <
(β―βπΉ) β
(πΉ(PathsβπΊ)π β (πβπΌ) β (πβ(πΌ + 1))))) |
29 | | simp3 1138 |
. . . . . 6
β’ ((πΌ β
(1..^(β―βπΉ))
β§ 1 < (β―βπΉ) β§ πΉ(PathsβπΊ)π) β πΉ(PathsβπΊ)π) |
30 | | id 22 |
. . . . . . . 8
β’ (πΌ β
(1..^(β―βπΉ))
β πΌ β
(1..^(β―βπΉ))) |
31 | | fzo0ss1 13664 |
. . . . . . . . . 10
β’
(1..^(β―βπΉ)) β (0..^(β―βπΉ)) |
32 | 31 | sseli 3978 |
. . . . . . . . 9
β’ (πΌ β
(1..^(β―βπΉ))
β πΌ β
(0..^(β―βπΉ))) |
33 | | fzofzp1 13731 |
. . . . . . . . 9
β’ (πΌ β
(0..^(β―βπΉ))
β (πΌ + 1) β
(0...(β―βπΉ))) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
β’ (πΌ β
(1..^(β―βπΉ))
β (πΌ + 1) β
(0...(β―βπΉ))) |
35 | | elfzoelz 13634 |
. . . . . . . . . . 11
β’ (πΌ β
(1..^(β―βπΉ))
β πΌ β
β€) |
36 | 35 | zcnd 12669 |
. . . . . . . . . 10
β’ (πΌ β
(1..^(β―βπΉ))
β πΌ β
β) |
37 | | 1cnd 11211 |
. . . . . . . . . 10
β’ (πΌ β
(1..^(β―βπΉ))
β 1 β β) |
38 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (πΌ β
(1..^(β―βπΉ))
β 1 β 0) |
39 | 36, 37, 38 | 3jca 1128 |
. . . . . . . . 9
β’ (πΌ β
(1..^(β―βπΉ))
β (πΌ β β
β§ 1 β β β§ 1 β 0)) |
40 | | addn0nid 11636 |
. . . . . . . . . 10
β’ ((πΌ β β β§ 1 β
β β§ 1 β 0) β (πΌ + 1) β πΌ) |
41 | 40 | necomd 2996 |
. . . . . . . . 9
β’ ((πΌ β β β§ 1 β
β β§ 1 β 0) β πΌ β (πΌ + 1)) |
42 | 39, 41 | syl 17 |
. . . . . . . 8
β’ (πΌ β
(1..^(β―βπΉ))
β πΌ β (πΌ + 1)) |
43 | 30, 34, 42 | 3jca 1128 |
. . . . . . 7
β’ (πΌ β
(1..^(β―βπΉ))
β (πΌ β
(1..^(β―βπΉ))
β§ (πΌ + 1) β
(0...(β―βπΉ))
β§ πΌ β (πΌ + 1))) |
44 | 43 | 3ad2ant1 1133 |
. . . . . 6
β’ ((πΌ β
(1..^(β―βπΉ))
β§ 1 < (β―βπΉ) β§ πΉ(PathsβπΊ)π) β (πΌ β (1..^(β―βπΉ)) β§ (πΌ + 1) β (0...(β―βπΉ)) β§ πΌ β (πΌ + 1))) |
45 | | pthdivtx 29024 |
. . . . . 6
β’ ((πΉ(PathsβπΊ)π β§ (πΌ β (1..^(β―βπΉ)) β§ (πΌ + 1) β (0...(β―βπΉ)) β§ πΌ β (πΌ + 1))) β (πβπΌ) β (πβ(πΌ + 1))) |
46 | 29, 44, 45 | syl2anc 584 |
. . . . 5
β’ ((πΌ β
(1..^(β―βπΉ))
β§ 1 < (β―βπΉ) β§ πΉ(PathsβπΊ)π) β (πβπΌ) β (πβ(πΌ + 1))) |
47 | 46 | 3exp 1119 |
. . . 4
β’ (πΌ β
(1..^(β―βπΉ))
β (1 < (β―βπΉ) β (πΉ(PathsβπΊ)π β (πβπΌ) β (πβ(πΌ + 1))))) |
48 | 28, 47 | jaoi 855 |
. . 3
β’ ((πΌ = 0 β¨ πΌ β (1..^(β―βπΉ))) β (1 <
(β―βπΉ) β
(πΉ(PathsβπΊ)π β (πβπΌ) β (πβ(πΌ + 1))))) |
49 | 1, 48 | syl 17 |
. 2
β’ (πΌ β
(0..^(β―βπΉ))
β (1 < (β―βπΉ) β (πΉ(PathsβπΊ)π β (πβπΌ) β (πβ(πΌ + 1))))) |
50 | 49 | 3imp31 1112 |
1
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ πΌ β (0..^(β―βπΉ))) β (πβπΌ) β (πβ(πΌ + 1))) |