Proof of Theorem caucvgprlemdisj
Step | Hyp | Ref
| Expression |
1 | | oveq1 5860 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑠 → (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑗, 1o〉]
~Q ))) |
2 | 1 | breq1d 3999 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑠 → ((𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗) ↔ (𝑠 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗))) |
3 | 2 | rexbidv 2471 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑠 → (∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗) ↔ ∃𝑗 ∈ N (𝑠 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗))) |
4 | | caucvgpr.lim |
. . . . . . . . . . . 12
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉 |
5 | 4 | fveq2i 5499 |
. . . . . . . . . . 11
⊢
(1st ‘𝐿) = (1st ‘〈{𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉) |
6 | | nqex 7325 |
. . . . . . . . . . . . 13
⊢
Q ∈ V |
7 | 6 | rabex 4133 |
. . . . . . . . . . . 12
⊢ {𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)} ∈ V |
8 | 6 | rabex 4133 |
. . . . . . . . . . . 12
⊢ {𝑢 ∈ Q ∣
∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢} ∈ V |
9 | 7, 8 | op1st 6125 |
. . . . . . . . . . 11
⊢
(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉) = {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)} |
10 | 5, 9 | eqtri 2191 |
. . . . . . . . . 10
⊢
(1st ‘𝐿) = {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)} |
11 | 3, 10 | elrab2 2889 |
. . . . . . . . 9
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗))) |
12 | 11 | simprbi 273 |
. . . . . . . 8
⊢ (𝑠 ∈ (1st
‘𝐿) →
∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)) |
13 | | opeq1 3765 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → 〈𝑗, 1o〉 = 〈𝑘,
1o〉) |
14 | 13 | eceq1d 6549 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → [〈𝑗, 1o〉]
~Q = [〈𝑘, 1o〉]
~Q ) |
15 | 14 | fveq2d 5500 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 →
(*Q‘[〈𝑗, 1o〉]
~Q ) = (*Q‘[〈𝑘, 1o〉]
~Q )) |
16 | 15 | oveq2d 5869 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑠 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑘, 1o〉]
~Q ))) |
17 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
18 | 16, 17 | breq12d 4002 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑠 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗) ↔ (𝑠 +Q
(*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘))) |
19 | 18 | cbvrexv 2697 |
. . . . . . . 8
⊢
(∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗) ↔ ∃𝑘 ∈ N (𝑠 +Q
(*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘)) |
20 | 12, 19 | sylib 121 |
. . . . . . 7
⊢ (𝑠 ∈ (1st
‘𝐿) →
∃𝑘 ∈
N (𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘)) |
21 | | breq2 3993 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑠 → (((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢 ↔ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
22 | 21 | rexbidv 2471 |
. . . . . . . . 9
⊢ (𝑢 = 𝑠 → (∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢 ↔ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
23 | 4 | fveq2i 5499 |
. . . . . . . . . 10
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉) |
24 | 7, 8 | op2nd 6126 |
. . . . . . . . . 10
⊢
(2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢}〉) = {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢} |
25 | 23, 24 | eqtri 2191 |
. . . . . . . . 9
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑢} |
26 | 22, 25 | elrab2 2889 |
. . . . . . . 8
⊢ (𝑠 ∈ (2nd
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
27 | 26 | simprbi 273 |
. . . . . . 7
⊢ (𝑠 ∈ (2nd
‘𝐿) →
∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠) |
28 | 20, 27 | anim12i 336 |
. . . . . 6
⊢ ((𝑠 ∈ (1st
‘𝐿) ∧ 𝑠 ∈ (2nd
‘𝐿)) →
(∃𝑘 ∈
N (𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
29 | | reeanv 2639 |
. . . . . 6
⊢
(∃𝑘 ∈
N ∃𝑗
∈ N ((𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠) ↔ (∃𝑘 ∈ N (𝑠 +Q
(*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
30 | 28, 29 | sylibr 133 |
. . . . 5
⊢ ((𝑠 ∈ (1st
‘𝐿) ∧ 𝑠 ∈ (2nd
‘𝐿)) →
∃𝑘 ∈
N ∃𝑗
∈ N ((𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
31 | 30 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → ∃𝑘 ∈ N
∃𝑗 ∈
N ((𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
32 | | caucvgpr.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:N⟶Q) |
33 | 32 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
𝐹:N⟶Q) |
34 | | caucvgpr.cau |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1o〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1o〉]
~Q ))))) |
35 | 34 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
∀𝑛 ∈
N ∀𝑘
∈ N (𝑛
<N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1o〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1o〉]
~Q ))))) |
36 | | simprl 526 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
𝑘 ∈
N) |
37 | | simprr 527 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
𝑗 ∈
N) |
38 | 11 | simplbi 272 |
. . . . . . . . 9
⊢ (𝑠 ∈ (1st
‘𝐿) → 𝑠 ∈
Q) |
39 | 38 | ad2antrl 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → 𝑠 ∈ Q) |
40 | 39 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
𝑠 ∈
Q) |
41 | 33, 35, 36, 37, 40 | caucvgprlemnkj 7628 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
¬ ((𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠)) |
42 | 41 | pm2.21d 614 |
. . . . 5
⊢ (((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧ (𝑘 ∈ N ∧ 𝑗 ∈ N)) →
(((𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠) →
⊥)) |
43 | 42 | rexlimdvva 2595 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → (∃𝑘 ∈ N
∃𝑗 ∈
N ((𝑠
+Q (*Q‘[〈𝑘, 1o〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1o〉]
~Q )) <Q 𝑠) →
⊥)) |
44 | 31, 43 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) →
⊥) |
45 | 44 | inegd 1367 |
. 2
⊢ (𝜑 → ¬ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) |
46 | 45 | ralrimivw 2544 |
1
⊢ (𝜑 → ∀𝑠 ∈ Q ¬ (𝑠 ∈ (1st
‘𝐿) ∧ 𝑠 ∈ (2nd
‘𝐿))) |