Step | Hyp | Ref
| Expression |
1 | | smat.a |
. . . . . . . 8
β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) |
2 | | elmapi 8839 |
. . . . . . . 8
β’ (π΄ β (π΅ βm ((1...π) Γ (1...π))) β π΄:((1...π) Γ (1...π))βΆπ΅) |
3 | | ffun 6717 |
. . . . . . . 8
β’ (π΄:((1...π) Γ (1...π))βΆπ΅ β Fun π΄) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
β’ (π β Fun π΄) |
5 | | eqid 2732 |
. . . . . . . . 9
β’ (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) = (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) |
6 | 5 | mpofun 7528 |
. . . . . . . 8
β’ Fun
(π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β Fun (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) |
8 | | funco 6585 |
. . . . . . 7
β’ ((Fun
π΄ β§ Fun (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) β Fun (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
9 | 4, 7, 8 | syl2anc 584 |
. . . . . 6
β’ (π β Fun (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
10 | | smat.s |
. . . . . . . 8
β’ π = (πΎ(subMat1βπ΄)πΏ) |
11 | | fz1ssnn 13528 |
. . . . . . . . . 10
β’
(1...π) β
β |
12 | | smat.k |
. . . . . . . . . 10
β’ (π β πΎ β (1...π)) |
13 | 11, 12 | sselid 3979 |
. . . . . . . . 9
β’ (π β πΎ β β) |
14 | | fz1ssnn 13528 |
. . . . . . . . . 10
β’
(1...π) β
β |
15 | | smat.l |
. . . . . . . . . 10
β’ (π β πΏ β (1...π)) |
16 | 14, 15 | sselid 3979 |
. . . . . . . . 9
β’ (π β πΏ β β) |
17 | | smatfval 32763 |
. . . . . . . . 9
β’ ((πΎ β β β§ πΏ β β β§ π΄ β (π΅ βm ((1...π) Γ (1...π)))) β (πΎ(subMat1βπ΄)πΏ) = (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
18 | 13, 16, 1, 17 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (πΎ(subMat1βπ΄)πΏ) = (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
19 | 10, 18 | eqtrid 2784 |
. . . . . . 7
β’ (π β π = (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
20 | 19 | funeqd 6567 |
. . . . . 6
β’ (π β (Fun π β Fun (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)))) |
21 | 9, 20 | mpbird 256 |
. . . . 5
β’ (π β Fun π) |
22 | | fdmrn 6746 |
. . . . 5
β’ (Fun
π β π:dom πβΆran π) |
23 | 21, 22 | sylib 217 |
. . . 4
β’ (π β π:dom πβΆran π) |
24 | 19 | dmeqd 5903 |
. . . . . 6
β’ (π β dom π = dom (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
25 | | dmco 6250 |
. . . . . . 7
β’ dom
(π΄ β (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) = (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) |
26 | | fdm 6723 |
. . . . . . . . . . . 12
β’ (π΄:((1...π) Γ (1...π))βΆπ΅ β dom π΄ = ((1...π) Γ (1...π))) |
27 | 1, 2, 26 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β dom π΄ = ((1...π) Γ (1...π))) |
28 | 27 | imaeq2d 6057 |
. . . . . . . . . 10
β’ (π β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) = (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π)))) |
29 | 28 | eleq2d 2819 |
. . . . . . . . 9
β’ (π β (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) β π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β ((1...π) Γ (1...π))))) |
30 | | opex 5463 |
. . . . . . . . . . . 12
β’
β¨if(π <
πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β© β V |
31 | 5, 30 | fnmpoi 8052 |
. . . . . . . . . . 11
β’ (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) Fn (β Γ
β) |
32 | | elpreima 7056 |
. . . . . . . . . . 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 767 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
36 | 35 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) = ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)ββ¨(1st
βπ₯), (2nd
βπ₯)β©)) |
37 | | df-ov 7408 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ₯)(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯)) = ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)ββ¨(1st
βπ₯), (2nd
βπ₯)β©) |
38 | 36, 37 | eqtr4di 2790 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) = ((1st βπ₯)(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯))) |
39 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ₯) β (π < πΎ β (1st βπ₯) < πΎ)) |
40 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ₯) β π = (1st βπ₯)) |
41 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ₯) β (π + 1) = ((1st βπ₯) + 1)) |
42 | 39, 40, 41 | ifbieq12d 4555 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (1st βπ₯) β if(π < πΎ, π, (π + 1)) = if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1))) |
43 | 42 | opeq1d 4878 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (1st βπ₯) β β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β© = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if(π < πΏ, π, (π + 1))β©) |
44 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2nd βπ₯) β (π < πΏ β (2nd βπ₯) < πΏ)) |
45 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2nd βπ₯) β π = (2nd βπ₯)) |
46 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2nd βπ₯) β (π + 1) = ((2nd βπ₯) + 1)) |
47 | 44, 45, 46 | ifbieq12d 4555 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (2nd βπ₯) β if(π < πΏ, π, (π + 1)) = if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))) |
48 | 47 | opeq2d 4879 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (2nd βπ₯) β
β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if(π < πΏ, π, (π + 1))β© = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
49 | | opex 5463 |
. . . . . . . . . . . . . . . . . . 19
β’
β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β© β V |
50 | 43, 48, 5, 49 | ovmpo 7564 |
. . . . . . . . . . . . . . . . . 18
β’
(((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β ((1st βπ₯)(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)(2nd βπ₯)) = β¨if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . 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 2772 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) = β¨if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)), if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1))β©) |
53 | 52 | eleq1d 2818 |
. . . . . . . . . . . . . . 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 5711 |
. . . . . . . . . . . . . . 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 286 |
. . . . . . . . . . . . . 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 4571 |
. . . . . . . . . . . . . . . 16
β’
(if((1st βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β (((1st βπ₯) < πΎ β§ (1st βπ₯) β (1...π)) β¨ (Β¬ (1st βπ₯) < πΎ β§ ((1st βπ₯) + 1) β (1...π)))) |
57 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β
β) |
58 | 57 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β
β) |
59 | 13 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΎ β β) |
60 | 59 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β πΎ β β) |
61 | | smat.m |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β) |
62 | 61 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β) |
63 | 62 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β π β β) |
64 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) < πΎ) |
65 | 58, 60, 64 | ltled 11358 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β€ πΎ) |
66 | | elfzle2 13501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΎ β (1...π) β πΎ β€ π) |
67 | 12, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΎ β€ π) |
68 | 67 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β πΎ β€ π) |
69 | 58, 60, 63, 65, 68 | letrd 11367 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β€ π) |
70 | 57, 69 | jca 512 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ π)) |
71 | 61 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β€) |
72 | | fznn 13565 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β
((1st βπ₯)
β (1...π) β
((1st βπ₯)
β β β§ (1st βπ₯) β€ π))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1st
βπ₯) β (1...π) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ π))) |
74 | 73 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) β (1...π) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ π))) |
75 | 70, 74 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) β (1...π)) |
76 | 58, 60, 63, 64, 68 | ltletrd 11370 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β (1st
βπ₯) < π) |
77 | 61 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β π β β) |
78 | | nnltlem1 12625 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ₯) β β β§ π β β) β ((1st
βπ₯) < π β (1st
βπ₯) β€ (π β 1))) |
79 | 57, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 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 264 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) β (1...π) β (1st
βπ₯) β€ (π β 1))) |
82 | 81 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) < πΎ β§ (1st
βπ₯) β (1...π)) β ((1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1)))) |
83 | | fznn 13565 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β€ β
(((1st βπ₯)
+ 1) β (1...π) β
(((1st βπ₯)
+ 1) β β β§ ((1st βπ₯) + 1) β€ π))) |
84 | 71, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (((1st
βπ₯) + 1) β
(1...π) β
(((1st βπ₯)
+ 1) β β β§ ((1st βπ₯) + 1) β€ π))) |
85 | 84 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β
(1...π) β
(((1st βπ₯)
+ 1) β β β§ ((1st βπ₯) + 1) β€ π))) |
86 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (1st
βπ₯) β
β) |
87 | 86 | peano2nnd 12225 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((1st
βπ₯) + 1) β
β) |
88 | 87 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β€ π β (((1st
βπ₯) + 1) β
β β§ ((1st βπ₯) + 1) β€ π))) |
89 | 86 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (1st
βπ₯) β
β€) |
90 | 71 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β π β β€) |
91 | | zltp1le 12608 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ₯) β β€ β§ π β β€) β ((1st
βπ₯) < π β ((1st
βπ₯) + 1) β€ π)) |
92 | | zltlem1 12611 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ₯) β β€ β§ π β β€) β ((1st
βπ₯) < π β (1st
βπ₯) β€ (π β 1))) |
93 | 91, 92 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((1st βπ₯) β β€ β§ π β β€) β (((1st
βπ₯) + 1) β€ π β (1st
βπ₯) β€ (π β 1))) |
94 | 89, 90, 93 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β€ π β (1st
βπ₯) β€ (π β 1))) |
95 | 85, 88, 94 | 3bitr2d 306 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((1st
βπ₯) + 1) β
(1...π) β
(1st βπ₯)
β€ (π β
1))) |
96 | 95 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((Β¬
(1st βπ₯)
< πΎ β§
((1st βπ₯)
+ 1) β (1...π)) β
(Β¬ (1st βπ₯) < πΎ β§ (1st βπ₯) β€ (π β 1)))) |
97 | 82, 96 | orbi12d 917 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((1st
βπ₯) < πΎ β§ (1st
βπ₯) β (1...π)) β¨ (Β¬ (1st
βπ₯) < πΎ β§ ((1st
βπ₯) + 1) β
(1...π))) β
(((1st βπ₯)
< πΎ β§
(1st βπ₯)
β€ (π β 1)) β¨
(Β¬ (1st βπ₯) < πΎ β§ (1st βπ₯) β€ (π β 1))))) |
98 | | pm4.42 1052 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ₯) β€ (π β 1) β (((1st
βπ₯) β€ (π β 1) β§
(1st βπ₯)
< πΎ) β¨
((1st βπ₯)
β€ (π β 1) β§
Β¬ (1st βπ₯) < πΎ))) |
99 | | ancom 461 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1st βπ₯) β€ (π β 1) β§ (1st
βπ₯) < πΎ) β ((1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1))) |
100 | | ancom 461 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1st βπ₯) β€ (π β 1) β§ Β¬ (1st
βπ₯) < πΎ) β (Β¬ (1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1))) |
101 | 99, 100 | orbi12i 913 |
. . . . . . . . . . . . . . . . . 18
β’
((((1st βπ₯) β€ (π β 1) β§ (1st
βπ₯) < πΎ) β¨ ((1st
βπ₯) β€ (π β 1) β§ Β¬
(1st βπ₯)
< πΎ)) β
(((1st βπ₯)
< πΎ β§
(1st βπ₯)
β€ (π β 1)) β¨
(Β¬ (1st βπ₯) < πΎ β§ (1st βπ₯) β€ (π β 1)))) |
102 | 98, 101 | bitri 274 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ₯) β€ (π β 1) β (((1st
βπ₯) < πΎ β§ (1st
βπ₯) β€ (π β 1)) β¨ (Β¬
(1st βπ₯)
< πΎ β§
(1st βπ₯)
β€ (π β
1)))) |
103 | 97, 102 | bitr4di 288 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((1st
βπ₯) < πΎ β§ (1st
βπ₯) β (1...π)) β¨ (Β¬ (1st
βπ₯) < πΎ β§ ((1st
βπ₯) + 1) β
(1...π))) β
(1st βπ₯)
β€ (π β
1))) |
104 | 56, 103 | bitrid 282 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (if((1st
βπ₯) < πΎ, (1st βπ₯), ((1st βπ₯) + 1)) β (1...π) β (1st
βπ₯) β€ (π β 1))) |
105 | | ifel 4571 |
. . . . . . . . . . . . . . . 16
β’
(if((2nd βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π) β (((2nd βπ₯) < πΏ β§ (2nd βπ₯) β (1...π)) β¨ (Β¬ (2nd βπ₯) < πΏ β§ ((2nd βπ₯) + 1) β (1...π)))) |
106 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β
β) |
107 | 106 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β
β) |
108 | 16 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΏ β β) |
109 | 108 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β πΏ β β) |
110 | | smat.n |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β) |
111 | 110 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β) |
112 | 111 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β π β β) |
113 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) < πΏ) |
114 | 107, 109,
113 | ltled 11358 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β€ πΏ) |
115 | | elfzle2 13501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΏ β (1...π) β πΏ β€ π) |
116 | 15, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΏ β€ π) |
117 | 116 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β πΏ β€ π) |
118 | 107, 109,
112, 114, 117 | letrd 11367 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β€ π) |
119 | 106, 118 | jca 512 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ π)) |
120 | 110 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β€) |
121 | | fznn 13565 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β
((2nd βπ₯)
β (1...π) β
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ π))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((2nd
βπ₯) β (1...π) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ π))) |
123 | 122 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) β (1...π) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ π))) |
124 | 119, 123 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) β (1...π)) |
125 | 107, 109,
112, 113, 117 | ltletrd 11370 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β (2nd
βπ₯) < π) |
126 | 110 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β π β β) |
127 | | nnltlem1 12625 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd βπ₯) β β β§ π β β) β ((2nd
βπ₯) < π β (2nd
βπ₯) β€ (π β 1))) |
128 | 106, 126,
127 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 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 264 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) β (1...π) β (2nd
βπ₯) β€ (π β 1))) |
131 | 130 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β (1...π)) β ((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1)))) |
132 | | fznn 13565 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β€ β
(((2nd βπ₯)
+ 1) β (1...π) β
(((2nd βπ₯)
+ 1) β β β§ ((2nd βπ₯) + 1) β€ π))) |
133 | 120, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (((2nd
βπ₯) + 1) β
(1...π) β
(((2nd βπ₯)
+ 1) β β β§ ((2nd βπ₯) + 1) β€ π))) |
134 | 133 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β
(1...π) β
(((2nd βπ₯)
+ 1) β β β§ ((2nd βπ₯) + 1) β€ π))) |
135 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (2nd
βπ₯) β
β) |
136 | 135 | peano2nnd 12225 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((2nd
βπ₯) + 1) β
β) |
137 | 136 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β€ π β (((2nd
βπ₯) + 1) β
β β§ ((2nd βπ₯) + 1) β€ π))) |
138 | 135 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (2nd
βπ₯) β
β€) |
139 | 120 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β π β β€) |
140 | | zltp1le 12608 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd βπ₯) β β€ β§ π β β€) β ((2nd
βπ₯) < π β ((2nd
βπ₯) + 1) β€ π)) |
141 | | zltlem1 12611 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd βπ₯) β β€ β§ π β β€) β ((2nd
βπ₯) < π β (2nd
βπ₯) β€ (π β 1))) |
142 | 140, 141 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((2nd βπ₯) β β€ β§ π β β€) β (((2nd
βπ₯) + 1) β€ π β (2nd
βπ₯) β€ (π β 1))) |
143 | 138, 139,
142 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β€ π β (2nd
βπ₯) β€ (π β 1))) |
144 | 134, 137,
143 | 3bitr2d 306 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((2nd
βπ₯) + 1) β
(1...π) β
(2nd βπ₯)
β€ (π β
1))) |
145 | 144 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((Β¬
(2nd βπ₯)
< πΏ β§
((2nd βπ₯)
+ 1) β (1...π)) β
(Β¬ (2nd βπ₯) < πΏ β§ (2nd βπ₯) β€ (π β 1)))) |
146 | 131, 145 | orbi12d 917 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β (1...π)) β¨ (Β¬ (2nd
βπ₯) < πΏ β§ ((2nd
βπ₯) + 1) β
(1...π))) β
(((2nd βπ₯)
< πΏ β§
(2nd βπ₯)
β€ (π β 1)) β¨
(Β¬ (2nd βπ₯) < πΏ β§ (2nd βπ₯) β€ (π β 1))))) |
147 | | pm4.42 1052 |
. . . . . . . . . . . . . . . . . 18
β’
((2nd βπ₯) β€ (π β 1) β (((2nd
βπ₯) β€ (π β 1) β§
(2nd βπ₯)
< πΏ) β¨
((2nd βπ₯)
β€ (π β 1) β§
Β¬ (2nd βπ₯) < πΏ))) |
148 | | ancom 461 |
. . . . . . . . . . . . . . . . . . 19
β’
(((2nd βπ₯) β€ (π β 1) β§ (2nd
βπ₯) < πΏ) β ((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1))) |
149 | | ancom 461 |
. . . . . . . . . . . . . . . . . . 19
β’
(((2nd βπ₯) β€ (π β 1) β§ Β¬ (2nd
βπ₯) < πΏ) β (Β¬ (2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1))) |
150 | 148, 149 | orbi12i 913 |
. . . . . . . . . . . . . . . . . 18
β’
((((2nd βπ₯) β€ (π β 1) β§ (2nd
βπ₯) < πΏ) β¨ ((2nd
βπ₯) β€ (π β 1) β§ Β¬
(2nd βπ₯)
< πΏ)) β
(((2nd βπ₯)
< πΏ β§
(2nd βπ₯)
β€ (π β 1)) β¨
(Β¬ (2nd βπ₯) < πΏ β§ (2nd βπ₯) β€ (π β 1)))) |
151 | 147, 150 | bitri 274 |
. . . . . . . . . . . . . . . . 17
β’
((2nd βπ₯) β€ (π β 1) β (((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β€ (π β 1)) β¨ (Β¬
(2nd βπ₯)
< πΏ β§
(2nd βπ₯)
β€ (π β
1)))) |
152 | 146, 151 | bitr4di 288 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β ((((2nd
βπ₯) < πΏ β§ (2nd
βπ₯) β (1...π)) β¨ (Β¬ (2nd
βπ₯) < πΏ β§ ((2nd
βπ₯) + 1) β
(1...π))) β
(2nd βπ₯)
β€ (π β
1))) |
153 | 105, 152 | bitrid 282 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (if((2nd
βπ₯) < πΏ, (2nd βπ₯), ((2nd βπ₯) + 1)) β (1...π) β (2nd
βπ₯) β€ (π β 1))) |
154 | 104, 153 | anbi12d 631 |
. . . . . . . . . . . . . 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 278 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β (((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)) β ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1)))) |
156 | 155 | pm5.32da 579 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β
((((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β§ ((π β β,
π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β (((1st βπ₯) β β β§
(2nd βπ₯)
β β) β§ ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1))))) |
157 | | 1zzd 12589 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β€) |
158 | 71, 157 | zsubcld 12667 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β 1) β β€) |
159 | | fznn 13565 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β β€
β ((1st βπ₯) β (1...(π β 1)) β ((1st
βπ₯) β β
β§ (1st βπ₯) β€ (π β 1)))) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((1st
βπ₯) β
(1...(π β 1)) β
((1st βπ₯)
β β β§ (1st βπ₯) β€ (π β 1)))) |
161 | 120, 157 | zsubcld 12667 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β 1) β β€) |
162 | | fznn 13565 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β β€
β ((2nd βπ₯) β (1...(π β 1)) β ((2nd
βπ₯) β β
β§ (2nd βπ₯) β€ (π β 1)))) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((2nd
βπ₯) β
(1...(π β 1)) β
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ (π β 1)))) |
164 | 160, 163 | anbi12d 631 |
. . . . . . . . . . . . . 14
β’ (π β (((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β 1)))
β (((1st βπ₯) β β β§ (1st
βπ₯) β€ (π β 1)) β§
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ (π β 1))))) |
165 | | an4 654 |
. . . . . . . . . . . . . 14
β’
((((1st βπ₯) β β β§ (1st
βπ₯) β€ (π β 1)) β§
((2nd βπ₯)
β β β§ (2nd βπ₯) β€ (π β 1))) β (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((1st
βπ₯) β€ (π β 1) β§
(2nd βπ₯)
β€ (π β
1)))) |
166 | 164, 165 | bitrdi 286 |
. . . . . . . . . . . . 13
β’ (π β (((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β 1)))
β (((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β§ ((1st βπ₯) β€ (π β 1) β§ (2nd
βπ₯) β€ (π β 1))))) |
167 | 166 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β
(((1st βπ₯)
β (1...(π β 1))
β§ (2nd βπ₯) β (1...(π β 1))) β (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((1st
βπ₯) β€ (π β 1) β§
(2nd βπ₯)
β€ (π β
1))))) |
168 | 156, 167 | bitr4d 281 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) β
((((1st βπ₯) β β β§ (2nd
βπ₯) β β)
β§ ((π β β,
π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β ((1st βπ₯) β (1...(π β 1)) β§ (2nd
βπ₯) β
(1...(π β
1))))) |
169 | 168 | pm5.32da 579 |
. . . . . . . . . 10
β’ (π β ((π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β
1)))))) |
170 | | elxp6 8005 |
. . . . . . . . . . . 12
β’ (π₯ β (β Γ
β) β (π₯ =
β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st βπ₯) β β β§
(2nd βπ₯)
β β))) |
171 | 170 | anbi1i 624 |
. . . . . . . . . . 11
β’ ((π₯ β (β Γ
β) β§ ((π β
β, π β β
β¦ β¨if(π <
πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β ((π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β β
β§ (2nd βπ₯) β β)) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π)))) |
172 | | anass 469 |
. . . . . . . . . . 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 274 |
. . . . . . . . . 10
β’ ((π₯ β (β Γ
β) β§ ((π β
β, π β β
β¦ β¨if(π <
πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ (((1st
βπ₯) β β
β§ (2nd βπ₯) β β) β§ ((π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))))) |
174 | | elxp6 8005 |
. . . . . . . . . 10
β’ (π₯ β ((1...(π β 1)) Γ (1...(π β 1))) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β
(1...(π β 1)) β§
(2nd βπ₯)
β (1...(π β
1))))) |
175 | 169, 173,
174 | 3bitr4g 313 |
. . . . . . . . 9
β’ (π β ((π₯ β (β Γ β) β§
((π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)βπ₯) β ((1...π) Γ (1...π))) β π₯ β ((1...(π β 1)) Γ (1...(π β 1))))) |
176 | 29, 34, 175 | 3bitrd 304 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) β π₯ β ((1...(π β 1)) Γ (1...(π β 1))))) |
177 | 176 | eqrdv 2730 |
. . . . . . 7
β’ (π β (β‘(π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©) β dom π΄) = ((1...(π β 1)) Γ (1...(π β 1)))) |
178 | 25, 177 | eqtrid 2784 |
. . . . . 6
β’ (π β dom (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) = ((1...(π β 1)) Γ (1...(π β 1)))) |
179 | 24, 178 | eqtrd 2772 |
. . . . 5
β’ (π β dom π = ((1...(π β 1)) Γ (1...(π β 1)))) |
180 | 179 | feq2d 6700 |
. . . 4
β’ (π β (π:dom πβΆran π β π:((1...(π β 1)) Γ (1...(π β 1)))βΆran π)) |
181 | 23, 180 | mpbid 231 |
. . 3
β’ (π β π:((1...(π β 1)) Γ (1...(π β 1)))βΆran π) |
182 | 19 | rneqd 5935 |
. . . . 5
β’ (π β ran π = ran (π΄ β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) |
183 | | rncoss 5969 |
. . . . 5
β’ ran
(π΄ β (π β β, π β β β¦
β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©)) β ran π΄ |
184 | 182, 183 | eqsstrdi 4035 |
. . . 4
β’ (π β ran π β ran π΄) |
185 | | frn 6721 |
. . . . 5
β’ (π΄:((1...π) Γ (1...π))βΆπ΅ β ran π΄ β π΅) |
186 | 1, 2, 185 | 3syl 18 |
. . . 4
β’ (π β ran π΄ β π΅) |
187 | 184, 186 | sstrd 3991 |
. . 3
β’ (π β ran π β π΅) |
188 | | fss 6731 |
. . 3
β’ ((π:((1...(π β 1)) Γ (1...(π β 1)))βΆran π β§ ran π β π΅) β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅) |
189 | 181, 187,
188 | syl2anc 584 |
. 2
β’ (π β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅) |
190 | | reldmmap 8825 |
. . . . . 6
β’ Rel dom
βm |
191 | 190 | ovrcl 7446 |
. . . . 5
β’ (π΄ β (π΅ βm ((1...π) Γ (1...π))) β (π΅ β V β§ ((1...π) Γ (1...π)) β V)) |
192 | 1, 191 | syl 17 |
. . . 4
β’ (π β (π΅ β V β§ ((1...π) Γ (1...π)) β V)) |
193 | 192 | simpld 495 |
. . 3
β’ (π β π΅ β V) |
194 | | ovex 7438 |
. . . 4
β’
(1...(π β 1))
β V |
195 | | ovex 7438 |
. . . 4
β’
(1...(π β 1))
β V |
196 | 194, 195 | xpex 7736 |
. . 3
β’
((1...(π β 1))
Γ (1...(π β
1))) β V |
197 | | elmapg 8829 |
. . 3
β’ ((π΅ β V β§ ((1...(π β 1)) Γ (1...(π β 1))) β V) β
(π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1)))) β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅)) |
198 | 193, 196,
197 | sylancl 586 |
. 2
β’ (π β (π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1)))) β π:((1...(π β 1)) Γ (1...(π β 1)))βΆπ΅)) |
199 | 189, 198 | mpbird 256 |
1
β’ (π β π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1))))) |