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

Theorem caucvgprprlemell 7244
Description: Lemma for caucvgprpr 7271. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.)
Hypothesis
Ref Expression
caucvgprprlemell.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
Assertion
Ref Expression
caucvgprprlemell (𝑋 ∈ (1st𝐿) ↔ (𝑋Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
Distinct variable groups:   𝐹,𝑏   𝐹,𝑙,𝑟   𝑢,𝐹,𝑟   𝑋,𝑏,𝑝   𝑋,𝑙,𝑟,𝑝   𝑢,𝑋,𝑝   𝑋,𝑞,𝑏   𝑞,𝑙,𝑟   𝑢,𝑞
Allowed substitution hints:   𝐹(𝑞,𝑝)   𝐿(𝑢,𝑟,𝑞,𝑝,𝑏,𝑙)

Proof of Theorem caucvgprprlemell
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 oveq1 5659 . . . . . . . 8 (𝑙 = 𝑋 → (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) = (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )))
21breq2d 3857 . . . . . . 7 (𝑙 = 𝑋 → (𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))))
32abbidv 2205 . . . . . 6 (𝑙 = 𝑋 → {𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))})
41breq1d 3855 . . . . . . 7 (𝑙 = 𝑋 → ((𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞))
54abbidv 2205 . . . . . 6 (𝑙 = 𝑋 → {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞})
63, 5opeq12d 3630 . . . . 5 (𝑙 = 𝑋 → ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
76breq1d 3855 . . . 4 (𝑙 = 𝑋 → (⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
87rexbidv 2381 . . 3 (𝑙 = 𝑋 → (∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
9 caucvgprprlemell.lim . . . . 5 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
109fveq2i 5308 . . . 4 (1st𝐿) = (1st ‘⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩)
11 nqex 6922 . . . . . 6 Q ∈ V
1211rabex 3983 . . . . 5 {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)} ∈ V
1311rabex 3983 . . . . 5 {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩} ∈ V
1412, 13op1st 5917 . . . 4 (1st ‘⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩) = {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}
1510, 14eqtri 2108 . . 3 (1st𝐿) = {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}
168, 15elrab2 2774 . 2 (𝑋 ∈ (1st𝐿) ↔ (𝑋Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
17 opeq1 3622 . . . . . . . . . . . 12 (𝑟 = 𝑎 → ⟨𝑟, 1𝑜⟩ = ⟨𝑎, 1𝑜⟩)
1817eceq1d 6328 . . . . . . . . . . 11 (𝑟 = 𝑎 → [⟨𝑟, 1𝑜⟩] ~Q = [⟨𝑎, 1𝑜⟩] ~Q )
1918fveq2d 5309 . . . . . . . . . 10 (𝑟 = 𝑎 → (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))
2019oveq2d 5668 . . . . . . . . 9 (𝑟 = 𝑎 → (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) = (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
2120breq2d 3857 . . . . . . . 8 (𝑟 = 𝑎 → (𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))))
2221abbidv 2205 . . . . . . 7 (𝑟 = 𝑎 → {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))})
2320breq1d 3855 . . . . . . . 8 (𝑟 = 𝑎 → ((𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞))
2423abbidv 2205 . . . . . . 7 (𝑟 = 𝑎 → {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞})
2522, 24opeq12d 3630 . . . . . 6 (𝑟 = 𝑎 → ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
26 fveq2 5305 . . . . . 6 (𝑟 = 𝑎 → (𝐹𝑟) = (𝐹𝑎))
2725, 26breq12d 3858 . . . . 5 (𝑟 = 𝑎 → (⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎)))
2827cbvrexv 2591 . . . 4 (∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ∃𝑎N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎))
29 opeq1 3622 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ⟨𝑎, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
3029eceq1d 6328 . . . . . . . . . . 11 (𝑎 = 𝑏 → [⟨𝑎, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
3130fveq2d 5309 . . . . . . . . . 10 (𝑎 = 𝑏 → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
3231oveq2d 5668 . . . . . . . . 9 (𝑎 = 𝑏 → (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
3332breq2d 3857 . . . . . . . 8 (𝑎 = 𝑏 → (𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) ↔ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))))
3433abbidv 2205 . . . . . . 7 (𝑎 = 𝑏 → {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))} = {𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))})
3532breq1d 3855 . . . . . . . 8 (𝑎 = 𝑏 → ((𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞 ↔ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞))
3635abbidv 2205 . . . . . . 7 (𝑎 = 𝑏 → {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞})
3734, 36opeq12d 3630 . . . . . 6 (𝑎 = 𝑏 → ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
38 fveq2 5305 . . . . . 6 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3937, 38breq12d 3858 . . . . 5 (𝑎 = 𝑏 → (⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ↔ ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
4039cbvrexv 2591 . . . 4 (∃𝑎N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ↔ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
4128, 40bitri 182 . . 3 (∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟) ↔ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
4241anbi2i 445 . 2 ((𝑋Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)) ↔ (𝑋Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
4316, 42bitri 182 1 (𝑋 ∈ (1st𝐿) ↔ (𝑋Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1289  wcel 1438  {cab 2074  wrex 2360  {crab 2363  cop 3449   class class class wbr 3845  cfv 5015  (class class class)co 5652  1st c1st 5909  1𝑜c1o 6174  [cec 6290  Ncnpi 6831   ~Q ceq 6838  Qcnq 6839   +Q cplq 6841  *Qcrq 6843   <Q cltq 6844   +P cpp 6852  <P cltp 6854
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-iinf 4403
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-id 4120  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-ov 5655  df-1st 5911  df-ec 6294  df-qs 6298  df-ni 6863  df-nqqs 6907
This theorem is referenced by:  caucvgprprlemopl  7256  caucvgprprlemlol  7257  caucvgprprlemdisj  7261  caucvgprprlemloc  7262
  Copyright terms: Public domain W3C validator