Step | Hyp | Ref
| Expression |
1 | | ltexnqi 6392 |
. . 3
⊢ (A <Q B → ∃x ∈ Q (A +Q x) = B) |
2 | 1 | adantl 262 |
. 2
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) →
∃x ∈ Q (A +Q x) = B) |
3 | | prml 6460 |
. . . 4
⊢
(〈𝐿, 𝑈〉 ∈ P → ∃𝑟 ∈
Q 𝑟 ∈ 𝐿) |
4 | 3 | ad2antrr 457 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) → ∃𝑟 ∈ Q 𝑟 ∈ 𝐿) |
5 | | simprl 483 |
. . . . . 6
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → 𝑟 ∈
Q) |
6 | | simplrl 487 |
. . . . . 6
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → x ∈
Q) |
7 | | mulclnq 6360 |
. . . . . 6
⊢ ((𝑟 ∈ Q ∧ x ∈ Q) → (𝑟 ·Q x) ∈
Q) |
8 | 5, 6, 7 | syl2anc 391 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → (𝑟 ·Q x) ∈
Q) |
9 | | ltrelnq 6349 |
. . . . . . . 8
⊢
<Q ⊆ (Q ×
Q) |
10 | 9 | brel 4335 |
. . . . . . 7
⊢ (A <Q B → (A
∈ Q ∧ B ∈ Q)) |
11 | 10 | simprd 107 |
. . . . . 6
⊢ (A <Q B → B ∈ Q) |
12 | 11 | ad3antlr 462 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → B ∈
Q) |
13 | | appdiv0nq 6545 |
. . . . 5
⊢ (((𝑟 ·Q
x) ∈
Q ∧ B ∈
Q) → ∃𝑝 ∈
Q (𝑝
·Q B)
<Q (𝑟 ·Q x)) |
14 | 8, 12, 13 | syl2anc 391 |
. . . 4
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → ∃𝑝 ∈
Q (𝑝
·Q B)
<Q (𝑟 ·Q x)) |
15 | | prarloc 6486 |
. . . . . . . . . 10
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝑝
∈ Q) → ∃𝑑 ∈ 𝐿 ∃u ∈ 𝑈 u
<Q (𝑑 +Q 𝑝)) |
16 | 15 | adantlr 446 |
. . . . . . . . 9
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ 𝑝
∈ Q) → ∃𝑑 ∈ 𝐿 ∃u ∈ 𝑈 u
<Q (𝑑 +Q 𝑝)) |
17 | 16 | adantlr 446 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ 𝑝 ∈ Q) → ∃𝑑 ∈ 𝐿 ∃u ∈ 𝑈 u
<Q (𝑑 +Q 𝑝)) |
18 | 17 | ad2ant2r 478 |
. . . . . . 7
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) → ∃𝑑 ∈ 𝐿 ∃u ∈ 𝑈 u
<Q (𝑑 +Q 𝑝)) |
19 | | r2ex 2338 |
. . . . . . 7
⊢ (∃𝑑 ∈ 𝐿 ∃u ∈ 𝑈 u
<Q (𝑑 +Q 𝑝) ↔ ∃𝑑∃u((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧
u <Q (𝑑 +Q 𝑝))) |
20 | 18, 19 | sylib 127 |
. . . . . 6
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) → ∃𝑑∃u((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧
u <Q (𝑑 +Q 𝑝))) |
21 | | elprnql 6464 |
. . . . . . . . . . . . . 14
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝑑
∈ 𝐿) → 𝑑 ∈
Q) |
22 | 21 | adantlr 446 |
. . . . . . . . . . . . 13
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ 𝑑
∈ 𝐿) → 𝑑 ∈
Q) |
23 | 22 | adantlr 446 |
. . . . . . . . . . . 12
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ 𝑑 ∈ 𝐿) → 𝑑 ∈
Q) |
24 | 23 | adantlr 446 |
. . . . . . . . . . 11
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ 𝑑 ∈ 𝐿) → 𝑑 ∈
Q) |
25 | 24 | ad2ant2r 478 |
. . . . . . . . . 10
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈)) → 𝑑 ∈
Q) |
26 | 25 | adantrr 448 |
. . . . . . . . 9
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → 𝑑 ∈
Q) |
27 | | simplll 485 |
. . . . . . . . . . 11
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → 〈𝐿, 𝑈〉 ∈
P) |
28 | 27 | ad2antrr 457 |
. . . . . . . . . 10
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → 〈𝐿, 𝑈〉 ∈
P) |
29 | | simprl 483 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈)) |
30 | 29 | simprd 107 |
. . . . . . . . . 10
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → u ∈ 𝑈) |
31 | | elprnqu 6465 |
. . . . . . . . . 10
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ u ∈ 𝑈) → u ∈
Q) |
32 | 28, 30, 31 | syl2anc 391 |
. . . . . . . . 9
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → u ∈
Q) |
33 | | prltlu 6470 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ 𝑟
∈ 𝐿 ∧ u ∈ 𝑈) → 𝑟 <Q u) |
34 | 33 | 3adant1r 1127 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ 𝑟
∈ 𝐿 ∧ u ∈ 𝑈) → 𝑟 <Q u) |
35 | 34 | 3adant2l 1128 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (𝑟 ∈
Q ∧ 𝑟 ∈ 𝐿) ∧ u ∈ 𝑈) → 𝑟 <Q u) |
36 | 35 | 3adant3l 1130 |
. . . . . . . . . . . . . 14
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (𝑟 ∈
Q ∧ 𝑟 ∈ 𝐿) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈)) → 𝑟 <Q u) |
37 | 36 | 3adant1r 1127 |
. . . . . . . . . . . . 13
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈)) → 𝑟 <Q u) |
38 | 37 | 3expa 1103 |
. . . . . . . . . . . 12
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈)) → 𝑟 <Q u) |
39 | 38 | ad2ant2r 478 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → 𝑟 <Q u) |
40 | | simprr 484 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → u <Q (𝑑 +Q 𝑝)) |
41 | | simplrr 488 |
. . . . . . . . . . . 12
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → (A +Q x) = B) |
42 | 41 | ad2antrr 457 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → (A +Q x) = B) |
43 | | simplrr 488 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → (𝑝 ·Q B) <Q (𝑟 ·Q x)) |
44 | 10 | simpld 105 |
. . . . . . . . . . . . 13
⊢ (A <Q B → A ∈ Q) |
45 | 44 | ad3antlr 462 |
. . . . . . . . . . . 12
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → A ∈
Q) |
46 | 45 | ad2antrr 457 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → A ∈
Q) |
47 | 12 | ad2antrr 457 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → B ∈
Q) |
48 | | simplrl 487 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → 𝑝 ∈
Q) |
49 | 6 | ad2antrr 457 |
. . . . . . . . . . 11
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → x ∈
Q) |
50 | 39, 40, 42, 43, 46, 47, 26, 48, 49 | prmuloclemcalc 6546 |
. . . . . . . . . 10
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → (u ·Q A) <Q (𝑑 ·Q B)) |
51 | | df-3an 886 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧ (u
·Q A)
<Q (𝑑 ·Q B)) ↔ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧
(u ·Q
A) <Q (𝑑 ·Q
B))) |
52 | 29, 50, 51 | sylanbrc 394 |
. . . . . . . . 9
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B))) |
53 | 26, 32, 52 | jca31 292 |
. . . . . . . 8
⊢
((((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) ∧ ((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧ u
<Q (𝑑 +Q 𝑝))) → ((𝑑 ∈
Q ∧ u ∈
Q) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B)))) |
54 | 53 | ex 108 |
. . . . . . 7
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) → (((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧
u <Q (𝑑 +Q 𝑝)) → ((𝑑 ∈
Q ∧ u ∈
Q) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B))))) |
55 | 54 | 2eximdv 1759 |
. . . . . 6
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) → (∃𝑑∃u((𝑑 ∈ 𝐿 ∧ u ∈ 𝑈) ∧
u <Q (𝑑 +Q 𝑝)) → ∃𝑑∃u((𝑑 ∈
Q ∧ u ∈
Q) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B))))) |
56 | 20, 55 | mpd 13 |
. . . . 5
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) → ∃𝑑∃u((𝑑 ∈
Q ∧ u ∈
Q) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B)))) |
57 | | r2ex 2338 |
. . . . 5
⊢ (∃𝑑 ∈
Q ∃u ∈
Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧ (u
·Q A)
<Q (𝑑 ·Q B)) ↔ ∃𝑑∃u((𝑑 ∈ Q ∧ u ∈ Q) ∧ (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B)))) |
58 | 56, 57 | sylibr 137 |
. . . 4
⊢
(((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) ∧ (𝑝 ∈ Q ∧ (𝑝 ·Q B) <Q (𝑟 ·Q x))) → ∃𝑑 ∈
Q ∃u ∈
Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧ (u
·Q A)
<Q (𝑑 ·Q B))) |
59 | 14, 58 | rexlimddv 2431 |
. . 3
⊢
((((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) ∧ (𝑟 ∈ Q ∧ 𝑟
∈ 𝐿)) → ∃𝑑 ∈
Q ∃u ∈
Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧ (u
·Q A)
<Q (𝑑 ·Q B))) |
60 | 4, 59 | rexlimddv 2431 |
. 2
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) ∧ (x ∈ Q ∧ (A
+Q x) = B)) → ∃𝑑 ∈ Q ∃u ∈ Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧
(u ·Q
A) <Q (𝑑 ·Q
B))) |
61 | 2, 60 | rexlimddv 2431 |
1
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ A
<Q B) →
∃𝑑 ∈
Q ∃u ∈
Q (𝑑 ∈ 𝐿 ∧ u ∈ 𝑈 ∧ (u
·Q A)
<Q (𝑑 ·Q B))) |