Step | Hyp | Ref
| Expression |
1 | | sseq1 3970 |
. . . . . . . . 9
β’ (π₯ = β
β (π₯ β β β β
β β)) |
2 | 1 | 3anbi1d 1441 |
. . . . . . . 8
β’ (π₯ = β
β ((π₯ β β β§ π β β β§ πΉ:ββΆβ) β
(β
β β β§ π β β β§ πΉ:ββΆβ))) |
3 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = β
β (βπ β π₯ ((πΉβπ) gcd π) = 1 β βπ β β
((πΉβπ) gcd π) = 1)) |
4 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = β
β (π₯ β {π}) = (β
β {π})) |
5 | 4 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = β
β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
6 | 5 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = β
β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
7 | 2, 3, 6 | 3anbi123d 1437 |
. . . . . . 7
β’ (π₯ = β
β (((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§
βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((β
β β
β§ π β β
β§ πΉ:ββΆβ) β§ βπ β β
((πΉβπ) gcd π) = 1 β§ βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1))) |
8 | | prodeq1 15797 |
. . . . . . . . 9
β’ (π₯ = β
β βπ β π₯ (πΉβπ) = βπ β β
(πΉβπ)) |
9 | 8 | oveq1d 7373 |
. . . . . . . 8
β’ (π₯ = β
β (βπ β π₯ (πΉβπ) gcd π) = (βπ β β
(πΉβπ) gcd π)) |
10 | 9 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = β
β ((βπ β π₯ (πΉβπ) gcd π) = 1 β (βπ β β
(πΉβπ) gcd π) = 1)) |
11 | 7, 10 | imbi12d 345 |
. . . . . 6
β’ (π₯ = β
β ((((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§
βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π₯ (πΉβπ) gcd π) = 1) β (((β
β β
β§ π β β
β§ πΉ:ββΆβ) β§ βπ β β
((πΉβπ) gcd π) = 1 β§ βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β β
(πΉβπ) gcd π) = 1))) |
12 | | sseq1 3970 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ β β β π¦ β β)) |
13 | 12 | 3anbi1d 1441 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π₯ β β β§ π β β β§ πΉ:ββΆβ) β (π¦ β β β§ π β β β§ πΉ:ββΆβ))) |
14 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β π₯ ((πΉβπ) gcd π) = 1 β βπ β π¦ ((πΉβπ) gcd π) = 1)) |
15 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π₯ β {π}) = (π¦ β {π})) |
16 | 15 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = π¦ β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
17 | 16 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
18 | 13, 14, 17 | 3anbi123d 1437 |
. . . . . . 7
β’ (π₯ = π¦ β (((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1))) |
19 | | prodeq1 15797 |
. . . . . . . . 9
β’ (π₯ = π¦ β βπ β π₯ (πΉβπ) = βπ β π¦ (πΉβπ)) |
20 | 19 | oveq1d 7373 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β π₯ (πΉβπ) gcd π) = (βπ β π¦ (πΉβπ) gcd π)) |
21 | 20 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = π¦ β ((βπ β π₯ (πΉβπ) gcd π) = 1 β (βπ β π¦ (πΉβπ) gcd π) = 1)) |
22 | 18, 21 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π¦ β ((((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π₯ (πΉβπ) gcd π) = 1) β (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1))) |
23 | | sseq1 3970 |
. . . . . . . . 9
β’ (π₯ = (π¦ βͺ {π§}) β (π₯ β β β (π¦ βͺ {π§}) β β)) |
24 | 23 | 3anbi1d 1441 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π§}) β ((π₯ β β β§ π β β β§ πΉ:ββΆβ) β ((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ))) |
25 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β π₯ ((πΉβπ) gcd π) = 1 β βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1)) |
26 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = (π¦ βͺ {π§}) β (π₯ β {π}) = ((π¦ βͺ {π§}) β {π})) |
27 | 26 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
28 | 27 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
29 | 24, 25, 28 | 3anbi123d 1437 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π§}) β (((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1))) |
30 | | prodeq1 15797 |
. . . . . . . . 9
β’ (π₯ = (π¦ βͺ {π§}) β βπ β π₯ (πΉβπ) = βπ β (π¦ βͺ {π§})(πΉβπ)) |
31 | 30 | oveq1d 7373 |
. . . . . . . 8
β’ (π₯ = (π¦ βͺ {π§}) β (βπ β π₯ (πΉβπ) gcd π) = (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π)) |
32 | 31 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = (π¦ βͺ {π§}) β ((βπ β π₯ (πΉβπ) gcd π) = 1 β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = 1)) |
33 | 29, 32 | imbi12d 345 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π§}) β ((((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π₯ (πΉβπ) gcd π) = 1) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = 1))) |
34 | | sseq1 3970 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β β β π β β)) |
35 | 34 | 3anbi1d 1441 |
. . . . . . . 8
β’ (π₯ = π β ((π₯ β β β§ π β β β§ πΉ:ββΆβ) β (π β β β§ π β β β§ πΉ:ββΆβ))) |
36 | | raleq 3308 |
. . . . . . . 8
β’ (π₯ = π β (βπ β π₯ ((πΉβπ) gcd π) = 1 β βπ β π ((πΉβπ) gcd π) = 1)) |
37 | | difeq1 4076 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ β {π}) = (π β {π})) |
38 | 37 | raleqdv 3312 |
. . . . . . . . 9
β’ (π₯ = π β (βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
39 | 38 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π₯ = π β (βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
40 | 35, 36, 39 | 3anbi123d 1437 |
. . . . . . 7
β’ (π₯ = π β (((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((π β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π ((πΉβπ) gcd π) = 1 β§ βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1))) |
41 | | prodeq1 15797 |
. . . . . . . . 9
β’ (π₯ = π β βπ β π₯ (πΉβπ) = βπ β π (πΉβπ)) |
42 | 41 | oveq1d 7373 |
. . . . . . . 8
β’ (π₯ = π β (βπ β π₯ (πΉβπ) gcd π) = (βπ β π (πΉβπ) gcd π)) |
43 | 42 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = π β ((βπ β π₯ (πΉβπ) gcd π) = 1 β (βπ β π (πΉβπ) gcd π) = 1)) |
44 | 40, 43 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π β ((((π₯ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π₯ ((πΉβπ) gcd π) = 1 β§ βπ β π₯ βπ β (π₯ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π₯ (πΉβπ) gcd π) = 1) β (((π β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π ((πΉβπ) gcd π) = 1 β§ βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π (πΉβπ) gcd π) = 1))) |
45 | | prod0 15831 |
. . . . . . . . . . 11
β’
βπ β
β
(πΉβπ) = 1 |
46 | 45 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
βπ β β
(πΉβπ) = 1) |
47 | 46 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β β β
(βπ β β
(πΉβπ) gcd π) = (1 gcd π)) |
48 | | nnz 12525 |
. . . . . . . . . 10
β’ (π β β β π β
β€) |
49 | | 1gcd 16419 |
. . . . . . . . . 10
β’ (π β β€ β (1 gcd
π) = 1) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
β’ (π β β β (1 gcd
π) = 1) |
51 | 47, 50 | eqtrd 2773 |
. . . . . . . 8
β’ (π β β β
(βπ β β
(πΉβπ) gcd π) = 1) |
52 | 51 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((β
β β β§ π
β β β§ πΉ:ββΆβ) β
(βπ β β
(πΉβπ) gcd π) = 1) |
53 | 52 | 3ad2ant1 1134 |
. . . . . 6
β’
(((β
β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β β
((πΉβπ) gcd π) = 1 β§ βπ β β
βπ β (β
β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β β
(πΉβπ) gcd π) = 1) |
54 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π(((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) |
55 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π(πΉβπ§) |
56 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β π¦ β Fin) |
57 | | unss 4145 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β β β§ {π§} β β) β (π¦ βͺ {π§}) β β) |
58 | | vex 3448 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π§ β V |
59 | 58 | snss 4747 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β β β {π§} β
β) |
60 | 59 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . 20
β’ ({π§} β β β π§ β
β) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β β β§ {π§} β β) β π§ β
β) |
62 | 57, 61 | sylbir 234 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ βͺ {π§}) β β β π§ β β) |
63 | 62 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β π§ β
β) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β π§ β β) |
65 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β Β¬ π§ β π¦) |
66 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§
(π¦ β Fin β§ Β¬
π§ β π¦)) β§ π β π¦) β πΉ:ββΆβ) |
67 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β β β§ {π§} β β) β π¦ β
β) |
68 | 57, 67 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ βͺ {π§}) β β β π¦ β β) |
69 | 68 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β π¦ β
β) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β π¦ β β) |
71 | 70 | sselda 3945 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§
(π¦ β Fin β§ Β¬
π§ β π¦)) β§ π β π¦) β π β β) |
72 | 66, 71 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . 17
β’
(((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§
(π¦ β Fin β§ Β¬
π§ β π¦)) β§ π β π¦) β (πΉβπ) β β) |
73 | 72 | nncnd 12174 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§
(π¦ β Fin β§ Β¬
π§ β π¦)) β§ π β π¦) β (πΉβπ) β β) |
74 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π = π§ β (πΉβπ) = (πΉβπ§)) |
75 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ βͺ {π§}) β β β§ πΉ:ββΆβ) β πΉ:ββΆβ) |
76 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ βͺ {π§}) β β β§ πΉ:ββΆβ) β π§ β
β) |
77 | 75, 76 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ βͺ {π§}) β β β§ πΉ:ββΆβ) β (πΉβπ§) β β) |
78 | 77 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β (πΉβπ§) β β) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (πΉβπ§) β β) |
80 | 79 | nncnd 12174 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (πΉβπ§) β β) |
81 | 54, 55, 56, 64, 65, 73, 74, 80 | fprodsplitsn 15877 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β βπ β (π¦ βͺ {π§})(πΉβπ) = (βπ β π¦ (πΉβπ) Β· (πΉβπ§))) |
82 | 81 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = ((βπ β π¦ (πΉβπ) Β· (πΉβπ§)) gcd π)) |
83 | 56, 72 | fprodnncl 15843 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β βπ β π¦ (πΉβπ) β β) |
84 | 83 | nnzd 12531 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β βπ β π¦ (πΉβπ) β β€) |
85 | 79 | nnzd 12531 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (πΉβπ§) β β€) |
86 | 84, 85 | zmulcld 12618 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (βπ β π¦ (πΉβπ) Β· (πΉβπ§)) β β€) |
87 | 48 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . 16
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β π β
β€) |
88 | 87 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β π β β€) |
89 | 86, 88 | gcdcomd 16399 |
. . . . . . . . . . . . . 14
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β ((βπ β π¦ (πΉβπ) Β· (πΉβπ§)) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§)))) |
90 | 82, 89 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§)))) |
91 | 90 | ex 414 |
. . . . . . . . . . . 12
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β ((π¦ β Fin β§ Β¬ π§ β π¦) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§))))) |
92 | 91 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((π¦ β Fin β§ Β¬ π§ β π¦) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§))))) |
93 | 92 | com12 32 |
. . . . . . . . . 10
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§))))) |
94 | 93 | adantr 482 |
. . . . . . . . 9
β’ (((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§))))) |
95 | 94 | imp 408 |
. . . . . . . 8
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§)))) |
96 | | simpl2 1193 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β π β β) |
97 | 96, 83, 79 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (π β β β§ βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β)) |
98 | 97 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β ((π¦ β Fin β§ Β¬ π§ β π¦) β (π β β β§ βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β))) |
99 | 98 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((π¦ β Fin β§ Β¬ π§ β π¦) β (π β β β§ βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β))) |
100 | 99 | com12 32 |
. . . . . . . . . . 11
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (π β β β§ βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β))) |
101 | 100 | adantr 482 |
. . . . . . . . . 10
β’ (((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (π β β β§ βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β))) |
102 | 101 | imp 408 |
. . . . . . . . 9
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (π β β β§ βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β)) |
103 | 88, 84 | gcdcomd 16399 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ (π¦ β Fin β§ Β¬ π§ β π¦)) β (π gcd βπ β π¦ (πΉβπ)) = (βπ β π¦ (πΉβπ) gcd π)) |
104 | 103 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β ((π¦ β Fin β§ Β¬ π§ β π¦) β (π gcd βπ β π¦ (πΉβπ)) = (βπ β π¦ (πΉβπ) gcd π))) |
105 | 104 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((π¦ β Fin β§ Β¬ π§ β π¦) β (π gcd βπ β π¦ (πΉβπ)) = (βπ β π¦ (πΉβπ) gcd π))) |
106 | 105 | com12 32 |
. . . . . . . . . . . 12
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (π gcd βπ β π¦ (πΉβπ)) = (βπ β π¦ (πΉβπ) gcd π))) |
107 | 106 | adantr 482 |
. . . . . . . . . . 11
β’ (((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (π gcd βπ β π¦ (πΉβπ)) = (βπ β π¦ (πΉβπ) gcd π))) |
108 | 107 | imp 408 |
. . . . . . . . . 10
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (π gcd βπ β π¦ (πΉβπ)) = (βπ β π¦ (πΉβπ) gcd π)) |
109 | 68 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((π¦ βͺ {π§}) β β β π¦ β β)) |
110 | | idd 24 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (π β β β π β β)) |
111 | | idd 24 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (πΉ:ββΆβ β πΉ:ββΆβ)) |
112 | 109, 110,
111 | 3anim123d 1444 |
. . . . . . . . . . . . 13
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β (π¦ β β β§ π β β β§ πΉ:ββΆβ))) |
113 | | ssun1 4133 |
. . . . . . . . . . . . . 14
β’ π¦ β (π¦ βͺ {π§}) |
114 | | ssralv 4011 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π¦ βͺ {π§}) β (βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β βπ β π¦ ((πΉβπ) gcd π) = 1)) |
115 | 113, 114 | mp1i 13 |
. . . . . . . . . . . . 13
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β βπ β π¦ ((πΉβπ) gcd π) = 1)) |
116 | | ssralv 4011 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π¦ βͺ {π§}) β (βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π¦ βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
117 | 113, 116 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π¦ βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
118 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ β Fin β§ Β¬ π§ β π¦) β§ π β π¦) β π¦ β (π¦ βͺ {π§})) |
119 | 118 | ssdifd 4101 |
. . . . . . . . . . . . . . . 16
β’ (((π¦ β Fin β§ Β¬ π§ β π¦) β§ π β π¦) β (π¦ β {π}) β ((π¦ βͺ {π§}) β {π})) |
120 | | ssralv 4011 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β {π}) β ((π¦ βͺ {π§}) β {π}) β (βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π¦ β Fin β§ Β¬ π§ β π¦) β§ π β π¦) β (βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
122 | 121 | ralimdva 3161 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (βπ β π¦ βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
123 | 117, 122 | syld 47 |
. . . . . . . . . . . . 13
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1)) |
124 | 112, 115,
123 | 3anim123d 1444 |
. . . . . . . . . . . 12
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β ((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1))) |
125 | 124 | imim1d 82 |
. . . . . . . . . . 11
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1))) |
126 | 125 | imp31 419 |
. . . . . . . . . 10
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (βπ β π¦ (πΉβπ) gcd π) = 1) |
127 | 108, 126 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (π gcd βπ β π¦ (πΉβπ)) = 1) |
128 | | rpmulgcd 16442 |
. . . . . . . . 9
β’ (((π β β β§
βπ β π¦ (πΉβπ) β β β§ (πΉβπ§) β β) β§ (π gcd βπ β π¦ (πΉβπ)) = 1) β (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§))) = (π gcd (πΉβπ§))) |
129 | 102, 127,
128 | syl2anc 585 |
. . . . . . . 8
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (π gcd (βπ β π¦ (πΉβπ) Β· (πΉβπ§))) = (π gcd (πΉβπ§))) |
130 | | vsnid 4624 |
. . . . . . . . . . . . . . 15
β’ π§ β {π§} |
131 | 130 | olci 865 |
. . . . . . . . . . . . . 14
β’ (π§ β π¦ β¨ π§ β {π§}) |
132 | | elun 4109 |
. . . . . . . . . . . . . 14
β’ (π§ β (π¦ βͺ {π§}) β (π§ β π¦ β¨ π§ β {π§})) |
133 | 131, 132 | mpbir 230 |
. . . . . . . . . . . . 13
β’ π§ β (π¦ βͺ {π§}) |
134 | 74 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π = π§ β ((πΉβπ) gcd π) = ((πΉβπ§) gcd π)) |
135 | 134 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ (π = π§ β (((πΉβπ) gcd π) = 1 β ((πΉβπ§) gcd π) = 1)) |
136 | 135 | rspcv 3576 |
. . . . . . . . . . . . 13
β’ (π§ β (π¦ βͺ {π§}) β (βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β ((πΉβπ§) gcd π) = 1)) |
137 | 133, 136 | mp1i 13 |
. . . . . . . . . . . 12
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β
(βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β ((πΉβπ§) gcd π) = 1)) |
138 | 137 | imp 408 |
. . . . . . . . . . 11
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1) β ((πΉβπ§) gcd π) = 1) |
139 | 78 | nnzd 12531 |
. . . . . . . . . . . . . 14
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β (πΉβπ§) β β€) |
140 | 87, 139 | gcdcomd 16399 |
. . . . . . . . . . . . 13
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β (π gcd (πΉβπ§)) = ((πΉβπ§) gcd π)) |
141 | 140 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β ((π gcd (πΉβπ§)) = 1 β ((πΉβπ§) gcd π) = 1)) |
142 | 141 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1) β ((π gcd (πΉβπ§)) = 1 β ((πΉβπ§) gcd π) = 1)) |
143 | 138, 142 | mpbird 257 |
. . . . . . . . . 10
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1) β (π gcd (πΉβπ§)) = 1) |
144 | 143 | 3adant3 1133 |
. . . . . . . . 9
β’ ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (π gcd (πΉβπ§)) = 1) |
145 | 144 | adantl 483 |
. . . . . . . 8
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (π gcd (πΉβπ§)) = 1) |
146 | 95, 129, 145 | 3eqtrd 2777 |
. . . . . . 7
β’ ((((π¦ β Fin β§ Β¬ π§ β π¦) β§ (((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1)) β§ (((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1)) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = 1) |
147 | 146 | exp31 421 |
. . . . . 6
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β π¦ ((πΉβπ) gcd π) = 1 β§ βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π¦ (πΉβπ) gcd π) = 1) β ((((π¦ βͺ {π§}) β β β§ π β β β§ πΉ:ββΆβ) β§ βπ β (π¦ βͺ {π§})((πΉβπ) gcd π) = 1 β§ βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β (π¦ βͺ {π§})(πΉβπ) gcd π) = 1))) |
148 | 11, 22, 33, 44, 53, 147 | findcard2s 9112 |
. . . . 5
β’ (π β Fin β (((π β β β§ π β β β§ πΉ:ββΆβ) β§
βπ β π ((πΉβπ) gcd π) = 1 β§ βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1) β (βπ β π (πΉβπ) gcd π) = 1)) |
149 | 148 | 3expd 1354 |
. . . 4
β’ (π β Fin β ((π β β β§ π β β β§ πΉ:ββΆβ) β
(βπ β π ((πΉβπ) gcd π) = 1 β (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β (βπ β π (πΉβπ) gcd π) = 1)))) |
150 | 149 | 3expd 1354 |
. . 3
β’ (π β Fin β (π β β β (π β β β (πΉ:ββΆβ β
(βπ β π ((πΉβπ) gcd π) = 1 β (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β (βπ β π (πΉβπ) gcd π) = 1)))))) |
151 | 150 | 3imp 1112 |
. 2
β’ ((π β Fin β§ π β β β§ π β β) β (πΉ:ββΆβ β
(βπ β π ((πΉβπ) gcd π) = 1 β (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β (βπ β π (πΉβπ) gcd π) = 1)))) |
152 | 151 | 3imp 1112 |
1
β’ (((π β Fin β§ π β β β§ π β β) β§ πΉ:ββΆβ β§
βπ β π ((πΉβπ) gcd π) = 1) β (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β (βπ β π (πΉβπ) gcd π) = 1)) |