Step | Hyp | Ref
| Expression |
1 | | fveq2 5516 |
. . . . . 6
⊢ (𝑗 = 1o → (𝐹‘𝑗) = (𝐹‘1o)) |
2 | 1 | breq2d 4016 |
. . . . 5
⊢ (𝑗 = 1o → (𝐴 <Q
(𝐹‘𝑗) ↔ 𝐴 <Q (𝐹‘1o))) |
3 | | caucvgpr.bnd |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) |
4 | | 1pi 7314 |
. . . . . 6
⊢
1o ∈ N |
5 | 4 | a1i 9 |
. . . . 5
⊢ (𝜑 → 1o ∈
N) |
6 | 2, 3, 5 | rspcdva 2847 |
. . . 4
⊢ (𝜑 → 𝐴 <Q (𝐹‘1o)) |
7 | | ltrelnq 7364 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
8 | 7 | brel 4679 |
. . . . 5
⊢ (𝐴 <Q
(𝐹‘1o)
→ (𝐴 ∈
Q ∧ (𝐹‘1o) ∈
Q)) |
9 | 8 | simpld 112 |
. . . 4
⊢ (𝐴 <Q
(𝐹‘1o)
→ 𝐴 ∈
Q) |
10 | | halfnqq 7409 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑠 ∈
Q (𝑠
+Q 𝑠) = 𝐴) |
11 | 6, 9, 10 | 3syl 17 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Q (𝑠 +Q 𝑠) = 𝐴) |
12 | | simplr 528 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → 𝑠 ∈ Q) |
13 | | archrecnq 7662 |
. . . . . . . 8
⊢ (𝑠 ∈ Q →
∃𝑗 ∈
N (*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) |
14 | 12, 13 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → ∃𝑗 ∈ N
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) |
15 | | simpr 110 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) →
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) |
16 | | simplr 528 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → 𝑗 ∈ N) |
17 | | nnnq 7421 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ N →
[⟨𝑗,
1o⟩] ~Q ∈
Q) |
18 | | recclnq 7391 |
. . . . . . . . . . . . . 14
⊢
([⟨𝑗,
1o⟩] ~Q ∈ Q →
(*Q‘[⟨𝑗, 1o⟩]
~Q ) ∈ Q) |
19 | 16, 17, 18 | 3syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) →
(*Q‘[⟨𝑗, 1o⟩]
~Q ) ∈ Q) |
20 | 12 | ad2antrr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → 𝑠 ∈ Q) |
21 | | ltanqg 7399 |
. . . . . . . . . . . . 13
⊢
(((*Q‘[⟨𝑗, 1o⟩]
~Q ) ∈ Q ∧ 𝑠 ∈ Q ∧ 𝑠 ∈ Q) →
((*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠 ↔ (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝑠 +Q
𝑠))) |
22 | 19, 20, 20, 21 | syl3anc 1238 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) →
((*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠 ↔ (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝑠 +Q
𝑠))) |
23 | 15, 22 | mpbid 147 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝑠 +Q
𝑠)) |
24 | | simpllr 534 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → (𝑠 +Q 𝑠) = 𝐴) |
25 | 23, 24 | breqtrd 4030 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝐴) |
26 | | rsp 2524 |
. . . . . . . . . . . . 13
⊢
(∀𝑗 ∈
N 𝐴
<Q (𝐹‘𝑗) → (𝑗 ∈ N → 𝐴 <Q
(𝐹‘𝑗))) |
27 | 3, 26 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ N → 𝐴 <Q
(𝐹‘𝑗))) |
28 | 27 | ad4antr 494 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → (𝑗 ∈ N → 𝐴 <Q
(𝐹‘𝑗))) |
29 | 16, 28 | mpd 13 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → 𝐴 <Q (𝐹‘𝑗)) |
30 | | ltsonq 7397 |
. . . . . . . . . . 11
⊢
<Q Or Q |
31 | 30, 7 | sotri 5025 |
. . . . . . . . . 10
⊢ (((𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝐴 ∧ 𝐴 <Q (𝐹‘𝑗)) → (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)) |
32 | 25, 29, 31 | syl2anc 411 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) = 𝐴) ∧ 𝑗 ∈ N) ∧
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)) |
33 | 32 | ex 115 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) ∧ 𝑗 ∈ N) →
((*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠 → (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗))) |
34 | 33 | reximdva 2579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → (∃𝑗 ∈ N
(*Q‘[⟨𝑗, 1o⟩]
~Q ) <Q 𝑠 → ∃𝑗 ∈ N (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗))) |
35 | 14, 34 | mpd 13 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → ∃𝑗 ∈ N (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)) |
36 | | oveq1 5882 |
. . . . . . . . 9
⊢ (𝑙 = 𝑠 → (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) = (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q ))) |
37 | 36 | breq1d 4014 |
. . . . . . . 8
⊢ (𝑙 = 𝑠 → ((𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗) ↔ (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗))) |
38 | 37 | rexbidv 2478 |
. . . . . . 7
⊢ (𝑙 = 𝑠 → (∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗) ↔ ∃𝑗 ∈ N (𝑠 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗))) |
39 | | caucvgpr.lim |
. . . . . . . . 9
⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢}⟩ |
40 | 39 | fveq2i 5519 |
. . . . . . . 8
⊢
(1st ‘𝐿) = (1st ‘⟨{𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢}⟩) |
41 | | nqex 7362 |
. . . . . . . . . 10
⊢
Q ∈ V |
42 | 41 | rabex 4148 |
. . . . . . . . 9
⊢ {𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)} ∈ V |
43 | 41 | rabex 4148 |
. . . . . . . . 9
⊢ {𝑢 ∈ Q ∣
∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢} ∈ V |
44 | 42, 43 | op1st 6147 |
. . . . . . . 8
⊢
(1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢}⟩) = {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)} |
45 | 40, 44 | eqtri 2198 |
. . . . . . 7
⊢
(1st ‘𝐿) = {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)} |
46 | 38, 45 | elrab2 2897 |
. . . . . 6
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑗 ∈
N (𝑠
+Q (*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗))) |
47 | 12, 35, 46 | sylanbrc 417 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ Q) ∧ (𝑠 +Q
𝑠) = 𝐴) → 𝑠 ∈ (1st ‘𝐿)) |
48 | 47 | ex 115 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ Q) → ((𝑠 +Q
𝑠) = 𝐴 → 𝑠 ∈ (1st ‘𝐿))) |
49 | 48 | reximdva 2579 |
. . 3
⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 +Q 𝑠) = 𝐴 → ∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿))) |
50 | 11, 49 | mpd 13 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿)) |
51 | | caucvgpr.f |
. . . . . 6
⊢ (𝜑 → 𝐹:N⟶Q) |
52 | 51, 5 | ffvelcdmd 5653 |
. . . . 5
⊢ (𝜑 → (𝐹‘1o) ∈
Q) |
53 | | 1nq 7365 |
. . . . 5
⊢
1Q ∈ Q |
54 | | addclnq 7374 |
. . . . 5
⊢ (((𝐹‘1o) ∈
Q ∧ 1Q ∈ Q)
→ ((𝐹‘1o)
+Q 1Q) ∈
Q) |
55 | 52, 53, 54 | sylancl 413 |
. . . 4
⊢ (𝜑 → ((𝐹‘1o)
+Q 1Q) ∈
Q) |
56 | | addclnq 7374 |
. . . 4
⊢ ((((𝐹‘1o)
+Q 1Q) ∈ Q
∧ 1Q ∈ Q) → (((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈
Q) |
57 | 55, 53, 56 | sylancl 413 |
. . 3
⊢ (𝜑 → (((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈
Q) |
58 | | df-1nqqs 7350 |
. . . . . . . . 9
⊢
1Q = [⟨1o, 1o⟩]
~Q |
59 | 58 | fveq2i 5519 |
. . . . . . . 8
⊢
(*Q‘1Q) =
(*Q‘[⟨1o, 1o⟩]
~Q ) |
60 | | rec1nq 7394 |
. . . . . . . 8
⊢
(*Q‘1Q) =
1Q |
61 | 59, 60 | eqtr3i 2200 |
. . . . . . 7
⊢
(*Q‘[⟨1o,
1o⟩] ~Q ) =
1Q |
62 | 61 | oveq2i 5886 |
. . . . . 6
⊢ ((𝐹‘1o)
+Q
(*Q‘[⟨1o, 1o⟩]
~Q )) = ((𝐹‘1o)
+Q 1Q) |
63 | | ltaddnq 7406 |
. . . . . . 7
⊢ ((((𝐹‘1o)
+Q 1Q) ∈ Q
∧ 1Q ∈ Q) → ((𝐹‘1o)
+Q 1Q)
<Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q)) |
64 | 55, 53, 63 | sylancl 413 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘1o)
+Q 1Q)
<Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q)) |
65 | 62, 64 | eqbrtrid 4039 |
. . . . 5
⊢ (𝜑 → ((𝐹‘1o)
+Q
(*Q‘[⟨1o, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q)) |
66 | | opeq1 3779 |
. . . . . . . . . 10
⊢ (𝑗 = 1o →
⟨𝑗,
1o⟩ = ⟨1o,
1o⟩) |
67 | 66 | eceq1d 6571 |
. . . . . . . . 9
⊢ (𝑗 = 1o →
[⟨𝑗,
1o⟩] ~Q = [⟨1o,
1o⟩] ~Q ) |
68 | 67 | fveq2d 5520 |
. . . . . . . 8
⊢ (𝑗 = 1o →
(*Q‘[⟨𝑗, 1o⟩]
~Q ) =
(*Q‘[⟨1o, 1o⟩]
~Q )) |
69 | 1, 68 | oveq12d 5893 |
. . . . . . 7
⊢ (𝑗 = 1o → ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) = ((𝐹‘1o)
+Q
(*Q‘[⟨1o, 1o⟩]
~Q ))) |
70 | 69 | breq1d 4014 |
. . . . . 6
⊢ (𝑗 = 1o → (((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q) ↔ ((𝐹‘1o)
+Q
(*Q‘[⟨1o, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q))) |
71 | 70 | rspcev 2842 |
. . . . 5
⊢
((1o ∈ N ∧ ((𝐹‘1o)
+Q
(*Q‘[⟨1o, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q)) → ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q)) |
72 | 5, 65, 71 | syl2anc 411 |
. . . 4
⊢ (𝜑 → ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q)) |
73 | | breq2 4008 |
. . . . . 6
⊢ (𝑢 = (((𝐹‘1o)
+Q 1Q)
+Q 1Q) → (((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢 ↔ ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q))) |
74 | 73 | rexbidv 2478 |
. . . . 5
⊢ (𝑢 = (((𝐹‘1o)
+Q 1Q)
+Q 1Q) → (∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢 ↔ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q))) |
75 | 39 | fveq2i 5519 |
. . . . . 6
⊢
(2nd ‘𝐿) = (2nd ‘⟨{𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢}⟩) |
76 | 42, 43 | op2nd 6148 |
. . . . . 6
⊢
(2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢}⟩) = {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢} |
77 | 75, 76 | eqtri 2198 |
. . . . 5
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q 𝑢} |
78 | 74, 77 | elrab2 2897 |
. . . 4
⊢ ((((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿) ↔ ((((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈ Q
∧ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[⟨𝑗, 1o⟩]
~Q )) <Q (((𝐹‘1o)
+Q 1Q)
+Q 1Q))) |
79 | 57, 72, 78 | sylanbrc 417 |
. . 3
⊢ (𝜑 → (((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿)) |
80 | | eleq1 2240 |
. . . 4
⊢ (𝑟 = (((𝐹‘1o)
+Q 1Q)
+Q 1Q) → (𝑟 ∈ (2nd
‘𝐿) ↔ (((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿))) |
81 | 80 | rspcev 2842 |
. . 3
⊢
(((((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈ Q
∧ (((𝐹‘1o)
+Q 1Q)
+Q 1Q) ∈ (2nd
‘𝐿)) →
∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐿)) |
82 | 57, 79, 81 | syl2anc 411 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐿)) |
83 | 50, 82 | jca 306 |
1
⊢ (𝜑 → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd
‘𝐿))) |