| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ltrelnq 10966 | . . . . 5
⊢ 
<Q ⊆ (Q ×
Q) | 
| 2 | 1 | brel 5750 | . . . 4
⊢
(1Q <Q 𝐵 →
(1Q ∈ Q ∧ 𝐵 ∈ Q)) | 
| 3 | 2 | simprd 495 | . . 3
⊢
(1Q <Q 𝐵 → 𝐵 ∈ Q) | 
| 4 | 3 | adantl 481 | . 2
⊢ ((𝐴 ∈ P ∧
1Q <Q 𝐵) → 𝐵 ∈ Q) | 
| 5 |  | breq2 5147 | . . . . 5
⊢ (𝑏 = 𝐵 → (1Q
<Q 𝑏 ↔ 1Q
<Q 𝐵)) | 
| 6 | 5 | anbi2d 630 | . . . 4
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ P ∧
1Q <Q 𝑏) ↔ (𝐴 ∈ P ∧
1Q <Q 𝐵))) | 
| 7 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑥 ·Q 𝑏) = (𝑥 ·Q 𝐵)) | 
| 8 | 7 | eleq1d 2826 | . . . . . 6
⊢ (𝑏 = 𝐵 → ((𝑥 ·Q 𝑏) ∈ 𝐴 ↔ (𝑥 ·Q 𝐵) ∈ 𝐴)) | 
| 9 | 8 | notbid 318 | . . . . 5
⊢ (𝑏 = 𝐵 → (¬ (𝑥 ·Q 𝑏) ∈ 𝐴 ↔ ¬ (𝑥 ·Q 𝐵) ∈ 𝐴)) | 
| 10 | 9 | rexbidv 3179 | . . . 4
⊢ (𝑏 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝐵) ∈ 𝐴)) | 
| 11 | 6, 10 | imbi12d 344 | . . 3
⊢ (𝑏 = 𝐵 → (((𝐴 ∈ P ∧
1Q <Q 𝑏) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴) ↔ ((𝐴 ∈ P ∧
1Q <Q 𝐵) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝐵) ∈ 𝐴))) | 
| 12 |  | prn0 11029 | . . . . . 6
⊢ (𝐴 ∈ P →
𝐴 ≠
∅) | 
| 13 |  | n0 4353 | . . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) | 
| 14 | 12, 13 | sylib 218 | . . . . 5
⊢ (𝐴 ∈ P →
∃𝑦 𝑦 ∈ 𝐴) | 
| 15 | 14 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ P ∧
1Q <Q 𝑏) → ∃𝑦 𝑦 ∈ 𝐴) | 
| 16 |  | elprnq 11031 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝑦 ∈ 𝐴) → 𝑦 ∈ Q) | 
| 17 | 16 | ad2ant2r 747 | . . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → 𝑦 ∈ Q) | 
| 18 |  | mulidnq 11003 | . . . . . . . . . 10
⊢ (𝑦 ∈ Q →
(𝑦
·Q 1Q) = 𝑦) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → (𝑦 ·Q
1Q) = 𝑦) | 
| 20 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → 1Q
<Q 𝑏) | 
| 21 |  | ltmnq 11012 | . . . . . . . . . . 11
⊢ (𝑦 ∈ Q →
(1Q <Q 𝑏 ↔ (𝑦 ·Q
1Q) <Q (𝑦 ·Q 𝑏))) | 
| 22 | 21 | biimpa 476 | . . . . . . . . . 10
⊢ ((𝑦 ∈ Q ∧
1Q <Q 𝑏) → (𝑦 ·Q
1Q) <Q (𝑦 ·Q 𝑏)) | 
| 23 | 17, 20, 22 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → (𝑦 ·Q
1Q) <Q (𝑦 ·Q 𝑏)) | 
| 24 | 19, 23 | eqbrtrrd 5167 | . . . . . . . 8
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → 𝑦 <Q (𝑦
·Q 𝑏)) | 
| 25 | 1 | brel 5750 | . . . . . . . . . . . 12
⊢
(1Q <Q 𝑏 →
(1Q ∈ Q ∧ 𝑏 ∈ Q)) | 
| 26 | 25 | simprd 495 | . . . . . . . . . . 11
⊢
(1Q <Q 𝑏 → 𝑏 ∈ Q) | 
| 27 | 26 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → 𝑏 ∈ Q) | 
| 28 |  | mulclnq 10987 | . . . . . . . . . 10
⊢ ((𝑦 ∈ Q ∧
𝑏 ∈ Q)
→ (𝑦
·Q 𝑏) ∈ Q) | 
| 29 | 17, 27, 28 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → (𝑦 ·Q 𝑏) ∈
Q) | 
| 30 |  | ltexnq 11015 | . . . . . . . . 9
⊢ ((𝑦
·Q 𝑏) ∈ Q → (𝑦 <Q
(𝑦
·Q 𝑏) ↔ ∃𝑧(𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏))) | 
| 31 | 29, 30 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → (𝑦 <Q (𝑦
·Q 𝑏) ↔ ∃𝑧(𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏))) | 
| 32 | 24, 31 | mpbid 232 | . . . . . . 7
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → ∃𝑧(𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) | 
| 33 |  | simplll 775 | . . . . . . . . 9
⊢ ((((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → 𝐴 ∈ P) | 
| 34 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑧 ∈ V | 
| 35 | 34 | prlem934 11073 | . . . . . . . . 9
⊢ (𝐴 ∈ P →
∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝑧) ∈ 𝐴) | 
| 36 | 33, 35 | syl 17 | . . . . . . . 8
⊢ ((((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝑧) ∈ 𝐴) | 
| 37 | 33 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ P) | 
| 38 |  | simprr 773 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → (𝑦 ·Q 𝑏) ∈ 𝐴) | 
| 39 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 +Q
𝑧) = (𝑦 ·Q 𝑏) → ((𝑦 +Q 𝑧) ∈ 𝐴 ↔ (𝑦 ·Q 𝑏) ∈ 𝐴)) | 
| 40 | 39 | biimparc 479 | . . . . . . . . . . . . . 14
⊢ (((𝑦
·Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → (𝑦 +Q 𝑧) ∈ 𝐴) | 
| 41 | 38, 40 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → (𝑦 +Q 𝑧) ∈ 𝐴) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (𝑦 +Q 𝑧) ∈ 𝐴) | 
| 43 |  | elprnq 11031 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → 𝑥 ∈ Q) | 
| 44 | 33, 43 | sylan 580 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ Q) | 
| 45 |  | elprnq 11031 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
(𝑦
+Q 𝑧) ∈ 𝐴) → (𝑦 +Q 𝑧) ∈
Q) | 
| 46 |  | addnqf 10988 | . . . . . . . . . . . . . . . . . . 19
⊢ 
+Q :(Q ×
Q)⟶Q | 
| 47 | 46 | fdmi 6747 | . . . . . . . . . . . . . . . . . 18
⊢ dom
+Q = (Q ×
Q) | 
| 48 |  | 0nnq 10964 | . . . . . . . . . . . . . . . . . 18
⊢  ¬
∅ ∈ Q | 
| 49 | 47, 48 | ndmovrcl 7619 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 +Q
𝑧) ∈ Q
→ (𝑦 ∈
Q ∧ 𝑧
∈ Q)) | 
| 50 | 49 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 +Q
𝑧) ∈ Q
→ 𝑧 ∈
Q) | 
| 51 | 45, 50 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
(𝑦
+Q 𝑧) ∈ 𝐴) → 𝑧 ∈ Q) | 
| 52 | 33, 41, 51 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → 𝑧 ∈ Q) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ Q) | 
| 54 |  | addclnq 10985 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑥
+Q 𝑧) ∈ Q) | 
| 55 | 44, 53, 54 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (𝑥 +Q 𝑧) ∈
Q) | 
| 56 |  | prub 11034 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
(𝑦
+Q 𝑧) ∈ 𝐴) ∧ (𝑥 +Q 𝑧) ∈ Q) →
(¬ (𝑥
+Q 𝑧) ∈ 𝐴 → (𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧))) | 
| 57 | 37, 42, 55, 56 | syl21anc 838 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 +Q 𝑧) ∈ 𝐴 → (𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧))) | 
| 58 | 27 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ Q) | 
| 59 |  | mulclnq 10987 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Q ∧
𝑏 ∈ Q)
→ (𝑥
·Q 𝑏) ∈ Q) | 
| 60 | 44, 58, 59 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ·Q 𝑏) ∈
Q) | 
| 61 | 17 | ad2antrr 726 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ Q) | 
| 62 |  | simplr 769 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) | 
| 63 |  | recclnq 11006 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Q →
(*Q‘𝑦) ∈ Q) | 
| 64 |  | mulclnq 10987 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ Q ∧
(*Q‘𝑦) ∈ Q) → (𝑧
·Q (*Q‘𝑦)) ∈
Q) | 
| 65 | 63, 64 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑧
·Q (*Q‘𝑦)) ∈
Q) | 
| 66 | 65 | ancoms 458 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑧
·Q (*Q‘𝑦)) ∈
Q) | 
| 67 |  | ltmnq 11012 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧
·Q (*Q‘𝑦)) ∈ Q →
(𝑦
<Q 𝑥 ↔ ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑦) <Q
((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 68 | 66, 67 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
<Q 𝑥 ↔ ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑦) <Q
((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 69 |  | mulassnq 10999 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧
·Q (*Q‘𝑦))
·Q 𝑦) = (𝑧 ·Q
((*Q‘𝑦) ·Q 𝑦)) | 
| 70 |  | mulcomnq 10993 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((*Q‘𝑦) ·Q 𝑦) = (𝑦 ·Q
(*Q‘𝑦)) | 
| 71 | 70 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧
·Q ((*Q‘𝑦)
·Q 𝑦)) = (𝑧 ·Q (𝑦
·Q (*Q‘𝑦))) | 
| 72 | 69, 71 | eqtri 2765 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧
·Q (*Q‘𝑦))
·Q 𝑦) = (𝑧 ·Q (𝑦
·Q (*Q‘𝑦))) | 
| 73 |  | recidnq 11005 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ Q →
(𝑦
·Q (*Q‘𝑦)) =
1Q) | 
| 74 | 73 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Q →
(𝑧
·Q (𝑦 ·Q
(*Q‘𝑦))) = (𝑧 ·Q
1Q)) | 
| 75 |  | mulidnq 11003 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ Q →
(𝑧
·Q 1Q) = 𝑧) | 
| 76 | 74, 75 | sylan9eq 2797 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑧
·Q (𝑦 ·Q
(*Q‘𝑦))) = 𝑧) | 
| 77 | 72, 76 | eqtrid 2789 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ ((𝑧
·Q (*Q‘𝑦))
·Q 𝑦) = 𝑧) | 
| 78 | 77 | breq1d 5153 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (((𝑧
·Q (*Q‘𝑦))
·Q 𝑦) <Q ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥) ↔ 𝑧 <Q ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 79 | 68, 78 | bitrd 279 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
<Q 𝑥 ↔ 𝑧 <Q ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 80 | 79 | adantll 714 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
𝑧 ∈ Q)
→ (𝑦
<Q 𝑥 ↔ 𝑧 <Q ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 81 |  | mulnqf 10989 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 
·Q :(Q ×
Q)⟶Q | 
| 82 | 81 | fdmi 6747 | . . . . . . . . . . . . . . . . . . . . 21
⊢ dom
·Q = (Q ×
Q) | 
| 83 | 82, 48 | ndmovrcl 7619 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥
·Q 𝑏) ∈ Q → (𝑥 ∈ Q ∧
𝑏 ∈
Q)) | 
| 84 | 83 | simpld 494 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥
·Q 𝑏) ∈ Q → 𝑥 ∈
Q) | 
| 85 |  | ltanq 11011 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ Q →
(𝑧
<Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
+Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥)))) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥
·Q 𝑏) ∈ Q → (𝑧 <Q
((𝑧
·Q (*Q‘𝑦))
·Q 𝑥) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
+Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥)))) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(𝑧
<Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
+Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥)))) | 
| 88 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V | 
| 89 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥
·Q (*Q‘𝑦)) ∈ V | 
| 90 |  | mulcomnq 10993 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢
·Q 𝑤) = (𝑤 ·Q 𝑢) | 
| 91 |  | distrnq 11001 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢
·Q (𝑤 +Q 𝑣)) = ((𝑢 ·Q 𝑤) +Q
(𝑢
·Q 𝑣)) | 
| 92 | 88, 34, 89, 90, 91 | caovdir 7667 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 +Q
𝑧)
·Q (𝑥 ·Q
(*Q‘𝑦))) = ((𝑦 ·Q (𝑥
·Q (*Q‘𝑦))) +Q
(𝑧
·Q (𝑥 ·Q
(*Q‘𝑦)))) | 
| 93 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑥 ∈ V | 
| 94 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(*Q‘𝑦) ∈ V | 
| 95 |  | mulassnq 10999 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢
·Q 𝑤) ·Q 𝑣) = (𝑢 ·Q (𝑤
·Q 𝑣)) | 
| 96 | 88, 93, 94, 90, 95 | caov12 7661 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦
·Q (𝑥 ·Q
(*Q‘𝑦))) = (𝑥 ·Q (𝑦
·Q (*Q‘𝑦))) | 
| 97 | 73 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ Q →
(𝑥
·Q (𝑦 ·Q
(*Q‘𝑦))) = (𝑥 ·Q
1Q)) | 
| 98 |  | mulidnq 11003 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) | 
| 99 | 84, 98 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥
·Q 𝑏) ∈ Q → (𝑥
·Q 1Q) = 𝑥) | 
| 100 | 97, 99 | sylan9eqr 2799 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(𝑥
·Q (𝑦 ·Q
(*Q‘𝑦))) = 𝑥) | 
| 101 | 96, 100 | eqtrid 2789 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(𝑦
·Q (𝑥 ·Q
(*Q‘𝑦))) = 𝑥) | 
| 102 |  | mulcomnq 10993 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥
·Q (*Q‘𝑦)) =
((*Q‘𝑦) ·Q 𝑥) | 
| 103 | 102 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧
·Q (𝑥 ·Q
(*Q‘𝑦))) = (𝑧 ·Q
((*Q‘𝑦) ·Q 𝑥)) | 
| 104 |  | mulassnq 10999 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥) = (𝑧 ·Q
((*Q‘𝑦) ·Q 𝑥)) | 
| 105 | 103, 104 | eqtr4i 2768 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧
·Q (𝑥 ·Q
(*Q‘𝑦))) = ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥) | 
| 106 | 105 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(𝑧
·Q (𝑥 ·Q
(*Q‘𝑦))) = ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥)) | 
| 107 | 101, 106 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
((𝑦
·Q (𝑥 ·Q
(*Q‘𝑦))) +Q (𝑧
·Q (𝑥 ·Q
(*Q‘𝑦)))) = (𝑥 +Q ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 108 | 92, 107 | eqtrid 2789 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))) = (𝑥 +Q ((𝑧
·Q (*Q‘𝑦))
·Q 𝑥))) | 
| 109 | 108 | breq2d 5155 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
((𝑥
+Q 𝑧) <Q ((𝑦 +Q
𝑧)
·Q (𝑥 ·Q
(*Q‘𝑦))) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
+Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥)))) | 
| 110 | 87, 109 | bitr4d 282 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
(𝑧
<Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥) ↔ (𝑥 +Q 𝑧) <Q
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))))) | 
| 111 | 110 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
𝑧 ∈ Q)
→ (𝑧
<Q ((𝑧 ·Q
(*Q‘𝑦)) ·Q 𝑥) ↔ (𝑥 +Q 𝑧) <Q
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))))) | 
| 112 | 80, 111 | bitrd 279 | . . . . . . . . . . . . . 14
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
𝑧 ∈ Q)
→ (𝑦
<Q 𝑥 ↔ (𝑥 +Q 𝑧) <Q
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))))) | 
| 113 | 112 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
(𝑧 ∈ Q
∧ (𝑦
+Q 𝑧) = (𝑦 ·Q 𝑏))) → (𝑦 <Q 𝑥 ↔ (𝑥 +Q 𝑧) <Q
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))))) | 
| 114 |  | ltanq 11011 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ Q →
(𝑦
<Q 𝑥 ↔ (𝑧 +Q 𝑦) <Q
(𝑧
+Q 𝑥))) | 
| 115 |  | addcomnq 10991 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 +Q
𝑦) = (𝑦 +Q 𝑧) | 
| 116 |  | addcomnq 10991 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 +Q
𝑥) = (𝑥 +Q 𝑧) | 
| 117 | 115, 116 | breq12i 5152 | . . . . . . . . . . . . . . 15
⊢ ((𝑧 +Q
𝑦)
<Q (𝑧 +Q 𝑥) ↔ (𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧)) | 
| 118 | 114, 117 | bitrdi 287 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ Q →
(𝑦
<Q 𝑥 ↔ (𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧))) | 
| 119 | 118 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
(𝑧 ∈ Q
∧ (𝑦
+Q 𝑧) = (𝑦 ·Q 𝑏))) → (𝑦 <Q 𝑥 ↔ (𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧))) | 
| 120 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 +Q
𝑧) = (𝑦 ·Q 𝑏) → ((𝑦 +Q 𝑧)
·Q (𝑥 ·Q
(*Q‘𝑦))) = ((𝑦 ·Q 𝑏)
·Q (𝑥 ·Q
(*Q‘𝑦)))) | 
| 121 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑏 ∈ V | 
| 122 | 88, 121, 93, 90, 95, 94 | caov411 7665 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦
·Q 𝑏) ·Q (𝑥
·Q (*Q‘𝑦))) = ((𝑥 ·Q 𝑏)
·Q (𝑦 ·Q
(*Q‘𝑦))) | 
| 123 | 73 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ Q →
((𝑥
·Q 𝑏) ·Q (𝑦
·Q (*Q‘𝑦))) = ((𝑥 ·Q 𝑏)
·Q
1Q)) | 
| 124 |  | mulidnq 11003 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥
·Q 𝑏) ∈ Q → ((𝑥
·Q 𝑏) ·Q
1Q) = (𝑥 ·Q 𝑏)) | 
| 125 | 123, 124 | sylan9eqr 2799 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
((𝑥
·Q 𝑏) ·Q (𝑦
·Q (*Q‘𝑦))) = (𝑥 ·Q 𝑏)) | 
| 126 | 122, 125 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) →
((𝑦
·Q 𝑏) ·Q (𝑥
·Q (*Q‘𝑦))) = (𝑥 ·Q 𝑏)) | 
| 127 | 120, 126 | sylan9eqr 2799 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
(𝑦
+Q 𝑧) = (𝑦 ·Q 𝑏)) → ((𝑦 +Q 𝑧)
·Q (𝑥 ·Q
(*Q‘𝑦))) = (𝑥 ·Q 𝑏)) | 
| 128 | 127 | breq2d 5155 | . . . . . . . . . . . . . 14
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
(𝑦
+Q 𝑧) = (𝑦 ·Q 𝑏)) → ((𝑥 +Q 𝑧) <Q
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏))) | 
| 129 | 128 | adantrl 716 | . . . . . . . . . . . . 13
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
(𝑧 ∈ Q
∧ (𝑦
+Q 𝑧) = (𝑦 ·Q 𝑏))) → ((𝑥 +Q 𝑧) <Q
((𝑦
+Q 𝑧) ·Q (𝑥
·Q (*Q‘𝑦))) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏))) | 
| 130 | 113, 119,
129 | 3bitr3d 309 | . . . . . . . . . . . 12
⊢ ((((𝑥
·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) ∧
(𝑧 ∈ Q
∧ (𝑦
+Q 𝑧) = (𝑦 ·Q 𝑏))) → ((𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏))) | 
| 131 | 60, 61, 53, 62, 130 | syl22anc 839 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → ((𝑦 +Q 𝑧) <Q
(𝑥
+Q 𝑧) ↔ (𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏))) | 
| 132 | 57, 131 | sylibd 239 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 +Q 𝑧) ∈ 𝐴 → (𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏))) | 
| 133 |  | prcdnq 11033 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
(𝑥
·Q 𝑏) ∈ 𝐴) → ((𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏) → (𝑥 +Q 𝑧) ∈ 𝐴)) | 
| 134 | 133 | impancom 451 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
(𝑥
+Q 𝑧) <Q (𝑥
·Q 𝑏)) → ((𝑥 ·Q 𝑏) ∈ 𝐴 → (𝑥 +Q 𝑧) ∈ 𝐴)) | 
| 135 | 134 | con3d 152 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
(𝑥
+Q 𝑧) <Q (𝑥
·Q 𝑏)) → (¬ (𝑥 +Q 𝑧) ∈ 𝐴 → ¬ (𝑥 ·Q 𝑏) ∈ 𝐴)) | 
| 136 | 135 | ex 412 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ P →
((𝑥
+Q 𝑧) <Q (𝑥
·Q 𝑏) → (¬ (𝑥 +Q 𝑧) ∈ 𝐴 → ¬ (𝑥 ·Q 𝑏) ∈ 𝐴))) | 
| 137 | 136 | com23 86 | . . . . . . . . . . 11
⊢ (𝐴 ∈ P →
(¬ (𝑥
+Q 𝑧) ∈ 𝐴 → ((𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏) → ¬ (𝑥 ·Q 𝑏) ∈ 𝐴))) | 
| 138 | 37, 137 | syl 17 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 +Q 𝑧) ∈ 𝐴 → ((𝑥 +Q 𝑧) <Q
(𝑥
·Q 𝑏) → ¬ (𝑥 ·Q 𝑏) ∈ 𝐴))) | 
| 139 | 132, 138 | mpdd 43 | . . . . . . . . 9
⊢
(((((𝐴 ∈
P ∧ 1Q
<Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 +Q 𝑧) ∈ 𝐴 → ¬ (𝑥 ·Q 𝑏) ∈ 𝐴)) | 
| 140 | 139 | reximdva 3168 | . . . . . . . 8
⊢ ((((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → (∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝑧) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴)) | 
| 141 | 36, 140 | mpd 15 | . . . . . . 7
⊢ ((((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) ∧ (𝑦 +Q 𝑧) = (𝑦 ·Q 𝑏)) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴) | 
| 142 | 32, 141 | exlimddv 1935 | . . . . . 6
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ (𝑦 ∈ 𝐴 ∧ (𝑦 ·Q 𝑏) ∈ 𝐴)) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴) | 
| 143 | 142 | expr 456 | . . . . 5
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ 𝑦 ∈ 𝐴) → ((𝑦 ·Q 𝑏) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴)) | 
| 144 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ·Q 𝑏) = (𝑦 ·Q 𝑏)) | 
| 145 | 144 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ·Q 𝑏) ∈ 𝐴 ↔ (𝑦 ·Q 𝑏) ∈ 𝐴)) | 
| 146 | 145 | notbid 318 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (¬ (𝑥 ·Q 𝑏) ∈ 𝐴 ↔ ¬ (𝑦 ·Q 𝑏) ∈ 𝐴)) | 
| 147 | 146 | rspcev 3622 | . . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ ¬ (𝑦 ·Q 𝑏) ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴) | 
| 148 | 147 | ex 412 | . . . . . 6
⊢ (𝑦 ∈ 𝐴 → (¬ (𝑦 ·Q 𝑏) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴)) | 
| 149 | 148 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ 𝑦 ∈ 𝐴) → (¬ (𝑦 ·Q 𝑏) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴)) | 
| 150 | 143, 149 | pm2.61d 179 | . . . 4
⊢ (((𝐴 ∈ P ∧
1Q <Q 𝑏) ∧ 𝑦 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴) | 
| 151 | 15, 150 | exlimddv 1935 | . . 3
⊢ ((𝐴 ∈ P ∧
1Q <Q 𝑏) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝑏) ∈ 𝐴) | 
| 152 | 11, 151 | vtoclg 3554 | . 2
⊢ (𝐵 ∈ Q →
((𝐴 ∈ P
∧ 1Q <Q 𝐵) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝐵) ∈ 𝐴)) | 
| 153 | 4, 152 | mpcom 38 | 1
⊢ ((𝐴 ∈ P ∧
1Q <Q 𝐵) → ∃𝑥 ∈ 𝐴 ¬ (𝑥 ·Q 𝐵) ∈ 𝐴) |