Step | Hyp | Ref
| Expression |
1 | | cleq1lem 14873 |
. . . . . . 7
β’ (π₯ = β
β ((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β
(β
β β β§ (πΎ β β β§ πΉ:ββΆβ)))) |
2 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = β
β (π₯ β {π}) = (β
β {π})) |
3 | 2 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = β
β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
4 | 3 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = β
β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
5 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = β
β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β β
(πΉβπ) β₯ πΎ)) |
6 | 4, 5 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = β
β
((βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ) β (βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β β
(πΉβπ) β₯ πΎ))) |
7 | 1, 6 | anbi12d 632 |
. . . . . 6
β’ (π₯ = β
β (((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β ((β
β β β§
(πΎ β β β§
πΉ:ββΆβ))
β§ (βπ β
β
βπ β
(β
β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β β
(πΉβπ) β₯ πΎ)))) |
8 | | prodeq1 15797 |
. . . . . . 7
β’ (π₯ = β
β βπ β π₯ (πΉβπ) = βπ β β
(πΉβπ)) |
9 | 8 | breq1d 5116 |
. . . . . 6
β’ (π₯ = β
β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β β
(πΉβπ) β₯ πΎ)) |
10 | 7, 9 | imbi12d 345 |
. . . . 5
β’ (π₯ = β
β ((((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β βπ β π₯ (πΉβπ) β₯ πΎ) β (((β
β β β§
(πΎ β β β§
πΉ:ββΆβ))
β§ (βπ β
β
βπ β
(β
β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β β
(πΉβπ) β₯ πΎ)) β βπ β β
(πΉβπ) β₯ πΎ))) |
11 | | cleq1lem 14873 |
. . . . . . 7
β’ (π₯ = π¦ β ((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β (π¦ β β β§ (πΎ β β β§ πΉ:ββΆβ)))) |
12 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π₯ β {π}) = (π¦ β {π})) |
13 | 12 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = π¦ β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
14 | 13 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
15 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β π¦ (πΉβπ) β₯ πΎ)) |
16 | 14, 15 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = π¦ β ((βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ) β (βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π¦ (πΉβπ) β₯ πΎ))) |
17 | 11, 16 | anbi12d 632 |
. . . . . 6
β’ (π₯ = π¦ β (((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β ((π¦ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π¦ (πΉβπ) β₯ πΎ)))) |
18 | | prodeq1 15797 |
. . . . . . 7
β’ (π₯ = π¦ β βπ β π₯ (πΉβπ) = βπ β π¦ (πΉβπ)) |
19 | 18 | breq1d 5116 |
. . . . . 6
β’ (π₯ = π¦ β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β π¦ (πΉβπ) β₯ πΎ)) |
20 | 17, 19 | imbi12d 345 |
. . . . 5
β’ (π₯ = π¦ β ((((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β βπ β π₯ (πΉβπ) β₯ πΎ) β (((π¦ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π¦ (πΉβπ) β₯ πΎ)) β βπ β π¦ (πΉβπ) β₯ πΎ))) |
21 | | cleq1lem 14873 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π§}) β ((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β ((π¦ βͺ {π§}) β β β§ (πΎ β β β§ πΉ:ββΆβ)))) |
22 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = (π¦ βͺ {π§}) β (π₯ β {π}) = ((π¦ βͺ {π§}) β {π})) |
23 | 22 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
24 | 23 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
25 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ)) |
26 | 24, 25 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π§}) β ((βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ) β (βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ))) |
27 | 21, 26 | anbi12d 632 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π§}) β (((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β (((π¦ βͺ {π§}) β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ)))) |
28 | | prodeq1 15797 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π§}) β βπ β π₯ (πΉβπ) = βπ β (π¦ βͺ {π§})(πΉβπ)) |
29 | 28 | breq1d 5116 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ)) |
30 | 27, 29 | imbi12d 345 |
. . . . 5
β’ (π₯ = (π¦ βͺ {π§}) β ((((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β βπ β π₯ (πΉβπ) β₯ πΎ) β ((((π¦ βͺ {π§}) β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ)) β βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ))) |
31 | | cleq1lem 14873 |
. . . . . . 7
β’ (π₯ = π β ((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β (π β β β§ (πΎ β β β§ πΉ:ββΆβ)))) |
32 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ β {π}) = (π β {π})) |
33 | 32 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = π β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
34 | 33 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = π β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
35 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = π β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β π (πΉβπ) β₯ πΎ)) |
36 | 34, 35 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = π β ((βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ) β (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ))) |
37 | 31, 36 | anbi12d 632 |
. . . . . 6
β’ (π₯ = π β (((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β ((π β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ)))) |
38 | | prodeq1 15797 |
. . . . . . 7
β’ (π₯ = π β βπ β π₯ (πΉβπ) = βπ β π (πΉβπ)) |
39 | 38 | breq1d 5116 |
. . . . . 6
β’ (π₯ = π β (βπ β π₯ (πΉβπ) β₯ πΎ β βπ β π (πΉβπ) β₯ πΎ)) |
40 | 37, 39 | imbi12d 345 |
. . . . 5
β’ (π₯ = π β ((((π₯ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π₯ (πΉβπ) β₯ πΎ)) β βπ β π₯ (πΉβπ) β₯ πΎ) β (((π β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ)) β βπ β π (πΉβπ) β₯ πΎ))) |
41 | | prod0 15831 |
. . . . . . . 8
β’
βπ β
β
(πΉβπ) = 1 |
42 | | nnz 12525 |
. . . . . . . . 9
β’ (πΎ β β β πΎ β
β€) |
43 | | 1dvds 16158 |
. . . . . . . . 9
β’ (πΎ β β€ β 1 β₯
πΎ) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
β’ (πΎ β β β 1 β₯
πΎ) |
45 | 41, 44 | eqbrtrid 5141 |
. . . . . . 7
β’ (πΎ β β β
βπ β β
(πΉβπ) β₯ πΎ) |
46 | 45 | adantr 482 |
. . . . . 6
β’ ((πΎ β β β§ πΉ:ββΆβ) β
βπ β β
(πΉβπ) β₯ πΎ) |
47 | 46 | ad2antlr 726 |
. . . . 5
β’
(((β
β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β β
(πΉβπ) β₯ πΎ)) β βπ β β
(πΉβπ) β₯ πΎ) |
48 | | coprmproddvdslem 16543 |
. . . . 5
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π¦ (πΉβπ) β₯ πΎ)) β βπ β π¦ (πΉβπ) β₯ πΎ) β ((((π¦ βͺ {π§}) β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ)) β βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ))) |
49 | 10, 20, 30, 40, 47, 48 | findcard2s 9112 |
. . . 4
β’ (π β Fin β (((π β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§
(βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ)) β βπ β π (πΉβπ) β₯ πΎ)) |
50 | 49 | exp4c 434 |
. . 3
β’ (π β Fin β (π β β β ((πΎ β β β§ πΉ:ββΆβ) β
((βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ) β βπ β π (πΉβπ) β₯ πΎ)))) |
51 | 50 | impcom 409 |
. 2
β’ ((π β β β§ π β Fin) β ((πΎ β β β§ πΉ:ββΆβ) β
((βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ) β βπ β π (πΉβπ) β₯ πΎ))) |
52 | 51 | 3imp 1112 |
1
β’ (((π β β β§ π β Fin) β§ (πΎ β β β§ πΉ:ββΆβ) β§
(βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ)) β βπ β π (πΉβπ) β₯ πΎ) |