| Step | Hyp | Ref
| Expression |
| 1 | | prn0 11029 |
. . . . 5
⊢ (𝐴 ∈ P →
𝐴 ≠
∅) |
| 2 | | r19.2z 4495 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) |
| 3 | 2 | ex 412 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
| 4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝐴 ∈ P →
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
| 5 | | prpssnq 11030 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
𝐴 ⊊
Q) |
| 6 | 5 | pssssd 4100 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
𝐴 ⊆
Q) |
| 7 | 6 | sseld 3982 |
. . . . . . 7
⊢ (𝐴 ∈ P →
((𝑥
+Q 𝐵) ∈ 𝐴 → (𝑥 +Q 𝐵) ∈
Q)) |
| 8 | | addnqf 10988 |
. . . . . . . . . 10
⊢
+Q :(Q ×
Q)⟶Q |
| 9 | 8 | fdmi 6747 |
. . . . . . . . 9
⊢ dom
+Q = (Q ×
Q) |
| 10 | | 0nnq 10964 |
. . . . . . . . 9
⊢ ¬
∅ ∈ Q |
| 11 | 9, 10 | ndmovrcl 7619 |
. . . . . . . 8
⊢ ((𝑥 +Q
𝐵) ∈ Q
→ (𝑥 ∈
Q ∧ 𝐵
∈ Q)) |
| 12 | 11 | simprd 495 |
. . . . . . 7
⊢ ((𝑥 +Q
𝐵) ∈ Q
→ 𝐵 ∈
Q) |
| 13 | 7, 12 | syl6com 37 |
. . . . . 6
⊢ ((𝑥 +Q
𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈
Q)) |
| 14 | 13 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈
Q)) |
| 15 | 14 | com12 32 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → 𝐵 ∈ Q)) |
| 16 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑥 +Q 𝑏) = (𝑥 +Q 𝐵)) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑥 +Q 𝐵) ∈ 𝐴)) |
| 18 | 17 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
| 19 | 18 | notbid 318 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)) |
| 20 | 19 | imbi2d 340 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ P → ¬
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ↔ (𝐴 ∈ P → ¬
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))) |
| 21 | | dfpss2 4088 |
. . . . . . . . . . 11
⊢ (𝐴 ⊊ Q ↔
(𝐴 ⊆ Q
∧ ¬ 𝐴 =
Q)) |
| 22 | 5, 21 | sylib 218 |
. . . . . . . . . 10
⊢ (𝐴 ∈ P →
(𝐴 ⊆ Q
∧ ¬ 𝐴 =
Q)) |
| 23 | 22 | simprd 495 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
¬ 𝐴 =
Q) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q)
→ ¬ 𝐴 =
Q) |
| 25 | 6 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 ⊆ Q) |
| 26 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝐴 ∈
P) |
| 27 | | n0 4353 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
| 28 | 1, 27 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ P →
∃𝑦 𝑦 ∈ 𝐴) |
| 29 | 26, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → ∃𝑦 𝑦 ∈ 𝐴) |
| 30 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ Q) |
| 31 | | simpl2 1193 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑏 ∈ Q) |
| 32 | | recclnq 11006 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ Q →
(*Q‘𝑏) ∈ Q) |
| 33 | | mulclnq 10987 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Q ∧
(*Q‘𝑏) ∈ Q) → (𝑤
·Q (*Q‘𝑏)) ∈
Q) |
| 34 | | archnq 11020 |
. . . . . . . . . . . . . . . . 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 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Q ∧
𝑏 ∈ Q)
→ ∃𝑧 ∈
N (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉) |
| 37 | 30, 31, 36 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → ∃𝑧 ∈ N (𝑤 ·Q
(*Q‘𝑏)) <Q 〈𝑧,
1o〉) |
| 38 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 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 11012 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Q →
((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ (𝑏
·Q (𝑤 ·Q
(*Q‘𝑏))) <Q (𝑏
·Q 〈𝑧, 1o〉))) |
| 42 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑏 ∈ V |
| 43 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑤 ∈ V |
| 44 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(*Q‘𝑏) ∈ V |
| 45 | | mulcomnq 10993 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣
·Q 𝑥) = (𝑥 ·Q 𝑣) |
| 46 | | mulassnq 10999 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣
·Q 𝑥) ·Q 𝑦) = (𝑣 ·Q (𝑥
·Q 𝑦)) |
| 47 | 42, 43, 44, 45, 46 | caov12 7661 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏
·Q (𝑤 ·Q
(*Q‘𝑏))) = (𝑤 ·Q (𝑏
·Q (*Q‘𝑏))) |
| 48 | | mulcomnq 10993 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏
·Q 〈𝑧, 1o〉) = (〈𝑧, 1o〉
·Q 𝑏) |
| 49 | 47, 48 | breq12i 5152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏
·Q (𝑤 ·Q
(*Q‘𝑏))) <Q (𝑏
·Q 〈𝑧, 1o〉) ↔ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏)) |
| 50 | 41, 49 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ Q →
((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
| 52 | | recidnq 11005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ Q →
(𝑏
·Q (*Q‘𝑏)) =
1Q) |
| 53 | 52 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Q →
(𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) = (𝑤 ·Q
1Q)) |
| 54 | | mulidnq 11003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ Q →
(𝑤
·Q 1Q) = 𝑤) |
| 55 | 53, 54 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) = 𝑤) |
| 56 | 55 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑤
·Q (𝑏 ·Q
(*Q‘𝑏))) <Q
(〈𝑧,
1o〉 ·Q 𝑏) ↔ 𝑤 <Q (〈𝑧, 1o〉
·Q 𝑏))) |
| 57 | 51, 56 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉 ↔ 𝑤 <Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
| 58 | 57 | biimpa 476 |
. . . . . . . . . . . . . . . . 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 10967 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ N →
〈𝑧,
1o〉 ∈ Q) |
| 62 | | mulclnq 10987 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑧,
1o〉 ∈ Q ∧ 𝑏 ∈ Q) → (〈𝑧, 1o〉
·Q 𝑏) ∈ Q) |
| 63 | 61, 62 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (〈𝑧,
1o〉 ·Q 𝑏) ∈ Q) |
| 64 | 60, 38, 63 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (〈𝑧, 1o〉
·Q 𝑏) ∈ Q) |
| 65 | | simpll1 1213 |
. . . . . . . . . . . . . . . . . 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 11031 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ P ∧
𝑦 ∈ 𝐴) → 𝑦 ∈ Q) |
| 68 | 65, 66, 67 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑦 ∈
Q) |
| 69 | | ltaddnq 11014 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑧,
1o〉 ·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(〈𝑧,
1o〉 ·Q 𝑏) <Q
((〈𝑧,
1o〉 ·Q 𝑏) +Q 𝑦)) |
| 70 | | addcomnq 10991 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑧,
1o〉 ·Q 𝑏) +Q 𝑦) = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) |
| 71 | 69, 70 | breqtrdi 5184 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑧,
1o〉 ·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(〈𝑧,
1o〉 ·Q 𝑏) <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
| 72 | 64, 68, 71 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → (〈𝑧, 1o〉
·Q 𝑏) <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
| 73 | | ltsonq 11009 |
. . . . . . . . . . . . . . . . 17
⊢
<Q Or Q |
| 74 | | ltrelnq 10966 |
. . . . . . . . . . . . . . . . 17
⊢
<Q ⊆ (Q ×
Q) |
| 75 | 73, 74 | sotri 6147 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 <Q
(〈𝑧,
1o〉 ·Q 𝑏) ∧ (〈𝑧, 1o〉
·Q 𝑏) <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) → 𝑤 <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏))) |
| 76 | 59, 72, 75 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → 𝑤 <Q
(𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏))) |
| 77 | | simpll3 1215 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤
·Q (*Q‘𝑏))
<Q 〈𝑧, 1o〉)) → ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) |
| 78 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 1o →
〈𝑤,
1o〉 = 〈1o,
1o〉) |
| 79 | | df-1nq 10956 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
1Q = 〈1o,
1o〉 |
| 80 | 78, 79 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 1o →
〈𝑤,
1o〉 = 1Q) |
| 81 | 80 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 1o →
(〈𝑤,
1o〉 ·Q 𝑏) = (1Q
·Q 𝑏)) |
| 82 | 81 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 1o → (𝑦 +Q
(〈𝑤,
1o〉 ·Q 𝑏)) = (𝑦 +Q
(1Q ·Q 𝑏))) |
| 83 | 82 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 1o → ((𝑦 +Q
(〈𝑤,
1o〉 ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴)) |
| 84 | 83 | imbi2d 340 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 1o → (((𝑏 ∈ Q ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴))) |
| 85 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → 〈𝑤, 1o〉 = 〈𝑧,
1o〉) |
| 86 | 85 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → (〈𝑤, 1o〉
·Q 𝑏) = (〈𝑧, 1o〉
·Q 𝑏)) |
| 87 | 86 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑧 → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏))) |
| 88 | 87 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑧 → ((𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴)) |
| 89 | 88 | imbi2d 340 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑧 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴))) |
| 90 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (𝑧 +N 1o)
→ 〈𝑤,
1o〉 = 〈(𝑧 +N 1o),
1o〉) |
| 91 | 90 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (𝑧 +N 1o)
→ (〈𝑤,
1o〉 ·Q 𝑏) = (〈(𝑧 +N 1o),
1o〉 ·Q 𝑏)) |
| 92 | 91 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝑧 +N 1o)
→ (𝑦
+Q (〈𝑤, 1o〉
·Q 𝑏)) = (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏))) |
| 93 | 92 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝑧 +N 1o)
→ ((𝑦
+Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴)) |
| 94 | 93 | imbi2d 340 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝑧 +N 1o)
→ (((𝑏 ∈
Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑤, 1o〉
·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
| 95 | | mulcomnq 10993 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1Q ·Q 𝑏) = (𝑏 ·Q
1Q) |
| 96 | | mulidnq 11003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ Q →
(𝑏
·Q 1Q) = 𝑏) |
| 97 | 95, 96 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Q →
(1Q ·Q 𝑏) = 𝑏) |
| 98 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝑥 +Q 𝑏) = (𝑦 +Q 𝑏)) |
| 99 | 98 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴)) |
| 100 | 99 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q 𝑏) ∈ 𝐴) |
| 101 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1Q ·Q 𝑏) = 𝑏 → (𝑦 +Q
(1Q ·Q 𝑏)) = (𝑦 +Q 𝑏)) |
| 102 | 101 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1Q ·Q 𝑏) = 𝑏 → ((𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴)) |
| 103 | 102 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1Q ·Q 𝑏) = 𝑏 ∧ (𝑦 +Q 𝑏) ∈ 𝐴) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴) |
| 104 | 97, 100, 103 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ Q ∧
(∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴) |
| 105 | 104 | 3impb 1115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ Q ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q
(1Q ·Q 𝑏)) ∈ 𝐴) |
| 106 | | 3simpa 1149 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ Q ∧
∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴)) |
| 107 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) → (𝑥 +Q 𝑏) = ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏)) |
| 108 | 107 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) ∈ 𝐴)) |
| 109 | 108 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) ∈ 𝐴) |
| 110 | | addassnq 10998 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏)) +Q 𝑏) = (𝑦 +Q ((〈𝑧, 1o〉
·Q 𝑏) +Q 𝑏)) |
| 111 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
〈𝑧,
1o〉 ∈ V |
| 112 | | 1nq 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
1Q ∈ Q |
| 113 | 112 | elexi 3503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
1Q ∈ V |
| 114 | | distrnq 11001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣
·Q (𝑥 +Q 𝑦)) = ((𝑣 ·Q 𝑥) +Q
(𝑣
·Q 𝑦)) |
| 115 | 111, 113,
42, 45, 114 | caovdir 7667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((〈𝑧,
1o〉 ∈ Q ∧ 1Q
∈ Q) → (〈𝑧, 1o〉
+Q 1Q) =
([Q]‘(〈𝑧, 1o〉
+pQ 1Q))) |
| 118 | 61, 112, 117 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ N →
(〈𝑧,
1o〉 +Q 1Q) =
([Q]‘(〈𝑧, 1o〉
+pQ 1Q))) |
| 119 | 79 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(〈𝑧,
1o〉 +pQ 1Q) =
(〈𝑧,
1o〉 +pQ 〈1o,
1o〉) |
| 120 | | 1pi 10923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
1o ∈ N |
| 121 | | addpipq 10977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 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 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ N →
(𝑧
·N 1o) = 𝑧) |
| 126 | | mulidpi 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(1o ∈ N → (1o
·N 1o) =
1o) |
| 127 | 120, 126 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ N →
(1o ·N 1o) =
1o) |
| 128 | 125, 127 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ N →
((𝑧
·N 1o) +N
(1o ·N 1o)) = (𝑧 +N
1o)) |
| 129 | 128, 127 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ N →
([Q]‘(〈𝑧, 1o〉
+pQ 1Q)) =
([Q]‘〈(𝑧 +N 1o),
1o〉)) |
| 132 | | addclpi 10932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑧 ∈ N ∧
1o ∈ N) → (𝑧 +N 1o)
∈ N) |
| 133 | 120, 132 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ N →
(𝑧
+N 1o) ∈
N) |
| 134 | | pinq 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑧 +N
1o) ∈ N → 〈(𝑧 +N 1o),
1o〉 ∈ Q) |
| 135 | | nqerid 10973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (〈𝑧,
1o〉 +Q 1Q) =
〈(𝑧
+N 1o),
1o〉) |
| 139 | 138 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((〈𝑧,
1o〉 +Q 1Q)
·Q 𝑏) = (〈(𝑧 +N 1o),
1o〉 ·Q 𝑏)) |
| 140 | 97 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (1Q ·Q 𝑏) = 𝑏) |
| 141 | 140 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 2826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (((𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏)) +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴)) |
| 146 | 109, 145 | imbitrid 244 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ ((∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴)) |
| 147 | 146 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ N ∧
𝑏 ∈ Q)
→ (∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → ((𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (〈(𝑧 +N
1o), 1o〉 ·Q 𝑏)) ∈ 𝐴))) |
| 148 | 147 | expimpd 453 |
. . . . . . . . . . . . . . . . . . . . 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 10947 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ N →
((𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴)) |
| 152 | 151 | imp 406 |
. . . . . . . . . . . . . . . . 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 11033 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
(𝑦
+Q (〈𝑧, 1o〉
·Q 𝑏)) ∈ 𝐴) → (𝑤 <Q (𝑦 +Q
(〈𝑧,
1o〉 ·Q 𝑏)) → 𝑤 ∈ 𝐴)) |
| 155 | 65, 153, 154 | syl2anc 584 |
. . . . . . . . . . . . . . 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 3161 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ 𝐴) |
| 158 | 157 | expr 456 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴)) |
| 159 | 158 | exlimdv 1933 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (∃𝑦 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴)) |
| 160 | 29, 159 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝑤 ∈ 𝐴) |
| 161 | 25, 160 | eqelssd 4005 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q
∧ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 = Q) |
| 162 | 161 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q)
→ (∀𝑥 ∈
𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → 𝐴 = Q)) |
| 163 | 24, 162 | mtod 198 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑏 ∈ Q)
→ ¬ ∀𝑥
∈ 𝐴 (𝑥 +Q
𝑏) ∈ 𝐴) |
| 164 | 163 | expcom 413 |
. . . . . 6
⊢ (𝑏 ∈ Q →
(𝐴 ∈ P
→ ¬ ∀𝑥
∈ 𝐴 (𝑥 +Q
𝑏) ∈ 𝐴)) |
| 165 | 20, 164 | vtoclga 3577 |
. . . . 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 190 |
. 2
⊢ (𝐴 ∈ P →
¬ ∀𝑥 ∈
𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) |
| 169 | | rexnal 3100 |
. 2
⊢
(∃𝑥 ∈
𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) |
| 170 | 168, 169 | sylibr 234 |
1
⊢ (𝐴 ∈ P →
∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴) |