Step | Hyp | Ref
| Expression |
1 | | prarloclemarch 6516 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐶 ∈ Q)
→ ∃𝑧 ∈
N 𝐴
<Q ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶)) |
2 | 1 | 3adant2 923 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ∃𝑧 ∈ N 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶)) |
3 | | pinn 6407 |
. . . . . . . 8
⊢ (𝑧 ∈ N →
𝑧 ∈
ω) |
4 | | 1pi 6413 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ N |
5 | 4 | elexi 2567 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ V |
6 | 5 | sucid 4154 |
. . . . . . . . . 10
⊢
1𝑜 ∈ suc 1𝑜 |
7 | | df-2o 6002 |
. . . . . . . . . 10
⊢
2𝑜 = suc 1𝑜 |
8 | 6, 7 | eleqtrri 2113 |
. . . . . . . . 9
⊢
1𝑜 ∈ 2𝑜 |
9 | | 2onn 6094 |
. . . . . . . . . . 11
⊢
2𝑜 ∈ ω |
10 | | nnaword2 6087 |
. . . . . . . . . . 11
⊢
((2𝑜 ∈ ω ∧ 𝑧 ∈ ω) → 2𝑜
⊆ (𝑧
+𝑜 2𝑜)) |
11 | 9, 10 | mpan 400 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω →
2𝑜 ⊆ (𝑧 +𝑜
2𝑜)) |
12 | 11 | sseld 2944 |
. . . . . . . . 9
⊢ (𝑧 ∈ ω →
(1𝑜 ∈ 2𝑜 →
1𝑜 ∈ (𝑧 +𝑜
2𝑜))) |
13 | 8, 12 | mpi 15 |
. . . . . . . 8
⊢ (𝑧 ∈ ω →
1𝑜 ∈ (𝑧 +𝑜
2𝑜)) |
14 | 3, 13 | syl 14 |
. . . . . . 7
⊢ (𝑧 ∈ N →
1𝑜 ∈ (𝑧 +𝑜
2𝑜)) |
15 | | o1p1e2 6048 |
. . . . . . . . 9
⊢
(1𝑜 +𝑜 1𝑜) =
2𝑜 |
16 | | addpiord 6414 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ N ∧
1𝑜 ∈ N) → (1𝑜
+N 1𝑜) = (1𝑜
+𝑜 1𝑜)) |
17 | 4, 4, 16 | mp2an 402 |
. . . . . . . . . 10
⊢
(1𝑜 +N
1𝑜) = (1𝑜 +𝑜
1𝑜) |
18 | | addclpi 6425 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ N ∧
1𝑜 ∈ N) → (1𝑜
+N 1𝑜) ∈
N) |
19 | 4, 4, 18 | mp2an 402 |
. . . . . . . . . 10
⊢
(1𝑜 +N
1𝑜) ∈ N |
20 | 17, 19 | eqeltrri 2111 |
. . . . . . . . 9
⊢
(1𝑜 +𝑜 1𝑜)
∈ N |
21 | 15, 20 | eqeltrri 2111 |
. . . . . . . 8
⊢
2𝑜 ∈ N |
22 | | addpiord 6414 |
. . . . . . . 8
⊢ ((𝑧 ∈ N ∧
2𝑜 ∈ N) → (𝑧 +N
2𝑜) = (𝑧
+𝑜 2𝑜)) |
23 | 21, 22 | mpan2 401 |
. . . . . . 7
⊢ (𝑧 ∈ N →
(𝑧
+N 2𝑜) = (𝑧 +𝑜
2𝑜)) |
24 | 14, 23 | eleqtrrd 2117 |
. . . . . 6
⊢ (𝑧 ∈ N →
1𝑜 ∈ (𝑧 +N
2𝑜)) |
25 | | addclpi 6425 |
. . . . . . . 8
⊢ ((𝑧 ∈ N ∧
2𝑜 ∈ N) → (𝑧 +N
2𝑜) ∈ N) |
26 | 21, 25 | mpan2 401 |
. . . . . . 7
⊢ (𝑧 ∈ N →
(𝑧
+N 2𝑜) ∈
N) |
27 | | ltpiord 6417 |
. . . . . . . 8
⊢
((1𝑜 ∈ N ∧ (𝑧 +N
2𝑜) ∈ N) → (1𝑜
<N (𝑧 +N
2𝑜) ↔ 1𝑜 ∈ (𝑧 +N
2𝑜))) |
28 | 4, 27 | mpan 400 |
. . . . . . 7
⊢ ((𝑧 +N
2𝑜) ∈ N → (1𝑜
<N (𝑧 +N
2𝑜) ↔ 1𝑜 ∈ (𝑧 +N
2𝑜))) |
29 | 26, 28 | syl 14 |
. . . . . 6
⊢ (𝑧 ∈ N →
(1𝑜 <N (𝑧 +N
2𝑜) ↔ 1𝑜 ∈ (𝑧 +N
2𝑜))) |
30 | 24, 29 | mpbird 156 |
. . . . 5
⊢ (𝑧 ∈ N →
1𝑜 <N (𝑧 +N
2𝑜)) |
31 | 30 | adantl 262 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → 1𝑜
<N (𝑧 +N
2𝑜)) |
32 | 31 | adantrr 448 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → 1𝑜
<N (𝑧 +N
2𝑜)) |
33 | | nna0 6053 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ω → (𝑧 +𝑜 ∅)
= 𝑧) |
34 | | 0lt1o 6023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ 1𝑜 |
35 | | 1on 6008 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1𝑜 ∈ On |
36 | 35 | onsuci 4242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ suc
1𝑜 ∈ On |
37 | | ontr1 4126 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (suc
1𝑜 ∈ On → ((∅ ∈ 1𝑜
∧ 1𝑜 ∈ suc 1𝑜) → ∅
∈ suc 1𝑜)) |
38 | 36, 37 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((∅
∈ 1𝑜 ∧ 1𝑜 ∈ suc
1𝑜) → ∅ ∈ suc
1𝑜) |
39 | 34, 6, 38 | mp2an 402 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
∈ suc 1𝑜 |
40 | 39, 7 | eleqtrri 2113 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ 2𝑜 |
41 | | nnaordi 6081 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2𝑜 ∈ ω ∧ 𝑧 ∈ ω) → (∅ ∈
2𝑜 → (𝑧 +𝑜 ∅) ∈ (𝑧 +𝑜
2𝑜))) |
42 | 9, 41 | mpan 400 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ω → (∅
∈ 2𝑜 → (𝑧 +𝑜 ∅) ∈ (𝑧 +𝑜
2𝑜))) |
43 | 40, 42 | mpi 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ω → (𝑧 +𝑜 ∅)
∈ (𝑧
+𝑜 2𝑜)) |
44 | 33, 43 | eqeltrrd 2115 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ω → 𝑧 ∈ (𝑧 +𝑜
2𝑜)) |
45 | 3, 44 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ N →
𝑧 ∈ (𝑧 +𝑜
2𝑜)) |
46 | 45, 23 | eleqtrrd 2117 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ N →
𝑧 ∈ (𝑧 +N
2𝑜)) |
47 | | ltpiord 6417 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ N ∧
(𝑧
+N 2𝑜) ∈ N)
→ (𝑧
<N (𝑧 +N
2𝑜) ↔ 𝑧 ∈ (𝑧 +N
2𝑜))) |
48 | 26, 47 | mpdan 398 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ N →
(𝑧
<N (𝑧 +N
2𝑜) ↔ 𝑧 ∈ (𝑧 +N
2𝑜))) |
49 | 46, 48 | mpbird 156 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ N →
𝑧
<N (𝑧 +N
2𝑜)) |
50 | | mulidpi 6416 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ N →
(𝑧
·N 1𝑜) = 𝑧) |
51 | | mulcompig 6429 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 +N
2𝑜) ∈ N ∧ 1𝑜
∈ N) → ((𝑧 +N
2𝑜) ·N
1𝑜) = (1𝑜
·N (𝑧 +N
2𝑜))) |
52 | 4, 51 | mpan2 401 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 +N
2𝑜) ∈ N → ((𝑧 +N
2𝑜) ·N
1𝑜) = (1𝑜
·N (𝑧 +N
2𝑜))) |
53 | 26, 52 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ N →
((𝑧
+N 2𝑜)
·N 1𝑜) =
(1𝑜 ·N (𝑧 +N
2𝑜))) |
54 | | mulidpi 6416 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 +N
2𝑜) ∈ N → ((𝑧 +N
2𝑜) ·N
1𝑜) = (𝑧
+N 2𝑜)) |
55 | 26, 54 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ N →
((𝑧
+N 2𝑜)
·N 1𝑜) = (𝑧 +N
2𝑜)) |
56 | 53, 55 | eqtr3d 2074 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ N →
(1𝑜 ·N (𝑧 +N
2𝑜)) = (𝑧 +N
2𝑜)) |
57 | 49, 50, 56 | 3brtr4d 3794 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ N →
(𝑧
·N 1𝑜)
<N (1𝑜
·N (𝑧 +N
2𝑜))) |
58 | | ordpipqqs 6472 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ N ∧
1𝑜 ∈ N) ∧ ((𝑧 +N
2𝑜) ∈ N ∧ 1𝑜
∈ N)) → ([〈𝑧, 1𝑜〉]
~Q <Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝑧 ·N
1𝑜) <N (1𝑜
·N (𝑧 +N
2𝑜)))) |
59 | 4, 58 | mpanl2 411 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ N ∧
((𝑧
+N 2𝑜) ∈ N ∧
1𝑜 ∈ N)) → ([〈𝑧, 1𝑜〉]
~Q <Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝑧 ·N
1𝑜) <N (1𝑜
·N (𝑧 +N
2𝑜)))) |
60 | 4, 59 | mpanr2 414 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ N ∧
(𝑧
+N 2𝑜) ∈ N)
→ ([〈𝑧,
1𝑜〉] ~Q
<Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝑧 ·N
1𝑜) <N (1𝑜
·N (𝑧 +N
2𝑜)))) |
61 | 26, 60 | mpdan 398 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ N →
([〈𝑧,
1𝑜〉] ~Q
<Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝑧 ·N
1𝑜) <N (1𝑜
·N (𝑧 +N
2𝑜)))) |
62 | 57, 61 | mpbird 156 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ N →
[〈𝑧,
1𝑜〉] ~Q
<Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ) |
63 | 62 | adantl 262 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ [〈𝑧,
1𝑜〉] ~Q
<Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ) |
64 | | opelxpi 4376 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 +N
2𝑜) ∈ N ∧ 1𝑜
∈ N) → 〈(𝑧 +N
2𝑜), 1𝑜〉 ∈ (N
× N)) |
65 | 4, 64 | mpan2 401 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 +N
2𝑜) ∈ N → 〈(𝑧 +N
2𝑜), 1𝑜〉 ∈ (N
× N)) |
66 | | enqex 6458 |
. . . . . . . . . . . . . . . 16
⊢
~Q ∈ V |
67 | 66 | ecelqsi 6160 |
. . . . . . . . . . . . . . 15
⊢
(〈(𝑧
+N 2𝑜), 1𝑜〉
∈ (N × N) → [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ∈ ((N × N)
/ ~Q )) |
68 | 26, 65, 67 | 3syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ N →
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ∈
((N × N) / ~Q
)) |
69 | | df-nqqs 6446 |
. . . . . . . . . . . . . 14
⊢
Q = ((N × N) /
~Q ) |
70 | 68, 69 | syl6eleqr 2131 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ N →
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ∈
Q) |
71 | | opelxpi 4376 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ N ∧
1𝑜 ∈ N) → 〈𝑧, 1𝑜〉 ∈
(N × N)) |
72 | 4, 71 | mpan2 401 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ N →
〈𝑧,
1𝑜〉 ∈ (N ×
N)) |
73 | 66 | ecelqsi 6160 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑧,
1𝑜〉 ∈ (N × N)
→ [〈𝑧,
1𝑜〉] ~Q ∈
((N × N) / ~Q
)) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ N →
[〈𝑧,
1𝑜〉] ~Q ∈
((N × N) / ~Q
)) |
75 | 74, 69 | syl6eleqr 2131 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ N →
[〈𝑧,
1𝑜〉] ~Q ∈
Q) |
76 | | ltmnqg 6499 |
. . . . . . . . . . . . . 14
⊢
(([〈𝑧,
1𝑜〉] ~Q ∈ Q
∧ [〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ∈ Q
∧ 𝐶 ∈
Q) → ([〈𝑧, 1𝑜〉]
~Q <Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝐶 ·Q
[〈𝑧,
1𝑜〉] ~Q )
<Q (𝐶 ·Q
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ))) |
77 | 75, 76 | syl3an1 1168 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ N ∧
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ∈ Q
∧ 𝐶 ∈
Q) → ([〈𝑧, 1𝑜〉]
~Q <Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝐶 ·Q
[〈𝑧,
1𝑜〉] ~Q )
<Q (𝐶 ·Q
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ))) |
78 | 70, 77 | syl3an2 1169 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ N ∧
𝑧 ∈ N
∧ 𝐶 ∈
Q) → ([〈𝑧, 1𝑜〉]
~Q <Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝐶 ·Q
[〈𝑧,
1𝑜〉] ~Q )
<Q (𝐶 ·Q
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ))) |
79 | 78 | 3anidm12 1192 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
𝐶 ∈ Q)
→ ([〈𝑧,
1𝑜〉] ~Q
<Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝐶 ·Q
[〈𝑧,
1𝑜〉] ~Q )
<Q (𝐶 ·Q
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ))) |
80 | 79 | ancoms 255 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ ([〈𝑧,
1𝑜〉] ~Q
<Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ↔ (𝐶 ·Q
[〈𝑧,
1𝑜〉] ~Q )
<Q (𝐶 ·Q
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ))) |
81 | 63, 80 | mpbid 135 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ (𝐶
·Q [〈𝑧, 1𝑜〉]
~Q ) <Q (𝐶 ·Q
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q )) |
82 | | mulcomnqg 6481 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Q ∧
[〈𝑧,
1𝑜〉] ~Q ∈
Q) → (𝐶
·Q [〈𝑧, 1𝑜〉]
~Q ) = ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶)) |
83 | 75, 82 | sylan2 270 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ (𝐶
·Q [〈𝑧, 1𝑜〉]
~Q ) = ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶)) |
84 | | mulcomnqg 6481 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Q ∧
[〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ∈
Q) → (𝐶
·Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ) = ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶)) |
85 | 70, 84 | sylan2 270 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ (𝐶
·Q [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ) = ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶)) |
86 | 81, 83, 85 | 3brtr3d 3793 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ ([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)) |
87 | 86 | 3ad2antl3 1068 |
. . . . . . 7
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)) |
88 | 87 | adantrr 448 |
. . . . . 6
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)) |
89 | | ltsonq 6496 |
. . . . . . . . . 10
⊢
<Q Or Q |
90 | | ltrelnq 6463 |
. . . . . . . . . 10
⊢
<Q ⊆ (Q ×
Q) |
91 | 89, 90 | sotri 4720 |
. . . . . . . . 9
⊢ ((𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶) ∧ ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)) → 𝐴 <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)) |
92 | 91 | ex 108 |
. . . . . . . 8
⊢ (𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶) → (([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) → 𝐴 <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) |
93 | 92 | adantl 262 |
. . . . . . 7
⊢ ((𝑧 ∈ N ∧
𝐴
<Q ([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶)) → (([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) → 𝐴 <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) |
94 | 93 | adantl 262 |
. . . . . 6
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → (([〈𝑧, 1𝑜〉]
~Q ·Q 𝐶) <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) → 𝐴 <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) |
95 | 88, 94 | mpd 13 |
. . . . 5
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → 𝐴 <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)) |
96 | | mulclnq 6474 |
. . . . . . . . . 10
⊢
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q ∈ Q
∧ 𝐶 ∈
Q) → ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶) ∈
Q) |
97 | 70, 96 | sylan 267 |
. . . . . . . . 9
⊢ ((𝑧 ∈ N ∧
𝐶 ∈ Q)
→ ([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) ∈ Q) |
98 | 97 | ancoms 255 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝑧 ∈ N)
→ ([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) ∈ Q) |
99 | 98 | 3ad2antl3 1068 |
. . . . . . 7
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶) ∈
Q) |
100 | | simpl2 908 |
. . . . . . 7
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → 𝐵 ∈ Q) |
101 | | ltaddnq 6505 |
. . . . . . 7
⊢
((([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) ∈ Q ∧ 𝐵 ∈ Q) →
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵)) |
102 | 99, 100, 101 | syl2anc 391 |
. . . . . 6
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶) <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵)) |
103 | 102 | adantrr 448 |
. . . . 5
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶) <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵)) |
104 | 89, 90 | sotri 4720 |
. . . . 5
⊢ ((𝐴 <Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) ∧ ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶) <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵)) → 𝐴 <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵)) |
105 | 95, 103, 104 | syl2anc 391 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → 𝐴 <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵)) |
106 | | addcomnqg 6479 |
. . . . . . 7
⊢
((([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) ∈ Q ∧ 𝐵 ∈ Q) →
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵) = (𝐵 +Q ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶))) |
107 | 99, 100, 106 | syl2anc 391 |
. . . . . 6
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → (([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶) +Q
𝐵) = (𝐵 +Q ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶))) |
108 | 107 | breq2d 3776 |
. . . . 5
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → (𝐴 <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵) ↔ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)))) |
109 | 108 | adantrr 448 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → (𝐴 <Q
(([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶) +Q 𝐵) ↔ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)))) |
110 | 105, 109 | mpbid 135 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) |
111 | | simpr 103 |
. . . . 5
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → 𝑧 ∈ N) |
112 | | breq2 3768 |
. . . . . . . 8
⊢ (𝑥 = (𝑧 +N
2𝑜) → (1𝑜
<N 𝑥 ↔ 1𝑜
<N (𝑧 +N
2𝑜))) |
113 | | opeq1 3549 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 +N
2𝑜) → 〈𝑥, 1𝑜〉 = 〈(𝑧 +N
2𝑜), 1𝑜〉) |
114 | 113 | eceq1d 6142 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 +N
2𝑜) → [〈𝑥, 1𝑜〉]
~Q = [〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ) |
115 | 114 | oveq1d 5527 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 +N
2𝑜) → ([〈𝑥, 1𝑜〉]
~Q ·Q 𝐶) = ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶)) |
116 | 115 | oveq2d 5528 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 +N
2𝑜) → (𝐵 +Q ([〈𝑥, 1𝑜〉]
~Q ·Q 𝐶)) = (𝐵 +Q ([〈(𝑧 +N
2𝑜), 1𝑜〉]
~Q ·Q 𝐶))) |
117 | 116 | breq2d 3776 |
. . . . . . . 8
⊢ (𝑥 = (𝑧 +N
2𝑜) → (𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶)) ↔ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)))) |
118 | 112, 117 | anbi12d 442 |
. . . . . . 7
⊢ (𝑥 = (𝑧 +N
2𝑜) → ((1𝑜
<N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶))) ↔ (1𝑜
<N (𝑧 +N
2𝑜) ∧ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))))) |
119 | 118 | rspcev 2656 |
. . . . . 6
⊢ (((𝑧 +N
2𝑜) ∈ N ∧ (1𝑜
<N (𝑧 +N
2𝑜) ∧ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶)))) → ∃𝑥 ∈ N
(1𝑜 <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶)))) |
120 | 119 | ex 108 |
. . . . 5
⊢ ((𝑧 +N
2𝑜) ∈ N → ((1𝑜
<N (𝑧 +N
2𝑜) ∧ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) → ∃𝑥 ∈ N
(1𝑜 <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶))))) |
121 | 111, 26, 120 | 3syl 17 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ 𝑧
∈ N) → ((1𝑜
<N (𝑧 +N
2𝑜) ∧ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) → ∃𝑥 ∈ N
(1𝑜 <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶))))) |
122 | 121 | adantrr 448 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → ((1𝑜
<N (𝑧 +N
2𝑜) ∧ 𝐴 <Q (𝐵 +Q
([〈(𝑧
+N 2𝑜),
1𝑜〉] ~Q
·Q 𝐶))) → ∃𝑥 ∈ N
(1𝑜 <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶))))) |
123 | 32, 110, 122 | mp2and 409 |
. 2
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) ∧ (𝑧
∈ N ∧ 𝐴 <Q
([〈𝑧,
1𝑜〉] ~Q
·Q 𝐶))) → ∃𝑥 ∈ N
(1𝑜 <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶)))) |
124 | 2, 123 | rexlimddv 2437 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ∃𝑥 ∈ N
(1𝑜 <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q
([〈𝑥,
1𝑜〉] ~Q
·Q 𝐶)))) |