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

Theorem caucvgprprlemcbv 7546
 Description: Lemma for caucvgprpr 7571. 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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
Assertion
Ref Expression
caucvgprprlemcbv (𝜑 → ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
2 breq1 3941 . . . 4 (𝑛 = 𝑎 → (𝑛 <N 𝑘𝑎 <N 𝑘))
3 fveq2 5432 . . . . . 6 (𝑛 = 𝑎 → (𝐹𝑛) = (𝐹𝑎))
4 opeq1 3714 . . . . . . . . . . . 12 (𝑛 = 𝑎 → ⟨𝑛, 1o⟩ = ⟨𝑎, 1o⟩)
54eceq1d 6476 . . . . . . . . . . 11 (𝑛 = 𝑎 → [⟨𝑛, 1o⟩] ~Q = [⟨𝑎, 1o⟩] ~Q )
65fveq2d 5436 . . . . . . . . . 10 (𝑛 = 𝑎 → (*Q‘[⟨𝑛, 1o⟩] ~Q ) = (*Q‘[⟨𝑎, 1o⟩] ~Q ))
76breq2d 3950 . . . . . . . . 9 (𝑛 = 𝑎 → (𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )))
87abbidv 2258 . . . . . . . 8 (𝑛 = 𝑎 → {𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )} = {𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )})
96breq1d 3948 . . . . . . . . 9 (𝑛 = 𝑎 → ((*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢))
109abbidv 2258 . . . . . . . 8 (𝑛 = 𝑎 → {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢})
118, 10opeq12d 3722 . . . . . . 7 (𝑛 = 𝑎 → ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)
1211oveq2d 5801 . . . . . 6 (𝑛 = 𝑎 → ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))
133, 12breq12d 3951 . . . . 5 (𝑛 = 𝑎 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))
143, 11oveq12d 5803 . . . . . 6 (𝑛 = 𝑎 → ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))
1514breq2d 3950 . . . . 5 (𝑛 = 𝑎 → ((𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))
1613, 15anbi12d 465 . . . 4 (𝑛 = 𝑎 → (((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))))
172, 16imbi12d 233 . . 3 (𝑛 = 𝑎 → ((𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))) ↔ (𝑎 <N 𝑘 → ((𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))))
18 breq2 3942 . . . 4 (𝑘 = 𝑏 → (𝑎 <N 𝑘𝑎 <N 𝑏))
19 fveq2 5432 . . . . . . 7 (𝑘 = 𝑏 → (𝐹𝑘) = (𝐹𝑏))
2019oveq1d 5800 . . . . . 6 (𝑘 = 𝑏 → ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))
2120breq2d 3950 . . . . 5 (𝑘 = 𝑏 → ((𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))
2219breq1d 3948 . . . . 5 (𝑘 = 𝑏 → ((𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))
2321, 22anbi12d 465 . . . 4 (𝑘 = 𝑏 → (((𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))))
2418, 23imbi12d 233 . . 3 (𝑘 = 𝑏 → ((𝑎 <N 𝑘 → ((𝐹𝑎)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))) ↔ (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))))
2517, 24cbvral2v 2669 . 2 (∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))) ↔ ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))))
261, 25sylib 121 1 (𝜑 → ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103  {cab 2126  ∀wral 2417  ⟨cop 3536   class class class wbr 3938  ⟶wf 5130  ‘cfv 5134  (class class class)co 5785  1oc1o 6317  [cec 6438  Ncnpi 7131
 Copyright terms: Public domain W3C validator