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

Theorem prarloclemarch2 6276
Description: Like prarloclemarch 6275 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 6357. (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 6275 . . 3 ((A Q 𝐶 Q) → z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))
213adant2 911 . 2 ((A Q B Q 𝐶 Q) → z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))
3 pinn 6169 . . . . . . . 8 (z Nz 𝜔)
4 1pi 6175 . . . . . . . . . . . 12 1𝑜 N
54elexi 2544 . . . . . . . . . . 11 1𝑜 V
65sucid 4103 . . . . . . . . . 10 1𝑜 suc 1𝑜
7 df-2o 5917 . . . . . . . . . 10 2𝑜 = suc 1𝑜
86, 7eleqtrri 2095 . . . . . . . . 9 1𝑜 2𝑜
9 2onn 6005 . . . . . . . . . . 11 2𝑜 𝜔
10 nnaword2 5998 . . . . . . . . . . 11 ((2𝑜 𝜔 z 𝜔) → 2𝑜 ⊆ (z +𝑜 2𝑜))
119, 10mpan 402 . . . . . . . . . 10 (z 𝜔 → 2𝑜 ⊆ (z +𝑜 2𝑜))
1211sseld 2921 . . . . . . . . 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 5963 . . . . . . . . 9 (1𝑜 +𝑜 1𝑜) = 2𝑜
16 addpiord 6176 . . . . . . . . . . 11 ((1𝑜 N 1𝑜 N) → (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜))
174, 4, 16mp2an 404 . . . . . . . . . 10 (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜)
18 addclpi 6187 . . . . . . . . . . 11 ((1𝑜 N 1𝑜 N) → (1𝑜 +N 1𝑜) N)
194, 4, 18mp2an 404 . . . . . . . . . 10 (1𝑜 +N 1𝑜) N
2017, 19eqeltrri 2093 . . . . . . . . 9 (1𝑜 +𝑜 1𝑜) N
2115, 20eqeltrri 2093 . . . . . . . 8 2𝑜 N
22 addpiord 6176 . . . . . . . 8 ((z N 2𝑜 N) → (z +N 2𝑜) = (z +𝑜 2𝑜))
2321, 22mpan2 403 . . . . . . 7 (z N → (z +N 2𝑜) = (z +𝑜 2𝑜))
2414, 23eleqtrrd 2099 . . . . . 6 (z N → 1𝑜 (z +N 2𝑜))
25 addclpi 6187 . . . . . . . 8 ((z N 2𝑜 N) → (z +N 2𝑜) N)
2621, 25mpan2 403 . . . . . . 7 (z N → (z +N 2𝑜) N)
27 ltpiord 6179 . . . . . . . 8 ((1𝑜 N (z +N 2𝑜) N) → (1𝑜 <N (z +N 2𝑜) ↔ 1𝑜 (z +N 2𝑜)))
284, 27mpan 402 . . . . . . 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 451 . . 3 (((A Q B Q 𝐶 Q) (z N A <Q ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶))) → 1𝑜 <N (z +N 2𝑜))
33 nna0 5968 . . . . . . . . . . . . . . . . 17 (z 𝜔 → (z +𝑜 ∅) = z)
34 0lt1o 5938 . . . . . . . . . . . . . . . . . . . 20 1𝑜
35 1on 5923 . . . . . . . . . . . . . . . . . . . . . 22 1𝑜 On
3635onsuci 4191 . . . . . . . . . . . . . . . . . . . . 21 suc 1𝑜 On
37 ontr1 4075 . . . . . . . . . . . . . . . . . . . . 21 (suc 1𝑜 On → ((∅ 1𝑜 1𝑜 suc 1𝑜) → ∅ suc 1𝑜))
3836, 37ax-mp 7 . . . . . . . . . . . . . . . . . . . 20 ((∅ 1𝑜 1𝑜 suc 1𝑜) → ∅ suc 1𝑜)
3934, 6, 38mp2an 404 . . . . . . . . . . . . . . . . . . 19 suc 1𝑜
4039, 7eleqtrri 2095 . . . . . . . . . . . . . . . . . 18 2𝑜
41 nnaordi 5992 . . . . . . . . . . . . . . . . . . 19 ((2𝑜 𝜔 z 𝜔) → (∅ 2𝑜 → (z +𝑜 ∅) (z +𝑜 2𝑜)))
429, 41mpan 402 . . . . . . . . . . . . . . . . . 18 (z 𝜔 → (∅ 2𝑜 → (z +𝑜 ∅) (z +𝑜 2𝑜)))
4340, 42mpi 15 . . . . . . . . . . . . . . . . 17 (z 𝜔 → (z +𝑜 ∅) (z +𝑜 2𝑜))
4433, 43eqeltrrd 2097 . . . . . . . . . . . . . . . 16 (z 𝜔 → z (z +𝑜 2𝑜))
453, 44syl 14 . . . . . . . . . . . . . . 15 (z Nz (z +𝑜 2𝑜))
4645, 23eleqtrrd 2099 . . . . . . . . . . . . . 14 (z Nz (z +N 2𝑜))
47 ltpiord 6179 . . . . . . . . . . . . . . 15 ((z N (z +N 2𝑜) N) → (z <N (z +N 2𝑜) ↔ z (z +N 2𝑜)))
4826, 47mpdan 400 . . . . . . . . . . . . . 14 (z N → (z <N (z +N 2𝑜) ↔ z (z +N 2𝑜)))
4946, 48mpbird 156 . . . . . . . . . . . . 13 (z Nz <N (z +N 2𝑜))
50 mulidpi 6178 . . . . . . . . . . . . 13 (z N → (z ·N 1𝑜) = z)
51 mulcompig 6191 . . . . . . . . . . . . . . . 16 (((z +N 2𝑜) N 1𝑜 N) → ((z +N 2𝑜) ·N 1𝑜) = (1𝑜 ·N (z +N 2𝑜)))
524, 51mpan2 403 . . . . . . . . . . . . . . 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 6178 . . . . . . . . . . . . . . 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 2056 . . . . . . . . . . . . 13 (z N → (1𝑜 ·N (z +N 2𝑜)) = (z +N 2𝑜))
5749, 50, 563brtr4d 3768 . . . . . . . . . . . 12 (z N → (z ·N 1𝑜) <N (1𝑜 ·N (z +N 2𝑜)))
58 ordpipqqs 6233 . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . 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 416 . . . . . . . . . . . . 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 400 . . . . . . . . . . . 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 4303 . . . . . . . . . . . . . . . 16 (((z +N 2𝑜) N 1𝑜 N) → ⟨(z +N 2𝑜), 1𝑜 (N × N))
654, 64mpan2 403 . . . . . . . . . . . . . . 15 ((z +N 2𝑜) N → ⟨(z +N 2𝑜), 1𝑜 (N × N))
66 enqex 6219 . . . . . . . . . . . . . . . 16 ~Q V
6766ecelqsi 6071 . . . . . . . . . . . . . . 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 6207 . . . . . . . . . . . . . 14 Q = ((N × N) / ~Q )
7068, 69syl6eleqr 2113 . . . . . . . . . . . . 13 (z N → [⟨(z +N 2𝑜), 1𝑜⟩] ~Q Q)
71 opelxpi 4303 . . . . . . . . . . . . . . . . 17 ((z N 1𝑜 N) → ⟨z, 1𝑜 (N × N))
724, 71mpan2 403 . . . . . . . . . . . . . . . 16 (z N → ⟨z, 1𝑜 (N × N))
7366ecelqsi 6071 . . . . . . . . . . . . . . . 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 2113 . . . . . . . . . . . . . 14 (z N → [⟨z, 1𝑜⟩] ~Q Q)
76 ltmnqg 6260 . . . . . . . . . . . . . 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 1154 . . . . . . . . . . . . 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 1155 . . . . . . . . . . . 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 1178 . . . . . . . . . . 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 6242 . . . . . . . . . 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 6242 . . . . . . . . . 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 3767 . . . . . . . 8 ((𝐶 Q z N) → ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
87863ad2antl3 1056 . . . . . . 7 (((A Q B Q 𝐶 Q) z N) → ([⟨z, 1𝑜⟩] ~Q ·Q 𝐶) <Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
8887adantrr 451 . . . . . 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 6257 . . . . . . . . . 10 <Q Or Q
90 ltrelnq 6224 . . . . . . . . . 10 <Q ⊆ (Q × Q)
9189, 90sotri 4647 . . . . . . . . 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 6235 . . . . . . . . . 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 1056 . . . . . . 7 (((A Q B Q 𝐶 Q) z N) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) Q)
100 simpl2 896 . . . . . . 7 (((A Q B Q 𝐶 Q) z N) → B Q)
101 ltaddnq 6265 . . . . . . 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 393 . . . . . 6 (((A Q B Q 𝐶 Q) z N) → ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) <Q (([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶) +Q B))
103102adantrr 451 . . . . 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 4647 . . . . 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 393 . . . 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 6240 . . . . . . 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 393 . . . . . 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 3750 . . . . 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 451 . . . 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 ax-ia2 100 . . . . 5 (((A Q B Q 𝐶 Q) z N) → z N)
112 breq2 3742 . . . . . . . 8 (x = (z +N 2𝑜) → (1𝑜 <N x ↔ 1𝑜 <N (z +N 2𝑜)))
113 opeq1 3523 . . . . . . . . . . . 12 (x = (z +N 2𝑜) → ⟨x, 1𝑜⟩ = ⟨(z +N 2𝑜), 1𝑜⟩)
114113eceq1d 6053 . . . . . . . . . . 11 (x = (z +N 2𝑜) → [⟨x, 1𝑜⟩] ~Q = [⟨(z +N 2𝑜), 1𝑜⟩] ~Q )
115114oveq1d 5451 . . . . . . . . . 10 (x = (z +N 2𝑜) → ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶) = ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶))
116115oveq2d 5452 . . . . . . . . 9 (x = (z +N 2𝑜) → (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶)) = (B +Q ([⟨(z +N 2𝑜), 1𝑜⟩] ~Q ·Q 𝐶)))
117116breq2d 3750 . . . . . . . 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 445 . . . . . . 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 2633 . . . . . 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 451 . . 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 411 . 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 2415 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 873   = wceq 1228   wcel 1374  wrex 2285  wss 2894  c0 3201  cop 3353   class class class wbr 3738  Oncon0 4049  suc csuc 4051  𝜔com 4240   × cxp 4270  (class class class)co 5436  1𝑜c1o 5909  2𝑜c2o 5910   +𝑜 coa 5913  [cec 6015   / cqs 6016  Ncnpi 6130   +N cpli 6131   ·N cmi 6132   <N clti 6133   ~Q ceq 6137  Qcnq 6138   +Q cplq 6140   ·Q cmq 6141   <Q cltq 6143
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 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-coll 3846  ax-sep 3849  ax-nul 3857  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204  ax-iinf 4238
This theorem depends on definitions:  df-bi 110  df-dc 734  df-3or 874  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-csb 2830  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-int 3590  df-iun 3633  df-br 3739  df-opab 3793  df-mpt 3794  df-tr 3829  df-eprel 4000  df-id 4004  df-po 4007  df-iso 4008  df-iord 4052  df-on 4054  df-suc 4057  df-iom 4241  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-fo 4835  df-f1o 4836  df-fv 4837  df-ov 5439  df-oprab 5440  df-mpt2 5441  df-1st 5690  df-2nd 5691  df-recs 5842  df-irdg 5878  df-1o 5916  df-2o 5917  df-oadd 5920  df-omul 5921  df-er 6017  df-ec 6019  df-qs 6023  df-ni 6164  df-pli 6165  df-mi 6166  df-lti 6167  df-plpq 6203  df-mpq 6204  df-enq 6206  df-nqqs 6207  df-plqqs 6208  df-mqqs 6209  df-1nqqs 6210  df-rq 6211  df-ltnqqs 6212
This theorem is referenced by:  prarloc  6357
  Copyright terms: Public domain W3C validator