MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cau3lem Structured version   Visualization version   GIF version

Theorem cau3lem 15341
Description: Lemma for cau3 15342. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.)
Hypotheses
Ref Expression
cau3lem.1 𝑍 ⊆ ℤ
cau3lem.2 (𝜏𝜓)
cau3lem.3 ((𝐹𝑘) = (𝐹𝑗) → (𝜓𝜒))
cau3lem.4 ((𝐹𝑘) = (𝐹𝑚) → (𝜓𝜃))
cau3lem.5 ((𝜑𝜒𝜓) → (𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) = (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))))
cau3lem.6 ((𝜑𝜃𝜒) → (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) = (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))))
cau3lem.7 ((𝜑 ∧ (𝜓𝜃) ∧ (𝜒𝑥 ∈ ℝ)) → (((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
Assertion
Ref Expression
cau3lem (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
Distinct variable groups:   𝑘,𝑚,𝜒   𝑥,𝑘,𝐷,𝑚   𝑘,𝐹,𝑚,𝑥   𝑗,𝑘,𝑚,𝑥,𝜑   𝑘,𝐺,𝑚,𝑥   𝜓,𝑚,𝑥   𝜏,𝑥   𝜃,𝑘   𝑥,𝑍
Allowed substitution hints:   𝜓(𝑗,𝑘)   𝜒(𝑥,𝑗)   𝜃(𝑥,𝑗,𝑚)   𝜏(𝑗,𝑘,𝑚)   𝐷(𝑗)   𝐹(𝑗)   𝐺(𝑗)   𝑍(𝑗,𝑘,𝑚)

Proof of Theorem cau3lem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 breq2 5156 . . . . . 6 (𝑥 = 𝑧 → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧))
21anbi2d 628 . . . . 5 (𝑥 = 𝑧 → ((𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ (𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧)))
32rexralbidv 3218 . . . 4 (𝑥 = 𝑧 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧)))
43cbvralvw 3232 . . 3 (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑧 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧))
5 rphalfcl 13041 . . . . . . 7 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
6 breq2 5156 . . . . . . . . . 10 (𝑧 = (𝑥 / 2) → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)))
76anbi2d 628 . . . . . . . . 9 (𝑧 = (𝑥 / 2) → ((𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) ↔ (𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))))
87rexralbidv 3218 . . . . . . . 8 (𝑧 = (𝑥 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))))
98rspcv 3607 . . . . . . 7 ((𝑥 / 2) ∈ ℝ+ → (∀𝑧 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))))
105, 9syl 17 . . . . . 6 (𝑥 ∈ ℝ+ → (∀𝑧 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))))
1110adantl 480 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∀𝑧 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))))
12 cau3lem.2 . . . . . . . . . 10 (𝜏𝜓)
1312ralimi 3080 . . . . . . . . 9 (∀𝑘 ∈ (ℤ𝑗)𝜏 → ∀𝑘 ∈ (ℤ𝑗)𝜓)
14 r19.26 3108 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) ↔ (∀𝑘 ∈ (ℤ𝑗)𝜓 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)))
15 fveq2 6902 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
16 cau3lem.4 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑘) = (𝐹𝑚) → (𝜓𝜃))
1715, 16syl 17 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝜓𝜃))
1815fvoveq1d 7448 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) = (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))))
1918breq1d 5162 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ↔ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))
2017, 19anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → ((𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) ↔ (𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))))
2120cbvralvw 3232 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) ↔ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))
2221biimpi 215 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))
2322a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))))
2414, 23biimtrrid 242 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((∀𝑘 ∈ (ℤ𝑗)𝜓 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))))
2524expdimp 451 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))))
26 cau3lem.1 . . . . . . . . . . . . . . 15 𝑍 ⊆ ℤ
2726sseli 3978 . . . . . . . . . . . . . 14 (𝑗𝑍𝑗 ∈ ℤ)
28 uzid 12875 . . . . . . . . . . . . . 14 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
2927, 28syl 17 . . . . . . . . . . . . 13 (𝑗𝑍𝑗 ∈ (ℤ𝑗))
30 fveq2 6902 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
31 cau3lem.3 . . . . . . . . . . . . . . 15 ((𝐹𝑘) = (𝐹𝑗) → (𝜓𝜒))
3230, 31syl 17 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝜓𝜒))
3332rspcva 3609 . . . . . . . . . . . . 13 ((𝑗 ∈ (ℤ𝑗) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → 𝜒)
3429, 33sylan 578 . . . . . . . . . . . 12 ((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → 𝜒)
3534adantll 712 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → 𝜒)
3625, 35jctild 524 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))))
37 simplll 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → 𝜑)
38 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → 𝜃)
39 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → 𝜒)
40 cau3lem.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝜃𝜒) → (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) = (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))))
4137, 38, 39, 40syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) = (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))))
4241breq1d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → ((𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2) ↔ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2)))
4342anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → (((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)) ↔ ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2))))
44 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → 𝜓)
45 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → 𝑥 ∈ ℝ+)
4645rpred 13056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → 𝑥 ∈ ℝ)
47 cau3lem.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝜓𝜃) ∧ (𝜒𝑥 ∈ ℝ)) → (((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
4837, 44, 38, 39, 46, 47syl122anc 1376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → (((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
4943, 48sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → (((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
5049expd 414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ 𝜓) → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ((𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
5150impr 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒𝜃)) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) → ((𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
5251an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) ∧ (𝜒𝜃)) → ((𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
5352anassrs 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥 ∈ ℝ+) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) ∧ 𝜒) ∧ 𝜃) → ((𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
5453expimpd 452 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) ∧ 𝜒) → ((𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)) → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
5554ralimdv 3166 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) ∧ 𝜒) → (∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
5655impr 453 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) → ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)
5756an32s 650 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) ∧ (𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2))) → ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)
5857expr 455 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) ∧ 𝜓) → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
59 uzss 12883 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ𝑗) → (ℤ𝑘) ⊆ (ℤ𝑗))
60 ssralv 4050 . . . . . . . . . . . . . . . . . . . 20 ((ℤ𝑘) ⊆ (ℤ𝑗) → (∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 → ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
6159, 60syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (ℤ𝑗) → (∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 → ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
6258, 61sylan9 506 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) ∧ 𝜓) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
6362an32s 650 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝜓) → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
6463expimpd 452 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
6564ralimdva 3164 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2)))) → (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
6665ex 411 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))) → (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
6766com23 86 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ((𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
6867adantr 479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝜓 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ((𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
6914, 68biimtrrid 242 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((∀𝑘 ∈ (ℤ𝑗)𝜓 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ((𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
7069expdimp 451 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ((𝜒 ∧ ∀𝑚 ∈ (ℤ𝑗)(𝜃 ∧ (𝐺‘((𝐹𝑚)𝐷(𝐹𝑗))) < (𝑥 / 2))) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
7136, 70mpdd 43 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
7213, 71sylan2 591 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜏) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
7372imdistanda 570 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → (∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
74 r19.26 3108 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) ↔ (∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)))
75 r19.26 3108 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) ↔ (∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
7673, 74, 753imtr4g 295 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
7776reximdva 3165 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
7811, 77syld 47 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∀𝑧 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
7978ralrimdva 3151 . . 3 (𝜑 → (∀𝑧 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑧) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
804, 79biimtrid 241 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
81 fveq2 6902 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (ℤ𝑘) = (ℤ𝑗))
8230fvoveq1d 7448 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) = (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))))
8382breq1d 5162 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 ↔ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥))
8481, 83raleqbidv 3340 . . . . . . . . . . 11 (𝑘 = 𝑗 → (∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥))
8584rspcv 3607 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑗) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 → ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥))
8685ad2antlr 725 . . . . . . . . 9 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 → ∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥))
87 fveq2 6902 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
8887oveq2d 7442 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → ((𝐹𝑗)𝐷(𝐹𝑚)) = ((𝐹𝑗)𝐷(𝐹𝑘)))
8988fveq2d 6906 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) = (𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))))
9089breq1d 5162 . . . . . . . . . . 11 (𝑚 = 𝑘 → ((𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥 ↔ (𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥))
9190cbvralvw 3232 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥)
9233anim2i 615 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ (ℤ𝑗) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓)) → (𝜑𝜒))
9392anassrs 466 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (𝜑𝜒))
94 simpr 483 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → ∀𝑘 ∈ (ℤ𝑗)𝜓)
95 cau3lem.5 . . . . . . . . . . . . . . 15 ((𝜑𝜒𝜓) → (𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) = (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))))
9695breq1d 5162 . . . . . . . . . . . . . 14 ((𝜑𝜒𝜓) → ((𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
97963expia 1118 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝜓 → ((𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
9897ralimdv 3166 . . . . . . . . . . . 12 ((𝜑𝜒) → (∀𝑘 ∈ (ℤ𝑗)𝜓 → ∀𝑘 ∈ (ℤ𝑗)((𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
9993, 94, 98sylc 65 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → ∀𝑘 ∈ (ℤ𝑗)((𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
100 ralbi 3100 . . . . . . . . . . 11 (∀𝑘 ∈ (ℤ𝑗)((𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
10199, 100syl 17 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑘))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
10291, 101bitrid 282 . . . . . . . . 9 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑚 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
10386, 102sylibd 238 . . . . . . . 8 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜓) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
10413, 103sylan2 591 . . . . . . 7 (((𝜑𝑗 ∈ (ℤ𝑗)) ∧ ∀𝑘 ∈ (ℤ𝑗)𝜏) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
105104imdistanda 570 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑗)) → ((∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) → (∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
10629, 105sylan2 591 . . . . 5 ((𝜑𝑗𝑍) → ((∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) → (∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
107 r19.26 3108 . . . . 5 (∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ (∀𝑘 ∈ (ℤ𝑗)𝜏 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥))
108106, 75, 1073imtr4g 295 . . . 4 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) → ∀𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
109108reximdva 3165 . . 3 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
110109ralimdv 3166 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥)))
11180, 110impbid 211 1 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ (𝐺‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ𝑘)(𝐺‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3058  wrex 3067  wss 3949   class class class wbr 5152  cfv 6553  (class class class)co 7426  cr 11145   < clt 11286   / cdiv 11909  2c2 12305  cz 12596  cuz 12860  +crp 13014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-2 12313  df-z 12597  df-uz 12861  df-rp 13015
This theorem is referenced by:  cau3  15342  iscau3  25226
  Copyright terms: Public domain W3C validator