Step | Hyp | Ref
| Expression |
1 | | sbc2rex 41139 |
. . . . . 6
β’
([(πβπ) / π£]βπ€ β β0 βπ₯ β β0
π β βπ€ β β0
βπ₯ β
β0 [(πβπ) / π£]π) |
2 | 1 | sbcbii 3804 |
. . . . 5
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 βπ₯ β β0
π β [(π βΎ (1...π)) / π’]βπ€ β β0 βπ₯ β β0
[(πβπ) / π£]π) |
3 | | sbc2rex 41139 |
. . . . 5
β’
([(π βΎ
(1...π)) / π’]βπ€ β β0
βπ₯ β
β0 [(πβπ) / π£]π β βπ€ β β0 βπ₯ β β0
[(π βΎ
(1...π)) / π’][(πβπ) / π£]π) |
4 | 2, 3 | bitri 275 |
. . . 4
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 βπ₯ β β0
π β βπ€ β β0
βπ₯ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π) |
5 | 4 | rabbii 3416 |
. . 3
β’ {π β (β0
βm (1...π))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 βπ₯ β β0
π} = {π β (β0
βm (1...π))
β£ βπ€ β
β0 βπ₯ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π} |
6 | | rexfrabdioph.1 |
. . . . . . 7
β’ π = (π + 1) |
7 | | nn0p1nn 12459 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β) |
8 | 6, 7 | eqeltrid 2842 |
. . . . . 6
β’ (π β β0
β π β
β) |
9 | 8 | nnnn0d 12480 |
. . . . 5
β’ (π β β0
β π β
β0) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ)) β π β
β0) |
11 | | sbcrot3 41143 |
. . . . . . . . . . 11
β’
([(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(πβπ) / π£]π) |
12 | 11 | sbcbii 3804 |
. . . . . . . . . 10
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π βΎ (1...π)) / π’][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(πβπ) / π£]π) |
13 | | sbcrot3 41143 |
. . . . . . . . . 10
β’
([(π βΎ
(1...π)) / π’][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(πβπ) / π£]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π) |
14 | 12, 13 | bitri 275 |
. . . . . . . . 9
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π) |
15 | 14 | sbcbii 3804 |
. . . . . . . 8
β’
([(π‘ βΎ
(1...π)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘ βΎ (1...π)) / π][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π) |
16 | | reseq1 5936 |
. . . . . . . . . 10
β’ (π = (π‘ βΎ (1...π)) β (π βΎ (1...π)) = ((π‘ βΎ (1...π)) βΎ (1...π))) |
17 | 16 | sbccomieg 41145 |
. . . . . . . . 9
β’
([(π‘ βΎ
(1...π)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [((π‘ βΎ (1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π) |
18 | | fzssp1 13491 |
. . . . . . . . . . . 12
β’
(1...π) β
(1...(π +
1)) |
19 | 6 | oveq2i 7373 |
. . . . . . . . . . . 12
β’
(1...π) =
(1...(π +
1)) |
20 | 18, 19 | sseqtrri 3986 |
. . . . . . . . . . 11
β’
(1...π) β
(1...π) |
21 | | resabs1 5972 |
. . . . . . . . . . 11
β’
((1...π) β
(1...π) β ((π‘ βΎ (1...π)) βΎ (1...π)) = (π‘ βΎ (1...π))) |
22 | | dfsbcq 3746 |
. . . . . . . . . . 11
β’ (((π‘ βΎ (1...π)) βΎ (1...π)) = (π‘ βΎ (1...π)) β ([((π‘ βΎ (1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
23 | 20, 21, 22 | mp2b 10 |
. . . . . . . . . 10
β’
([((π‘ βΎ
(1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π) |
24 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π‘ β V |
25 | 24 | resex 5990 |
. . . . . . . . . . . . 13
β’ (π‘ βΎ (1...π)) β V |
26 | | fveq1 6846 |
. . . . . . . . . . . . . 14
β’ (π = (π‘ βΎ (1...π)) β (πβπ) = ((π‘ βΎ (1...π))βπ)) |
27 | 26 | sbcco3gw 4387 |
. . . . . . . . . . . . 13
β’ ((π‘ βΎ (1...π)) β V β ([(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [((π‘ βΎ (1...π))βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
28 | 25, 27 | ax-mp 5 |
. . . . . . . . . . . 12
β’
([(π‘ βΎ
(1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [((π‘ βΎ (1...π))βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π) |
29 | | elfz1end 13478 |
. . . . . . . . . . . . . 14
β’ (π β β β π β (1...π)) |
30 | 8, 29 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β (1...π)) |
31 | | fvres 6866 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β ((π‘ βΎ (1...π))βπ) = (π‘βπ)) |
32 | | dfsbcq 3746 |
. . . . . . . . . . . . 13
β’ (((π‘ βΎ (1...π))βπ) = (π‘βπ) β ([((π‘ βΎ (1...π))βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β β0
β ([((π‘ βΎ
(1...π))βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
34 | 28, 33 | bitrid 283 |
. . . . . . . . . . 11
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
35 | 34 | sbcbidv 3803 |
. . . . . . . . . 10
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
36 | 23, 35 | bitrid 283 |
. . . . . . . . 9
β’ (π β β0
β ([((π‘ βΎ
(1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
37 | 17, 36 | bitrid 283 |
. . . . . . . 8
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
38 | 15, 37 | bitr3id 285 |
. . . . . . 7
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π)) |
39 | 38 | rabbidv 3418 |
. . . . . 6
β’ (π β β0
β {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π} = {π‘ β (β0
βm (1...πΎ))
β£ [(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π}) |
40 | 39 | eleq1d 2823 |
. . . . 5
β’ (π β β0
β ({π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (DiophβπΎ) β {π‘ β (β0
βm (1...πΎ))
β£ [(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ))) |
41 | 40 | biimpar 479 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ)) β {π‘ β (β0
βm (1...πΎ))
β£ [(π‘ βΎ
(1...π)) / π][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (DiophβπΎ)) |
42 | | rexfrabdioph.2 |
. . . . 5
β’ πΏ = (π + 1) |
43 | | rexfrabdioph.3 |
. . . . 5
β’ πΎ = (πΏ + 1) |
44 | 42, 43 | 2rexfrabdioph 41148 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (DiophβπΎ)) β {π β (β0
βm (1...π))
β£ βπ€ β
β0 βπ₯ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (Diophβπ)) |
45 | 10, 41, 44 | syl2anc 585 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ)) β {π β (β0
βm (1...π))
β£ βπ€ β
β0 βπ₯ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (Diophβπ)) |
46 | 5, 45 | eqeltrid 2842 |
. 2
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ)) β {π β (β0
βm (1...π))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 βπ₯ β β0
π} β (Diophβπ)) |
47 | 6 | rexfrabdioph 41147 |
. 2
β’ ((π β β0
β§ {π β
(β0 βm (1...π)) β£ [(π βΎ (1...π)) / π’][(πβπ) / π£]βπ€ β β0 βπ₯ β β0
π} β (Diophβπ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 βπ₯ β β0
π} β (Diophβπ)) |
48 | 46, 47 | syldan 592 |
1
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 βπ₯ β β0
π} β (Diophβπ)) |