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

Theorem caucvgprprlemcbv 6991
 Description: Lemma for caucvgprpr 7016. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-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
caucvgprprlemcbv (𝜑 → ∀𝑎N𝑏N (𝑎 <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 caucvgprprlemcbv
StepHypRef Expression
1 caucvgprpr.cau . 2 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
2 breq1 3808 . . . 4 (𝑛 = 𝑎 → (𝑛 <N 𝑘𝑎 <N 𝑘))
3 fveq2 5229 . . . . . 6 (𝑛 = 𝑎 → (𝐹𝑛) = (𝐹𝑎))
4 opeq1 3590 . . . . . . . . . . . 12 (𝑛 = 𝑎 → ⟨𝑛, 1𝑜⟩ = ⟨𝑎, 1𝑜⟩)
54eceq1d 6229 . . . . . . . . . . 11 (𝑛 = 𝑎 → [⟨𝑛, 1𝑜⟩] ~Q = [⟨𝑎, 1𝑜⟩] ~Q )
65fveq2d 5233 . . . . . . . . . 10 (𝑛 = 𝑎 → (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))
76breq2d 3817 . . . . . . . . 9 (𝑛 = 𝑎 → (𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
87abbidv 2200 . . . . . . . 8 (𝑛 = 𝑎 → {𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )} = {𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )})
96breq1d 3815 . . . . . . . . 9 (𝑛 = 𝑎 → ((*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢))
109abbidv 2200 . . . . . . . 8 (𝑛 = 𝑎 → {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢})
118, 10opeq12d 3598 . . . . . . 7 (𝑛 = 𝑎 → ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)
1211oveq2d 5579 . . . . . 6 (𝑛 = 𝑎 → ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
133, 12breq12d 3818 . . . . 5 (𝑛 = 𝑎 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
143, 11oveq12d 5581 . . . . . 6 (𝑛 = 𝑎 → ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
1514breq2d 3817 . . . . 5 (𝑛 = 𝑎 → ((𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
1613, 15anbi12d 457 . . . 4 (𝑛 = 𝑎 → (((𝐹𝑛)<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 𝑢}⟩))))
172, 16imbi12d 232 . . 3 (𝑛 = 𝑎 → ((𝑛 <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 𝑢}⟩)))))
18 breq2 3809 . . . 4 (𝑘 = 𝑏 → (𝑎 <N 𝑘𝑎 <N 𝑏))
19 fveq2 5229 . . . . . . 7 (𝑘 = 𝑏 → (𝐹𝑘) = (𝐹𝑏))
2019oveq1d 5578 . . . . . 6 (𝑘 = 𝑏 → ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2120breq2d 3817 . . . . 5 (𝑘 = 𝑏 → ((𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2219breq1d 3815 . . . . 5 (𝑘 = 𝑏 → ((𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2321, 22anbi12d 457 . . . 4 (𝑘 = 𝑏 → (((𝐹𝑎)<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 𝑢}⟩))))
2418, 23imbi12d 232 . . 3 (𝑘 = 𝑏 → ((𝑎 <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 𝑢}⟩)))))
2517, 24cbvral2v 2590 . 2 (∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) ↔ ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
261, 25sylib 120 1 (𝜑 → ∀𝑎N𝑏N (𝑎 <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 102  {cab 2069  ∀wral 2353  ⟨cop 3419   class class class wbr 3805  ⟶wf 4948  ‘cfv 4952  (class class class)co 5563  1𝑜c1o 6078  [cec 6191  Ncnpi 6576
 Copyright terms: Public domain W3C validator