Step | Hyp | Ref
| Expression |
1 | | smat.a |
. . . . . . . 8
β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) |
2 | | elmapi 8790 |
. . . . . . . 8
β’ (π΄ β (π΅ βm ((1...π) Γ (1...π))) β π΄:((1...π) Γ (1...π))βΆπ΅) |
3 | | ffun 6672 |
. . . . . . . 8
β’ (π΄:((1...π) Γ (1...π))βΆπ΅ β Fun π΄) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
β’ (π β Fun π΄) |
5 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) = (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) |
6 | 5 | mpofun 7481 |
. . . . . . . 8
β’ Fun
(π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β Fun (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) |
8 | | funco 6542 |
. . . . . . 7
β’ ((Fun
π΄ β§ Fun (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) β Fun (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
9 | 4, 7, 8 | syl2anc 585 |
. . . . . 6
β’ (π β Fun (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
10 | | smat.s |
. . . . . . . 8
β’ π = (πΎ(subMat1βπ΄)πΏ) |
11 | | fz1ssnn 13478 |
. . . . . . . . . 10
β’
(1...π) β
β |
12 | | smat.k |
. . . . . . . . . 10
β’ (π β πΎ β (1...π)) |
13 | 11, 12 | sselid 3943 |
. . . . . . . . 9
β’ (π β πΎ β β) |
14 | | fz1ssnn 13478 |
. . . . . . . . . 10
β’
(1...π) β
β |
15 | | smat.l |
. . . . . . . . . 10
β’ (π β πΏ β (1...π)) |
16 | 14, 15 | sselid 3943 |
. . . . . . . . 9
β’ (π β πΏ β β) |
17 | | smatfval 32433 |
. . . . . . . . 9
β’ ((πΎ β β β§ πΏ β β β§ π΄ β (π΅ βm ((1...π) Γ (1...π)))) β (πΎ(subMat1βπ΄)πΏ) = (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
18 | 13, 16, 1, 17 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (πΎ(subMat1βπ΄)πΏ) = (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
19 | 10, 18 | eqtrid 2785 |
. . . . . . 7
β’ (π β π = (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
20 | 19 | funeqd 6524 |
. . . . . 6
β’ (π β (Fun π β Fun (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)))) |
21 | 9, 20 | mpbird 257 |
. . . . 5
β’ (π β Fun π) |
22 | | fdmrn 6701 |
. . . . 5
β’ (Fun
π β π:dom πβΆran π) |
23 | 21, 22 | sylib 217 |
. . . 4
β’ (π β π:dom πβΆran π) |
24 | 19 | dmeqd 5862 |
. . . . . 6
β’ (π β dom π = dom (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
25 | | dmco 6207 |
. . . . . . 7
β’ dom
(π΄ β (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) = (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) |
26 | | fdm 6678 |
. . . . . . . . . . . 12
β’ (π΄:((1...π) Γ (1...π))βΆπ΅ β dom π΄ = ((1...π) Γ (1...π))) |
27 | 1, 2, 26 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β dom π΄ = ((1...π) Γ (1...π))) |
28 | 27 | imaeq2d 6014 |
. . . . . . . . . 10
β’ (π β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) = (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π)))) |
29 | 28 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) β π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π))))) |
30 | | opex 5422 |
. . . . . . . . . . . 12
β’
β¨if(π <
πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β© β V |
31 | 5, 30 | fnmpoi 8003 |
. . . . . . . . . . 11
β’ (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) Fn (β Γ
β) |
32 | | elpreima 7009 |
. . . . . . . . . . 11
β’ ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) Fn (β Γ β)
β (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π))) β (π₯ β (β Γ β) β§
((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))))) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . 10
β’ (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π))) β (π₯ β (β Γ β) β§
((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)))) |
34 | 33 | a1i 11 |
. . . . . . . . 9
β’ (π β (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π))) β (π₯ β (β Γ β) β§
((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))))) |
35 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
36 | 35 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) = ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)ββ¨(1st
βπ₯), (2nd
βπ₯)β©)) |
37 | | df-ov 7361 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ₯)(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯)) = ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)ββ¨(1st
βπ₯), (2nd
βπ₯)β©) |
38 | 36, 37 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) = ((1st βπ₯)(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯))) |
39 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ₯) β (π < πΎ β (1st βπ₯) < πΎ)) |
40 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ₯) β π = (1st βπ₯)) |
41 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ₯) β (π + 1) = ((1st βπ₯) + 1)) |
42 | 39, 40, 41 | ifbieq12d 4515 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (1st βπ₯) β if(π < πΎ, π, (π + 1)) = if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1))) |
43 | 42 | opeq1d 4837 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (1st βπ₯) β β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β© = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if(π < πΏ, π, (π + 1))β©) |
44 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2nd βπ₯) β (π < πΏ β (2nd βπ₯) < πΏ)) |
45 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2nd βπ₯) β π = (2nd βπ₯)) |
46 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2nd βπ₯) β (π + 1) = ((2nd βπ₯) + 1)) |
47 | 44, 45, 46 | ifbieq12d 4515 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (2nd βπ₯) β if(π < πΏ, π, (π + 1)) = if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))) |
48 | 47 | opeq2d 4838 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (2nd βπ₯) β
β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if(π < πΏ, π, (π + 1))β© = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
49 | | opex 5422 |
. . . . . . . . . . . . . . . . . . 19
β’
β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β© β V |
50 | 43, 48, 5, 49 | ovmpo 7516 |
. . . . . . . . . . . . . . . . . 18
β’
(((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β ((1st βπ₯)(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯)) = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((1st
βπ₯)(π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯)) = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
52 | 38, 51 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) = β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
53 | 52 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)) β β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β© β ((1...π) Γ (1...π)))) |
54 | | opelxp 5670 |
. . . . . . . . . . . . . . 15
β’
(β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β© β ((1...π) Γ (1...π)) β (if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β§ if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π))) |
55 | 53, 54 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)) β (if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β§ if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π)))) |
56 | | ifel 4531 |
. . . . . . . . . . . . . . . 16
β’
(if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β (((1st βπ₯) < πΎ β§ (1st βπ₯) β (1...π)) β¨ (Β¬ (1st βπ₯) < πΎ β§ ((1st βπ₯) + 1) β (1...π)))) |
57 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β
β) |
58 | 57 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β
β) |
59 | 13 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΎ β β) |
60 | 59 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β πΎ β β) |
61 | | smat.m |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β) |
62 | 61 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β) |
63 | 62 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β π β β) |
64 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) < πΎ) |
65 | 58, 60, 64 | ltled 11308 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β€ πΎ) |
66 | | elfzle2 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΎ β (1...π) β πΎ β€ π) |
67 | 12, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΎ β€ π) |
68 | 67 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β πΎ β€ π) |
69 | 58, 60, 63, 65, 68 | letrd 11317 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β€ π) |
70 | 57, 69 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ π)) |
71 | 61 | nnzd 12531 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β€) |
72 | | fznn 13515 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β
((1st βπ₯)
β (1...π) β
((1st βπ₯)
β β β§ (1st βπ₯) β€ π))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1st
βπ₯) β (1...π) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ π))) |
74 | 73 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) β (1...π) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ π))) |
75 | 70, 74 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β (1...π)) |
76 | 58, 60, 63, 64, 68 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) < π) |
77 | 61 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β π β β) |
78 | | nnltlem1 12575 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ₯) β β β§ π β β) β ((1st
βπ₯) < π β (1st
βπ₯) β€ (π β 1))) |
79 | 57, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) < π β (1st
βπ₯) β€ (π β 1))) |
80 | 76, 79 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β€ (π β 1)) |
81 | 75, 80 | 2thd 265 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) β (1...π) β (1st
βπ₯) β€ (π β 1))) |
82 | 81 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) < πΎ β§ (1st
βπ₯) β (1...π)) β ((1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1)))) |
83 | | fznn 13515 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β€ β
(((1st βπ₯)
+ 1) β (1...π) β
(((1st βπ₯)
+ 1) β β β§ ((1st βπ₯) + 1) β€ π))) |
84 | 71, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (((1st
βπ₯) + 1) β
(1...π) β
(((1st βπ₯)
+ 1) β β β§ ((1st βπ₯) + 1) β€ π))) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β
(1...π) β
(((1st βπ₯)
+ 1) β β β§ ((1st βπ₯) + 1) β€ π))) |
86 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (1st
βπ₯) β
β) |
87 | 86 | peano2nnd 12175 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((1st
βπ₯) + 1) β
β) |
88 | 87 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β€ π β (((1st
βπ₯) + 1) β
β β§ ((1st βπ₯) + 1) β€ π))) |
89 | 86 | nnzd 12531 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (1st
βπ₯) β
β€) |
90 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β π β β€) |
91 | | zltp1le 12558 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ₯) β β€ β§ π β β€) β ((1st
βπ₯) < π β ((1st
βπ₯) + 1) β€ π)) |
92 | | zltlem1 12561 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ₯) β β€ β§ π β β€) β ((1st
βπ₯) < π β (1st
βπ₯) β€ (π β 1))) |
93 | 91, 92 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((1st βπ₯) β β€ β§ π β β€) β (((1st
βπ₯) + 1) β€ π β (1st
βπ₯) β€ (π β 1))) |
94 | 89, 90, 93 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β€ π β (1st
βπ₯) β€ (π β 1))) |
95 | 85, 88, 94 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β
(1...π) β
(1st βπ₯)
β€ (π β
1))) |
96 | 95 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((Β¬
(1st βπ₯)
< πΎ β§
((1st βπ₯)
+ 1) β (1...π)) β
(Β¬ (1st βπ₯) < πΎ β§ (1st βπ₯) β€ (π β 1)))) |
97 | 82, 96 | orbi12d 918 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((1st
βπ₯) < πΎ β§ (1st
βπ₯) β (1...π)) β¨ (Β¬ (1st
βπ₯) < πΎ β§ ((1st
βπ₯) + 1) β
(1...π))) β
(((1st βπ₯)
< πΎ β§
(1st βπ₯)
β€ (π β 1)) β¨
(Β¬ (1st βπ₯) < πΎ β§ (1st βπ₯) β€ (π β 1))))) |
98 | | pm4.42 1053 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ₯) β€ (π β 1) β (((1st
βπ₯) β€ (π β 1) β§
(1st βπ₯)
< πΎ) β¨
((1st βπ₯)
β€ (π β 1) β§
Β¬ (1st βπ₯) < πΎ))) |
99 | | ancom 462 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1st βπ₯) β€ (π β 1) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1))) |
100 | | ancom 462 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1st βπ₯) β€ (π β 1) β§ Β¬ (1st
βπ₯) < πΎ) β (Β¬ (1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1))) |
101 | 99, 100 | orbi12i 914 |
. . . . . . . . . . . . . . . . . 18
β’
((((1st βπ₯) β€ (π β 1) β§ (1st
βπ₯) < πΎ) β¨ ((1st
βπ₯) β€ (π β 1) β§ Β¬
(1st βπ₯)
< πΎ)) β
(((1st βπ₯)
< πΎ β§
(1st βπ₯)
β€ (π β 1)) β¨
(Β¬ (1st βπ₯) < πΎ β§ (1st βπ₯) β€ (π β 1)))) |
102 | 98, 101 | bitri 275 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ₯) β€ (π β 1) β (((1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1)) β¨ (Β¬
(1st βπ₯)
< πΎ β§
(1st βπ₯)
β€ (π β
1)))) |
103 | 97, 102 | bitr4di 289 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((1st
βπ₯) < πΎ β§ (1st
βπ₯) β (1...π)) β¨ (Β¬ (1st
βπ₯) < πΎ β§ ((1st
βπ₯) + 1) β
(1...π))) β
(1st βπ₯)
β€ (π β
1))) |
104 | 56, 103 | bitrid 283 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β (1st
βπ₯) β€ (π β 1))) |
105 | | ifel 4531 |
. . . . . . . . . . . . . . . 16
β’
(if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π) β (((2nd βπ₯) < πΏ β§ (2nd βπ₯) β (1...π)) β¨ (Β¬ (2nd βπ₯) < πΏ β§ ((2nd βπ₯) + 1) β (1...π)))) |
106 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β
β) |
107 | 106 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β
β) |
108 | 16 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΏ β β) |
109 | 108 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β πΏ β β) |
110 | | smat.n |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β) |
111 | 110 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β) |
112 | 111 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β π β β) |
113 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) < πΏ) |
114 | 107, 109,
113 | ltled 11308 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β€ πΏ) |
115 | | elfzle2 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΏ β (1...π) β πΏ β€ π) |
116 | 15, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΏ β€ π) |
117 | 116 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β πΏ β€ π) |
118 | 107, 109,
112, 114, 117 | letrd 11317 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β€ π) |
119 | 106, 118 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ π)) |
120 | 110 | nnzd 12531 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β€) |
121 | | fznn 13515 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β
((2nd βπ₯)
β (1...π) β
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ π))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((2nd
βπ₯) β (1...π) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ π))) |
123 | 122 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) β (1...π) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ π))) |
124 | 119, 123 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β (1...π)) |
125 | 107, 109,
112, 113, 117 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) < π) |
126 | 110 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β π β β) |
127 | | nnltlem1 12575 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd βπ₯) β β β§ π β β) β ((2nd
βπ₯) < π β (2nd
βπ₯) β€ (π β 1))) |
128 | 106, 126,
127 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) < π β (2nd
βπ₯) β€ (π β 1))) |
129 | 125, 128 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β€ (π β 1)) |
130 | 124, 129 | 2thd 265 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) β (1...π) β (2nd
βπ₯) β€ (π β 1))) |
131 | 130 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β (1...π)) β ((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1)))) |
132 | | fznn 13515 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β€ β
(((2nd βπ₯)
+ 1) β (1...π) β
(((2nd βπ₯)
+ 1) β β β§ ((2nd βπ₯) + 1) β€ π))) |
133 | 120, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (((2nd
βπ₯) + 1) β
(1...π) β
(((2nd βπ₯)
+ 1) β β β§ ((2nd βπ₯) + 1) β€ π))) |
134 | 133 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β
(1...π) β
(((2nd βπ₯)
+ 1) β β β§ ((2nd βπ₯) + 1) β€ π))) |
135 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (2nd
βπ₯) β
β) |
136 | 135 | peano2nnd 12175 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((2nd
βπ₯) + 1) β
β) |
137 | 136 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β€ π β (((2nd
βπ₯) + 1) β
β β§ ((2nd βπ₯) + 1) β€ π))) |
138 | 135 | nnzd 12531 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (2nd
βπ₯) β
β€) |
139 | 120 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β π β β€) |
140 | | zltp1le 12558 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd βπ₯) β β€ β§ π β β€) β ((2nd
βπ₯) < π β ((2nd
βπ₯) + 1) β€ π)) |
141 | | zltlem1 12561 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd βπ₯) β β€ β§ π β β€) β ((2nd
βπ₯) < π β (2nd
βπ₯) β€ (π β 1))) |
142 | 140, 141 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((2nd βπ₯) β β€ β§ π β β€) β (((2nd
βπ₯) + 1) β€ π β (2nd
βπ₯) β€ (π β 1))) |
143 | 138, 139,
142 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β€ π β (2nd
βπ₯) β€ (π β 1))) |
144 | 134, 137,
143 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β
(1...π) β
(2nd βπ₯)
β€ (π β
1))) |
145 | 144 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((Β¬
(2nd βπ₯)
< πΏ β§
((2nd βπ₯)
+ 1) β (1...π)) β
(Β¬ (2nd βπ₯) < πΏ β§ (2nd βπ₯) β€ (π β 1)))) |
146 | 131, 145 | orbi12d 918 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β (1...π)) β¨ (Β¬ (2nd
βπ₯) < πΏ β§ ((2nd
βπ₯) + 1) β
(1...π))) β
(((2nd βπ₯)
< πΏ β§
(2nd βπ₯)
β€ (π β 1)) β¨
(Β¬ (2nd βπ₯) < πΏ β§ (2nd βπ₯) β€ (π β 1))))) |
147 | | pm4.42 1053 |
. . . . . . . . . . . . . . . . . 18
β’
((2nd βπ₯) β€ (π β 1) β (((2nd
βπ₯) β€ (π β 1) β§
(2nd βπ₯)
< πΏ) β¨
((2nd βπ₯)
β€ (π β 1) β§
Β¬ (2nd βπ₯) < πΏ))) |
148 | | ancom 462 |
. . . . . . . . . . . . . . . . . . 19
β’
(((2nd βπ₯) β€ (π β 1) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1))) |
149 | | ancom 462 |
. . . . . . . . . . . . . . . . . . 19
β’
(((2nd βπ₯) β€ (π β 1) β§ Β¬ (2nd
βπ₯) < πΏ) β (Β¬ (2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1))) |
150 | 148, 149 | orbi12i 914 |
. . . . . . . . . . . . . . . . . 18
β’
((((2nd βπ₯) β€ (π β 1) β§ (2nd
βπ₯) < πΏ) β¨ ((2nd
βπ₯) β€ (π β 1) β§ Β¬
(2nd βπ₯)
< πΏ)) β
(((2nd βπ₯)
< πΏ β§
(2nd βπ₯)
β€ (π β 1)) β¨
(Β¬ (2nd βπ₯) < πΏ β§ (2nd βπ₯) β€ (π β 1)))) |
151 | 147, 150 | bitri 275 |
. . . . . . . . . . . . . . . . 17
β’
((2nd βπ₯) β€ (π β 1) β (((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1)) β¨ (Β¬
(2nd βπ₯)
< πΏ β§
(2nd βπ₯)
β€ (π β
1)))) |
152 | 146, 151 | bitr4di 289 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β (1...π)) β¨ (Β¬ (2nd
βπ₯) < πΏ β§ ((2nd
βπ₯) + 1) β
(1...π))) β
(2nd βπ₯)
β€ (π β
1))) |
153 | 105, 152 | bitrid 283 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π) β (2nd
βπ₯) β€ (π β 1))) |
154 | 104, 153 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β
((if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β§ if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π)) β ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1)))) |
155 | 55, 154 | bitrd 279 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)) β ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1)))) |
156 | 155 | pm5.32da 580 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β
((((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β§ ((π β β,
π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β (((1st βπ₯) β β β§
(2nd βπ₯)
β β) β§ ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1))))) |
157 | | 1zzd 12539 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β€) |
158 | 71, 157 | zsubcld 12617 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β 1) β β€) |
159 | | fznn 13515 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β β€
β ((1st βπ₯) β (1...(π β 1)) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ (π β 1)))) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((1st
βπ₯) β
(1...(π β 1)) β
((1st βπ₯)
β β β§ (1st βπ₯) β€ (π β 1)))) |
161 | 120, 157 | zsubcld 12617 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β 1) β β€) |
162 | | fznn 13515 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β β€
β ((2nd βπ₯) β (1...(π β 1)) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ (π β 1)))) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((2nd
βπ₯) β
(1...(π β 1)) β
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ (π β 1)))) |
164 | 160, 163 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π β (((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β 1)))
β (((1st βπ₯) β β β§ (1st
βπ₯) β€ (π β 1)) β§
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ (π β 1))))) |
165 | | an4 655 |
. . . . . . . . . . . . . 14
β’
((((1st βπ₯) β β β§ (1st
βπ₯) β€ (π β 1)) β§
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ (π β 1))) β (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((1st
βπ₯) β€ (π β 1) β§
(2nd βπ₯)
β€ (π β
1)))) |
166 | 164, 165 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ (π β (((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β 1)))
β (((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β§ ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1))))) |
167 | 166 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β
(((1st βπ₯)
β (1...(π β 1))
β§ (2nd βπ₯) β (1...(π β 1))) β (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((1st
βπ₯) β€ (π β 1) β§
(2nd βπ₯)
β€ (π β
1))))) |
168 | 156, 167 | bitr4d 282 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β
((((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β§ ((π β β,
π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β ((1st βπ₯) β (1...(π β 1)) β§ (2nd
βπ₯) β
(1...(π β
1))))) |
169 | 168 | pm5.32da 580 |
. . . . . . . . . 10
β’ (π β ((π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β
1)))))) |
170 | | elxp6 7956 |
. . . . . . . . . . . 12
β’ (π₯ β (β Γ
β) β (π₯ =
β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st βπ₯) β β β§
(2nd βπ₯)
β β))) |
171 | 170 | anbi1i 625 |
. . . . . . . . . . 11
β’ ((π₯ β (β Γ
β) β§ ((π β
β, π β β
β¦ β¨if(π <
πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β ((π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)))) |
172 | | anass 470 |
. . . . . . . . . . 11
β’ (((π₯ = β¨(1st
βπ₯), (2nd
βπ₯)β© β§
((1st βπ₯)
β β β§ (2nd βπ₯) β β)) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))))) |
173 | 171, 172 | bitri 275 |
. . . . . . . . . 10
β’ ((π₯ β (β Γ
β) β§ ((π β
β, π β β
β¦ β¨if(π <
πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))))) |
174 | | elxp6 7956 |
. . . . . . . . . 10
β’ (π₯ β ((1...(π β 1)) Γ (1...(π β 1))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β
1))))) |
175 | 169, 173,
174 | 3bitr4g 314 |
. . . . . . . . 9
β’ (π β ((π₯ β (β Γ β) β§
((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β π₯ β ((1...(π β 1)) Γ (1...(π β 1))))) |
176 | 29, 34, 175 | 3bitrd 305 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) β π₯ β ((1...(π β 1)) Γ (1...(π β 1))))) |
177 | 176 | eqrdv 2731 |
. . . . . . 7
β’ (π β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) = ((1...(π β 1)) Γ (1...(π β 1)))) |
178 | 25, 177 | eqtrid 2785 |
. . . . . 6
β’ (π β dom (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) = ((1...(π β 1)) Γ (1...(π β 1)))) |
179 | 24, 178 | eqtrd 2773 |
. . . . 5
β’ (π β dom π = ((1...(π β 1)) Γ (1...(π β 1)))) |
180 | 179 | feq2d 6655 |
. . . 4
β’ (π β (π:dom πβΆran π β π:((1...(π β 1)) Γ (1...(π β 1)))βΆran π)) |
181 | 23, 180 | mpbid 231 |
. . 3
β’ (π β π:((1...(π β 1)) Γ (1...(π β 1)))βΆran π) |
182 | 19 | rneqd 5894 |
. . . . 5
β’ (π β ran π = ran (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
183 | | rncoss 5928 |
. . . . 5
β’ ran
(π΄ β (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) β ran π΄ |
184 | 182, 183 | eqsstrdi 3999 |
. . . 4
β’ (π β ran π β ran π΄) |
185 | | frn 6676 |
. . . . 5
β’ (π΄:((1...π) Γ (1...π))βΆπ΅ β ran π΄ β π΅) |
186 | 1, 2, 185 | 3syl 18 |
. . . 4
β’ (π β ran π΄ β π΅) |
187 | 184, 186 | sstrd 3955 |
. . 3
β’ (π β ran π β π΅) |
188 | | fss 6686 |
. . 3
β’ ((π:((1...(π β 1)) Γ (1...(π β 1)))βΆran π β§ ran π β π΅) β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅) |
189 | 181, 187,
188 | syl2anc 585 |
. 2
β’ (π β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅) |
190 | | reldmmap 8777 |
. . . . . 6
β’ Rel dom
βm |
191 | 190 | ovrcl 7399 |
. . . . 5
β’ (π΄ β (π΅ βm ((1...π) Γ (1...π))) β (π΅ β V β§ ((1...π) Γ (1...π)) β V)) |
192 | 1, 191 | syl 17 |
. . . 4
β’ (π β (π΅ β V β§ ((1...π) Γ (1...π)) β V)) |
193 | 192 | simpld 496 |
. . 3
β’ (π β π΅ β V) |
194 | | ovex 7391 |
. . . 4
β’
(1...(π β 1))
β V |
195 | | ovex 7391 |
. . . 4
β’
(1...(π β 1))
β V |
196 | 194, 195 | xpex 7688 |
. . 3
β’
((1...(π β 1))
Γ (1...(π β
1))) β V |
197 | | elmapg 8781 |
. . 3
β’ ((π΅ β V β§ ((1...(π β 1)) Γ (1...(π β 1))) β V) β
(π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1)))) β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅)) |
198 | 193, 196,
197 | sylancl 587 |
. 2
β’ (π β (π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1)))) β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅)) |
199 | 189, 198 | mpbird 257 |
1
β’ (π β π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1))))) |