prarloclemarch2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > prarloclemarch2		GIF version

Theorem prarloclemarch2 6517

Description: Like prarloclemarch 6516 but the integer must be at least two, and there is also 𝐵 added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6601. (Contributed by Jim Kingdon, 25-Nov-2019.)

**Assertion**
Ref	Expression
prarloclemarch2	⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ∃𝑥 ∈ N (1_𝑜 <_N 𝑥 ∧ 𝐴 <_Q (𝐵 +_Q ([⟨𝑥, 1_𝑜⟩] ~_Q ·_Q 𝐶))))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐶

Proof of Theorem prarloclemarch2 Dummy variable 𝑧 is distinct from all other variables.

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 𝐶))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∧ w3a 885 = wceq 1243 ∈ wcel 1393 ∃wrex 2307 ⊆ wss 2917 ∅c0 3224 ⟨cop 3378 class class class wbr 3764 Oncon0 4100 suc csuc 4102 ωcom 4313 × cxp 4343 (class class class)co 5512 1_𝑜c1o 5994 2_𝑜c2o 5995 +_𝑜 coa 5998 [cec 6104 / cqs 6105 Ncnpi 6370 +_N cpli 6371 ·_N cmi 6372 <_N clti 6373 ~_Q ceq 6377 Qcnq 6378 +_Q cplq 6380 ·_Q cmq 6381 <_Q cltq 6383

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-13 1404 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-coll 3872 ax-sep 3875 ax-nul 3883 ax-pow 3927 ax-pr 3944 ax-un 4170 ax-setind 4262 ax-iinf 4311

This theorem depends on definitions: df-bi 110 df-dc 743 df-3or 886 df-3an 887 df-tru 1246 df-fal 1249 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ne 2206 df-ral 2311 df-rex 2312 df-reu 2313 df-rab 2315 df-v 2559 df-sbc 2765 df-csb 2853 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-nul 3225 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-int 3616 df-iun 3659 df-br 3765 df-opab 3819 df-mpt 3820 df-tr 3855 df-eprel 4026 df-id 4030 df-po 4033 df-iso 4034 df-iord 4103 df-on 4105 df-suc 4108 df-iom 4314 df-xp 4351 df-rel 4352 df-cnv 4353 df-co 4354 df-dm 4355 df-rn 4356 df-res 4357 df-ima 4358 df-iota 4867 df-fun 4904 df-fn 4905 df-f 4906 df-f1 4907 df-fo 4908 df-f1o 4909 df-fv 4910 df-ov 5515 df-oprab 5516 df-mpt2 5517 df-1st 5767 df-2nd 5768 df-recs 5920 df-irdg 5957 df-1o 6001 df-2o 6002 df-oadd 6005 df-omul 6006 df-er 6106 df-ec 6108 df-qs 6112 df-ni 6402 df-pli 6403 df-mi 6404 df-lti 6405 df-plpq 6442 df-mpq 6443 df-enq 6445 df-nqqs 6446 df-plqqs 6447 df-mqqs 6448 df-1nqqs 6449 df-rq 6450 df-ltnqqs 6451

This theorem is referenced by: prarloc 6601

W3C validator