Step | Hyp | Ref
| Expression |
1 | | prn0 10603 |
. . . . 5
⊢ (𝐴 ∈ P →
𝐴 ≠
∅) |
2 | | r19.2z 4406 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) |
3 | 2 | ex 416 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝐴 ∈ P →
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
5 | | prpssnq 10604 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
𝐴 ⊊
Q) |
6 | 5 | pssssd 4012 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
𝐴 ⊆
Q) |
7 | 6 | sseld 3900 |
. . . . . . 7
⊢ (𝐴 ∈ P →
((𝑥
+Q 𝐵) ∈ 𝐴 → (𝑥 +Q 𝐵) ∈
Q)) |
8 | | addnqf 10562 |
. . . . . . . . . 10
⊢
+Q :(Q ×
Q)⟶Q |
9 | 8 | fdmi 6557 |
. . . . . . . . 9
⊢ dom
+Q = (Q ×
Q) |
10 | | 0nnq 10538 |
. . . . . . . . 9
⊢ ¬
∅ ∈ Q |
11 | 9, 10 | ndmovrcl 7394 |
. . . . . . . 8
⊢ ((𝑥 +Q
𝐵) ∈ Q
→ (𝑥 ∈
Q ∧ 𝐵
∈ Q)) |
12 | 11 | simprd 499 |
. . . . . . 7
⊢ ((𝑥 +Q
𝐵) ∈ Q
→ 𝐵 ∈
Q) |
13 | 7, 12 | syl6com 37 |
. . . . . 6
⊢ ((𝑥 +Q
𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈
Q)) |
14 | 13 | rexlimivw 3201 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈
Q)) |
15 | 14 | com12 32 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → 𝐵 ∈ Q)) |
16 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑥 +Q 𝑏) = (𝑥 +Q 𝐵)) |
17 | 16 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑥 +Q 𝐵) ∈ 𝐴)) |
18 | 17 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
19 | 18 | notbid 321 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
20 | 19 | imbi2d 344 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ P → ¬
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ↔ (𝐴 ∈ P → ¬
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))) |
21 | | dfpss2 4000 |
. . . . . . . . . . 11
⊢ (𝐴 ⊊ Q ↔
(𝐴 ⊆ Q
∧ ¬ 𝐴 =
Q)) |
22 | 5, 21 | sylib 221 |
. . . . . . . . . 10
⊢ (𝐴 ∈ P →
(𝐴 ⊆ Q
∧ ¬ 𝐴 =
Q)) |
23 | 22 | simprd 499 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
¬ 𝐴 =
Q) |
24 | 23 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q)
→ ¬ 𝐴 =
Q) |
25 | 6 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 ⊆ Q) |
26 | | simpl1 1193 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝐴 ∈
P) |
27 | | n0 4261 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
28 | 1, 27 | sylib 221 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ P →
∃𝑦 𝑦 ∈ 𝐴) |
29 | 26, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → ∃𝑦 𝑦 ∈ 𝐴) |
30 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ Q) |
31 | | simpl2 1194 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑏 ∈ Q) |
32 | | recclnq 10580 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ Q →
(*Q‘𝑏) ∈ Q) |
33 | | mulclnq 10561 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Q ∧
(*Q‘𝑏) ∈ Q) → (𝑤
·Q (*Q‘𝑏)) ∈
Q) |
34 | | archnq 10594 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤
·Q (*Q‘𝑏)) ∈ Q →
∃𝑧 ∈
N (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Q ∧
(*Q‘𝑏) ∈ Q) → ∃𝑧 ∈ N (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉) |
36 | 32, 35 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Q ∧
𝑏 ∈ Q)
→ ∃𝑧 ∈
N (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉) |
37 | 30, 31, 36 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → ∃𝑧 ∈ N (𝑤 ·Q
(*Q‘𝑏)) <Q 〈𝑧,
1o〉) |
38 | | simpll2 1215 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑏 ∈
Q) |
39 | | simplrl 777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑤 ∈
Q) |
40 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉) |
41 | | ltmnq 10586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Q →
((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ (𝑏
·Q (𝑤 ·Q
(*Q‘𝑏))) <Q (𝑏
·Q 〈𝑧, 1o〉))) |
42 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑏 ∈ V |
43 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑤 ∈ V |
44 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(*Q‘𝑏) ∈ V |
45 | | mulcomnq 10567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣
·Q 𝑥) = (𝑥 ·Q 𝑣) |
46 | | mulassnq 10573 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣
·Q 𝑥) ·Q 𝑦) = (𝑣 ·Q (𝑥
·Q 𝑦)) |
47 | 42, 43, 44, 45, 46 | caov12 7436 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏
·Q (𝑤 ·Q
(*Q‘𝑏))) = (𝑤 ·Q (𝑏
·Q (*Q‘𝑏))) |
48 | | mulcomnq 10567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏
·Q 〈𝑧, 1o〉) = (〈𝑧, 1o〉
·Q 𝑏) |
49 | 47, 48 | breq12i 5062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏
·Q (𝑤 ·Q
(*Q‘𝑏))) <Q (𝑏
·Q 〈𝑧, 1o〉) ↔ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏)) |
50 | 41, 49 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ Q →
((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
51 | 50 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
52 | | recidnq 10579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ Q →
(𝑏
·Q (*Q‘𝑏)) =
1Q) |
53 | 52 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Q →
(𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) = (𝑤 ·Q
1Q)) |
54 | | mulidnq 10577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ Q →
(𝑤
·Q 1Q) = 𝑤) |
55 | 53, 54 | sylan9eq 2798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) = 𝑤) |
56 | 55 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏) ↔ 𝑤 <Q (〈𝑧, 1o〉
·Q 𝑏))) |
57 | 51, 56 | bitrd 282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ 𝑤 <Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
58 | 57 | biimpa 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉) → 𝑤 <Q
(〈𝑧,
1o〉 ·Q 𝑏)) |
59 | 38, 39, 40, 58 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑤 <Q
(〈𝑧,
1o〉 ·Q 𝑏)) |
60 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑧 ∈
N) |
61 | | pinq 10541 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ N →
〈𝑧,
1o〉 ∈ Q) |
62 | | mulclnq 10561 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑧,
1o〉 ∈ Q ∧ 𝑏 ∈ Q) → (〈𝑧, 1o〉
·Q 𝑏) ∈ Q) |
63 | 61, 62 | sylan 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (〈𝑧,
1o〉 ·Q 𝑏) ∈ Q) |
64 | 60, 38, 63 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (〈𝑧, 1o〉
·Q 𝑏) ∈ Q) |
65 | | simpll1 1214 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝐴 ∈
P) |
66 | | simplrr 778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑦 ∈ 𝐴) |
67 | | elprnq 10605 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ P ∧
𝑦 ∈ 𝐴) → 𝑦 ∈ Q) |
68 | 65, 66, 67 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑦 ∈
Q) |
69 | | ltaddnq 10588 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑧,
1o〉 ·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(〈𝑧,
1o〉 ·Q 𝑏) <Q
((〈𝑧,
1o〉 ·Q 𝑏) +Q 𝑦)) |
70 | | addcomnq 10565 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑧,
1o〉 ·Q 𝑏) +Q 𝑦) = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) |
71 | 69, 70 | breqtrdi 5094 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑧,
1o〉 ·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(〈𝑧,
1o〉 ·Q 𝑏) <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
72 | 64, 68, 71 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (〈𝑧, 1o〉
·Q 𝑏) <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
73 | | ltsonq 10583 |
. . . . . . . . . . . . . . . . 17
⊢
<Q Or Q |
74 | | ltrelnq 10540 |
. . . . . . . . . . . . . . . . 17
⊢
<Q ⊆ (Q ×
Q) |
75 | 73, 74 | sotri 5992 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 <Q
(〈𝑧,
1o〉 ·Q 𝑏) ∧ (〈𝑧, 1o〉
·Q 𝑏) <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) → 𝑤 <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
76 | 59, 72, 75 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑤 <Q
(𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏))) |
77 | | simpll3 1216 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) |
78 | | opeq1 4784 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 1o →
〈𝑤,
1o〉 = 〈1o,
1o〉) |
79 | | df-1nq 10530 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
1Q = 〈1o,
1o〉 |
80 | 78, 79 | eqtr4di 2796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 1o →
〈𝑤,
1o〉 = 1Q) |
81 | 80 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 1o →
(〈𝑤,
1o〉 ·Q 𝑏) = (1Q
·Q 𝑏)) |
82 | 81 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 1o → (𝑦 +Q
(〈𝑤,
1o〉 ·Q 𝑏)) = (𝑦 +Q
(1Q ·Q 𝑏))) |
83 | 82 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 1o → ((𝑦 +Q
(〈𝑤,
1o〉 ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴)) |
84 | 83 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 1o → (((𝑏 ∈ Q ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴))) |
85 | | opeq1 4784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → 〈𝑤, 1o〉 = 〈𝑧,
1o〉) |
86 | 85 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → (〈𝑤, 1o〉
·Q 𝑏) = (〈𝑧, 1o〉
·Q 𝑏)) |
87 | 86 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑧 → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏))) |
88 | 87 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑧 → ((𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴)) |
89 | 88 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑧 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴))) |
90 | | opeq1 4784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (𝑧 +N 1o)
→ 〈𝑤,
1o〉 = 〈(𝑧 +N 1o),
1o〉) |
91 | 90 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (𝑧 +N 1o)
→ (〈𝑤,
1o〉 ·Q 𝑏) = (〈(𝑧 +N 1o),
1o〉 ·Q 𝑏)) |
92 | 91 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝑧 +N 1o)
→ (𝑦
+Q (〈𝑤, 1o〉
·Q 𝑏)) = (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏))) |
93 | 92 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝑧 +N 1o)
→ ((𝑦
+Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴)) |
94 | 93 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝑧 +N 1o)
→ (((𝑏 ∈
Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
95 | | mulcomnq 10567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1Q ·Q 𝑏) = (𝑏 ·Q
1Q) |
96 | | mulidnq 10577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ Q →
(𝑏
·Q 1Q) = 𝑏) |
97 | 95, 96 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Q →
(1Q ·Q 𝑏) = 𝑏) |
98 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝑥 +Q 𝑏) = (𝑦 +Q 𝑏)) |
99 | 98 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴)) |
100 | 99 | rspccva 3536 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q 𝑏) ∈ 𝐴) |
101 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1Q ·Q 𝑏) = 𝑏 → (𝑦 +Q
(1Q ·Q 𝑏)) = (𝑦 +Q 𝑏)) |
102 | 101 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1Q ·Q 𝑏) = 𝑏 → ((𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴)) |
103 | 102 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1Q ·Q 𝑏) = 𝑏 ∧ (𝑦 +Q 𝑏) ∈ 𝐴) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴) |
104 | 97, 100, 103 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ Q ∧
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴) |
105 | 104 | 3impb 1117 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ Q ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴) |
106 | | 3simpa 1150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ Q ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴)) |
107 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) → (𝑥 +Q 𝑏) = ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏)) |
108 | 107 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) ∈ 𝐴)) |
109 | 108 | rspccva 3536 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) ∈ 𝐴) |
110 | | addassnq 10572 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏)) +Q 𝑏) = (𝑦 +Q ((〈𝑧, 1o〉
·Q 𝑏) +Q 𝑏)) |
111 | | opex 5348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
〈𝑧,
1o〉 ∈ V |
112 | | 1nq 10542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
1Q ∈ Q |
113 | 112 | elexi 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
1Q ∈ V |
114 | | distrnq 10575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣
·Q (𝑥 +Q 𝑦)) = ((𝑣 ·Q 𝑥) +Q
(𝑣
·Q 𝑦)) |
115 | 111, 113,
42, 45, 114 | caovdir 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((〈𝑧,
1o〉 +Q 1Q)
·Q 𝑏) = ((〈𝑧, 1o〉
·Q 𝑏) +Q
(1Q ·Q 𝑏)) |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((〈𝑧,
1o〉 +Q 1Q)
·Q 𝑏) = ((〈𝑧, 1o〉
·Q 𝑏) +Q
(1Q ·Q 𝑏))) |
117 | | addpqnq 10552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((〈𝑧,
1o〉 ∈ Q ∧ 1Q
∈ Q) → (〈𝑧, 1o〉
+Q 1Q) =
([Q]‘(〈𝑧, 1o〉
+pQ 1Q))) |
118 | 61, 112, 117 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ N →
(〈𝑧,
1o〉 +Q 1Q) =
([Q]‘(〈𝑧, 1o〉
+pQ 1Q))) |
119 | 79 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(〈𝑧,
1o〉 +pQ 1Q) =
(〈𝑧,
1o〉 +pQ 〈1o,
1o〉) |
120 | | 1pi 10497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
1o ∈ N |
121 | | addpipq 10551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑧 ∈ N ∧
1o ∈ N) ∧ (1o ∈
N ∧ 1o ∈ N)) →
(〈𝑧,
1o〉 +pQ 〈1o,
1o〉) = 〈((𝑧 ·N
1o) +N (1o
·N 1o)), (1o
·N 1o)〉) |
122 | 120, 120,
121 | mpanr12 705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ N ∧
1o ∈ N) → (〈𝑧, 1o〉
+pQ 〈1o, 1o〉) =
〈((𝑧
·N 1o) +N
(1o ·N 1o)),
(1o ·N
1o)〉) |
123 | 120, 122 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ N →
(〈𝑧,
1o〉 +pQ 〈1o,
1o〉) = 〈((𝑧 ·N
1o) +N (1o
·N 1o)), (1o
·N 1o)〉) |
124 | 119, 123 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ N →
(〈𝑧,
1o〉 +pQ 1Q) =
〈((𝑧
·N 1o) +N
(1o ·N 1o)),
(1o ·N
1o)〉) |
125 | | mulidpi 10500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ N →
(𝑧
·N 1o) = 𝑧) |
126 | | mulidpi 10500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(1o ∈ N → (1o
·N 1o) =
1o) |
127 | 120, 126 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ N →
(1o ·N 1o) =
1o) |
128 | 125, 127 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ N →
((𝑧
·N 1o) +N
(1o ·N 1o)) = (𝑧 +N
1o)) |
129 | 128, 127 | opeq12d 4792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ N →
〈((𝑧
·N 1o) +N
(1o ·N 1o)),
(1o ·N 1o)〉 =
〈(𝑧
+N 1o),
1o〉) |
130 | 124, 129 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ N →
(〈𝑧,
1o〉 +pQ 1Q) =
〈(𝑧
+N 1o),
1o〉) |
131 | 130 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ N →
([Q]‘(〈𝑧, 1o〉
+pQ 1Q)) =
([Q]‘〈(𝑧 +N 1o),
1o〉)) |
132 | | addclpi 10506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑧 ∈ N ∧
1o ∈ N) → (𝑧 +N 1o)
∈ N) |
133 | 120, 132 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ N →
(𝑧
+N 1o) ∈
N) |
134 | | pinq 10541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑧 +N
1o) ∈ N → 〈(𝑧 +N 1o),
1o〉 ∈ Q) |
135 | | nqerid 10547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(〈(𝑧
+N 1o), 1o〉 ∈
Q → ([Q]‘〈(𝑧 +N 1o),
1o〉) = 〈(𝑧 +N 1o),
1o〉) |
136 | 133, 134,
135 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ N →
([Q]‘〈(𝑧 +N 1o),
1o〉) = 〈(𝑧 +N 1o),
1o〉) |
137 | 118, 131,
136 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ N →
(〈𝑧,
1o〉 +Q 1Q) =
〈(𝑧
+N 1o),
1o〉) |
138 | 137 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (〈𝑧,
1o〉 +Q 1Q) =
〈(𝑧
+N 1o),
1o〉) |
139 | 138 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((〈𝑧,
1o〉 +Q 1Q)
·Q 𝑏) = (〈(𝑧 +N 1o),
1o〉 ·Q 𝑏)) |
140 | 97 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (1Q ·Q 𝑏) = 𝑏) |
141 | 140 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((〈𝑧,
1o〉 ·Q 𝑏) +Q
(1Q ·Q 𝑏)) = ((〈𝑧, 1o〉
·Q 𝑏) +Q 𝑏)) |
142 | 116, 139,
141 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((〈𝑧,
1o〉 ·Q 𝑏) +Q 𝑏) = (〈(𝑧 +N 1o),
1o〉 ·Q 𝑏)) |
143 | 142 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (𝑦
+Q ((〈𝑧, 1o〉
·Q 𝑏) +Q 𝑏)) = (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏))) |
144 | 110, 143 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) = (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏))) |
145 | 144 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (((𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴)) |
146 | 109, 145 | syl5ib 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴)) |
147 | 146 | expd 419 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
148 | 147 | expimpd 457 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ N →
((𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
149 | 106, 148 | syl5 34 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ N →
((𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
150 | 149 | a2d 29 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ N →
(((𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
151 | 84, 89, 94, 89, 105, 150 | indpi 10521 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ N →
((𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴)) |
152 | 151 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ N ∧
(𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) |
153 | 60, 38, 77, 66, 152 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏)) ∈ 𝐴) |
154 | | prcdnq 10607 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
(𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → (𝑤 <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏)) → 𝑤 ∈ 𝐴)) |
155 | 65, 153, 154 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (𝑤 <Q
(𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏)) → 𝑤 ∈ 𝐴)) |
156 | 76, 155 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑤 ∈ 𝐴) |
157 | 37, 156 | rexlimddv 3210 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ 𝐴) |
158 | 157 | expr 460 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴)) |
159 | 158 | exlimdv 1941 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (∃𝑦 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴)) |
160 | 29, 159 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝑤 ∈ 𝐴) |
161 | 25, 160 | eqelssd 3922 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 = Q) |
162 | 161 | 3expia 1123 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q)
→ (∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → 𝐴 = Q)) |
163 | 24, 162 | mtod 201 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q)
→ ¬ ∀𝑥
∈ 𝐴 (𝑥 +Q
𝑏) ∈ 𝐴) |
164 | 163 | expcom 417 |
. . . . . 6
⊢ (𝑏 ∈ Q →
(𝐴 ∈ P
→ ¬ ∀𝑥
∈ 𝐴 (𝑥 +Q
𝑏) ∈ 𝐴)) |
165 | 20, 164 | vtoclga 3489 |
. . . . 5
⊢ (𝐵 ∈ Q →
(𝐴 ∈ P
→ ¬ ∀𝑥
∈ 𝐴 (𝑥 +Q
𝐵) ∈ 𝐴)) |
166 | 165 | com12 32 |
. . . 4
⊢ (𝐴 ∈ P →
(𝐵 ∈ Q
→ ¬ ∀𝑥
∈ 𝐴 (𝑥 +Q
𝐵) ∈ 𝐴)) |
167 | 4, 15, 166 | 3syld 60 |
. . 3
⊢ (𝐴 ∈ P →
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
168 | 167 | pm2.01d 193 |
. 2
⊢ (𝐴 ∈ P →
¬ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) |
169 | | rexnal 3160 |
. 2
⊢
(∃𝑥 ∈
𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) |
170 | 168, 169 | sylibr 237 |
1
⊢ (𝐴 ∈ P →
∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴) |