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

Theorem caucvgprprlemval 6786
 Description: Lemma for caucvgprpr 6810. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
Assertion
Ref Expression
caucvgprprlemval ((𝜑𝐴 <N 𝐵) → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
Distinct variable groups:   𝐴,𝑙   𝑢,𝐴   𝐴,𝑝,𝑙   𝐴,𝑞,𝑢   𝑘,𝐹,𝑛   𝑘,𝑙,𝑛   𝑢,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝐴(𝑘,𝑛)   𝐵(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝐹(𝑢,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemval
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelpi 6422 . . . . 5 <N ⊆ (N × N)
21brel 4392 . . . 4 (𝐴 <N 𝐵 → (𝐴N𝐵N))
32adantl 262 . . 3 ((𝜑𝐴 <N 𝐵) → (𝐴N𝐵N))
4 caucvgprpr.f . . . . 5 (𝜑𝐹:NP)
5 caucvgprpr.cau . . . . 5 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
64, 5caucvgprprlemcbv 6785 . . . 4 (𝜑 → ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
76adantr 261 . . 3 ((𝜑𝐴 <N 𝐵) → ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
8 simpr 103 . . 3 ((𝜑𝐴 <N 𝐵) → 𝐴 <N 𝐵)
9 breq1 3767 . . . . 5 (𝑎 = 𝐴 → (𝑎 <N 𝑏𝐴 <N 𝑏))
10 fveq2 5178 . . . . . . 7 (𝑎 = 𝐴 → (𝐹𝑎) = (𝐹𝐴))
11 opeq1 3549 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ⟨𝑎, 1𝑜⟩ = ⟨𝐴, 1𝑜⟩)
1211eceq1d 6142 . . . . . . . . . . . 12 (𝑎 = 𝐴 → [⟨𝑎, 1𝑜⟩] ~Q = [⟨𝐴, 1𝑜⟩] ~Q )
1312fveq2d 5182 . . . . . . . . . . 11 (𝑎 = 𝐴 → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ))
1413breq2d 3776 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )))
1514abbidv 2155 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )} = {𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )})
1613breq1d 3774 . . . . . . . . . 10 (𝑎 = 𝐴 → ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢))
1716abbidv 2155 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢})
1815, 17opeq12d 3557 . . . . . . . 8 (𝑎 = 𝐴 → ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)
1918oveq2d 5528 . . . . . . 7 (𝑎 = 𝐴 → ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2010, 19breq12d 3777 . . . . . 6 (𝑎 = 𝐴 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2110, 18oveq12d 5530 . . . . . . 7 (𝑎 = 𝐴 → ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2221breq2d 3776 . . . . . 6 (𝑎 = 𝐴 → ((𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2320, 22anbi12d 442 . . . . 5 (𝑎 = 𝐴 → (((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
249, 23imbi12d 223 . . . 4 (𝑎 = 𝐴 → ((𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) ↔ (𝐴 <N 𝑏 → ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))))
25 breq2 3768 . . . . 5 (𝑏 = 𝐵 → (𝐴 <N 𝑏𝐴 <N 𝐵))
26 fveq2 5178 . . . . . . . 8 (𝑏 = 𝐵 → (𝐹𝑏) = (𝐹𝐵))
2726oveq1d 5527 . . . . . . 7 (𝑏 = 𝐵 → ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2827breq2d 3776 . . . . . 6 (𝑏 = 𝐵 → ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2926breq1d 3774 . . . . . 6 (𝑏 = 𝐵 → ((𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
3028, 29anbi12d 442 . . . . 5 (𝑏 = 𝐵 → (((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
3125, 30imbi12d 223 . . . 4 (𝑏 = 𝐵 → ((𝐴 <N 𝑏 → ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) ↔ (𝐴 <N 𝐵 → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))))
3224, 31rspc2v 2662 . . 3 ((𝐴N𝐵N) → (∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) → (𝐴 <N 𝐵 → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))))
333, 7, 8, 32syl3c 57 . 2 ((𝜑𝐴 <N 𝐵) → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
34 breq1 3767 . . . . . . 7 (𝑙 = 𝑝 → (𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )))
3534cbvabv 2161 . . . . . 6 {𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}
36 breq2 3768 . . . . . . 7 (𝑢 = 𝑞 → ((*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞))
3736cbvabv 2161 . . . . . 6 {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}
3835, 37opeq12i 3554 . . . . 5 ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩
3938oveq2i 5523 . . . 4 ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4039breq2i 3772 . . 3 ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4138oveq2i 5523 . . . 4 ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4241breq2i 3772 . . 3 ((𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4340, 42anbi12i 433 . 2 (((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
4433, 43sylib 127 1 ((𝜑𝐴 <N 𝐵) → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243   ∈ wcel 1393  {cab 2026  ∀wral 2306  ⟨cop 3378   class class class wbr 3764  ⟶wf 4898  ‘cfv 4902  (class class class)co 5512  1𝑜c1o 5994  [cec 6104  Ncnpi 6370
 Copyright terms: Public domain W3C validator