Step | Hyp | Ref
| Expression |
1 | | df-rex 3095 |
. . . . 5
⊢
(∃𝑔 ∈
1P 𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔))) |
2 | | 19.42v 1996 |
. . . . . 6
⊢
(∃𝑔(𝑥 <Q
𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
3 | | elprnq 10148 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → 𝑓 ∈ Q) |
4 | | breq1 4889 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ (𝑓 ·Q 𝑔) <Q
𝑓)) |
5 | | df-1p 10139 |
. . . . . . . . . . . . 13
⊢
1P = {𝑔 ∣ 𝑔 <Q
1Q} |
6 | 5 | abeq2i 2894 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈
1P ↔ 𝑔 <Q
1Q) |
7 | | ltmnq 10129 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑔
<Q 1Q ↔ (𝑓
·Q 𝑔) <Q (𝑓
·Q
1Q))) |
8 | | mulidnq 10120 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Q →
(𝑓
·Q 1Q) = 𝑓) |
9 | 8 | breq2d 4898 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
((𝑓
·Q 𝑔) <Q (𝑓
·Q 1Q) ↔ (𝑓
·Q 𝑔) <Q 𝑓)) |
10 | 7, 9 | bitrd 271 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Q →
(𝑔
<Q 1Q ↔ (𝑓
·Q 𝑔) <Q 𝑓)) |
11 | 6, 10 | syl5rbb 276 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ Q →
((𝑓
·Q 𝑔) <Q 𝑓 ↔ 𝑔 ∈
1P)) |
12 | 4, 11 | sylan9bbr 506 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Q ∧
𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P)) |
13 | 3, 12 | sylan 575 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P)) |
14 | 13 | ex 403 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P))) |
15 | 14 | pm5.32rd 573 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → ((𝑥 <Q 𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)))) |
16 | 15 | exbidv 1964 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔(𝑥 <Q 𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ ∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)))) |
17 | 2, 16 | syl5rbbr 278 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
18 | 1, 17 | syl5bb 275 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
19 | 18 | rexbidva 3233 |
. . 3
⊢ (𝐴 ∈ P →
(∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
20 | | 1pr 10172 |
. . . 4
⊢
1P ∈ P |
21 | | df-mp 10141 |
. . . . 5
⊢
·P = (𝑦 ∈ P, 𝑧 ∈ P ↦ {𝑤 ∣ ∃𝑢 ∈ 𝑦 ∃𝑣 ∈ 𝑧 𝑤 = (𝑢 ·Q 𝑣)}) |
22 | | mulclnq 10104 |
. . . . 5
⊢ ((𝑢 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑢
·Q 𝑣) ∈ Q) |
23 | 21, 22 | genpelv 10157 |
. . . 4
⊢ ((𝐴 ∈ P ∧
1P ∈ P) → (𝑥 ∈ (𝐴 ·P
1P) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔))) |
24 | 20, 23 | mpan2 681 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ (𝐴
·P 1P) ↔
∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔))) |
25 | | prnmax 10152 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝐴 𝑥 <Q 𝑓) |
26 | | ltrelnq 10083 |
. . . . . . . . . . 11
⊢
<Q ⊆ (Q ×
Q) |
27 | 26 | brel 5414 |
. . . . . . . . . 10
⊢ (𝑥 <Q
𝑓 → (𝑥 ∈ Q ∧
𝑓 ∈
Q)) |
28 | | vex 3400 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
29 | | vex 3400 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
30 | | fvex 6459 |
. . . . . . . . . . . . . 14
⊢
(*Q‘𝑓) ∈ V |
31 | | mulcomnq 10110 |
. . . . . . . . . . . . . 14
⊢ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦) |
32 | | mulassnq 10116 |
. . . . . . . . . . . . . 14
⊢ ((𝑦
·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧
·Q 𝑤)) |
33 | 28, 29, 30, 31, 32 | caov12 7139 |
. . . . . . . . . . . . 13
⊢ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q (𝑓
·Q (*Q‘𝑓))) |
34 | | recidnq 10122 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Q →
(𝑓
·Q (*Q‘𝑓)) =
1Q) |
35 | 34 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑥
·Q (𝑓 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
36 | 33, 35 | syl5eq 2825 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Q →
(𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
37 | | mulidnq 10120 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) |
38 | 36, 37 | sylan9eqr 2835 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = 𝑥) |
39 | 38 | eqcomd 2783 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ 𝑥 = (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓)))) |
40 | | ovex 6954 |
. . . . . . . . . . 11
⊢ (𝑥
·Q (*Q‘𝑓)) ∈ V |
41 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑥 ·Q
(*Q‘𝑓)) → (𝑓 ·Q 𝑔) = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓)))) |
42 | 41 | eqeq2d 2787 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑥 ·Q
(*Q‘𝑓)) → (𝑥 = (𝑓 ·Q 𝑔) ↔ 𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))))) |
43 | 40, 42 | spcev 3501 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))) → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) |
44 | 27, 39, 43 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 <Q
𝑓 → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐴 → (𝑥 <Q 𝑓 → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
46 | 45 | ancld 546 |
. . . . . . 7
⊢ (𝑓 ∈ 𝐴 → (𝑥 <Q 𝑓 → (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
47 | 46 | reximia 3189 |
. . . . . 6
⊢
(∃𝑓 ∈
𝐴 𝑥 <Q 𝑓 → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
48 | 25, 47 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
49 | 48 | ex 403 |
. . . 4
⊢ (𝐴 ∈ P →
(𝑥 ∈ 𝐴 → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
50 | | prcdnq 10150 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (𝑥 <Q 𝑓 → 𝑥 ∈ 𝐴)) |
51 | 50 | adantrd 487 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → ((𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ 𝐴)) |
52 | 51 | rexlimdva 3212 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ 𝐴)) |
53 | 49, 52 | impbid 204 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ 𝐴 ↔ ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
54 | 19, 24, 53 | 3bitr4d 303 |
. 2
⊢ (𝐴 ∈ P →
(𝑥 ∈ (𝐴
·P 1P) ↔ 𝑥 ∈ 𝐴)) |
55 | 54 | eqrdv 2775 |
1
⊢ (𝐴 ∈ P →
(𝐴
·P 1P) = 𝐴) |