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

Theorem prarloclemarch2 6402
Description: Like prarloclemarch 6401 but the integer must be at least two, and there is also B added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6485. (Contributed by Jim Kingdon, 25-Nov-2019.)
Assertion
Ref Expression
prarloclemarch2 ((A Q B Q 𝐶 Q) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))))
Distinct variable groups:   x,A   x,B   x,𝐶

Proof of Theorem prarloclemarch2
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 prarloclemarch 6401 . . 3 ((A Q 𝐶 Q) → z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))
213adant2 922 . 2 ((A Q B Q 𝐶 Q) → z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))
3 pinn 6293 . . . . . . . 8 (z Nz 𝜔)
4 1pi 6299 . . . . . . . . . . . 12 1𝑜 N
54elexi 2561 . . . . . . . . . . 11 1𝑜 V
65sucid 4120 . . . . . . . . . 10 1𝑜 suc 1𝑜
7 df-2o 5941 . . . . . . . . . 10 2𝑜 = suc 1𝑜
86, 7eleqtrri 2110 . . . . . . . . 9 1𝑜 2𝑜
9 2onn 6030 . . . . . . . . . . 11 2𝑜 𝜔
10 nnaword2 6023 . . . . . . . . . . 11 ((2𝑜 𝜔 z 𝜔) → 2𝑜 ⊆ (z +𝑜 2𝑜))
119, 10mpan 400 . . . . . . . . . 10 (z 𝜔 → 2𝑜 ⊆ (z +𝑜 2𝑜))
1211sseld 2938 . . . . . . . . 9 (z 𝜔 → (1𝑜 2𝑜 → 1𝑜 (z +𝑜 2𝑜)))
138, 12mpi 15 . . . . . . . 8 (z 𝜔 → 1𝑜 (z +𝑜 2𝑜))
143, 13syl 14 . . . . . . 7 (z N → 1𝑜 (z +𝑜 2𝑜))
15 o1p1e2 5987 . . . . . . . . 9 (1𝑜 +𝑜 1𝑜) = 2𝑜
16 addpiord 6300 . . . . . . . . . . 11 ((1𝑜 N 1𝑜 N) → (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜))
174, 4, 16mp2an 402 . . . . . . . . . 10 (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜)
18 addclpi 6311 . . . . . . . . . . 11 ((1𝑜 N 1𝑜 N) → (1𝑜 +N 1𝑜) N)
194, 4, 18mp2an 402 . . . . . . . . . 10 (1𝑜 +N 1𝑜) N
2017, 19eqeltrri 2108 . . . . . . . . 9 (1𝑜 +𝑜 1𝑜) N
2115, 20eqeltrri 2108 . . . . . . . 8 2𝑜 N
22 addpiord 6300 . . . . . . . 8 ((z N 2𝑜 N) → (z +N 2𝑜) = (z +𝑜 2𝑜))
2321, 22mpan2 401 . . . . . . 7 (z N → (z +N 2𝑜) = (z +𝑜 2𝑜))
2414, 23eleqtrrd 2114 . . . . . 6 (z N → 1𝑜 (z +N 2𝑜))
25 addclpi 6311 . . . . . . . 8 ((z N 2𝑜 N) → (z +N 2𝑜) N)
2621, 25mpan2 401 . . . . . . 7 (z N → (z +N 2𝑜) N)
27 ltpiord 6303 . . . . . . . 8 ((1𝑜 N (z +N 2𝑜) N) → (1𝑜 <N (z +N 2𝑜) ↔ 1𝑜 (z +N 2𝑜)))
284, 27mpan 400 . . . . . . 7 ((z +N 2𝑜) N → (1𝑜 <N (z +N 2𝑜) ↔ 1𝑜 (z +N 2𝑜)))
2926, 28syl 14 . . . . . 6 (z N → (1𝑜 <N (z +N 2𝑜) ↔ 1𝑜 (z +N 2𝑜)))
3024, 29mpbird 156 . . . . 5 (z N → 1𝑜 <N (z +N 2𝑜))
3130adantl 262 . . . 4 (((A Q B Q 𝐶 Q) z N) → 1𝑜 <N (z +N 2𝑜))
3231adantrr 448 . . 3 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → 1𝑜 <N (z +N 2𝑜))
33 nna0 5992 . . . . . . . . . . . . . . . . 17 (z 𝜔 → (z +𝑜 ∅) = z)
34 0lt1o 5962 . . . . . . . . . . . . . . . . . . . 20 1𝑜
35 1on 5947 . . . . . . . . . . . . . . . . . . . . . 22 1𝑜 On
3635onsuci 4207 . . . . . . . . . . . . . . . . . . . . 21 suc 1𝑜 On
37 ontr1 4092 . . . . . . . . . . . . . . . . . . . . 21 (suc 1𝑜 On → ((∅ 1𝑜 1𝑜 suc 1𝑜) → ∅ suc 1𝑜))
3836, 37ax-mp 7 . . . . . . . . . . . . . . . . . . . 20 ((∅ 1𝑜 1𝑜 suc 1𝑜) → ∅ suc 1𝑜)
3934, 6, 38mp2an 402 . . . . . . . . . . . . . . . . . . 19 suc 1𝑜
4039, 7eleqtrri 2110 . . . . . . . . . . . . . . . . . 18 2𝑜
41 nnaordi 6017 . . . . . . . . . . . . . . . . . . 19 ((2𝑜 𝜔 z 𝜔) → (∅ 2𝑜 → (z +𝑜 ∅) (z +𝑜 2𝑜)))
429, 41mpan 400 . . . . . . . . . . . . . . . . . 18 (z 𝜔 → (∅ 2𝑜 → (z +𝑜 ∅) (z +𝑜 2𝑜)))
4340, 42mpi 15 . . . . . . . . . . . . . . . . 17 (z 𝜔 → (z +𝑜 ∅) (z +𝑜 2𝑜))
4433, 43eqeltrrd 2112 . . . . . . . . . . . . . . . 16 (z 𝜔 → z (z +𝑜 2𝑜))
453, 44syl 14 . . . . . . . . . . . . . . 15 (z Nz (z +𝑜 2𝑜))
4645, 23eleqtrrd 2114 . . . . . . . . . . . . . 14 (z Nz (z +N 2𝑜))
47 ltpiord 6303 . . . . . . . . . . . . . . 15 ((z N (z +N 2𝑜) N) → (z <N (z +N 2𝑜) ↔ z (z +N 2𝑜)))
4826, 47mpdan 398 . . . . . . . . . . . . . 14 (z N → (z <N (z +N 2𝑜) ↔ z (z +N 2𝑜)))
4946, 48mpbird 156 . . . . . . . . . . . . 13 (z Nz <N (z +N 2𝑜))
50 mulidpi 6302 . . . . . . . . . . . . 13 (z N → (z ·N 1𝑜) = z)
51 mulcompig 6315 . . . . . . . . . . . . . . . 16 (((z +N 2𝑜) N 1𝑜 N) → ((z +N 2𝑜) ·N 1𝑜) = (1𝑜 ·N (z +N 2𝑜)))
524, 51mpan2 401 . . . . . . . . . . . . . . 15 ((z +N 2𝑜) N → ((z +N 2𝑜) ·N 1𝑜) = (1𝑜 ·N (z +N 2𝑜)))
5326, 52syl 14 . . . . . . . . . . . . . 14 (z N → ((z +N 2𝑜) ·N 1𝑜) = (1𝑜 ·N (z +N 2𝑜)))
54 mulidpi 6302 . . . . . . . . . . . . . . 15 ((z +N 2𝑜) N → ((z +N 2𝑜) ·N 1𝑜) = (z +N 2𝑜))
5526, 54syl 14 . . . . . . . . . . . . . 14 (z N → ((z +N 2𝑜) ·N 1𝑜) = (z +N 2𝑜))
5653, 55eqtr3d 2071 . . . . . . . . . . . . 13 (z N → (1𝑜 ·N (z +N 2𝑜)) = (z +N 2𝑜))
5749, 50, 563brtr4d 3785 . . . . . . . . . . . 12 (z N → (z ·N 1𝑜) <N (1𝑜 ·N (z +N 2𝑜)))
58 ordpipqqs 6358 . . . . . . . . . . . . . . 15 (((z N 1𝑜 N) ((z +N 2𝑜) N 1𝑜 N)) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (z ·N 1𝑜) <N (1𝑜 ·N (z +N 2𝑜))))
594, 58mpanl2 411 . . . . . . . . . . . . . 14 ((z N ((z +N 2𝑜) N 1𝑜 N)) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (z ·N 1𝑜) <N (1𝑜 ·N (z +N 2𝑜))))
604, 59mpanr2 414 . . . . . . . . . . . . 13 ((z N (z +N 2𝑜) N) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (z ·N 1𝑜) <N (1𝑜 ·N (z +N 2𝑜))))
6126, 60mpdan 398 . . . . . . . . . . . 12 (z N → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (z ·N 1𝑜) <N (1𝑜 ·N (z +N 2𝑜))))
6257, 61mpbird 156 . . . . . . . . . . 11 (z N → [⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )
6362adantl 262 . . . . . . . . . 10 ((𝐶 Q z N) → [⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )
64 opelxpi 4319 . . . . . . . . . . . . . . . 16 (((z +N 2𝑜) N 1𝑜 N) → ⟨(z +N 2𝑜), 1𝑜 (N × N))
654, 64mpan2 401 . . . . . . . . . . . . . . 15 ((z +N 2𝑜) N → ⟨(z +N 2𝑜), 1𝑜 (N × N))
66 enqex 6344 . . . . . . . . . . . . . . . 16 ~Q V
6766ecelqsi 6096 . . . . . . . . . . . . . . 15 (⟨(z +N 2𝑜), 1𝑜 (N × N) → [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ((N × N) / ~Q ))
6826, 65, 673syl 17 . . . . . . . . . . . . . 14 (z N → [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ((N × N) / ~Q ))
69 df-nqqs 6332 . . . . . . . . . . . . . 14 Q = ((N × N) / ~Q )
7068, 69syl6eleqr 2128 . . . . . . . . . . . . 13 (z N → [⟨(z +N 2𝑜), 1𝑜⟩] ~Q Q)
71 opelxpi 4319 . . . . . . . . . . . . . . . . 17 ((z N 1𝑜 N) → ⟨z, 1𝑜 (N × N))
724, 71mpan2 401 . . . . . . . . . . . . . . . 16 (z N → ⟨z, 1𝑜 (N × N))
7366ecelqsi 6096 . . . . . . . . . . . . . . . 16 (⟨z, 1𝑜 (N × N) → [⟨z, 1𝑜⟩] ~Q ((N × N) / ~Q ))
7472, 73syl 14 . . . . . . . . . . . . . . 15 (z N → [⟨z, 1𝑜⟩] ~Q ((N × N) / ~Q ))
7574, 69syl6eleqr 2128 . . . . . . . . . . . . . 14 (z N → [⟨z, 1𝑜⟩] ~Q Q)
76 ltmnqg 6385 . . . . . . . . . . . . . 14 (([⟨z, 1𝑜⟩] ~Q Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q Q 𝐶 Q) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) <Q (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )))
7775, 76syl3an1 1167 . . . . . . . . . . . . 13 ((z N [⟨(z +N 2𝑜), 1𝑜⟩] ~Q Q 𝐶 Q) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) <Q (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )))
7870, 77syl3an2 1168 . . . . . . . . . . . 12 ((z N z N 𝐶 Q) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) <Q (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )))
79783anidm12 1191 . . . . . . . . . . 11 ((z N 𝐶 Q) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) <Q (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )))
8079ancoms 255 . . . . . . . . . 10 ((𝐶 Q z N) → ([⟨z, 1𝑜⟩] ~Q <Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ↔ (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) <Q (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )))
8163, 80mpbid 135 . . . . . . . . 9 ((𝐶 Q z N) → (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) <Q (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ))
82 mulcomnqg 6367 . . . . . . . . . 10 ((𝐶 Q [⟨z, 1𝑜⟩] ~Q Q) → (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) = ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))
8375, 82sylan2 270 . . . . . . . . 9 ((𝐶 Q z N) → (𝐶 ·Q [⟨z, 1𝑜⟩] ~Q ) = ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))
84 mulcomnqg 6367 . . . . . . . . . 10 ((𝐶 Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q Q) → (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ) = ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
8570, 84sylan2 270 . . . . . . . . 9 ((𝐶 Q z N) → (𝐶 ·Q [⟨(z +N 2𝑜), 1𝑜⟩] ~Q ) = ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
8681, 83, 853brtr3d 3784 . . . . . . . 8 ((𝐶 Q z N) → ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
87863ad2antl3 1067 . . . . . . 7 (((A Q B Q 𝐶 Q) z N) → ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
8887adantrr 448 . . . . . 6 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
89 ltsonq 6382 . . . . . . . . . 10 <Q Or Q
90 ltrelnq 6349 . . . . . . . . . 10 <Q ⊆ (Q × Q)
9189, 90sotri 4663 . . . . . . . . 9 ((A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)) → A <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
9291ex 108 . . . . . . . 8 (A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) → (([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) → A <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
9392adantl 262 . . . . . . 7 ((z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶)) → (([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) → A <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
9493adantl 262 . . . . . 6 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → (([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) → A <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
9588, 94mpd 13 . . . . 5 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → A <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
96 mulclnq 6360 . . . . . . . . . 10 (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q Q 𝐶 Q) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q)
9770, 96sylan 267 . . . . . . . . 9 ((z N 𝐶 Q) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q)
9897ancoms 255 . . . . . . . 8 ((𝐶 Q z N) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q)
99983ad2antl3 1067 . . . . . . 7 (((A Q B Q 𝐶 Q) z N) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q)
100 simpl2 907 . . . . . . 7 (((A Q B Q 𝐶 Q) z N) → B Q)
101 ltaddnq 6390 . . . . . . 7 ((([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q B Q) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B))
10299, 100, 101syl2anc 391 . . . . . 6 (((A Q B Q 𝐶 Q) z N) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B))
103102adantrr 448 . . . . 5 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B))
10489, 90sotri 4663 . . . . 5 ((A <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B)) → A <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B))
10595, 103, 104syl2anc 391 . . . 4 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → A <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B))
106 addcomnqg 6365 . . . . . . 7 ((([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q B Q) → (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B) = (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
10799, 100, 106syl2anc 391 . . . . . 6 (((A Q B Q 𝐶 Q) z N) → (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B) = (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
108107breq2d 3767 . . . . 5 (((A Q B Q 𝐶 Q) z N) → (A <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B) ↔ A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))))
109108adantrr 448 . . . 4 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → (A <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B) ↔ A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))))
110105, 109mpbid 135 . . 3 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
111 simpr 103 . . . . 5 (((A Q B Q 𝐶 Q) z N) → z N)
112 breq2 3759 . . . . . . . 8 (x = (z +N 2𝑜) → (1𝑜 <N x ↔ 1𝑜 <N (z +N 2𝑜)))
113 opeq1 3540 . . . . . . . . . . . 12 (x = (z +N 2𝑜) → ⟨x, 1𝑜⟩ = ⟨(z +N 2𝑜), 1𝑜⟩)
114113eceq1d 6078 . . . . . . . . . . 11 (x = (z +N 2𝑜) → [⟨x, 1𝑜⟩] ~Q = [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )
115114oveq1d 5470 . . . . . . . . . 10 (x = (z +N 2𝑜) → ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶) = ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
116115oveq2d 5471 . . . . . . . . 9 (x = (z +N 2𝑜) → (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶)) = (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
117116breq2d 3767 . . . . . . . 8 (x = (z +N 2𝑜) → (A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶)) ↔ A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))))
118112, 117anbi12d 442 . . . . . . 7 (x = (z +N 2𝑜) → ((1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))) ↔ (1𝑜 <N (z +N 2𝑜) A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))))
119118rspcev 2650 . . . . . 6 (((z +N 2𝑜) N (1𝑜 <N (z +N 2𝑜) A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))))
120119ex 108 . . . . 5 ((z +N 2𝑜) N → ((1𝑜 <N (z +N 2𝑜) A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶)))))
121111, 26, 1203syl 17 . . . 4 (((A Q B Q 𝐶 Q) z N) → ((1𝑜 <N (z +N 2𝑜) A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶)))))
122121adantrr 448 . . 3 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → ((1𝑜 <N (z +N 2𝑜) A <Q (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶)))))
12332, 110, 122mp2and 409 . 2 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))))
1242, 123rexlimddv 2431 1 ((A Q B Q 𝐶 Q) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 884   = wceq 1242   wcel 1390  wrex 2301  wss 2911  c0 3218  cop 3370   class class class wbr 3755  Oncon0 4066  suc csuc 4068  𝜔com 4256   × cxp 4286  (class class class)co 5455  1𝑜c1o 5933  2𝑜c2o 5934   +𝑜 coa 5937  [cec 6040   / cqs 6041  Ncnpi 6256   +N cpli 6257   ·N cmi 6258   <N clti 6259   ~Q ceq 6263  Qcnq 6264   +Q cplq 6266   ·Q cmq 6267   <Q cltq 6269
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337
This theorem is referenced by:  prarloc  6485
  Copyright terms: Public domain W3C validator