Step | Hyp | Ref
| Expression |
1 | | 2sbcrex 41136 |
. . . . . . 7
β’
([(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π β βπ₯ β β0
[(πβπ) / π£][(πβπΏ) / π€]βπ¦ β β0 π) |
2 | | 2sbcrex 41136 |
. . . . . . . 8
β’
([(πβπ) / π£][(πβπΏ) / π€]βπ¦ β β0 π β βπ¦ β β0 [(πβπ) / π£][(πβπΏ) / π€]π) |
3 | 2 | rexbii 3098 |
. . . . . . 7
β’
(βπ₯ β
β0 [(πβπ) / π£][(πβπΏ) / π€]βπ¦ β β0 π β βπ₯ β β0 βπ¦ β β0
[(πβπ) / π£][(πβπΏ) / π€]π) |
4 | 1, 3 | bitri 275 |
. . . . . 6
β’
([(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π β βπ₯ β β0
βπ¦ β
β0 [(πβπ) / π£][(πβπΏ) / π€]π) |
5 | 4 | sbcbii 3804 |
. . . . 5
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π β [(π βΎ (1...π)) / π’]βπ₯ β β0 βπ¦ β β0
[(πβπ) / π£][(πβπΏ) / π€]π) |
6 | | sbc2rex 41139 |
. . . . 5
β’
([(π βΎ
(1...π)) / π’]βπ₯ β β0
βπ¦ β
β0 [(πβπ) / π£][(πβπΏ) / π€]π β βπ₯ β β0 βπ¦ β β0
[(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
7 | 5, 6 | bitri 275 |
. . . 4
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π β βπ₯ β β0
βπ¦ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
8 | 7 | rabbii 3416 |
. . 3
β’ {π β (β0
βm (1...πΏ))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π} = {π β (β0
βm (1...πΏ))
β£ βπ₯ β
β0 βπ¦ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} |
9 | | rexfrabdioph.2 |
. . . . . . 7
β’ πΏ = (π + 1) |
10 | | rexfrabdioph.1 |
. . . . . . . . 9
β’ π = (π + 1) |
11 | | nn0p1nn 12459 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β) |
12 | 10, 11 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
13 | 12 | peano2nnd 12177 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β) |
14 | 9, 13 | eqeltrid 2842 |
. . . . . 6
β’ (π β β0
β πΏ β
β) |
15 | 14 | nnnn0d 12480 |
. . . . 5
β’ (π β β0
β πΏ β
β0) |
16 | 15 | adantr 482 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½)) β πΏ β
β0) |
17 | | sbcrot3 41143 |
. . . . . . . . . 10
β’
([(π βΎ
(1...π)) / π’][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(πβπ) / π£][(πβπΏ) / π€]π β [(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
18 | | sbcrot3 41143 |
. . . . . . . . . . . . 13
β’
([(π‘βπ½) / π¦][(πβπ) / π£][(πβπΏ) / π€]π β [(πβπ) / π£][(πβπΏ) / π€][(π‘βπ½) / π¦]π) |
19 | 18 | sbcbii 3804 |
. . . . . . . . . . . 12
β’
([(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(πβπ) / π£][(πβπΏ) / π€]π β [(π‘βπΎ) / π₯][(πβπ) / π£][(πβπΏ) / π€][(π‘βπ½) / π¦]π) |
20 | | sbcrot3 41143 |
. . . . . . . . . . . 12
β’
([(π‘βπΎ) / π₯][(πβπ) / π£][(πβπΏ) / π€][(π‘βπ½) / π¦]π β [(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
21 | 19, 20 | bitri 275 |
. . . . . . . . . . 11
β’
([(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(πβπ) / π£][(πβπΏ) / π€]π β [(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
22 | 21 | sbcbii 3804 |
. . . . . . . . . 10
β’
([(π βΎ
(1...π)) / π’][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(πβπ) / π£][(πβπΏ) / π€]π β [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
23 | 17, 22 | bitr3i 277 |
. . . . . . . . 9
β’
([(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π β [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
24 | 23 | sbcbii 3804 |
. . . . . . . 8
β’
([(π‘ βΎ
(1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π β [(π‘ βΎ (1...πΏ)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
25 | | reseq1 5936 |
. . . . . . . . . 10
β’ (π = (π‘ βΎ (1...πΏ)) β (π βΎ (1...π)) = ((π‘ βΎ (1...πΏ)) βΎ (1...π))) |
26 | 25 | sbccomieg 41145 |
. . . . . . . . 9
β’
([(π‘ βΎ
(1...πΏ)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [((π‘ βΎ (1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
27 | | fzssp1 13491 |
. . . . . . . . . . . . 13
β’
(1...π) β
(1...(π +
1)) |
28 | 10 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’
(1...π) =
(1...(π +
1)) |
29 | 27, 28 | sseqtrri 3986 |
. . . . . . . . . . . 12
β’
(1...π) β
(1...π) |
30 | | fzssp1 13491 |
. . . . . . . . . . . . 13
β’
(1...π) β
(1...(π +
1)) |
31 | 9 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’
(1...πΏ) =
(1...(π +
1)) |
32 | 30, 31 | sseqtrri 3986 |
. . . . . . . . . . . 12
β’
(1...π) β
(1...πΏ) |
33 | 29, 32 | sstri 3958 |
. . . . . . . . . . 11
β’
(1...π) β
(1...πΏ) |
34 | | resabs1 5972 |
. . . . . . . . . . 11
β’
((1...π) β
(1...πΏ) β ((π‘ βΎ (1...πΏ)) βΎ (1...π)) = (π‘ βΎ (1...π))) |
35 | | dfsbcq 3746 |
. . . . . . . . . . 11
β’ (((π‘ βΎ (1...πΏ)) βΎ (1...π)) = (π‘ βΎ (1...π)) β ([((π‘ βΎ (1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . 10
β’
([((π‘ βΎ
(1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
37 | | fveq1 6846 |
. . . . . . . . . . . . 13
β’ (π = (π‘ βΎ (1...πΏ)) β (πβπ) = ((π‘ βΎ (1...πΏ))βπ)) |
38 | 37 | sbccomieg 41145 |
. . . . . . . . . . . 12
β’
([(π‘ βΎ
(1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [((π‘ βΎ (1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
39 | | elfz1end 13478 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β (1...π)) |
40 | 12, 39 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β (1...π)) |
41 | 32, 40 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β (1...πΏ)) |
42 | | fvres 6866 |
. . . . . . . . . . . . . 14
β’ (π β (1...πΏ) β ((π‘ βΎ (1...πΏ))βπ) = (π‘βπ)) |
43 | | dfsbcq 3746 |
. . . . . . . . . . . . . 14
β’ (((π‘ βΎ (1...πΏ))βπ) = (π‘βπ) β ([((π‘ βΎ (1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
45 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π‘ β V |
46 | 45 | resex 5990 |
. . . . . . . . . . . . . . . 16
β’ (π‘ βΎ (1...πΏ)) β V |
47 | | fveq1 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π‘ βΎ (1...πΏ)) β (πβπΏ) = ((π‘ βΎ (1...πΏ))βπΏ)) |
48 | 47 | sbcco3gw 4387 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ βΎ (1...πΏ)) β V β ([(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [((π‘ βΎ (1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
([(π‘ βΎ
(1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [((π‘ βΎ (1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π) |
50 | | elfz1end 13478 |
. . . . . . . . . . . . . . . . 17
β’ (πΏ β β β πΏ β (1...πΏ)) |
51 | 14, 50 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β πΏ β (1...πΏ)) |
52 | | fvres 6866 |
. . . . . . . . . . . . . . . 16
β’ (πΏ β (1...πΏ) β ((π‘ βΎ (1...πΏ))βπΏ) = (π‘βπΏ)) |
53 | | dfsbcq 3746 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ βΎ (1...πΏ))βπΏ) = (π‘βπΏ) β ([((π‘ βΎ (1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
54 | 51, 52, 53 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
55 | 49, 54 | bitrid 283 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
56 | 55 | sbcbidv 3803 |
. . . . . . . . . . . . 13
β’ (π β β0
β ([(π‘βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
57 | 44, 56 | bitrd 279 |
. . . . . . . . . . . 12
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
58 | 38, 57 | bitrid 283 |
. . . . . . . . . . 11
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
59 | 58 | sbcbidv 3803 |
. . . . . . . . . 10
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
60 | 36, 59 | bitrid 283 |
. . . . . . . . 9
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
61 | 26, 60 | bitrid 283 |
. . . . . . . 8
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
62 | 24, 61 | bitrid 283 |
. . . . . . 7
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π)) |
63 | 62 | rabbidv 3418 |
. . . . . 6
β’ (π β β0
β {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} = {π‘ β (β0
βm (1...π½))
β£ [(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π}) |
64 | 63 | eleq1d 2823 |
. . . . 5
β’ (π β β0
β ({π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (Diophβπ½) β {π‘ β (β0
βm (1...π½))
β£ [(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½))) |
65 | 64 | biimpar 479 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½)) β {π‘ β (β0
βm (1...π½))
β£ [(π‘ βΎ
(1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (Diophβπ½)) |
66 | | rexfrabdioph.3 |
. . . . 5
β’ πΎ = (πΏ + 1) |
67 | | rexfrabdioph.4 |
. . . . 5
β’ π½ = (πΎ + 1) |
68 | 66, 67 | 2rexfrabdioph 41148 |
. . . 4
β’ ((πΏ β β0
β§ {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (Diophβπ½)) β {π β (β0
βm (1...πΏ))
β£ βπ₯ β
β0 βπ¦ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (DiophβπΏ)) |
69 | 16, 65, 68 | syl2anc 585 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½)) β {π β (β0
βm (1...πΏ))
β£ βπ₯ β
β0 βπ¦ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (DiophβπΏ)) |
70 | 8, 69 | eqeltrid 2842 |
. 2
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½)) β {π β (β0
βm (1...πΏ))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π} β (DiophβπΏ)) |
71 | 10, 9 | 2rexfrabdioph 41148 |
. 2
β’ ((π β β0
β§ {π β
(β0 βm (1...πΏ)) β£ [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
π} β (DiophβπΏ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 βπ₯ β β0
βπ¦ β
β0 π} β
(Diophβπ)) |
72 | 70, 71 | syldan 592 |
1
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π½)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 βπ₯ β β0
βπ¦ β
β0 π} β
(Diophβπ)) |